CBMC
require_expr.cpp File Reference

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>
+ Include dependency graph for require_expr.cpp:

Go to the source code of this file.

Detailed Description

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.