cprover
|
Symbolic Execution. More...
Go to the source code of this file.
Functions | |
guardt & | operator-= (guardt &g1, const guardt &g2) |
guardt & | operator|= (guardt &g1, const guardt &g2) |
Symbolic Execution.
Definition in file guard.cpp.
Definition at line 93 of file guard.cpp.
References conjunction(), irept::id(), exprt::op1(), exprt::op2(), exprt::operands(), and sort_and_join().
Referenced by bv_arithmetict::to_ansi_c_string(), ieee_floatt::to_ansi_c_string(), and fixedbvt::zero().
Definition at line 122 of file guard.cpp.
References guardt::add(), conjunction(), exprt::exprt(), forall_expr_list, irept::id(), exprt::is_false(), exprt::is_true(), exprt::make_false(), exprt::make_not(), exprt::make_true(), exprt::op1(), exprt::op2(), exprt::operands(), operator<<(), and sort_and_join().