CBMC
instrument_preconditions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Move preconditions of a function
4  to the call-site of the function
5 
6 Author: Daniel Kroening
7 
8 Date: September 2017
9 
10 \*******************************************************************/
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
13 #define CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
14 
15 class goto_functiont;
16 class goto_modelt;
17 
18 void instrument_preconditions(goto_modelt &);
19 void remove_preconditions(goto_modelt &);
20 void remove_preconditions(goto_functiont &);
21 
22 #endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_modelt
Definition: goto_model.h:27
instrument_preconditions
void instrument_preconditions(goto_modelt &)
Definition: instrument_preconditions.cpp:143
remove_preconditions
void remove_preconditions(goto_modelt &)
Definition: instrument_preconditions.cpp:167