Merge pull request diffblue#2523 from peterschrammel/do-not-ignore-full-slice

Do not ignore --full-slice

Author: Daniel Kroening

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

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.

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();