CBMC
remove_asm.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove 'asm' statements by compiling them into suitable
4  standard goto program instructions
5 
6 Author: Daniel Kroening
7 
8 Date: December 2014
9 
10 \*******************************************************************/
11 
51 
52 #ifndef CPROVER_ASSEMBLER_REMOVE_ASM_H
53 #define CPROVER_ASSEMBLER_REMOVE_ASM_H
54 
55 class goto_functionst;
56 class goto_modelt;
57 class message_handlert;
58 class symbol_tablet;
59 
60 void remove_asm(goto_functionst &, symbol_tablet &, message_handlert &);
61 
62 void remove_asm(goto_modelt &, message_handlert &);
63 
65 bool has_asm(const goto_functionst &);
66 
68 bool has_asm(const goto_modelt &);
69 
70 #endif // CPROVER_ASSEMBLER_REMOVE_ASM_H
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt
Definition: goto_model.h:27
message_handlert
Definition: message.h:27
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
remove_asm
void remove_asm(goto_functionst &, symbol_tablet &, message_handlert &)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:575
has_asm
bool has_asm(const goto_functionst &)
returns true iff the given goto functions use asm instructions
Definition: remove_asm.cpp:598