Merge pull request #3207 from smowton/smowton/feature/jbmc-list-symbols

JBMC: support list-symbols

Author: smowton

jbmc/regression/jbmc/list-symbols/Test.class

@@ -0,0 +1,8 @@
+
+public class Test {
+
+  public static void main(String[] args) {
+
+  }
+
+}

jbmc/regression/jbmc/list-symbols/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--list-symbols --json-ui
+"java::Test.main:\(\[Ljava/lang/String;\)V": \{
+^EXIT=0$
+^SIGNAL=0$
+--
+"value":

jbmc/regression/jbmc/list-symbols/test_json.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--list-symbols
+^java::Test\.main:\(\[Ljava/lang/String;\)V \(struct java::array\[reference\] \*\) -> void$
+^EXIT=0$
+^SIGNAL=0$

jbmc/regression/jbmc/list-symbols/test_plain.desc

@@ -649,8 +649,12 @@ int jbmc_parse_optionst::get_goto_program(
     // values, etc
     if(cmdline.isset("show-symbol-table"))
     {
-      show_symbol_table(
-        lazy_goto_model.symbol_table, ui_message_handler);
+      show_symbol_table(lazy_goto_model.symbol_table, ui_message_handler);
+      return 0;
+    }
+    else if(cmdline.isset("list-symbols"))
+    {
+      show_symbol_table_brief(lazy_goto_model.symbol_table, ui_message_handler);
       return 0;
     }
 
@@ -821,8 +825,12 @@ bool jbmc_parse_optionst::show_loaded_functions(
 {
   if(cmdline.isset("show-symbol-table"))
   {
-    show_symbol_table(
-      goto_model.get_symbol_table(), ui_message_handler);
+    show_symbol_table(goto_model.get_symbol_table(), ui_message_handler);
+    return true;
+  }
+  else if(cmdline.isset("list-symbols"))
+  {
+    show_symbol_table_brief(goto_model.get_symbol_table(), ui_message_handler);
     return true;
   }
 
@@ -1056,6 +1064,7 @@ void jbmc_parse_optionst::help()
     "Program representations:\n"
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show loaded symbol table\n"
+    " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
     " --drop-unused-functions      drop functions trivially unreachable\n"
     "                              from main function\n"

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -59,7 +59,9 @@ class optionst;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_CLASS_HIERARCHY \
   "(show-loops)" \
-  "(show-symbol-table)(show-parse-tree)" \
+  "(show-symbol-table)" \
+  "(list-symbols)" \
+  "(show-parse-tree)" \
   OPT_SHOW_PROPERTIES \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \

jbmc/src/jbmc/jbmc_parse_options.h

@@ -266,9 +266,6 @@ static void show_symbol_table_brief_json_ui(
     if(symbol.type.is_not_nil())
       ptr->from_type(symbol.type, type_str, ns);
 
-    if(symbol.value.is_not_nil())
-      ptr->from_expr(symbol.value, value_str, ns);
-
     json_objectt symbol_json;
     symbol_json["prettyName"] = json_stringt(symbol.pretty_name);
     symbol_json["baseName"] = json_stringt(symbol.base_name);