Enable show-properties with symex-driven lazy loading

This can be accommodated using the same post-symex reporting phase as show-goto-functions et al.
The one cbmc-java test that uses --show-properties is consequently re-enabled.

Author: smowton

regression/cbmc-java/covered1/test.desc

@@ -1,19 +1,19 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE
 covered1.class
---cover location --json-ui --show-properties
+--cover location --json-ui --show-properties --function 'covered1.<init>'
 ^EXIT=0$
 ^SIGNAL=0$
 .*\"coveredLines\": \"22\",$
-.*\"coveredLines\": \"4\",$
-.*\"coveredLines\": \"6\",$
-.*\"coveredLines\": \"7\",$
-.*\"coveredLines\": \"23\",$
-.*\"coveredLines\": \"24\",$
-.*\"coveredLines\": \"25\",$
-.*\"coveredLines\": \"31\",$
-.*\"coveredLines\": \"32\",$
-.*\"coveredLines\": \"33\",$
-.*\"coveredLines\": \"36\",$
+(.*\"coveredLines\": \"4\")|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"6\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"7\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"23\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"24\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"25\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"31\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"32\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"33\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"36\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
 .*\"coveredLines\": \"26\",$
 .*\"coveredLines\": \"28\",$
 .*\"coveredLines\": \"28\",$
@@ -26,4 +26,8 @@ covered1.class
 --
 ^warning: ignoring
 --
-This fails with symex-driven lazy loading because it does not currently support --show-properties.
+The alternation between the grouped and ungrouped reporting formats for coveredLines accommodates the
+difference between symex-driven-lazy-loading (which currently causes jbmc to use the grouped format)
+and normal loading (which uses the ungrouped format).
+The cause of the difference appears to be symex-driven loading being more pessimistic about possible
+exceptions coming from callees, which in turn changes the shape of the CFG.

src/jbmc/jbmc_parse_options.cpp

@@ -384,7 +384,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     for(const char *opt :
       { "nondet-static",
         "full-slice",
-        "show-properties",
         "lazy-methods" })
     {
       if(cmdline.isset(opt))
@@ -851,6 +850,17 @@ bool jbmc_parse_optionst::show_loaded_functions(
     return true;
   }
 
+  if(cmdline.isset("show-properties"))
+  {
+    namespacet ns(goto_model.get_symbol_table());
+    show_properties(
+      ns,
+      get_message_handler(),
+      ui_message_handler.get_ui(),
+      goto_model.get_goto_functions());
+    return true;
+  }
+
   return false;
 }