12 #define USE_DEPRECATED_STATIC_ANALYSIS_H 35 exprt tmp(from->guard);
49 if(to->is_end_function())
53 assert(to->is_function_call());
78 std::ostream &out)
const 82 if(f_it->second.body_available())
85 out <<
"//// Function: " << f_it->first <<
"\n";
89 output(f_it->second.body, f_it->first, out);
97 std::ostream &out)
const 101 out <<
"**** " << i_it->location_number <<
" " 102 << i_it->source_location <<
"\n";
131 update(f_it->second.body);
159 assert(!working_set.empty());
161 working_sett::iterator i=working_set.begin();
163 working_set.erase(i);
183 while(!working_set.empty())
187 if(
visit(l, working_set, goto_program, goto_functions))
211 std::unique_ptr<statet> tmp_state(
214 statet &new_values=*tmp_state;
216 if(l->is_function_call())
234 bool have_new_values=
235 merge(other, new_values, to_l);
240 if(have_new_values || !other.
seen)
250 const goto_functionst::function_mapt::const_iterator f_it,
259 assert(!goto_function.
body.instructions.empty());
274 if(
merge(begin_state, *tmp_state, l_begin))
297 assert(l_end->is_end_function());
302 std::unique_ptr<statet> tmp_state(
309 merge(new_state, *tmp_state, l_return);
320 const exprt &
function,
329 if(
function.
id()==ID_symbol)
331 const irep_idt &identifier=
function.get(ID_identifier);
341 goto_functionst::function_mapt::const_iterator it=
345 throw "failed to find function "+
id2string(identifier);
356 else if(
function.
id()==ID_if)
358 if(
function.operands().size()!=3)
359 throw "if takes three arguments";
377 merge(new_state, *n2, l_return);
379 else if(
function.
id()==ID_dereference)
382 std::list<exprt> values;
388 for(
const auto &value : values)
390 if(value.id()==ID_object_descriptor)
395 l_call, l_return, o.
object(), arguments, *n2, goto_functions);
396 merge(new_state, *n2, l_return);
400 else if(
function.
id()==
"NULL-object" ||
401 function.
id()==ID_integer_address)
405 else if(
function.
id()==ID_member ||
function.
id()==ID_index)
409 else if(
function.
id()==
"builtin-function")
415 throw "unexpected function_call argument: "+
416 function.id_string();
447 thread_wlt thread_wl;
452 if(is_threaded(t_it))
454 thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
457 it->second.body.instructions.end();
467 bool new_shared=
true;
472 for(
const auto &thread : thread_wl)
478 merge(begin_state, shared_state, thread.second);
480 while(!working_set.empty())
484 visit(l, working_set, *thread.first, goto_functions);
489 if(l->is_end_function())
492 new_shared|=
merge_shared(shared_state, end_state, sh_target);
const irept & get_nil_irep()
bool body_available() const
static exprt get_guard(locationt from, locationt to)
Over-approximate Concurrency for Threaded Goto Programs.
std::map< unsigned, locationt > working_sett
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
virtual statet & get_state(locationt l)=0
recursion_sett recursion_set
instructionst instructions
The list of instructions in the goto program.
void sequential_fixedpoint(const goto_functionst &goto_functions)
virtual void transform(const namespacet &ns, locationt from, locationt to)=0
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
static exprt get_return_lhs(locationt to)
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual bool has_location(locationt l) const =0
virtual statet * make_temporary_state(statet &s)=0
virtual void generate_state(locationt l)=0
functions_donet functions_done
std::list< Target > get_successors(Target target) const
void do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
instructionst::const_iterator const_targett
void put_in_working_set(working_sett &working_set, locationt l)
The boolean constant true.
virtual bool merge(statet &a, const statet &b, locationt to)=0
API to expression classes.
void concurrent_fixedpoint(const goto_functionst &goto_functions)
goto_programt::const_targett locationt
split an expression into a base object and a (byte) offset
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
function_mapt function_map
std::vector< exprt > operandst
void generate_states(const goto_functionst &goto_functions)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
virtual void output(const namespacet &ns, std::ostream &out) const
Base class for all expressions.
virtual void operator()(const goto_programt &goto_program)
virtual void update(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
void do_function_call(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)
virtual void initialize(const goto_programt &goto_program)
#define forall_goto_functions(it, functions)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
const code_function_callt & to_code_function_call(const codet &code)