|
CBMC
|
#include "remove_asm.h"#include <util/c_types.h>#include <util/pointer_expr.h>#include <util/std_code.h>#include <util/string_constant.h>#include <goto-programs/goto_model.h>#include <goto-programs/remove_skip.h>#include "assembler_parser.h"
Include dependency graph for remove_asm.cpp:Go to the source code of this file.
Classes | |
| class | remove_asmt |
Functions | |
| 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). More... | |
| 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). More... | |
Remove 'asm' statements by compiling them into suitable standard goto program instructions
Definition in file remove_asm.cpp.
| 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 512 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 525 of file remove_asm.cpp.