CBMC
call_sequences.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Memory-mapped I/O Instrumentation for Goto Programs
4
5
Author: Daniel Kroening
6
7
Date: September 2011
8
9
\*******************************************************************/
10
13
14
#ifndef CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H
15
#define CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H
16
17
class
goto_modelt
;
18
19
void
show_call_sequences
(
const
goto_modelt
&);
20
void
check_call_sequence
(
const
goto_modelt
&);
21
void
list_calls_and_arguments
(
const
goto_modelt
&);
22
23
#endif
// CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H
show_call_sequences
void show_call_sequences(const goto_modelt &)
Definition:
call_sequences.cpp:67
check_call_sequence
void check_call_sequence(const goto_modelt &)
Definition:
call_sequences.cpp:252
list_calls_and_arguments
void list_calls_and_arguments(const goto_modelt &)
Definition:
call_sequences.cpp:314
goto_modelt
Definition:
goto_model.h:27
src
goto-instrument
call_sequences.h
Generated by
1.9.1