CBMC
|
Memory-mapped I/O Instrumentation for Goto Programs. More...
Go to the source code of this file.
Functions | |
void | show_call_sequences (const goto_modelt &) |
void | check_call_sequence (const goto_modelt &) |
void | list_calls_and_arguments (const goto_modelt &) |
Memory-mapped I/O Instrumentation for Goto Programs.
Definition in file call_sequences.h.
void check_call_sequence | ( | const goto_modelt & | goto_model | ) |
Definition at line 252 of file call_sequences.cpp.
void list_calls_and_arguments | ( | const goto_modelt & | goto_model | ) |
Definition at line 314 of file call_sequences.cpp.
void show_call_sequences | ( | const goto_modelt & | goto_model | ) |
Definition at line 67 of file call_sequences.cpp.