|
cprover
|
Public Member Functions | |
| remove_asmt (symbol_tablet &_symbol_table, goto_functionst &_goto_functions, message_handlert &message_handler) | |
| void | operator() () |
Protected Member Functions | |
| void | process_function (const irep_idt &, goto_functionst::goto_functiont &) |
| Replaces inline assembly instructions in the goto function by non-assembly goto program instructions. | |
| void | process_instruction (const irep_idt &function_id, 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 goto program instructions. | |
| 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 | process_instruction_msc (const irep_idt &, const code_asmt &, goto_programt &dest) |
| Translates the given inline assembly code (in msc style) to non-assembly goto program instructions. | |
| void | gcc_asm_function_call (const irep_idt &function_base_name, const code_asm_gcct &code, std::size_t n_args, goto_programt &dest) |
| Adds a call to a library function that implements the given gcc-style inline assembly statement. | |
| void | msc_asm_function_call (const irep_idt &function_base_name, const exprt::operandst &operands, const code_asmt &code, goto_programt &dest) |
| Adds a call to a library function that implements the given msc-style inline assembly statement. | |
Protected Attributes | |
| symbol_tablet & | symbol_table |
| goto_functionst & | goto_functions |
| message_handlert & | message_handler |
Definition at line 30 of file remove_asm.cpp.
|
inline |
Definition at line 33 of file remove_asm.cpp.
|
protected |
Adds a call to a library function that implements the given gcc-style inline assembly statement.
| function_base_name | Name of the function to call |
| code | gcc-style inline assembly statement to translate to function call |
| n_args | Number of arguments required by function_base_name |
| dest | Goto program to append the function call to |
Definition at line 89 of file remove_asm.cpp.
|
protected |
Adds a call to a library function that implements the given msc-style inline assembly statement.
| function_base_name | Name of the function to call |
| operands | Arguments to be passed to function |
| code | msc-style inline assembly statement to translate to function call |
| dest | Goto program to append the function call to |
Definition at line 173 of file remove_asm.cpp.
|
inline |
Definition at line 43 of file remove_asm.cpp.
|
protected |
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
| function_id | Name of function being processed |
| goto_function | The goto function |
Definition at line 544 of file remove_asm.cpp.
|
protected |
Translates the given inline assembly code (which must be in either gcc or msc style) to non-assembly goto program instructions.
| function_id | Name of function being processed |
| instruction | The goto program instruction containing the inline assembly statements |
| dest | The goto program to append the new instructions to |
Definition at line 225 of file remove_asm.cpp.
|
protected |
Translates the given inline assembly code (in gcc style) to non-assembly goto program instructions.
| code | The inline assembly code statement to translate |
| dest | The goto program to append the new instructions to |
Definition at line 247 of file remove_asm.cpp.
|
protected |
Translates the given inline assembly code (in msc style) to non-assembly goto program instructions.
| function_id | Name of function being processed |
| code | The inline assembly code statement to translate |
| dest | The goto program to append the new instructions to |
Definition at line 417 of file remove_asm.cpp.
|
protected |
Definition at line 51 of file remove_asm.cpp.
|
protected |
Definition at line 52 of file remove_asm.cpp.
|
protected |
Definition at line 50 of file remove_asm.cpp.