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 
21 
22 #endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
void instrument_preconditions(goto_modelt &)
void remove_preconditions(goto_modelt &)