88 if(it->operands().size() == 2)
98 if(it->operands().size() == 2)
119 symbol.
name = function_identifier;
133 "function types should match");
167 symbol.
name = function_identifier;
181 "function types should match");
224 bool unknown =
false;
229 if(instruction.empty())
233 std::cout <<
"A ********************\n";
234 for(
const auto &
ins : instruction)
236 std::cout <<
"XX: " <<
ins.pretty() <<
'\n';
239 std::cout <<
"B ********************\n";
255 if(
pos == instruction.size())
264 if(command ==
"xchg" || command ==
"xchgl")
282 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
287 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
331 else if(command ==
"dmb" || command ==
"dsb")
347 else if(command ==
"isb")
393 bool unknown =
false;
398 if(instruction.empty())
402 std::cout <<
"A ********************\n";
403 for(
const auto &
ins : instruction)
405 std::cout <<
"XX: " <<
ins.pretty() <<
'\n';
408 std::cout <<
"B ********************\n";
424 if(
pos == instruction.size())
433 if(command ==
"xchg" || command ==
"xchgl")
451 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
456 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
490 if(it->is_other() && it->get_other().get_statement() ==
ID_asm)
494 it->turn_into_skip();
500 goto_function.body.destructive_insert(next,
tmp_dest);
assembler_parsert assembler_parser
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::list< instructiont > instructions
codet representation of an inline assembler statement, for the gcc flavor.
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
codet representation of a function call statement.
exprt::operandst argumentst
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const source_locationt & source_location() const
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
const codet & get_other() const
Get the statement for OTHER.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
goto_functionst & goto_functions
symbol_tablet & symbol_table
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
void process_instruction_gcc(const code_asm_gcct &, goto_programt &dest)
Translates the given inline assembly code (in gcc style) to non-assembly goto program instructions.
void msc_asm_function_call(const irep_idt &function_base_name, const code_asmt &code, goto_programt &dest)
Adds a call to a library function that implements the given msc-style inline assembly statement.
void process_instruction_msc(const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in msc style) to non-assembly goto program instructions.
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
Translates the given inline assembly code (which must be in either gcc or msc style) to non-assembly ...
void gcc_asm_function_call(const irep_idt &function_base_name, const code_asm_gcct &code, goto_programt &dest)
Adds a call to a library function that implements the given gcc-style inline assembly statement.
void process_function(goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
const irep_idt & get_value() const
Expression to hold a symbol (variable)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Semantic type conversion.
The type of an expression, extends irept.
#define forall_operands(it, expr)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
code_asm_gcct & to_code_asm_gcc(codet &code)
code_asmt & to_code_asm(codet &code)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const string_constantt & to_string_constant(const exprt &expr)