43 goto_programt::instructiont &instruction,
60 irep_idt function_identifier=function_base_name;
65 const typet void_pointer=
71 if(it->operands().size()==2)
81 if(it->operands().size()==2)
97 call->code=function_call;
105 symbol.
name=function_identifier;
106 symbol.
type=fkt_type;
116 goto_programt::instructiont &instruction,
130 std::istringstream str(
id2string(i_str));
137 bool x86_32_locked_atomic=
false;
141 if(instruction.empty())
145 std::cout <<
"A ********************\n";
146 for(
const auto &ins : instruction)
148 std::cout <<
"XX: " << ins.pretty() <<
'\n';
151 std::cout <<
"B ********************\n";
158 if(instruction.front().id()==ID_symbol &&
159 instruction.front().get(ID_identifier)==
"lock")
161 x86_32_locked_atomic=
true;
166 if(pos==instruction.size())
169 if(instruction[pos].
id()==ID_symbol)
171 command=instruction[
pos].get(ID_identifier);
175 if(command==
"xchg" || command==
"xchgl")
176 x86_32_locked_atomic=
true;
178 if(x86_32_locked_atomic)
185 t->code=
codet(ID_fence);
187 t->code.
set(ID_WWfence,
true);
188 t->code.set(ID_RRfence,
true);
189 t->code.set(ID_RWfence,
true);
190 t->code.set(ID_WRfence,
true);
193 if(command==
"fstcw" ||
199 else if(command==
"mfence" ||
205 else if(command==
"sync")
209 t->code=
codet(ID_fence);
211 t->code.
set(ID_WWfence,
true);
212 t->code.set(ID_RRfence,
true);
213 t->code.set(ID_RWfence,
true);
214 t->code.set(ID_WRfence,
true);
215 t->code.set(ID_WWcumul,
true);
216 t->code.set(ID_RWcumul,
true);
217 t->code.set(ID_RRcumul,
true);
218 t->code.set(ID_WRcumul,
true);
220 else if(command==
"lwsync")
224 t->code=
codet(ID_fence);
226 t->code.
set(ID_WWfence,
true);
227 t->code.set(ID_RRfence,
true);
228 t->code.set(ID_RWfence,
true);
229 t->code.set(ID_WWcumul,
true);
230 t->code.set(ID_RWcumul,
true);
231 t->code.set(ID_RRcumul,
true);
233 else if(command==
"isync")
237 t->code=
codet(ID_fence);
242 else if(command==
"dmb" || command==
"dsb")
246 t->code=
codet(ID_fence);
248 t->code.
set(ID_WWfence,
true);
249 t->code.set(ID_RRfence,
true);
250 t->code.set(ID_RWfence,
true);
251 t->code.set(ID_WRfence,
true);
252 t->code.set(ID_WWcumul,
true);
253 t->code.set(ID_RWcumul,
true);
254 t->code.set(ID_RRcumul,
true);
255 t->code.set(ID_WRcumul,
true);
257 else if(command==
"isb")
261 t->code=
codet(ID_fence);
269 if(x86_32_locked_atomic)
274 x86_32_locked_atomic=
false;
293 if(it->is_other() && it->code.get_statement()==ID_asm)
302 goto_function.body.destructive_insert(next, tmp_dest);
The type of an expression.
irep_idt name
The unique identifier.
assembler_parsert assembler_parser
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
exprt value
Initial value of symbol.
const irep_idt & get_flavor() const
symbol_tablet symbol_table
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Remove 'asm' statements by compiling into suitable standard code.
void gcc_asm_function_call(const irep_idt &function_base_name, const codet &code, goto_programt &dest)
symbol_tablet & symbol_table
void process_function(goto_functionst::goto_functiont &)
removes assembler
API to expression classes.
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
removes assembler
#define forall_operands(it, expr)
goto_functionst & goto_functions
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_function_templatet< goto_programt > goto_functiont
Operator to return the address of an object.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
const string_constantt & to_string_constant(const exprt &expr)
irep_idt base_name
Base (non-scoped) name.
std::list< instructiont > instructions
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
An inline assembler statement.
void operator()()
removes assembler
bool has_symbol(const irep_idt &name) const
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
A statement in a programming language.
code_asmt & to_code_asm(codet &code)
goto_functionst goto_functions
const typet & return_type() const
void set(const irep_namet &name, const irep_idt &value)
instructionst::iterator targett