Skip to content

Commit 1f53246

Browse files
author
Daniel Kroening
committed
expose remove_preconditions
1 parent c6d0427 commit 1f53246

File tree

2 files changed

+13
-0
lines changed

2 files changed

+13
-0
lines changed

src/goto-programs/instrument_preconditions.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,3 +146,14 @@ void instrument_preconditions(goto_modelt &goto_model)
146146
for(auto &f_it : goto_model.goto_functions.function_map)
147147
remove_preconditions(f_it.second.body);
148148
}
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+
}

src/goto-programs/instrument_preconditions.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,5 +15,7 @@ Date: September 2017
1515
#include <goto-programs/goto_model.h>
1616

1717
void instrument_preconditions(goto_modelt &);
18+
void remove_preconditions(goto_modelt &);
19+
void remove_preconditions(goto_functiont &);
1820

1921
#endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H

0 commit comments

Comments
 (0)