CBMC
|
Remove 'asm' statements by compiling them into suitable standard goto program instructions. More...
#include "remove_asm.h"
#include <util/c_types.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/range.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"
Go to the source code of this file.
Classes | |
class | remove_asmt |
Functions | |
void | remove_asm (goto_functionst &goto_functions, symbol_tablet &symbol_table, message_handlert &message_handler) |
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, message_handlert &message_handler) |
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... | |
bool | has_asm (const goto_functionst &goto_functions) |
returns true iff the given goto functions use asm instructions More... | |
bool | has_asm (const goto_modelt &goto_model) |
returns true iff the given goto model uses asm instructions More... | |
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
Definition in file remove_asm.cpp.
bool has_asm | ( | const goto_functionst & | goto_functions | ) |
returns true iff the given goto functions use asm instructions
Definition at line 598 of file remove_asm.cpp.
bool has_asm | ( | const goto_modelt & | goto_model | ) |
returns true iff the given goto model uses asm instructions
Definition at line 612 of file remove_asm.cpp.
void remove_asm | ( | goto_functionst & | goto_functions, |
symbol_tablet & | symbol_table, | ||
message_handlert & | message_handler | ||
) |
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 |
message_handler | Message handler |
Definition at line 575 of file remove_asm.cpp.
void remove_asm | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler | ||
) |
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 |
message_handler | Message handler |
Definition at line 592 of file remove_asm.cpp.