34 std::cout <<
"Checking following program for satness:\n";
52 std::cout <<
"Trivially unsat\n";
60 std::cout <<
"Finished symex, invoking decision procedure.\n";
79 new_instructions.begin(),
80 new_instructions.end());
89 instruction->code=assignment;
97 instruction->guard=guard;
109 if(expr.
id()==ID_equal ||
110 expr.
id()==ID_notequal ||
129 for(goto_programt::instructionst::iterator it=
instructions.begin();
143 else if(it->is_assume() || it->is_assert())
152 for(patht::iterator it=path.begin();
156 if(it->loc->is_assign() || it->loc->is_assume())
160 else if(it->loc->is_goto())
162 if(it->guard.id()!=ID_nil)
167 else if(it->loc->is_assert())
199 if(t->is_backwards_goto())
202 t->targets.push_back(end);
void update()
Update all indices.
void slice(symex_target_equationt &equation)
symbol_tablet symex_symbol_table
targett assign(const exprt &lhs, const exprt &rhs)
void convert(prop_convt &prop_conv)
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual exprt get(const exprt &expr) const =0
bool constant_propagation
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Decision Procedure Interface.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::list< instructiont > instructionst
const code_assignt & to_code_assign(const codet &code)
std::map< irep_idt, exprt > valuest
const irep_idt & id() const
goto_functionst functions
virtual resultt dec_solve()=0
instructionst::iterator targett
targett assume(const exprt &guard)
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
exprt eval(const exprt &e)
instructionst instructions
The list of instructions in the goto program.
void append_loop(goto_programt &program, goto_programt::targett loop_header)
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
bool constant_propagation
The boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
symex_target_equationt equation
void append_path(patht &path)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::size_t count_assertions() const
#define Forall_operands(it, expr)
goto_symex_statet symex_state
static void fix_types(exprt &expr)