12#define USE_DEPRECATED_STATIC_ANALYSIS_H
29 else if(std::next(from) == to)
32 return from->get_condition();
41 if(to->is_end_function())
45 assert(to->is_function_call());
47 return to->call_lhs();
63 fixedpoint(function_identifier, goto_program, goto_functions);
68 std::ostream &out)
const
75 out <<
"//// Function: " <<
gf_entry.first <<
"\n";
87 std::ostream &out)
const
91 out <<
"**** " <<
i_it->location_number <<
" " <<
i_it->source_location()
159 const irep_idt &function_identifier,
178 if(
visit(function_identifier, l,
working_set, goto_program, goto_functions))
186 const irep_idt &function_identifier,
208 if(l->is_function_call())
222 ns, function_identifier, l, function_identifier,
to_l);
244 const goto_functionst::function_mapt::const_iterator
f_it,
250 if(!goto_function.body_available())
253 assert(!goto_function.body.instructions.empty());
317 const exprt &function,
338 goto_functionst::function_mapt::const_iterator it=
342 throw "failed to find function "+
id2string(identifier);
358 throw "if takes three arguments";
385 std::list<exprt> values;
391 for(
const auto &value : values)
418 else if(function.
id()==
"builtin-function")
424 throw "unexpected function_call argument: "+
451 tmp.add_instruction();
480 if(is_threaded(
t_it))
486 gf_entry.second.body.instructions.end();
515 thread.function_identifier,
518 *thread.goto_program,
524 if(l->is_end_function())
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
const std::string & id_string() const
const irep_idt & id() const
Split an expression into a base object and a (byte) offset.
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
void generate_states(const goto_functionst &goto_functions)
void do_function_call(const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
locationt get_next(working_sett &working_set)
virtual bool has_location(locationt l) const =0
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
void put_in_working_set(working_sett &working_set, locationt l)
void sequential_fixedpoint(const goto_functionst &goto_functions)
void concurrent_fixedpoint(const goto_functionst &goto_functions)
virtual void operator()(const irep_idt &function_identifier, const goto_programt &goto_program)
static exprt get_return_lhs(locationt to)
virtual void generate_state(locationt l)=0
virtual void update(const goto_programt &goto_program)
void do_function_call_rec(const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
static exprt get_guard(locationt from, locationt to)
functions_donet functions_done
virtual statet & get_state(locationt l)=0
virtual void initialize(const goto_programt &goto_program)
std::map< unsigned, locationt > working_sett
goto_programt::const_targett locationt
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
virtual bool merge(statet &a, const statet &b, locationt to)=0
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
recursion_sett recursion_set
const irep_idt & get_identifier() const
The Boolean constant true.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
#define forall_goto_program_instructions(it, program)
const irept & get_nil_irep()
const std::string & id2string(const irep_idt &d)
Over-approximate Concurrency for Threaded Goto Programs.
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.