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.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_c.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 

jbmc/src/jbmc/jbmc_parse_options.cpp

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

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -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);

jbmc/src/jdiff/jdiff_parse_options.h

@@ -12,7 +12,8 @@ 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_c.h>
+#include <analyses/goto_check_java.h>
 
 #include <util/parse_options.h>
 #include <util/timestamper.h>

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 \