Do not ignore --full-slice

peterschrammel · peterschrammel · commit 19bddce08110 · 2018-07-04T21:02:28.000+01:00
diff --git a/regression/cbmc/full_slice1/test.desc b/regression/cbmc/full_slice1/test.desc
@@ -1,8 +1,13 @@
 CORE
 main.c
---full-slice --property main.assertion.1 --unwind 1
+--full-slice --property main.assertion.1 --unwind 1 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED
 --
 ^warning: ignoring
+^Thread 0 file main.c line 16 function doit
+^Thread 0 file main.c line 19 function doit
+^Thread 0 file main.c line 21 function doit
+^Thread 0 file main.c line 41 function main
+^Thread 0 file main.c line 42 function main
diff --git a/regression/cbmc/full_slice2/test.desc b/regression/cbmc/full_slice2/test.desc
@@ -1,10 +1,14 @@
 CORE
 main.c
---full-slice --property main.assertion.2 --unwind 1
+--full-slice --property main.assertion.2 --unwind 1 --verbosity 10
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED
 --
 ^warning: ignoring
+^Thread 0 file main.c line 19 function doit
+^Thread 0 file main.c line 21 function doit
+^Thread 0 file main.c line 43 function main
+^Thread 0 file main.c line 44 function main
 --
 Tests whether properties are not relabelled after slicing.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -134,6 +134,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("full-slice"))
+    options.set_option("full-slice", true);
+
   if(cmdline.isset("show-symex-strategies"))
   {
     std::cout << path_strategy_chooser.show_strategies();

Original file line number	Diff line number	Diff line change
`@@ -134,6 +134,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)`
`134`	`134`	`exit(CPROVER_EXIT_USAGE_ERROR);`
`135`	`135`	`}`
`136`	`136`
	`137`	`+ if(cmdline.isset("full-slice"))`
	`138`	`+ options.set_option("full-slice", true);`
	`139`	`+`
`137`	`140`	`if(cmdline.isset("show-symex-strategies"))`
`138`	`141`	`{`
`139`	`142`	`std::cout << path_strategy_chooser.show_strategies();`