|
CBMC
|
#include "require_expr.h"#include <testing-utils/use_catch.h>#include <util/arith_tools.h>#include <util/std_code.h>
Include dependency graph for require_expr.cpp: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.