CBMC
|
Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression. More...
#include "require_expr.h"
#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/std_code.h>
Go to the source code of this file.
Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression.
Definition in file require_expr.cpp.