File tree Expand file tree Collapse file tree 2 files changed +13
-0
lines changed Expand file tree Collapse file tree 2 files changed +13
-0
lines changed Original file line number Diff line number Diff line change @@ -146,3 +146,14 @@ void instrument_preconditions(goto_modelt &goto_model)
146
146
for (auto &f_it : goto_model.goto_functions .function_map )
147
147
remove_preconditions (f_it.second .body );
148
148
}
149
+
150
+ void remove_preconditions (goto_functiont &goto_function)
151
+ {
152
+ remove_preconditions (goto_function.body );
153
+ }
154
+
155
+ void remove_preconditions (goto_modelt &goto_model)
156
+ {
157
+ for (auto &f_it : goto_model.goto_functions .function_map )
158
+ remove_preconditions (f_it.second );
159
+ }
Original file line number Diff line number Diff line change @@ -15,5 +15,7 @@ Date: September 2017
15
15
#include <goto-programs/goto_model.h>
16
16
17
17
void instrument_preconditions (goto_modelt & );
18
+ void remove_preconditions (goto_modelt & );
19
+ void remove_preconditions (goto_functiont & );
18
20
19
21
#endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
You can’t perform that action at this time.
0 commit comments