Go to the documentation of this file.
52 program.append(
fixed);
53 program.append(
fixed);
62 for(distinguish_valuest::iterator jt=it->begin();
66 exprt distinguisher=jt->first;
67 bool taken=jt->second;
72 distinguisher.
swap(negated);
75 or_exprt disjunct(new_path, distinguisher);
76 new_path.
swap(disjunct);
79 program.assume(new_path);
89 std::cout <<
"Found a path\n";
97 catch(
const std::string &s)
99 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
103 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
121 for(
const auto &succ : succs)
147 assert(succs.size() > 0);
159 bool found_branch=
false;
161 for(
const auto &succ : succs)
164 bool taken=scratch_program.
eval(distinguisher).
is_true();
169 (succ->location_number <
next->location_number))
178 assert(found_branch);
189 for(goto_programt::targetst::iterator it=t->targets.begin();
190 it!=t->targets.end();
195 cond = t->get_condition();
215 std::map<exprt, exprt> shadow_distinguishers;
248 exprt &distinguisher=*it;
252 shadow_distinguishers[distinguisher]=shadow;
271 fixedt->turn_into_skip();
279 exprt &distinguisher=d->second;
280 exprt &shadow=shadow_distinguishers[distinguisher];
286 assign->swap(*fixedt);
292 assert(fixedt->is_goto());
302 for(
const auto &target : t->targets)
304 if(target->location_number > t->location_number)
315 fixedt->targets.clear();
316 fixedt->targets.push_back(kill);
326 fixedt->targets.clear();
327 fixedt->targets.push_back(end);
332 fixedt->targets.clear();
333 fixedt->targets.push_back(kill);
346 const exprt &shadow=shadow_distinguishers[expr];
#define Forall_goto_program_instructions(it, program)
Generate Equation using Symbolic Execution.
std::map< exprt, bool > distinguish_valuest
symbolt fresh_symbol(std::string base, typet type)
void find_distinguishing_points()
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
goto_programt::targett loop_header
void update()
Update all indices.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
const_iterator end() const
Iterator over this loop's instructions.
Base class for all expressions.
guard_managert & guard_manager
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
bool is_true() const
Return whether the expression is a constant representing true.
Expression to hold a symbol (variable)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
const_iterator begin() const
Iterator over this loop's instructions.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
loop_instructionst::const_iterator const_iterator
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
exprt eval(const exprt &e)
void build_path(scratch_programt &scratch_program, patht &path)
std::list< exprt > distinguishers
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
std::list< distinguish_valuest > accelerated_paths
The Boolean constant false.
natural_loops_mutablet::natural_loopt & loop
message_handlert & message_handler
instructionst instructions
The list of instructions in the goto program.
std::list< path_nodet > patht
goto_programt & goto_program
void record_path(scratch_programt &scratch_program)
Goto Programs with Functions.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
distinguish_mapt distinguishing_points
A codet representing an assignment in the program.
The Boolean constant true.
acceleration_utilst utils
API to expression classes.
symbol_tablet & symbol_table
instructionst::iterator targett
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.