split up goto_check

goto_check inserts assertions that check for suspect bugs in both C/C++ and
Java programs.  The criteria differ vastly given that Java has basically no
instances of undefined behavior.

This commit splits the file, separating it into a checker for C/C++ and one
for Java.  The long-term plan is to move these checkers into the directory
of the corresponding language frontend.

Author: kroening

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -797,7 +797,7 @@ void janalyzer_parse_optionst::help()
     HELP_SHOW_PROPERTIES
     "\n"
     "Program instrumentation options:\n"
-    HELP_GOTO_CHECK
+    HELP_GOTO_CHECK_JAVA
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -108,7 +108,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/goto_check.h>
+#include <analyses/goto_check_java.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
@@ -128,7 +128,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
-  OPT_GOTO_CHECK \
+  OPT_GOTO_CHECK_JAVA \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
   "(show-reachable-properties)(property):" \

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -228,8 +228,8 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     "self-loops-to-assumptions",
     !cmdline.isset("no-self-loops-to-assumptions"));
 
-  // all checks supported by goto_check
-  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
+  // all checks supported by goto_check_java
+  PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options);
 
   // unwind loops in java enum static initialization
   if(cmdline.isset("java-unwind-enum-static"))
@@ -811,7 +811,7 @@ void jbmc_parse_optionst::process_goto_function(
   }
 
   // add generic checks
-  goto_check(
+  goto_check_java(
     function.get_function_id(),
     function.get_goto_function(),
     ns,

jbmc/src/jbmc/jbmc_parse_options.h

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language.h>
 
-#include <analyses/goto_check.h>
+#include <analyses/goto_check_java.h>
 
 #include <goto-checker/bmc_util.h>
 

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -75,7 +75,7 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("mm", cmdline.get_value("mm"));
 
   // all checks supported by goto_check
-  PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
+  PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options);
 
   if(cmdline.isset("debug-level"))
     options.set_option("debug-level", cmdline.get_value("debug-level"));
@@ -278,7 +278,7 @@ bool jdiff_parse_optionst::process_goto_program(
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
-    goto_check(options, goto_model, ui_message_handler);
+    goto_check_java(options, goto_model, ui_message_handler);
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);
@@ -344,7 +344,7 @@ void jdiff_parse_optionst::help()
     " --compact-output             output dependencies in compact mode\n"
     "\n"
     "Program instrumentation options:\n"
-    HELP_GOTO_CHECK
+    HELP_GOTO_CHECK_JAVA
     HELP_COVER
     "Java Bytecode frontend options:\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP

jbmc/src/jdiff/jdiff_parse_options.h

@@ -12,7 +12,7 @@ Author: Peter Schrammel
 #ifndef CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
 #define CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
 
-#include <analyses/goto_check.h>
+#include <analyses/goto_check_java.h>
 
 #include <util/parse_options.h>
 #include <util/timestamper.h>
@@ -29,7 +29,7 @@ class goto_modelt;
   "(json-ui)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
-  OPT_GOTO_CHECK \
+  OPT_GOTO_CHECK_JAVA \
   OPT_COVER \
   "(verbosity):(version)" \
   "(no-lazy-methods)" /* should go away */ \

src/analyses/Makefile

@@ -13,6 +13,8 @@ SRC = ai.cpp \
       flow_insensitive_analysis.cpp \
       global_may_alias.cpp \
       goto_check.cpp \
+      goto_check_c.cpp \
+      goto_check_java.cpp \
       goto_rw.cpp \
       guard_bdd.cpp \
       guard_expr.cpp \