cprover
|
Remove 'asm' statements by compiling them into suitable standard goto program instructions. More...
Go to the source code of this file.
Functions | |
void | remove_asm (goto_functionst &, symbol_tablet &) |
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a code member of type code_asmt ) with an appropriate (sequence of) non-assembly goto program instruction(s). | |
void | remove_asm (goto_modelt &) |
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a code member of type code_asmt ) with an appropriate (sequence of) non-assembly goto program instruction(s). | |
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Inline assembly statements in the source program (in either gcc- or msc-style) are represented by instructions of kind OTHER
with a code
member of type code_asmt
in the goto program.
For example, the gcc inline assembly statement below
would be represented by a code_asmt
statement with op0()
being the string literal "mov %1, %0; add $1, %0" (as a string_constantt
expression) and op1()
, op2()
, and op3()
, respectively, containing the output list, input list, and clobbered registers.
The remove_asm()
function replaces the inline assembly statements in a given goto program with appropriate (sequences of) non-assembly goto program instructions.
It first parses the assembly instructions string (via assembler_parsert
) and inspects the input/output/clobber lists. Then, it generates a sequence of goto program instructions that either directly implement the assembly instructions, or call a suitable library function (see library/x86_assembler.c
).
At present only a small number of x86 and Power instructions are supported. Unrecognised assembly instructions are ignored (i.e., they are simply removed from the goto program).
Definition in file remove_asm.h.
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 code
member of type code_asmt
) with an appropriate (sequence of) non-assembly goto program instruction(s).
goto_functions | The goto functions |
symbol_table | The symbol table |
Definition at line 551 of file remove_asm.cpp.
void remove_asm | ( | goto_modelt & | goto_model | ) |
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER
with a code
member of type code_asmt
) with an appropriate (sequence of) non-assembly goto program instruction(s).
At present only a small number of x86 and Power instructions are supported. Unrecognised assembly instructions are ignored.
goto_model | The goto model |
Definition at line 564 of file remove_asm.cpp.