35 std::cout <<
"Checking following program for satness:\n";
53 std::cout <<
"Trivially unsat\n";
61 std::cout <<
"Finished symex, invoking decision procedure.\n";
80 new_instructions.begin(),
81 new_instructions.end());
90 instruction->code=assignment;
98 instruction->guard=guard;
110 if(expr.
id()==ID_equal ||
111 expr.
id()==ID_notequal ||
130 for(goto_programt::instructionst::iterator it=
instructions.begin();
144 else if(it->is_assume() || it->is_assert())
153 for(patht::iterator it=path.begin();
157 if(it->loc->is_assign() || it->loc->is_assume())
161 else if(it->loc->is_goto())
163 if(it->guard.id()!=ID_nil)
168 else if(it->loc->is_assert())
200 if(t->is_backwards_goto())
203 t->targets.push_back(end);
void update()
Update all indices.
void slice(symex_target_equationt &equation)
targett add_instruction()
Adds an instruction at the end.
targett assign(const exprt &lhs, const exprt &rhs)
std::list< instructiont > instructionst
void convert(prop_convt &prop_conv)
instructionst instructions
The list of instructions in the goto program.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual exprt get(const exprt &expr) const =0
bool constant_propagation
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Decision Procedure Interface.
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
targett assume(const exprt &guard)
exprt eval(const exprt &e)
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
symex_target_equationt equation
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
void append_path(patht &path)
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
Base class for all expressions.
#define Forall_operands(it, expr)
void destructive_append(goto_program_templatet< codet, exprt > &p)
Appends the given program, which is destroyed.
goto_symex_statet symex_state
unsigned count_assertions() const
instructionst::iterator targett