Merge pull request #1861 from peterschrammel/goto-diff-properties

Show properties for goto-diff

Author: peterschrammel

regression/goto-diff/java-properties/new.jar

@@ -0,0 +1,19 @@
+public class Test {
+
+  private static Test static_test = null;
+  private Test test = new Test();
+
+  public Test() {
+  }
+  
+  public int foo(int x) {
+    if (x > 10) {
+      return x;
+    } else {
+      return x * 10;
+    }
+  }
+  
+  public void newfun() {
+  }
+}

regression/goto-diff/java-properties/new/Test.java

@@ -0,0 +1,19 @@
+public class Test {
+
+  private static Test static_test = new Test();
+  private Test test = null;
+
+  public Test() {
+  }
+  
+  public int foo(int x) {
+    if (x > 10) {
+      return x;
+    } else {
+      return x * 10;
+    }
+  }
+  
+  public void obsolete() {
+  }
+}

regression/goto-diff/java-properties/old.jar

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar --json-ui --show-properties --cover location
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+  "deletedFunctions": \[\n    {\n      "name": "java::Test\.obsolete:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.obsolete:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "0",\n            "file": "Test\.java",\n            "function": "java::Test\.obsolete:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.obsolete:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n  "modifiedFunctions": \[\n    {\n      "name": "java::Test\.<init>:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "6",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "1",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "6"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 2",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.2",\n          "sourceLocation": {\n            "bytecodeIndex": "3",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 3",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.3",\n          "sourceLocation": {\n            "bytecodeIndex": "5",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4,7",\n          "description": "block 4",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.4",\n          "sourceLocation": {\n            "bytecodeIndex": "6",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.<init>:\(\)V",\n        "line": "6"\n      }\n    },\n    {\n      "name": "java::Test\.<clinit>:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "3",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.<clinit>:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "1",\n            "file": "Test\.java",\n            "function": "java::Test\.<clinit>:\(\)V",\n            "line": "3"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.<clinit>:\(\)V",\n        "line": "3"\n      }\n    }\n  ],\n  "newFunctions": \[\n    {\n      "name": "java::Test\.newfun:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.newfun:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "0",\n            "file": "Test\.java",\n            "function": "java::Test\.newfun:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.newfun:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n
+--
+^warning: ignoring

regression/goto-diff/java-properties/old/Test.java

@@ -534,7 +534,8 @@ int cbmc_parse_optionst::doit()
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
-    show_properties(goto_model, ui_message_handler.get_ui());
+    show_properties(
+      goto_model, get_message_handler(), ui_message_handler.get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -923,7 +924,7 @@ void cbmc_parse_optionst::help()
     " cbmc file.c ...              source file names\n"
     "\n"
     "Analysis options:\n"
-    " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+    HELP_SHOW_PROPERTIES
     " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n" // NOLINT(*)
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)

regression/goto-diff/java-properties/test.desc

@@ -53,9 +53,9 @@ class optionst;
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-claims)(claim):(show-properties)" \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
@@ -72,7 +72,7 @@ class optionst;
   "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
-  "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+  "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
 class cbmc_parse_optionst:

src/cbmc/cbmc_parse_options.cpp

@@ -150,7 +150,7 @@ int clobber_parse_optionst::doit()
 
     if(cmdline.isset("show-properties"))
     {
-      show_properties(goto_model, get_ui());
+      show_properties(goto_model, get_message_handler(), get_ui());
       return 0;
     }
 

src/cbmc/cbmc_parse_options.h

@@ -19,23 +19,27 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/goto_check.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define CLOBBER_OPTIONS \
   "(depth):(context-bound):(unwind):" \
   OPT_GOTO_CHECK \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(no-assertions)(no-assumptions)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
   "(string-abstraction)" \
-  "(show-locs)(show-vcc)(show-properties)(show-trace)" \
+  "(show-locs)(show-vcc)(show-trace)" \
   "(property):" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS
+// clang-format on
 
 class clobber_parse_optionst:
   public parse_options_baset,

src/clobber/clobber_parse_options.cpp

@@ -592,7 +592,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, get_ui());
+    show_properties(goto_model, get_message_handler(), get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -815,6 +815,7 @@ void goto_analyzer_parse_optionst::help()
 
   std::cout << " * *\n";
 
+  // clang-format off
   std::cout <<
     "* *                Daniel Kroening, DiffBlue                * *\n"
     "* *                 [email protected]                   * *\n"
@@ -898,8 +899,7 @@ void goto_analyzer_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --show-properties            show the properties, but don't run analysis\n"
+    HELP_SHOW_PROPERTIES
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
@@ -908,4 +908,5 @@ void goto_analyzer_parse_optionst::help()
     " --version                    show version and exit\n"
     HELP_TIMESTAMP
     "\n";
+  // clang-format on
 }