Go to the documentation of this file.
35 std::cout <<
"Checking following program for satness:\n";
63 std::cout <<
"Trivially unsat\n";
71 std::cout <<
"Finished symex, invoking decision procedure.\n";
86 new_instructions.begin(),
87 new_instructions.end());
109 if(expr.
id()==ID_equal ||
110 expr.
id()==ID_notequal ||
117 exprt &lhs = rel_expr.lhs();
118 exprt &rhs = rel_expr.rhs();
123 rel_expr.rhs().swap(typecast);
130 for(goto_programt::instructionst::iterator it=
instructions.begin();
144 else if(it->is_assume() || it->is_assert())
146 exprt cond = it->get_condition();
148 it->set_condition(cond);
155 for(patht::iterator it=path.begin();
159 if(it->loc->is_assign() || it->loc->is_assume())
163 else if(it->loc->is_goto())
165 if(it->guard.id()!=ID_nil)
170 else if(it->loc->is_assert())
203 if(t->is_backwards_goto())
206 t->targets.push_back(end);
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
virtual void symex_with_state(statet &state, const get_goto_functiont &get_goto_functions, symbol_tablet &new_symbol_table)
Symbolically execute the entire program starting from entry point.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
symbol_tablet symex_symbol_table
#define Forall_operands(it, expr)
std::list< instructiont > instructionst
decision_proceduret * checker
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.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
Base class for all expressions.
void set_option(const std::string &option, const bool value)
function_mapt function_map
void append(goto_programt::instructionst &instructions)
Decision Procedure Interface.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
This is unused by this implementation of guards, but can be used by other implementations of the same...
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.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
exprt eval(const exprt &e)
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
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.
::goto_functiont goto_functiont
instructionst instructions
The list of instructions in the goto program.
std::unique_ptr< goto_symex_statet > symex_state
const code_assignt & to_code_assign(const codet &code)
std::list< path_nodet > patht
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Identifies source in the context of symbolic execution.
static optionst get_default_options()
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool check_sat(bool do_slice, guard_managert &guard_manager)
Semantic type conversion.
A codet representing an assignment in the program.
std::size_t get_unique_l2_index(const irep_idt &id)
targett assign(const exprt &lhs, const exprt &rhs)
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
instructionst::iterator targett