move goto_check_ct to ansi-c/

The checks done in goto_check_ct are specific to C/C++, and thus belong into
the ansi-c/ directory.

This also moves goto_checkt to goto-programs/, which right now is merely a
wrapper around goto_check_ct.

Author: kroening

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -27,7 +27,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/constant_propagator.h>
 #include <analyses/dependence_graph.h>
-#include <analyses/goto_check.h>
 #include <analyses/interval_domain.h>
 #include <analyses/local_may_alias.h>
 
@@ -703,8 +702,8 @@ void janalyzer_parse_optionst::process_goto_function(
 
   remove_returns(function, function_is_stub);
 
-  // add generic checks
-  goto_check(
+  // add Java-specific checks
+  goto_check_java(
     function.get_function_id(),
     function.get_goto_function(),
     ns,

src/Makefile

@@ -59,6 +59,8 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
 .PHONY: languages
 .PHONY: clean
 
+ansi-c.dir: analyses.dir
+
 cpp.dir: ansi-c.dir linking.dir
 
 crangler.dir: util.dir json.dir

src/analyses/Makefile

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

src/ansi-c/CMakeLists.txt

@@ -127,4 +127,4 @@ set_source_files_properties(
 
 generic_includes(ansi-c)
 
-target_link_libraries(ansi-c util linking goto-programs assembler)
+target_link_libraries(ansi-c analyses util linking goto-programs assembler)

src/ansi-c/Makefile

@@ -31,6 +31,7 @@ SRC = anonymous_member.cpp \
       expr2c.cpp \
       gcc_types.cpp \
       gcc_version.cpp \
+      goto_check_c.cpp \
       literals/convert_character_literal.cpp \
       literals/convert_float_literal.cpp \
       literals/convert_integer_literal.cpp \

src/analyses/goto_check_c.cpp renamed to src/ansi-c/goto_check_c.cpp

@@ -11,9 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_check_c.h"
 
-#include <algorithm>
-#include <optional>
-
 #include <util/arith_tools.h>
 #include <util/array_name.h>
 #include <util/bitvector_expr.h>
@@ -37,13 +34,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-#include <langapi/language.h>
-#include <langapi/mode.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include "local_bitvector_analysis.h"
+#include <analyses/local_bitvector_analysis.h>
+#include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <algorithm>
+#include <optional>
 
 class goto_check_ct
 {

src/analyses/goto_check_c.h renamed to src/ansi-c/goto_check_c.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Program Transformation
 
-#ifndef CPROVER_ANALYSES_GOTO_CHECK_C_H
-#define CPROVER_ANALYSES_GOTO_CHECK_C_H
+#ifndef CPROVER_ANSI_C_GOTO_CHECK_C_H
+#define CPROVER_ANSI_C_GOTO_CHECK_C_H
 
 #include <goto-programs/goto_functions.h>
 

src/ansi-c/module_dependencies.txt

@@ -1,3 +1,4 @@
+analyses
 ansi-c
 goto-programs
 langapi # should go away

src/cbmc/cbmc_parse_options.h

@@ -12,29 +12,23 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 #define CPROVER_CBMC_CBMC_PARSE_OPTIONS_H
 
-#include <ansi-c/ansi_c_language.h>
-
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
 #include <util/validation_interface.h>
 
-#include <langapi/language.h>
-
-#include <analyses/goto_check_c.h>
-
-#include <goto-checker/bmc_util.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/goto_trace.h>
 
-#include <solvers/strings/string_refinement.h>
-
+#include <ansi-c/ansi_c_language.h>
+#include <ansi-c/goto_check_c.h>
+#include <goto-checker/bmc_util.h>
+#include <goto-instrument/cover.h>
 #include <json/json_interface.h>
+#include <langapi/language.h>
+#include <solvers/strings/string_refinement.h>
 #include <xmllang/xml_interface.h>
 
-#include <goto-instrument/cover.h>
-
 class optionst;
 
 // clang-format off

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -94,14 +94,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/ui_message.h>
 #include <util/validation_interface.h>
 
-#include <langapi/language.h>
-
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/goto_check_c.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_domain.h>
+#include <ansi-c/goto_check_c.h>
+#include <langapi/language.h>
 
 class optionst;