|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <util/ssa/goto_expr_factory.h>Functions | |
| expr2tc | create_value_expr (int value, const type2tc &type) |
| Create a constant_int expression. | |
| expr2tc | create_lessthanequal_relation (expr2tc &lhs, expr2tc &rhs) |
| Create a lessthanequal expression of the form LHS <= RHS The comparation will use LHS for typecast. | |
| expr2tc | create_greaterthanequal_relation (expr2tc &lhs, expr2tc &rhs) |
| Create a lessthanequal expression of the form LHS <= RHS The comparation will use LHS for typecast. | |
Create a lessthanequal expression of the form LHS <= RHS The comparation will use LHS for typecast.
| lhs | left operator |
| rhs | right operator |
Create a lessthanequal expression of the form LHS <= RHS The comparation will use LHS for typecast.
| lhs | left operator |
| rhs | right operator |