Add parse option to display points-to set information for pointer dereference

The points to set information provides some intuition about the complexity
of the resulting case split expression in case of a pointer dereference.
This commit adds parse option --show-points-to-sets to track the size and
contents of the points-to set for pointers.

cpp lint bmc_util.h

Add error message for plain and xml format output

Author: Natasha Yogananda Jeppu

src/cbmc/cbmc_parse_options.cpp

@@ -522,7 +522,16 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show-goto-symex-steps", true);
 
   if(cmdline.isset("show-points-to-sets"))
+  {
+    if(!cmdline.isset("json-ui"))
+    {
+      log.error() << "--show-points-to-sets supports only"
+                     " json output. Use --json-ui."
+                  << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
     options.set_option("show-points-to-sets", true);
+  }
 
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }

src/goto-checker/bmc_util.h

@@ -205,7 +205,7 @@ void run_property_decider(
   " --show-goto-symex-steps      show which steps symex travels, includes " \
   "                              diagnostic information\n" \
   " --show-points-to-sets        show points-to sets for\n" \
-  "                              pointer dereference\n" \
+  "                              pointer dereference. Requires --json-ui.\n" \
   " --program-only               only show program expression\n" \
   " --show-byte-ops              show all byte extracts and updates\n" \
   " --show-loops                 show the loops in the program\n" \