Go to the documentation of this file.
34 std::cout <<
"Checking following program for satness:\n";
49 std::cout <<
"Trivially unsat\n";
57 std::cout <<
"Finished symex, invoking decision procedure.\n";
76 new_instructions.begin(),
77 new_instructions.end());
86 instruction->code=assignment;
94 instruction->guard=guard;
106 if(expr.
id()==ID_equal ||
107 expr.
id()==ID_notequal ||
126 for(goto_programt::instructionst::iterator it=
instructions.begin();
140 else if(it->is_assume() || it->is_assert())
149 for(patht::iterator it=path.begin();
153 if(it->loc->is_assign() || it->loc->is_assume())
157 else if(it->loc->is_goto())
159 if(it->guard.id()!=ID_nil)
164 else if(it->loc->is_assert())
197 if(t->is_backwards_goto())
200 t->targets.push_back(end);
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
virtual exprt get(const exprt &expr) const =0
symbol_tablet symex_symbol_table
#define Forall_operands(it, expr)
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
std::list< instructiont > instructionst
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void update()
Update all indices.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Base class for all expressions.
void set_option(const std::string &option, const bool value)
void append(goto_programt::instructionst &instructions)
targett add_instruction()
Adds an instruction at the end.
std::size_t count_assertions() const
typet & type()
Return the type of the expression.
void append_loop(goto_programt &program, goto_programt::targett loop_header)
goto_functionst functions
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
exprt eval(const exprt &e)
virtual resultt dec_solve()=0
static void fix_types(exprt &expr)
targett assume(const exprt &guard)
const irep_idt & id() const
The Boolean constant false.
symex_target_equationt equation
void append_path(patht &path)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
instructionst instructions
The list of instructions in the goto program.
const code_assignt & to_code_assign(const codet &code)
std::list< path_nodet > patht
A generic container class for the GOTO intermediate representation of one function.
static optionst get_default_options()
Semantic type conversion.
A codet representing an assignment in the program.
targett assign(const exprt &lhs, const exprt &rhs)
goto_symex_statet symex_state
instructionst::iterator targett
void slice(symex_target_equationt &equation)