Merge pull request #8546 from diffblue/show-local-bitvector

goto-analyzer: `--show-local-bitvector`

Author: tautschnig

Diff for: doc/man/goto-analyzer.1

@@ -409,6 +409,9 @@ perform taint analysis using rules in given file
 \fB\-\-show\-taint\fR
 print taint analysis results on stdout
 .TP
+\fB\-\-show\-local\-bitvector\fR
+perform procedure\-local bitvector analysis
+.TP
 \fB\-\-show\-local\-may\-alias\fR
 perform procedure\-local may alias analysis
 .SS "C/C++ frontend options:"

Diff for: regression/goto-analyzer/bitvector-analysis/basic1.c

@@ -0,0 +1,8 @@
+int some_int;
+int *pointer_global;
+
+void foobar(int *pointer_parameter)
+{
+  int *pointer_local;
+  pointer_local = &some_int;
+}

Diff for: regression/goto-analyzer/bitvector-analysis/basic1.desc

@@ -0,0 +1,8 @@
+CORE
+basic1.c
+--show-local-bitvector
+^  foobar::pointer_parameter: \+unknown$
+^  foobar::1::pointer_local: \+static_lifetime$
+^EXIT=0$
+^SIGNAL=0$
+--

Diff for: src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_symbol_table.h>
 
 #include <analyses/ai.h>
+#include <analyses/local_bitvector_analysis.h>
 #include <analyses/local_may_alias.h>
 #include <ansi-c/cprover_library.h>
 #include <ansi-c/gcc_version.h>
@@ -139,6 +140,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show-local-may-alias", true);
     options.set_option("specific-analysis", true);
   }
+  if(cmdline.isset("show-local-bitvector"))
+  {
+    options.set_option("show-local-bitvector", true);
+    options.set_option("specific-analysis", true);
+  }
 
   // Output format choice
   if(cmdline.isset("text"))
@@ -572,6 +578,23 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
     return CPROVER_EXIT_SUCCESS;
   }
 
+  if(options.get_bool_option("show-local-bitvector"))
+  {
+    namespacet ns(goto_model.symbol_table);
+
+    for(const auto &gf_entry : goto_model.goto_functions.function_map)
+    {
+      std::cout << ">>>>\n";
+      std::cout << ">>>> " << gf_entry.first << '\n';
+      std::cout << ">>>>\n";
+      local_bitvector_analysist local_bitvector_analysis(gf_entry.second, ns);
+      local_bitvector_analysis.output(std::cout, gf_entry.second, ns);
+      std::cout << '\n';
+    }
+
+    return CPROVER_EXIT_SUCCESS;
+  }
+
   label_properties(goto_model);
 
   if(cmdline.isset("show-properties"))
@@ -802,6 +825,7 @@ void goto_analyzer_parse_optionst::help()
     " {y--taint} {ufile_name} \t perform taint analysis using rules in given"
     " file\n"
     " {y--show-taint} \t print taint analysis results on stdout\n"
+    " {y--show-local-bitvector} \t perform procedure-local bitvector analysis\n"
     " {y--show-local-may-alias} \t perform procedure-local may alias analysis\n"
     "\n"
     "C/C++ frontend options:\n"

Diff for: src/goto-analyzer/goto_analyzer_parse_options.h

@@ -144,7 +144,8 @@ class optionst;
 
 #define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES \
   "(taint):(show-taint)" \
-  "(show-local-may-alias)"
+  "(show-local-may-alias)" \
+  "(show-local-bitvector)"
 
 #define GOTO_ANALYSER_OPTIONS \
   OPT_FUNCTIONS \