cprover
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 
16 
20 
21 #endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
void remove_preconditions(goto_modelt &)
void instrument_preconditions(goto_modelt &)
Symbol Table + CFG.
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
Definition: goto_function.h:26