12 #ifndef CPROVER_MUSKETEER_REPLACE_ASYNC_H 13 #define CPROVER_MUSKETEER_REPLACE_ASYNC_H 31 const goto_programt::instructiont &instruction=*i_it;
33 if(instruction.is_function_call())
47 if(fct_name.
id()==ID_address_of)
56 new_call.function()=fct_name;
59 new_call.arguments().resize(1);
61 new_call.arguments()[0]=fct.
arguments()[3];
65 i_it->labels.push_front(
"__CPROVER_ASYNC_0");
75 goto2->make_goto(skip);
76 call->make_function_call(new_call);
86 #endif // CPROVER_MUSKETEER_REPLACE_ASYNC_H virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const irep_idt & get_identifier() const
const irep_idt & id() const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
targett insert_after(const_targett target)
Insertion after the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
void replace_async(const namespacet &ns, goto_functionst &goto_functions)
Expression to hold a symbol (variable)
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett