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);
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
A codet representing an assignment in the program.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
The Boolean constant false.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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())
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void update()
Update all indices.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
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.
const irep_idt & id() const
void set_option(const std::string &option, const bool value)
std::size_t get_unique_l2_index(const irep_idt &id)
goto_functionst functions
bool check_sat(bool do_slice, guard_managert &guard_manager)
targett assume(const exprt &guard)
void append_loop(goto_programt &program, goto_programt::targett loop_header)
targett assign(const exprt &lhs, const exprt &rhs)
symbol_tablet symex_symbol_table
static optionst get_default_options()
void append(goto_programt::instructionst &instructions)
decision_proceduret * checker
std::unique_ptr< goto_symex_statet > symex_state
exprt eval(const exprt &e)
void append_path(patht &path)
symex_target_equationt equation
std::size_t count_assertions() const
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Semantic type conversion.
Decision Procedure Interface.
#define Forall_operands(it, expr)
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
std::list< path_nodet > patht
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
static void fix_types(exprt &expr)
const code_assignt & to_code_assign(const codet &code)
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Identifies source in the context of symbolic execution.