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;
 

src/goto-diff/goto_diff_parse_options.h

@@ -12,15 +12,14 @@ Author: Peter Schrammel
 #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
 #define CPROVER_GOTO_DIFF_GOTO_DIFF_PARSE_OPTIONS_H
 
-#include <analyses/goto_check_c.h>
-
-#include <util/ui_message.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
+#include <util/ui_message.h>
 
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
+#include <ansi-c/goto_check_c.h>
 #include <goto-instrument/cover.h>
 
 class goto_modelt;

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/ensure_one_backedge_per_target.h>
+#include <goto-programs/goto_check.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/interpreter.h>
 #include <goto-programs/label_function_pointer_call_sites.h>
@@ -50,10 +51,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/write_goto_binary.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
-#include <pointer-analysis/show_value_sets.h>
-#include <pointer-analysis/value_set_analysis.h>
-
 #include <analyses/call_graph.h>
 #include <analyses/constant_propagator.h>
 #include <analyses/custom_bitvector_analysis.h>
@@ -69,16 +66,15 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/natural_loops.h>
 #include <analyses/reaching_definitions.h>
 #include <analyses/sese_regions.h>
-
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
-
 #include <assembler/remove_asm.h>
-
 #include <cpp/cprover_library.h>
+#include <pointer-analysis/add_failed_symbols.h>
+#include <pointer-analysis/show_value_sets.h>
+#include <pointer-analysis/value_set_analysis.h>
 
-#include "accelerate/accelerate.h"
 #include "alignment_checks.h"
 #include "branch.h"
 #include "call_sequences.h"
@@ -109,6 +105,8 @@ Author: Daniel Kroening, [email protected]
 #include "unwind.h"
 #include "value_set_fi_fp_removal.h"
 
+#include "accelerate/accelerate.h"
+
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
 {

src/goto-instrument/goto_instrument_parse_options.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
 #define CPROVER_GOTO_INSTRUMENT_GOTO_INSTRUMENT_PARSE_OPTIONS_H
 
-#include <ansi-c/ansi_c_language.h>
-
 #include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
@@ -27,13 +25,11 @@ 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 <ansi-c/ansi_c_language.h>
+#include <ansi-c/goto_check_c.h>
 #include <pointer-analysis/goto_program_dereference.h>
 
 #include "aggressive_slicer.h"
-#include "contracts/contracts.h"
 #include "count_eloc.h"
 #include "document_properties.h"
 #include "dump_c.h"
@@ -43,6 +39,8 @@ Author: Daniel Kroening, [email protected]
 #include "replace_calls.h"
 #include "uninitialized.h"
 #include "unwindset.h"
+
+#include "contracts/contracts.h"
 #include "wmm/weak_memory.h"
 
 // clang-format off

src/goto-programs/Makefile

@@ -10,6 +10,7 @@ SRC = allocate_objects.cpp \
       ensure_one_backedge_per_target.cpp \
       format_strings.cpp \
       goto_asm.cpp \
+      goto_check.cpp \
       goto_clean_expr.cpp \
       goto_convert.cpp \
       goto_convert_exceptions.cpp \

src/analyses/goto_check.cpp renamed to src/goto-programs/goto_check.cpp

@@ -11,10 +11,10 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_check.h"
 
-#include "goto_check_c.h"
-
 #include <util/symbol.h>
 
+#include <ansi-c/goto_check_c.h>
+
 void goto_check(
   const irep_idt &function_identifier,
   goto_functionst::goto_functiont &goto_function,

src/analyses/goto_check.h renamed to src/goto-programs/goto_check.h

@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Checks for Errors in C and Java Programs
 
-#ifndef CPROVER_ANALYSES_GOTO_CHECK_H
-#define CPROVER_ANALYSES_GOTO_CHECK_H
+#ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
+#define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 
-#include <goto-programs/goto_functions.h>
+#include "goto_functions.h"
 
 class goto_modelt;
 class namespacet;
@@ -34,4 +34,4 @@ void goto_check(
 
 void goto_check(const optionst &, goto_modelt &, message_handlert &);
 
-#endif // CPROVER_ANALYSES_GOTO_CHECK_H
+#endif // CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H

src/goto-programs/process_goto_program.cpp

@@ -11,7 +11,8 @@ Author: Martin Brain, [email protected]
 
 #include "process_goto_program.h"
 
-#include <analyses/goto_check.h>
+#include <util/message.h>
+#include <util/options.h>
 
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_inline.h>
@@ -26,8 +27,7 @@ Author: Martin Brain, [email protected]
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
-#include <util/message.h>
-#include <util/options.h>
+#include "goto_check.h"
 
 bool process_goto_program(
   goto_modelt &goto_model,