Skip to content

Commit 6e66834

Browse files
Expose equation post-processing
Will allow us to remove perform_symex utilities later
1 parent 178c6d8 commit 6e66834

File tree

2 files changed

+12
-1
lines changed

2 files changed

+12
-1
lines changed

src/goto-checker/bmc_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -302,7 +302,7 @@ void output_coverage_report(
302302
}
303303
}
304304

305-
static void postprocess_equation(
305+
void postprocess_equation(
306306
symex_bmct &symex,
307307
symex_target_equationt &equation,
308308
const optionst &options,

src/goto-checker/bmc_util.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,17 @@ void slice(
7070
const optionst &,
7171
ui_message_handlert &);
7272

73+
/// Post process the equation
74+
/// - add partial order constraints
75+
/// - slice
76+
/// - perform validation
77+
void postprocess_equation(
78+
symex_bmct &symex,
79+
symex_target_equationt &equation,
80+
const optionst &options,
81+
const namespacet &ns,
82+
ui_message_handlert &ui_message_handler);
83+
7384
/// Perform symbolic execution from the entry point
7485
void perform_symex(
7586
abstract_goto_modelt &,

0 commit comments

Comments
 (0)