File tree 1 file changed +25
-0
lines changed
1 file changed +25
-0
lines changed Original file line number Diff line number Diff line change @@ -868,6 +868,7 @@ bool cbmc_parse_optionst::process_goto_program(
868
868
status () << " Generic Property Instrumentation" << eom;
869
869
goto_check (ns, options, goto_functions);
870
870
871
+ <<<<<<< c57f66383a75e4e764b58815c18b87ea2672a756
871
872
// full slice?
872
873
if (cmdline.isset (" full-slice" ))
873
874
{
@@ -977,6 +978,30 @@ bool cbmc_parse_optionst::process_goto_program(
977
978
// remove skips
978
979
remove_skip (goto_functions);
979
980
goto_functions.update ();
981
+
982
+ // full slice?
983
+ if (cmdline.isset (" full-slice" ))
984
+ {
985
+ status () << " Performing a full slice" << eom;
986
+ remove_virtual_functions (symbol_table,goto_functions);
987
+ remove_function_pointers (symbol_table,goto_functions,cmdline.isset (" pointer-check" ));
988
+ remove_returns (symbol_table,goto_functions);
989
+ goto_functions.update ();
990
+
991
+ // status() << "Performing full inlining" << eom;
992
+ // goto_inline(goto_functions, ns, ui_message_handler);
993
+
994
+ try
995
+ {
996
+ full_slicer (goto_functions, ns);
997
+ }
998
+
999
+ catch (const char *error_msg)
1000
+ {
1001
+ error () << error_msg << eom;
1002
+ return 1 ;
1003
+ }
1004
+ }
980
1005
}
981
1006
982
1007
catch (const char *e)
You can’t perform that action at this time.
0 commit comments