From 75b960299c1e8e188a29e9e146afece26754c2d7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 1 Apr 2024 13:49:06 -0700 Subject: [PATCH 1/2] move goto_convert from goto-programs/ to ansi-c/ The goto_convertt class and associated helpers convert a C parse tree into a set of GOTO functions. They are specific to C, and hence, should be in the ansi-c/ directory. --- .../java_bytecode/assignments_from_json.cpp | 3 +- .../src/java_bytecode/convert_java_nondet.cpp | 3 +- jbmc/src/java_bytecode/java_object_factory.h | 6 +- .../java_string_library_preprocess.cpp | 3 +- .../java_bytecode/lazy_goto_functions_map.h | 11 +- jbmc/src/java_bytecode/nondet.cpp | 4 +- jbmc/src/java_bytecode/remove_java_new.cpp | 3 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 2 +- .../module_dependencies.txt | 1 + .../virtual_call_null_checks.cpp | 9 +- .../module_dependencies.txt | 1 + .../java_replace_nondet/replace_nondet.cpp | 6 +- .../module_dependencies.txt | 1 + .../virtual_functions.cpp | 12 +- .../java_bytecode/module_dependencies.txt | 1 + src/ansi-c/Makefile | 19 +- .../allocate_objects.cpp | 2 +- .../allocate_objects.h | 0 src/ansi-c/c_nondet_symbol_factory.cpp | 4 +- src/ansi-c/c_nondet_symbol_factory.h | 4 +- .../goto-conversion}/builtin_functions.cpp | 0 .../goto-conversion}/destructor.cpp | 3 +- .../goto-conversion}/destructor.h | 0 .../goto-conversion}/format_strings.cpp | 0 .../goto-conversion}/format_strings.h | 0 .../goto-conversion}/goto_asm.cpp | 0 .../{ => goto-conversion}/goto_check_c.cpp | 2 +- .../{ => goto-conversion}/goto_check_c.h | 0 .../goto-conversion}/goto_clean_expr.cpp | 0 .../goto-conversion}/goto_convert.cpp | 4 +- .../goto-conversion}/goto_convert.h | 0 .../goto-conversion}/goto_convert_class.h | 8 +- .../goto_convert_exceptions.cpp | 0 .../goto_convert_function_call.cpp | 0 .../goto_convert_functions.cpp | 2 +- .../goto-conversion}/goto_convert_functions.h | 3 +- .../goto_convert_side_effect.cpp | 0 .../goto-conversion}/link_to_library.cpp | 7 +- .../goto-conversion}/link_to_library.h | 0 .../goto-conversion/module_dependencies.txt | 4 + .../goto-conversion}/scope_tree.cpp | 0 .../goto-conversion}/scope_tree.h | 0 .../string_instrumentation.cpp | 3 +- .../goto-conversion}/string_instrumentation.h | 0 .../printf_formatter.h | 0 src/cbmc/cbmc_parse_options.cpp | 2 +- src/cbmc/cbmc_parse_options.h | 2 +- .../goto_analyzer_parse_options.cpp | 2 +- .../goto_analyzer_parse_options.h | 2 +- src/goto-cc/compile.cpp | 2 +- src/goto-cc/linker_script_merge.cpp | 2 +- src/goto-diff/goto_diff_parse_options.cpp | 2 +- src/goto-diff/goto_diff_parse_options.h | 2 +- .../function_call_harness_generator.cpp | 5 +- .../memory_snapshot_harness_generator.cpp | 2 +- src/goto-instrument/contracts/cfg_info.h | 2 +- src/goto-instrument/contracts/contracts.h | 2 +- .../contracts/dynamic-frames/dfcc.cpp | 4 +- .../dfcc_contract_clauses_codegen.h | 2 +- .../dynamic-frames/dfcc_contract_functions.h | 2 +- .../dynamic-frames/dfcc_contract_handler.h | 2 +- .../dynamic-frames/dfcc_instrument_loop.cpp | 2 +- .../contracts/dynamic-frames/dfcc_library.cpp | 2 +- .../dynamic-frames/dfcc_spec_functions.cpp | 2 +- .../dynamic-frames/dfcc_swap_and_wrap.cpp | 2 +- .../dynamic-frames/dfcc_swap_and_wrap.h | 2 +- .../contracts/dynamic-frames/dfcc_utils.cpp | 2 +- .../dynamic-frames/dfcc_wrapper_program.h | 2 +- .../contracts/memory_predicates.cpp | 3 +- src/goto-instrument/contracts/utils.h | 2 +- .../generate_function_bodies.cpp | 14 +- .../goto_instrument_parse_options.cpp | 2 +- .../goto_instrument_parse_options.h | 2 +- src/goto-instrument/model_argc_argv.cpp | 14 +- src/goto-instrument/stack_depth.cpp | 2 +- src/goto-programs/Makefile | 17 +- src/goto-programs/goto_trace.cpp | 3 +- src/goto-programs/initialize_goto_model.cpp | 2 +- src/goto-programs/printf_formatter.cpp | 322 ------------------ src/goto-programs/process_goto_program.cpp | 4 +- src/goto-programs/xml_goto_trace.cpp | 2 +- src/goto-synthesizer/cegis_verifier.cpp | 4 +- src/libcprover-cpp/api.cpp | 2 +- src/libcprover-cpp/api_options.cpp | 2 +- src/linking/module_dependencies.txt | 1 + src/linking/static_lifetime_init.cpp | 3 +- src/memory-analyzer/analyze_symbol.h | 12 +- src/symtab2gb/symtab2gb_parse_options.cpp | 2 +- unit/Makefile | 2 +- unit/analyses/ai/ai.cpp | 16 +- unit/analyses/call_graph.cpp | 13 +- unit/analyses/constant_propagator.cpp | 12 +- unit/analyses/dependence_graph.cpp | 9 +- .../disconnect_unreachable_nodes_in_graph.cpp | 13 +- .../allocate_objects.cpp | 2 +- unit/goto-programs/goto_program_validate.cpp | 2 +- unit/goto-programs/module_dependencies.txt | 1 + unit/testing-utils/get_goto_model_from_c.cpp | 11 +- 98 files changed, 184 insertions(+), 494 deletions(-) rename src/{goto-programs => ansi-c}/allocate_objects.cpp (99%) rename src/{goto-programs => ansi-c}/allocate_objects.h (100%) rename src/{goto-programs => ansi-c/goto-conversion}/builtin_functions.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/destructor.cpp (96%) rename src/{goto-programs => ansi-c/goto-conversion}/destructor.h (100%) rename src/{goto-programs => ansi-c/goto-conversion}/format_strings.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/format_strings.h (100%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_asm.cpp (100%) rename src/ansi-c/{ => goto-conversion}/goto_check_c.cpp (99%) rename src/ansi-c/{ => goto-conversion}/goto_check_c.h (100%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_clean_expr.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert.cpp (99%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert.h (100%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert_class.h (99%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert_exceptions.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert_function_call.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert_functions.cpp (99%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert_functions.h (97%) rename src/{goto-programs => ansi-c/goto-conversion}/goto_convert_side_effect.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/link_to_library.cpp (97%) rename src/{goto-programs => ansi-c/goto-conversion}/link_to_library.h (100%) create mode 100644 src/ansi-c/goto-conversion/module_dependencies.txt rename src/{goto-programs => ansi-c/goto-conversion}/scope_tree.cpp (100%) rename src/{goto-programs => ansi-c/goto-conversion}/scope_tree.h (100%) rename src/{goto-programs => ansi-c/goto-conversion}/string_instrumentation.cpp (99%) rename src/{goto-programs => ansi-c/goto-conversion}/string_instrumentation.h (100%) rename src/{goto-programs => ansi-c}/printf_formatter.h (100%) rename unit/{goto-programs => ansi-c}/allocate_objects.cpp (95%) diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index f9e7a075807..27c24522499 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -16,7 +16,8 @@ Author: Diffblue Ltd. #include #include -#include +#include + #include #include diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp index 73cfbba2aab..8df3b972964 100644 --- a/jbmc/src/java_bytecode/convert_java_nondet.cpp +++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp @@ -11,10 +11,11 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com #include "convert_java_nondet.h" -#include #include #include +#include + #include "java_object_factory.h" // gen_nondet_init #include "java_object_factory_parameters.h" #include "java_utils.h" diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index f55c5e31c09..34b1a51a5d8 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -71,11 +71,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H #define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H -#include "nondet.h" +#include -#include +#include -#include +#include "nondet.h" class message_handlert; class select_pointer_typet; diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 3fed7144ed6..992b4c2c925 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -29,9 +29,10 @@ Date: April 2017 #include #include -#include #include +#include + #include "java_types.h" #include "java_utils.h" diff --git a/jbmc/src/java_bytecode/lazy_goto_functions_map.h b/jbmc/src/java_bytecode/lazy_goto_functions_map.h index aaff168b2a6..4d7e2dcd641 100644 --- a/jbmc/src/java_bytecode/lazy_goto_functions_map.h +++ b/jbmc/src/java_bytecode/lazy_goto_functions_map.h @@ -6,15 +6,16 @@ #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H -#include +#include +#include +#include -#include #include +#include #include -#include -#include -#include + +#include /// Provides a wrapper for a map of lazily loaded goto_functiont. /// This incrementally builds a goto-functions object, while permitting diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp index 5269e7004b3..e07ff81f441 100644 --- a/jbmc/src/java_bytecode/nondet.cpp +++ b/jbmc/src/java_bytecode/nondet.cpp @@ -8,10 +8,10 @@ Author: Diffblue Ltd. #include "nondet.h" -#include - #include +#include + symbol_exprt generate_nondet_int( const exprt &min_value_expr, const exprt &max_value_expr, diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp index 09bb31e5c47..c30f5f6d925 100644 --- a/jbmc/src/java_bytecode/remove_java_new.cpp +++ b/jbmc/src/java_bytecode/remove_java_new.cpp @@ -19,9 +19,10 @@ Author: Peter Schrammel #include #include -#include #include +#include + #include "java_types.h" #include "java_utils.h" diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 127d2baa290..52d682a497b 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -33,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt b/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt index 4eee39351ab..8522973946b 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/module_dependencies.txt @@ -1,3 +1,4 @@ +ansi-c testing-utils java-testing-utils analyses diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp index 03858d427a1..18ec6f3747a 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp @@ -8,13 +8,14 @@ Author: Diffblue Limited. \*******************************************************************/ #include -#include -#include -#include -#include #include +#include +#include +#include +#include + // We're expecting a call "something->field . B.virtualmethod()": static bool is_expected_virtualmethod_call( const goto_programt::instructiont &instruction) diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt b/jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt index 0107f1ecef3..5e7f5fe02ee 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt @@ -1,3 +1,4 @@ +ansi-c goto-programs java_bytecode java-testing-utils diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index 1368a14874e..f6ec3b17f85 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -8,18 +8,18 @@ Author: Diffblue Ltd. \*******************************************************************/ #include -#include -#include #include -#include #include #include +#include #include #include #include #include +#include +#include void validate_nondet_method_removed( std::list instructions) diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt b/jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt index b139ad5e0b6..1e7ec2cef1f 100644 --- a/jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt @@ -1,3 +1,4 @@ +ansi-c/goto-conversion goto-instrument goto-programs java_bytecode diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index 8d0e4e77205..032e258d1a0 100644 --- a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -7,15 +7,17 @@ Author: Diffblue Ltd. \*******************************************************************/ #include -#include -#include -#include -#include #include -#include #include +#include + +#include +#include +#include +#include + void check_function_call( const equal_exprt &eq_expr, const irep_idt &class_name, diff --git a/jbmc/unit/java_bytecode/module_dependencies.txt b/jbmc/unit/java_bytecode/module_dependencies.txt index cf76ca4cef0..39be06fe9c3 100644 --- a/jbmc/unit/java_bytecode/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/module_dependencies.txt @@ -1,3 +1,4 @@ +ansi-c java_bytecode linking testing-utils diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 64ffa497072..642fb39ee9f 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -1,4 +1,5 @@ -SRC = anonymous_member.cpp \ +SRC = allocate_objects.cpp \ + anonymous_member.cpp \ ansi_c_convert_type.cpp \ ansi_c_declaration.cpp \ ansi_c_entry_point.cpp \ @@ -11,6 +12,7 @@ SRC = anonymous_member.cpp \ ansi_c_typecheck.cpp \ ansi_c_y.tab.cpp \ builtin_factory.cpp \ + printf_formatter.cpp \ c_expr.cpp \ c_misc.cpp \ c_nondet_symbol_factory.cpp \ @@ -32,7 +34,20 @@ SRC = anonymous_member.cpp \ expr2c.cpp \ gcc_types.cpp \ gcc_version.cpp \ - goto_check_c.cpp \ + goto-conversion/builtin_functions.cpp \ + goto-conversion/goto_asm.cpp \ + goto-conversion/destructor.cpp \ + goto-conversion/format_strings.cpp \ + goto-conversion/goto_convert.cpp \ + goto-conversion/goto_check_c.cpp \ + goto-conversion/goto_convert_exceptions.cpp \ + goto-conversion/goto_clean_expr.cpp \ + goto-conversion/goto_convert_functions.cpp \ + goto-conversion/goto_convert_function_call.cpp \ + goto-conversion/goto_convert_side_effect.cpp \ + goto-conversion/link_to_library.cpp \ + goto-conversion/scope_tree.cpp \ + goto-conversion/string_instrumentation.cpp \ literals/convert_character_literal.cpp \ literals/convert_float_literal.cpp \ literals/convert_integer_literal.cpp \ diff --git a/src/goto-programs/allocate_objects.cpp b/src/ansi-c/allocate_objects.cpp similarity index 99% rename from src/goto-programs/allocate_objects.cpp rename to src/ansi-c/allocate_objects.cpp index 7c743725b33..b691e06e0a9 100644 --- a/src/goto-programs/allocate_objects.cpp +++ b/src/ansi-c/allocate_objects.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "goto_instruction_code.h" +#include /// Allocates a new object, either by creating a local variable with automatic /// lifetime, a global variable with static lifetime, or by dynamically diff --git a/src/goto-programs/allocate_objects.h b/src/ansi-c/allocate_objects.h similarity index 100% rename from src/goto-programs/allocate_objects.h rename to src/ansi-c/allocate_objects.h diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 7154bbfd5cd..7f32b16e122 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -20,10 +20,10 @@ Author: Diffblue Ltd. #include #include -#include #include -#include +#include "allocate_objects.h" +#include "c_object_factory_parameters.h" /// Creates a nondet for expr, including calling itself recursively to make /// appropriate symbols to point to if expr is a pointer. diff --git a/src/ansi-c/c_nondet_symbol_factory.h b/src/ansi-c/c_nondet_symbol_factory.h index ebca599694c..2d7d768233c 100644 --- a/src/ansi-c/c_nondet_symbol_factory.h +++ b/src/ansi-c/c_nondet_symbol_factory.h @@ -12,9 +12,9 @@ Author: Diffblue Ltd. #ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H #define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H -#include +#include "allocate_objects.h" -#include +#include struct c_object_factory_parameterst; diff --git a/src/goto-programs/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp similarity index 100% rename from src/goto-programs/builtin_functions.cpp rename to src/ansi-c/goto-conversion/builtin_functions.cpp diff --git a/src/goto-programs/destructor.cpp b/src/ansi-c/goto-conversion/destructor.cpp similarity index 96% rename from src/goto-programs/destructor.cpp rename to src/ansi-c/goto-conversion/destructor.cpp index 29ff573929b..2ecc88dfa7a 100644 --- a/src/goto-programs/destructor.cpp +++ b/src/ansi-c/goto-conversion/destructor.cpp @@ -10,7 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com /// Destructor Calls #include "destructor.h" -#include "goto_instruction_code.h" + +#include #include #include diff --git a/src/goto-programs/destructor.h b/src/ansi-c/goto-conversion/destructor.h similarity index 100% rename from src/goto-programs/destructor.h rename to src/ansi-c/goto-conversion/destructor.h diff --git a/src/goto-programs/format_strings.cpp b/src/ansi-c/goto-conversion/format_strings.cpp similarity index 100% rename from src/goto-programs/format_strings.cpp rename to src/ansi-c/goto-conversion/format_strings.cpp diff --git a/src/goto-programs/format_strings.h b/src/ansi-c/goto-conversion/format_strings.h similarity index 100% rename from src/goto-programs/format_strings.h rename to src/ansi-c/goto-conversion/format_strings.h diff --git a/src/goto-programs/goto_asm.cpp b/src/ansi-c/goto-conversion/goto_asm.cpp similarity index 100% rename from src/goto-programs/goto_asm.cpp rename to src/ansi-c/goto-conversion/goto_asm.cpp diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp similarity index 99% rename from src/ansi-c/goto_check_c.cpp rename to src/ansi-c/goto-conversion/goto_check_c.cpp index a05a6520a69..39451755393 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -39,7 +39,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "c_expr.h" +#include #include diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto-conversion/goto_check_c.h similarity index 100% rename from src/ansi-c/goto_check_c.h rename to src/ansi-c/goto-conversion/goto_check_c.h diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp similarity index 100% rename from src/goto-programs/goto_clean_expr.cpp rename to src/ansi-c/goto-conversion/goto_clean_expr.cpp diff --git a/src/goto-programs/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp similarity index 99% rename from src/goto-programs/goto_convert.cpp rename to src/ansi-c/goto-conversion/goto_convert.cpp index f7725df3136..2a79ffd9f35 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Program Transformation +#include "destructor.h" #include "goto_convert.h" #include "goto_convert_class.h" @@ -24,8 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "destructor.h" -#include "remove_skip.h" +#include static bool is_empty(const goto_programt &goto_program) { diff --git a/src/goto-programs/goto_convert.h b/src/ansi-c/goto-conversion/goto_convert.h similarity index 100% rename from src/goto-programs/goto_convert.h rename to src/ansi-c/goto-conversion/goto_convert.h diff --git a/src/goto-programs/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h similarity index 99% rename from src/goto-programs/goto_convert_class.h rename to src/ansi-c/goto-conversion/goto_convert_class.h index ee10e914326..b23f569b692 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -17,14 +17,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "allocate_objects.h" -#include "goto_program.h" -#include "scope_tree.h" +#include + +#include #include #include #include +#include "scope_tree.h" + class side_effect_expr_overflowt; struct build_declaration_hops_inputst; diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp similarity index 100% rename from src/goto-programs/goto_convert_exceptions.cpp rename to src/ansi-c/goto-conversion/goto_convert_exceptions.cpp diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp similarity index 100% rename from src/goto-programs/goto_convert_function_call.cpp rename to src/ansi-c/goto-conversion/goto_convert_function_call.cpp diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/ansi-c/goto-conversion/goto_convert_functions.cpp similarity index 99% rename from src/goto-programs/goto_convert_functions.cpp rename to src/ansi-c/goto-conversion/goto_convert_functions.cpp index 6370dbd9ad7..c12dd711bf7 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_functions.cpp @@ -15,7 +15,7 @@ Date: June 2003 #include -#include "goto_model.h" +#include goto_convert_functionst::goto_convert_functionst( symbol_table_baset &_symbol_table, diff --git a/src/goto-programs/goto_convert_functions.h b/src/ansi-c/goto-conversion/goto_convert_functions.h similarity index 97% rename from src/goto-programs/goto_convert_functions.h rename to src/ansi-c/goto-conversion/goto_convert_functions.h index 374a51b84aa..b19d9008fa5 100644 --- a/src/goto-programs/goto_convert_functions.h +++ b/src/ansi-c/goto-conversion/goto_convert_functions.h @@ -15,7 +15,8 @@ Date: June 2003 #define CPROVER_GOTO_PROGRAMS_GOTO_CONVERT_FUNCTIONS_H #include "goto_convert_class.h" -#include "goto_functions.h" + +#include class goto_modelt; diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp similarity index 100% rename from src/goto-programs/goto_convert_side_effect.cpp rename to src/ansi-c/goto-conversion/goto_convert_side_effect.cpp diff --git a/src/goto-programs/link_to_library.cpp b/src/ansi-c/goto-conversion/link_to_library.cpp similarity index 97% rename from src/goto-programs/link_to_library.cpp rename to src/ansi-c/goto-conversion/link_to_library.cpp index f3743320920..b66fe9fec93 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/ansi-c/goto-conversion/link_to_library.cpp @@ -13,10 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "compute_called_functions.h" +#include +#include +#include + #include "goto_convert_functions.h" -#include "goto_model.h" -#include "link_goto_model.h" /// Try to add \p missing_function from \p library to \p goto_model. static std::pair, bool> diff --git a/src/goto-programs/link_to_library.h b/src/ansi-c/goto-conversion/link_to_library.h similarity index 100% rename from src/goto-programs/link_to_library.h rename to src/ansi-c/goto-conversion/link_to_library.h diff --git a/src/ansi-c/goto-conversion/module_dependencies.txt b/src/ansi-c/goto-conversion/module_dependencies.txt new file mode 100644 index 00000000000..124027548b1 --- /dev/null +++ b/src/ansi-c/goto-conversion/module_dependencies.txt @@ -0,0 +1,4 @@ +ansi-c +goto-programs +linking +util diff --git a/src/goto-programs/scope_tree.cpp b/src/ansi-c/goto-conversion/scope_tree.cpp similarity index 100% rename from src/goto-programs/scope_tree.cpp rename to src/ansi-c/goto-conversion/scope_tree.cpp diff --git a/src/goto-programs/scope_tree.h b/src/ansi-c/goto-conversion/scope_tree.h similarity index 100% rename from src/goto-programs/scope_tree.h rename to src/ansi-c/goto-conversion/scope_tree.h diff --git a/src/goto-programs/string_instrumentation.cpp b/src/ansi-c/goto-conversion/string_instrumentation.cpp similarity index 99% rename from src/goto-programs/string_instrumentation.cpp rename to src/ansi-c/goto-conversion/string_instrumentation.cpp index 62db57cf331..84138e98d4c 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/ansi-c/goto-conversion/string_instrumentation.cpp @@ -20,10 +20,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include +#include "format_strings.h" + exprt is_zero_string(const exprt &what, bool write) { unary_exprt result{"is_zero_string", what, c_bool_type()}; diff --git a/src/goto-programs/string_instrumentation.h b/src/ansi-c/goto-conversion/string_instrumentation.h similarity index 100% rename from src/goto-programs/string_instrumentation.h rename to src/ansi-c/goto-conversion/string_instrumentation.h diff --git a/src/goto-programs/printf_formatter.h b/src/ansi-c/printf_formatter.h similarity index 100% rename from src/goto-programs/printf_formatter.h rename to src/ansi-c/printf_formatter.h diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ae9c2876c9d..ccc9a9991e4 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -34,6 +33,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 303c6feddac..de50b68b1f0 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include #include diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4c18f105002..830f3f9f509 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -29,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index a78643b12d7..20561d539da 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -100,7 +100,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include class optionst; diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 8eec5b937ae..3631189d812 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -23,13 +23,13 @@ Date: June 2006 #include #include -#include #include #include #include #include #include +#include #include #include #include diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index c5210821505..5736e05a5af 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -17,10 +17,10 @@ Author: Kareem Khazem , 2017 #include #include -#include #include #include +#include #include #include diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 97c98673100..627ae6e3d41 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -18,7 +18,6 @@ Author: Peter Schrammel #include #include -#include #include #include #include @@ -27,6 +26,7 @@ Author: Peter Schrammel #include #include +#include #include #include #include diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index c0518775a64..0bb4855de78 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -19,7 +19,7 @@ Author: Peter Schrammel #include #include -#include +#include #include class goto_modelt; diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index d32e51bf6d5..4cc363d4319 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -16,10 +16,11 @@ Author: Diffblue Ltd. #include #include -#include -#include #include +#include +#include + #include "function_harness_generator_options.h" #include "goto_harness_generator_factory.h" #include "recursive_initialization.h" diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index e45f5c5856f..c91da54f11d 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -16,9 +16,9 @@ Author: Daniel Poetzl #include #include -#include #include +#include #include #include diff --git a/src/goto-instrument/contracts/cfg_info.h b/src/goto-instrument/contracts/cfg_info.h index c8d1c5f1482..42c2c35a127 100644 --- a/src/goto-instrument/contracts/cfg_info.h +++ b/src/goto-instrument/contracts/cfg_info.h @@ -15,7 +15,7 @@ Date: June 2022 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CFG_INFO_H -#include +#include #include #include diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index ddf4358bc57..79a462815fd 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -14,7 +14,7 @@ Date: February 2016 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H -#include +#include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 4adf164a203..0e420e372c7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -23,12 +23,10 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include -#include #include #include #include #include -#include #include #include @@ -36,6 +34,8 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include +#include +#include #include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h index 1bd4ab125bd..e78b59b660e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h @@ -14,7 +14,7 @@ Date: February 2023 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H -#include +#include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h index 963dc5fdf60..9a407761388 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h @@ -14,7 +14,7 @@ Date: August 2022 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H -#include +#include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h index 0f77b883876..40a1e4ef70a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h @@ -13,7 +13,7 @@ Date: August 2022 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_HANDLER_H -#include +#include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index f0fab83d6bb..b14187a44e9 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -11,7 +11,7 @@ Date: April 2023 \*******************************************************************/ #include "dfcc_instrument_loop.h" -#include +#include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 4dcb8c9316d..63c4d804600 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -18,13 +18,13 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include -#include #include #include #include #include #include +#include #include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 266e447ef43..3bfa11b4ffc 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -7,7 +7,7 @@ Author: Remi Delmas, delmarsd@amazon.com \*******************************************************************/ #include "dfcc_spec_functions.h" -#include +#include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp index 642aa105604..21c886befe0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp @@ -25,11 +25,11 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include -#include #include #include #include +#include #include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h index 391ea29db93..737bd3392c8 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h @@ -22,7 +22,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include -#include +#include #include "dfcc_contract_handler.h" #include "dfcc_instrument.h" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index 4df01f60750..bd501d020a1 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -19,10 +19,10 @@ Date: August 2022 #include #include -#include #include #include +#include #include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h index 945999f9bfd..224bdf8f795 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h @@ -13,7 +13,7 @@ Author: Remi Delmas, delmasrd@amazon.com #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_WRAPPER_PROGRAM_H -#include +#include #include #include diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index d36da815fb2..c0d2dbe5ce6 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -19,9 +19,8 @@ Date: July 2021 #include #include -#include - #include +#include #include #include "instrument_spec_assigns.h" diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 0d1546965ef..f7b7ac5e285 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -11,7 +11,7 @@ Date: September 2021 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H -#include +#include #include #include diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index be24ed70d30..bff129baa70 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -8,19 +8,19 @@ Author: Diffblue Ltd. #include "generate_function_bodies.h" -#include - -#include -#include -#include -#include - #include #include #include #include #include +#include +#include + +#include +#include +#include + void generate_function_bodiest::generate_function_body( goto_functiont &function, symbol_tablet &symbol_table, diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index b26f65efe26..80be4eb8166 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -68,6 +67,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5b64af490e5..1eeae98c837 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "aggressive_slicer.h" diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index 70d9e209208..2306737d06b 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -13,23 +13,23 @@ Date: April 2016 #include "model_argc_argv.h" -#include - +#include #include #include #include #include -#include +#include #include #include -#include -#include - -#include #include #include +#include +#include + +#include + /// Set up argv with up to max_argc pointers into an array of 4096 bytes. /// \param goto_model: Contains the input program's symbol table and /// intermediate representation diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index b8affc60471..2b370cf1d3b 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -17,9 +17,9 @@ Date: November 2011 #include #include -#include #include +#include #include static symbol_exprt add_stack_depth_symbol( diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 12d48868fc7..21b06168563 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,21 +1,10 @@ -SRC = allocate_objects.cpp \ - adjust_float_expressions.cpp \ - builtin_functions.cpp \ +SRC = adjust_float_expressions.cpp \ class_hierarchy.cpp \ class_identifier.cpp \ compute_called_functions.cpp \ - destructor.cpp \ elf_reader.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 \ - goto_convert_function_call.cpp \ - goto_convert_functions.cpp \ - goto_convert_side_effect.cpp \ goto_function.cpp \ goto_functions.cpp \ goto_inline_class.cpp \ @@ -32,14 +21,12 @@ SRC = allocate_objects.cpp \ json_goto_trace.cpp \ label_function_pointer_call_sites.cpp \ link_goto_model.cpp \ - link_to_library.cpp \ loop_ids.cpp \ mm_io.cpp \ name_mangler.cpp \ osx_fat_reader.cpp \ parameter_assignments.cpp \ pointer_arithmetic.cpp \ - printf_formatter.cpp \ process_goto_program.cpp \ read_bin_goto_object.cpp \ read_goto_binary.cpp \ @@ -59,7 +46,6 @@ SRC = allocate_objects.cpp \ rewrite_union.cpp \ resolve_inherited_component.cpp \ safety_checker.cpp \ - scope_tree.cpp \ set_properties.cpp \ show_goto_functions.cpp \ show_goto_functions_json.cpp \ @@ -68,7 +54,6 @@ SRC = allocate_objects.cpp \ show_symbol_table.cpp \ slice_global_inits.cpp \ string_abstraction.cpp \ - string_instrumentation.cpp \ structured_trace_util.cpp \ system_library_symbols.cpp \ validate_code.cpp \ diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 1c1f1625028..0a7797af2d3 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -24,10 +24,9 @@ Author: Daniel Kroening #include #include +#include #include -#include "printf_formatter.h" - #include static std::optional get_object_rec(const exprt &src) diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 11c0870f1f7..e61eb0f2907 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -19,11 +19,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include -#include "goto_convert_functions.h" #include "read_goto_binary.h" #include diff --git a/src/goto-programs/printf_formatter.cpp b/src/goto-programs/printf_formatter.cpp index afc598fbfa6..e69de29bb2d 100644 --- a/src/goto-programs/printf_formatter.cpp +++ b/src/goto-programs/printf_formatter.cpp @@ -1,322 +0,0 @@ -/*******************************************************************\ - -Module: printf Formatting - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// printf Formatting - -#include "printf_formatter.h" - -#include -#include -#include -#include -#include -#include - -#include - -const exprt printf_formattert::make_type( - const exprt &src, const typet &dest) -{ - if(src.type()==dest) - return src; - return simplify_expr(typecast_exprt(src, dest), ns); -} - -void printf_formattert::operator()( - const std::string &_format, - const std::list &_operands) -{ - format=_format; - operands=_operands; -} - -void printf_formattert::print(std::ostream &out) -{ - format_pos=0; - next_operand=operands.begin(); - - try - { - while(!eol()) process_char(out); - } - - catch(const eol_exceptiont &) - { - } -} - -std::string printf_formattert::as_string() -{ - std::ostringstream stream; - print(stream); - return stream.str(); -} - -void printf_formattert::process_format(std::ostream &out) -{ - exprt tmp; - format_constantt format_constant; - - format_constant.precision=6; - format_constant.min_width=0; - format_constant.zero_padding=false; - - std::string length_modifier; - - char ch=next(); - - if(ch=='0') // leading zeros - { - format_constant.zero_padding=true; - ch=next(); - } - - while(isdigit(ch)) // width - { - format_constant.min_width*=10; - format_constant.min_width+=ch-'0'; - ch=next(); - } - - if(ch=='.') // precision - { - format_constant.precision=0; - ch=next(); - - while(isdigit(ch)) - { - format_constant.precision*=10; - format_constant.precision+=ch-'0'; - ch=next(); - } - } - - switch(ch) - { - case 'h': - ch = next(); - if(ch == 'h') - { - length_modifier = "hh"; - ch = next(); - } - else - { - length_modifier = "h"; - } - break; - - case 'l': - ch = next(); - if(ch == 'l') - { - length_modifier = "ll"; - ch = next(); - } - else - { - length_modifier = "l"; - } - break; - - case 'q': - ch = next(); - length_modifier = "ll"; - break; - - case 'L': - case 'j': - case 'z': - case 't': - length_modifier = ch; - ch = next(); - break; - - case 'Z': - ch = next(); - length_modifier = "z"; - break; - - default: - break; - } - - switch(ch) - { - case '%': - out << ch; - break; - - case 'e': - case 'E': - format_constant.style=format_spect::stylet::SCIENTIFIC; - if(next_operand==operands.end()) - break; - if(length_modifier == "L") - out << format_constant(make_type(*(next_operand++), long_double_type())); - else - out << format_constant(make_type(*(next_operand++), double_type())); - break; - - case 'a': // TODO: hexadecimal output - case 'A': // TODO: hexadecimal output - case 'f': - case 'F': - format_constant.style=format_spect::stylet::DECIMAL; - if(next_operand==operands.end()) - break; - if(length_modifier == "L") - out << format_constant(make_type(*(next_operand++), long_double_type())); - else - out << format_constant(make_type(*(next_operand++), double_type())); - break; - - case 'g': - case 'G': - format_constant.style=format_spect::stylet::AUTOMATIC; - if(format_constant.precision==0) - format_constant.precision=1; - if(next_operand==operands.end()) - break; - if(length_modifier == "L") - out << format_constant(make_type(*(next_operand++), long_double_type())); - else - out << format_constant(make_type(*(next_operand++), double_type())); - break; - - case 'S': - length_modifier = 'l'; - case 's': - { - if(next_operand==operands.end()) - break; - // this is the address of a string - const exprt &op=*(next_operand++); - if( - auto pointer_constant = - expr_try_dynamic_cast(op)) - { - if( - auto address_of = expr_try_dynamic_cast( - skip_typecast(pointer_constant->symbolic_pointer()))) - { - if(address_of->object().id() == ID_string_constant) - { - out << format_constant(address_of->object()); - } - else if( - auto index_expr = - expr_try_dynamic_cast(address_of->object())) - { - if( - index_expr->index().is_zero() && - index_expr->array().id() == ID_string_constant) - { - out << format_constant(index_expr->array()); - } - } - } - } - } - break; - - case 'd': - case 'i': - { - if(next_operand==operands.end()) - break; - typet conversion_type; - if(length_modifier == "hh") - conversion_type = signed_char_type(); - else if(length_modifier == "h") - conversion_type = signed_short_int_type(); - else if(length_modifier == "l") - conversion_type = signed_long_int_type(); - else if(length_modifier == "ll") - conversion_type = signed_long_long_int_type(); - else if(length_modifier == "j") // intmax_t - conversion_type = signed_long_long_int_type(); - else if(length_modifier == "z") - conversion_type = signed_size_type(); - else if(length_modifier == "t") - conversion_type = pointer_diff_type(); - else - conversion_type = signed_int_type(); - out << format_constant(make_type(*(next_operand++), conversion_type)); - } - break; - - case 'o': // TODO: octal output - case 'x': // TODO: hexadecimal output - case 'X': // TODO: hexadecimal output - case 'u': - { - if(next_operand == operands.end()) - break; - typet conversion_type; - if(length_modifier == "hh") - conversion_type = unsigned_char_type(); - else if(length_modifier == "h") - conversion_type = unsigned_short_int_type(); - else if(length_modifier == "l") - conversion_type = unsigned_long_int_type(); - else if(length_modifier == "ll") - conversion_type = unsigned_long_long_int_type(); - else if(length_modifier == "j") // intmax_t - conversion_type = unsigned_long_long_int_type(); - else if(length_modifier == "z") - conversion_type = size_type(); - else if(length_modifier == "t") - conversion_type = pointer_diff_type(); - else - conversion_type = unsigned_int_type(); - out << format_constant(make_type(*(next_operand++), conversion_type)); - } - break; - - case 'C': - length_modifier = 'l'; - case 'c': - if(next_operand == operands.end()) - break; - if(length_modifier == "l") - out << format_constant(make_type(*(next_operand++), wchar_t_type())); - else - out << format_constant( - make_type(*(next_operand++), unsigned_char_type())); - break; - - case 'p': - // TODO: hexadecimal output - out << format_constant(make_type(*(next_operand++), size_type())); - break; - - case 'n': - if(next_operand == operands.end()) - break; - // printf would store the number of characters written so far in the - // object pointed to by this operand. We do not implement this side-effect - // here, and just skip one operand. - ++next_operand; - break; - - default: - out << '%' << ch; - } -} - -void printf_formattert::process_char(std::ostream &out) -{ - char ch=next(); - - if(ch=='%') - process_format(out); - else - out << ch; -} diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 6b72d3f0002..4b7e712ee68 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -26,9 +26,9 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include #include -#include -#include +#include +#include #include "goto_check.h" diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 498f59d91f1..446cf102059 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -19,10 +19,10 @@ Author: Daniel Kroening #include #include +#include #include #include "goto_trace.h" -#include "printf_formatter.h" #include "structured_trace_util.h" #include "xml_expr.h" diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index b017840a378..f959361f41e 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -17,8 +17,6 @@ Author: Qinheping Hu #include #include -#include -#include #include #include #include @@ -26,6 +24,8 @@ Author: Qinheping Hu #include #include +#include +#include #include #include #include diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp index f2285331d22..7339e87729d 100644 --- a/src/libcprover-cpp/api.cpp +++ b/src/libcprover-cpp/api.cpp @@ -12,7 +12,6 @@ #include #include -#include #include #include #include @@ -22,6 +21,7 @@ #include #include #include +#include #include #include #include diff --git a/src/libcprover-cpp/api_options.cpp b/src/libcprover-cpp/api_options.cpp index c4d1839ddec..17c0eacbbea 100644 --- a/src/libcprover-cpp/api_options.cpp +++ b/src/libcprover-cpp/api_options.cpp @@ -5,7 +5,7 @@ #include #include -#include +#include #include api_optionst api_optionst::create() diff --git a/src/linking/module_dependencies.txt b/src/linking/module_dependencies.txt index c686b60d2d7..713bdb74bf3 100644 --- a/src/linking/module_dependencies.txt +++ b/src/linking/module_dependencies.txt @@ -1,3 +1,4 @@ +ansi-c goto-programs langapi # should go away linking diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index c7a44367f2a..336c848d7dd 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -16,9 +16,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include +#include + #include static std::optional static_lifetime_init( diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h index e37f6fe6765..308fa9590ae 100644 --- a/src/memory-analyzer/analyze_symbol.h +++ b/src/memory-analyzer/analyze_symbol.h @@ -13,17 +13,17 @@ Author: Malte Mues #ifndef CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H #define CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H -#include -#include - -#include "gdb_api.h" - #include #include #include -#include +#include + +#include "gdb_api.h" + +#include +#include class pointer_typet; class source_locationt; diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp index c299b9acb13..dd9a2d79dba 100644 --- a/src/symtab2gb/symtab2gb_parse_options.cpp +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -14,11 +14,11 @@ Author: Diffblue Ltd. #include #include -#include #include #include #include +#include #include #include #include diff --git a/unit/Makefile b/unit/Makefile index b29f8c56ee1..3885db56603 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -48,6 +48,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ + ansi-c/allocate_objects.cpp \ ansi-c/expr2c.cpp \ ansi-c/max_malloc_size.cpp \ ansi-c/type2name.cpp \ @@ -61,7 +62,6 @@ SRC += analyses/ai/ai.cpp \ goto-instrument/cover_instrument.cpp \ goto-instrument/cover/cover_only.cpp \ goto-synthesizer/expr_enumerator/expr_enumerator.cpp \ - goto-programs/allocate_objects.cpp \ goto-programs/goto_program_assume.cpp \ goto-programs/goto_program_dead.cpp \ goto-programs/goto_program_declaration.cpp \ diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp index 5b9ea1dcd46..94160148a76 100644 --- a/unit/analyses/ai/ai.cpp +++ b/unit/analyses/ai/ai.cpp @@ -9,20 +9,16 @@ Author: Diffblue Ltd. /// \file /// Unit tests for ait -#include -#include +#include +#include +#include #include - #include - -#include - +#include #include - -#include -#include -#include +#include +#include /// A very simple analysis that counts executed instructions along a particular /// path, taking the max at merge points and saturating at 100 instructions. diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index e2fc44b41c0..d72b32ae765 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -6,18 +6,17 @@ Module: Unit test for call graph generation \*******************************************************************/ -#include +#include -#include -#include +#include #include #include +#include +#include +#include -#include - -#include -#include +#include SCENARIO("call_graph", "[core][util][call_graph]") diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index 36bd4ace8c0..b6961b99a0f 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -6,18 +6,16 @@ Author: Diffblue Ltd \*******************************************************************/ -#include -#include - -#include - -#include - #include #include #include #include +#include +#include +#include +#include + static bool starts_with_x(const exprt &e, const namespacet &) { if(e.id() != ID_symbol) diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp index ddcd12af2e7..b98eafda0b6 100644 --- a/unit/analyses/dependence_graph.cpp +++ b/unit/analyses/dependence_graph.cpp @@ -6,10 +6,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com \*******************************************************************/ -#include -#include -#include - #include #include #include @@ -17,8 +13,11 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include -#include +#include #include +#include +#include +#include const std::set & dependence_graph_test_get_control_deps(const dep_graph_domaint &domain) diff --git a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp index d29ba936a3e..b33b9b13258 100644 --- a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp +++ b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp @@ -6,17 +6,16 @@ Module: Unit test for graph class functions \*******************************************************************/ -#include +#include -#include -#include +#include #include +#include +#include +#include -#include - -#include -#include +#include SCENARIO("graph", "[core][util][graph]") { diff --git a/unit/goto-programs/allocate_objects.cpp b/unit/ansi-c/allocate_objects.cpp similarity index 95% rename from unit/goto-programs/allocate_objects.cpp rename to unit/ansi-c/allocate_objects.cpp index 314ebf32137..8f4a97f6d09 100644 --- a/unit/goto-programs/allocate_objects.cpp +++ b/unit/ansi-c/allocate_objects.cpp @@ -6,7 +6,7 @@ Author: Diffblue Ltd \*******************************************************************/ -#include +#include #include #include diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 64f77436953..68e6c0339e9 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -17,10 +17,10 @@ #include #include -#include #include #include +#include #include #include diff --git a/unit/goto-programs/module_dependencies.txt b/unit/goto-programs/module_dependencies.txt index d0aaf35d60d..a5a50846f22 100644 --- a/unit/goto-programs/module_dependencies.txt +++ b/unit/goto-programs/module_dependencies.txt @@ -1,3 +1,4 @@ +ansi-c goto-programs json testing-utils diff --git a/unit/testing-utils/get_goto_model_from_c.cpp b/unit/testing-utils/get_goto_model_from_c.cpp index e1f3c879cce..f44daaadd4a 100644 --- a/unit/testing-utils/get_goto_model_from_c.cpp +++ b/unit/testing-utils/get_goto_model_from_c.cpp @@ -8,13 +8,6 @@ Author: Daniel Poetzl #include "get_goto_model_from_c.h" -#include - -#include - -#include -#include - #include #include #include @@ -22,6 +15,10 @@ Author: Daniel Poetzl #include #include +#include +#include +#include +#include #include goto_modelt get_goto_model_from_c(std::istream &in) From 174b89c96fec1172cf8addc03583be27f839e8aa Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 1 Apr 2024 14:02:32 -0700 Subject: [PATCH 2/2] clang-format the moved files --- .../java_bytecode/assignments_from_json.cpp | 4 +- .../goto-conversion/builtin_functions.cpp | 388 +++++++++--------- src/ansi-c/goto-conversion/destructor.cpp | 19 +- src/ansi-c/goto-conversion/destructor.h | 5 +- src/ansi-c/goto-conversion/format_strings.cpp | 228 +++++----- src/ansi-c/goto-conversion/format_strings.h | 21 +- src/ansi-c/goto-conversion/goto_asm.cpp | 4 +- src/ansi-c/goto-conversion/goto_check_c.cpp | 12 +- .../goto-conversion/goto_clean_expr.cpp | 108 ++--- src/ansi-c/goto-conversion/goto_convert.cpp | 344 ++++++++-------- .../goto-conversion/goto_convert_class.h | 154 ++++--- .../goto_convert_exceptions.cpp | 18 +- .../goto_convert_function_call.cpp | 18 +- .../goto_convert_functions.cpp | 4 +- .../goto-conversion/goto_convert_functions.h | 6 +- .../goto_convert_side_effect.cpp | 197 ++++----- .../goto-conversion/link_to_library.cpp | 4 +- src/ansi-c/goto-conversion/link_to_library.h | 4 +- .../string_instrumentation.cpp | 280 +++++++------ .../goto-conversion/string_instrumentation.h | 2 +- src/ansi-c/printf_formatter.h | 17 +- unit/ansi-c/allocate_objects.cpp | 3 +- 22 files changed, 893 insertions(+), 947 deletions(-) diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 27c24522499..ecc1d3450d6 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -16,11 +16,11 @@ Author: Diffblue Ltd. #include #include -#include - #include #include +#include + #include "ci_lazy_methods_needed.h" #include "code_with_references.h" #include "java_static_initializers.h" diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index 9277593a30e..67c263793c2 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -38,16 +38,16 @@ void goto_convertt::do_prob_uniform( const irep_idt &identifier = function.get_identifier(); // make it a side effect if there is an LHS - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } if(lhs.is_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have LHS" << eom; throw 0; } @@ -55,27 +55,26 @@ void goto_convertt::do_prob_uniform( auto rhs = side_effect_exprt("prob_uniform", lhs.type(), function.source_location()); - if(lhs.type().id()!=ID_unsignedbv && - lhs.type().id()!=ID_signedbv) + if(lhs.type().id() != ID_unsignedbv && lhs.type().id() != ID_signedbv) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected other type" << eom; throw 0; } - if(arguments[0].type().id()!=lhs.type().id() || - arguments[1].type().id()!=lhs.type().id()) + if( + arguments[0].type().id() != lhs.type().id() || + arguments[1].type().id() != lhs.type().id()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected operands to be of same type as LHS" << eom; throw 0; } - if(!arguments[0].is_constant() || - !arguments[1].is_constant()) + if(!arguments[0].is_constant() || !arguments[1].is_constant()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected operands to be constant literals" << eom; throw 0; @@ -87,14 +86,14 @@ void goto_convertt::do_prob_uniform( to_integer(to_constant_expr(arguments[0]), lb) || to_integer(to_constant_expr(arguments[1]), ub)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error converting operands" << eom; throw 0; } if(lb > ub) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "expected lower bound to be smaller or equal to the " << "upper bound" << eom; throw 0; @@ -103,7 +102,7 @@ void goto_convertt::do_prob_uniform( rhs.add_to_operands(exprt{arguments[0]}, exprt{arguments[1]}); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } @@ -116,32 +115,32 @@ void goto_convertt::do_prob_coin( const irep_idt &identifier = function.get_identifier(); // make it a side effect if there is an LHS - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } if(lhs.is_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have LHS" << eom; throw 0; } side_effect_exprt rhs("prob_coin", lhs.type(), function.source_location()); - if(lhs.type()!=bool_typet()) + if(lhs.type() != bool_typet()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected bool" << eom; throw 0; } if(arguments[0].type().id() != ID_unsignedbv || !arguments[0].is_constant()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected first operand to be " << "a constant literal of type unsigned long" << eom; throw 0; @@ -161,21 +160,21 @@ void goto_convertt::do_prob_coin( to_integer(to_constant_expr(arguments[0]), num) || to_integer(to_constant_expr(arguments[1]), den)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error converting operands" << eom; throw 0; } - if(num-den > mp_integer(0)) + if(num - den > mp_integer(0)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "probability has to be smaller than 1" << eom; throw 0; } if(den == mp_integer(0)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "denominator may not be zero" << eom; throw 0; } @@ -186,7 +185,7 @@ void goto_convertt::do_prob_coin( rhs.copy_to_operands(from_rational(prob)); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } @@ -212,11 +211,11 @@ void goto_convertt::do_scanf( { const irep_idt &f_id = function.get_identifier(); - if(f_id==CPROVER_PREFIX "scanf") + if(f_id == CPROVER_PREFIX "scanf") { if(arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "scanf takes at least one argument" << eom; throw 0; } @@ -226,10 +225,10 @@ void goto_convertt::do_scanf( if(!get_string_constant(arguments[0], format_string)) { // use our model - format_token_listt token_list= + format_token_listt token_list = parse_format_string(id2string(format_string)); - std::size_t argument_number=1; + std::size_t argument_number = 1; for(const auto &t : token_list) { @@ -237,7 +236,7 @@ void goto_convertt::do_scanf( if(type.has_value()) { - if(argument_numberid() == ID_array) { - #if 0 +#if 0 // A string. We first need a nondeterministic size. exprt size=side_effect_expr_nondett(size_type()); to_array_type(*type).size()=size; @@ -269,16 +268,16 @@ void goto_convertt::do_scanf( function.source_location(); copy(array_copy_statement, OTHER, dest); - #else +#else const index_exprt new_lhs( dereference_exprt{ptr}, from_integer(0, c_index_type())); const side_effect_expr_nondett rhs( to_array_type(*type).element_type(), function.source_location()); code_assignt assign(new_lhs, rhs); - assign.add_source_location()=function.source_location(); + assign.add_source_location() = function.source_location(); copy(assign, ASSIGN, dest); - #endif +#endif } else { @@ -287,7 +286,7 @@ void goto_convertt::do_scanf( const side_effect_expr_nondett rhs( *type, function.source_location()); code_assignt assign(new_lhs, rhs); - assign.add_source_location()=function.source_location(); + assign.add_source_location() = function.source_location(); copy(assign, ASSIGN, dest); } } @@ -298,7 +297,7 @@ void goto_convertt::do_scanf( { // we'll just do nothing code_function_callt function_call(lhs, function, arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); copy(function_call, FUNCTION_CALL, dest); } @@ -312,9 +311,9 @@ void goto_convertt::do_input( const exprt::operandst &arguments, goto_programt &dest) { - if(arguments.size()<2) + if(arguments.size() < 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "input takes at least two arguments" << eom; throw 0; } @@ -327,9 +326,9 @@ void goto_convertt::do_output( const exprt::operandst &arguments, goto_programt &dest) { - if(arguments.size()<2) + if(arguments.size() < 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "output takes at least two arguments" << eom; throw 0; } @@ -345,14 +344,14 @@ void goto_convertt::do_atomic_begin( { if(lhs.is_not_nil()) { - error().source_location=lhs.find_source_location(); + error().source_location = lhs.find_source_location(); error() << "atomic_begin does not expect an LHS" << eom; throw 0; } if(!arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "atomic_begin takes no arguments" << eom; throw 0; } @@ -368,14 +367,14 @@ void goto_convertt::do_atomic_end( { if(lhs.is_not_nil()) { - error().source_location=lhs.find_source_location(); + error().source_location = lhs.find_source_location(); error() << "atomic_end does not expect an LHS" << eom; throw 0; } if(!arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "atomic_end takes no arguments" << eom; throw 0; } @@ -390,16 +389,15 @@ void goto_convertt::do_cpp_new( { if(lhs.is_nil()) { - error().source_location=lhs.find_source_location(); + error().source_location = lhs.find_source_location(); error() << "do_cpp_new without lhs is yet to be implemented" << eom; throw 0; } // build size expression - exprt object_size= - static_cast(rhs.find(ID_sizeof)); + exprt object_size = static_cast(rhs.find(ID_sizeof)); - bool new_array=rhs.get(ID_statement)==ID_cpp_new_array; + bool new_array = rhs.get(ID_statement) == ID_cpp_new_array; exprt count; @@ -418,14 +416,12 @@ void goto_convertt::do_cpp_new( if(rhs.operands().empty()) // no, "regular" one { // call __new or __new_array - exprt new_symbol= - ns.lookup(new_array?"__new_array":"__new").symbol_expr(); + exprt new_symbol = + ns.lookup(new_array ? "__new_array" : "__new").symbol_expr(); - const code_typet &code_type= - to_code_type(new_symbol.type()); + const code_typet &code_type = to_code_type(new_symbol.type()); - const typet &return_type= - code_type.return_type(); + const typet &return_type = code_type.return_type(); DATA_INVARIANT( code_type.parameters().size() == 1 || code_type.parameters().size() == 2, @@ -434,7 +430,7 @@ void goto_convertt::do_cpp_new( const symbolt &tmp_symbol = new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); - tmp_symbol_expr=tmp_symbol.symbol_expr(); + tmp_symbol_expr = tmp_symbol.symbol_expr(); code_function_callt new_call(new_symbol); if(new_array) @@ -442,22 +438,21 @@ void goto_convertt::do_cpp_new( new_call.arguments().push_back(object_size); new_call.set( ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype()); - new_call.lhs()=tmp_symbol_expr; - new_call.add_source_location()=rhs.source_location(); + new_call.lhs() = tmp_symbol_expr; + new_call.add_source_location() = rhs.source_location(); convert(new_call, dest, ID_cpp); } - else if(rhs.operands().size()==1) + else if(rhs.operands().size() == 1) { // call __placement_new - exprt new_symbol= - ns.lookup( - new_array?"__placement_new_array":"__placement_new").symbol_expr(); + exprt new_symbol = + ns.lookup(new_array ? "__placement_new_array" : "__placement_new") + .symbol_expr(); - const code_typet &code_type= - to_code_type(new_symbol.type()); + const code_typet &code_type = to_code_type(new_symbol.type()); - const typet &return_type=code_type.return_type(); + const typet &return_type = code_type.return_type(); DATA_INVARIANT( code_type.parameters().size() == 2 || code_type.parameters().size() == 3, @@ -466,7 +461,7 @@ void goto_convertt::do_cpp_new( const symbolt &tmp_symbol = new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); - tmp_symbol_expr=tmp_symbol.symbol_expr(); + tmp_symbol_expr = tmp_symbol.symbol_expr(); code_function_callt new_call(new_symbol); if(new_array) @@ -475,10 +470,10 @@ void goto_convertt::do_cpp_new( new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location new_call.set( ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype()); - new_call.lhs()=tmp_symbol_expr; - new_call.add_source_location()=rhs.source_location(); + new_call.lhs() = tmp_symbol_expr; + new_call.add_source_location() = rhs.source_location(); - for(std::size_t i=0; i(rhs.find(ID_initializer)); + exprt initializer = static_cast(rhs.find(ID_initializer)); if(initializer.is_not_nil()) { - if(rhs.get_statement()=="cpp_new[]") + if(rhs.get_statement() == "cpp_new[]") { // build loop } - else if(rhs.get_statement()==ID_cpp_new) + else if(rhs.get_statement() == ID_cpp_new) { // just one object const dereference_exprt deref_lhs( @@ -536,12 +530,12 @@ void goto_convertt::cpp_new_initializer( exprt goto_convertt::get_array_argument(const exprt &src) { - if(src.id()==ID_typecast) + if(src.id() == ID_typecast) return get_array_argument(to_typecast_expr(src).op()); - if(src.id()!=ID_address_of) + if(src.id() != ID_address_of) { - error().source_location=src.find_source_location(); + error().source_location = src.find_source_location(); error() << "expected array-pointer as argument" << eom; throw 0; } @@ -550,7 +544,7 @@ exprt goto_convertt::get_array_argument(const exprt &src) if(address_of_expr.object().id() != ID_index) { - error().source_location=src.find_source_location(); + error().source_location = src.find_source_location(); error() << "expected array-element as argument" << eom; throw 0; } @@ -559,7 +553,7 @@ exprt goto_convertt::get_array_argument(const exprt &src) if(index_expr.array().type().id() != ID_array) { - error().source_location=src.find_source_location(); + error().source_location = src.find_source_location(); error() << "expected array as argument" << eom; throw 0; } @@ -574,16 +568,16 @@ void goto_convertt::do_array_op( const exprt::operandst &arguments, goto_programt &dest) { - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << id << " expects two arguments" << eom; throw 0; } codet array_op_statement(id); - array_op_statement.operands()=arguments; - array_op_statement.add_source_location()=function.source_location(); + array_op_statement.operands() = arguments; + array_op_statement.add_source_location() = function.source_location(); // lhs is only used with array_equal, in all other cases it should be nil (as // they are of type void) @@ -812,19 +806,19 @@ void goto_convertt::do_function_call_symbol( return; // ignore // lookup symbol - const irep_idt &identifier=function.get_identifier(); + const irep_idt &identifier = function.get_identifier(); const symbolt *symbol; if(ns.lookup(identifier, symbol)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error: function '" << identifier << "' not found" << eom; throw 0; } - if(symbol->type.id()!=ID_code) + if(symbol->type.id() != ID_code) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error: function '" << identifier << "' type mismatch: expected code" << eom; throw 0; @@ -865,9 +859,9 @@ void goto_convertt::do_function_call_symbol( else if( identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume") { - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -881,16 +875,16 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } } - else if(identifier=="__VERIFIER_error") + else if(identifier == "__VERIFIER_error") { if(!arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have no arguments" << eom; throw 0; } @@ -902,7 +896,7 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } @@ -918,9 +912,9 @@ void goto_convertt::do_function_call_symbol( identifier == "assert" && to_code_type(symbol->type).return_type() == signed_int_type()) { - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -937,7 +931,7 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } @@ -947,19 +941,17 @@ void goto_convertt::do_function_call_symbol( identifier == CPROVER_PREFIX "precondition" || identifier == CPROVER_PREFIX "postcondition") { - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } - bool is_precondition= - identifier==CPROVER_PREFIX "precondition"; + bool is_precondition = identifier == CPROVER_PREFIX "precondition"; bool is_postcondition = identifier == CPROVER_PREFIX "postcondition"; - const irep_idt description= - get_string_constant(arguments[1]); + const irep_idt description = get_string_constant(arguments[1]); // let's double-check the type of the argument source_locationt annotated_location = function.source_location(); @@ -986,23 +978,23 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } } - else if(identifier==CPROVER_PREFIX "havoc_object") + else if(identifier == CPROVER_PREFIX "havoc_object") { - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } @@ -1013,53 +1005,55 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_other(havoc, function.source_location())); } - else if(identifier==CPROVER_PREFIX "printf") + else if(identifier == CPROVER_PREFIX "printf") { do_printf(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "scanf") + else if(identifier == CPROVER_PREFIX "scanf") { do_scanf(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "input" || - identifier=="__CPROVER::input") + else if( + identifier == CPROVER_PREFIX "input" || identifier == "__CPROVER::input") { if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } do_input(function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "output" || - identifier=="__CPROVER::output") + else if( + identifier == CPROVER_PREFIX "output" || identifier == "__CPROVER::output") { if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } do_output(function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "atomic_begin" || - identifier=="__CPROVER::atomic_begin" || - identifier=="java::org.cprover.CProver.atomicBegin:()V" || - identifier=="__VERIFIER_atomic_begin") + else if( + identifier == CPROVER_PREFIX "atomic_begin" || + identifier == "__CPROVER::atomic_begin" || + identifier == "java::org.cprover.CProver.atomicBegin:()V" || + identifier == "__VERIFIER_atomic_begin") { do_atomic_begin(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "atomic_end" || - identifier=="__CPROVER::atomic_end" || - identifier=="java::org.cprover.CProver.atomicEnd:()V" || - identifier=="__VERIFIER_atomic_end") + else if( + identifier == CPROVER_PREFIX "atomic_end" || + identifier == "__CPROVER::atomic_end" || + identifier == "java::org.cprover.CProver.atomicEnd:()V" || + identifier == "__VERIFIER_atomic_end") { do_atomic_end(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "prob_biased_coin") + else if(identifier == CPROVER_PREFIX "prob_biased_coin") { do_prob_coin(lhs, function, arguments, dest); } @@ -1079,11 +1073,11 @@ void goto_convertt::do_function_call_symbol( // We need to special-case for _Bool, which // can only be 0 or 1. - if(lhs.type().id()==ID_c_bool) + if(lhs.type().id() == ID_c_bool) { rhs = side_effect_expr_nondett(bool_typet(), function.source_location()); rhs.set(ID_C_identifier, identifier); - rhs=typecast_exprt(rhs, lhs.type()); + rhs = typecast_exprt(rhs, lhs.type()); } else { @@ -1092,7 +1086,7 @@ void goto_convertt::do_function_call_symbol( } code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_")) @@ -1114,35 +1108,34 @@ void goto_convertt::do_function_call_symbol( mathematical_function_typet::domaint domain; for(const auto ¶meter : function_call_type.parameters()) domain.push_back(parameter.type()); - mathematical_function_typet function_type{domain, - function_call_type.return_type()}; + mathematical_function_typet function_type{ + domain, function_call_type.return_type()}; const function_application_exprt rhs( symbol_exprt{function.get_identifier(), function_type}, arguments); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } - else if(identifier==CPROVER_PREFIX "array_equal") + else if(identifier == CPROVER_PREFIX "array_equal") { do_array_op(ID_array_equal, lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "array_set") + else if(identifier == CPROVER_PREFIX "array_set") { do_array_op(ID_array_set, lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "array_copy") + else if(identifier == CPROVER_PREFIX "array_copy") { do_array_op(ID_array_copy, lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "array_replace") + else if(identifier == CPROVER_PREFIX "array_replace") { do_array_op(ID_array_replace, lhs, function, arguments, dest); } - else if(identifier=="__assert_fail" || - identifier=="_assert" || - identifier=="__assert_c99" || - identifier=="_wassert") + else if( + identifier == "__assert_fail" || identifier == "_assert" || + identifier == "__assert_c99" || identifier == "_wassert") { // __assert_fail is Linux // These take four arguments: @@ -1163,17 +1156,16 @@ void goto_convertt::do_function_call_symbol( // _wassert is Windows. The arguments are // L"expression", L"file.c", line - if(arguments.size()!=4 && - arguments.size()!=3) + if(arguments.size() != 4 && arguments.size() != 3) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; } - const irep_idt description= - "assertion "+id2string(get_string_constant(arguments[0])); + const irep_idt description = + "assertion " + id2string(get_string_constant(arguments[0])); source_locationt annotated_location = function.source_location(); annotated_location.set("user-provided", true); @@ -1182,8 +1174,7 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } - else if(identifier=="__assert_rtn" || - identifier=="__assert") + else if(identifier == "__assert_rtn" || identifier == "__assert") { // __assert_rtn has been seen on MacOS; // __assert is FreeBSD and Solaris 11. @@ -1194,19 +1185,17 @@ void goto_convertt::do_function_call_symbol( irep_idt description; - if(arguments.size()==4) + if(arguments.size() == 4) { - description= - "assertion "+id2string(get_string_constant(arguments[3])); + description = "assertion " + id2string(get_string_constant(arguments[3])); } - else if(arguments.size()==3) + else if(arguments.size() == 3) { - description= - "assertion "+id2string(get_string_constant(arguments[1])); + description = "assertion " + id2string(get_string_constant(arguments[1])); } else { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; @@ -1228,9 +1217,9 @@ void goto_convertt::do_function_call_symbol( // __assert13 is NetBSD // These take four arguments: // "file.c", line, __func__, "expression" - if(arguments.size()!=4) + if(arguments.size() != 4) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; @@ -1239,14 +1228,14 @@ void goto_convertt::do_function_call_symbol( irep_idt description; try { - description="assertion "+id2string(get_string_constant(arguments[3])); + description = "assertion " + id2string(get_string_constant(arguments[3])); } catch(int) { // we might be building newlib, where __assert_func is passed // a pointer-typed symbol; the warning will still have been // printed - description="assertion"; + description = "assertion"; } source_locationt annotated_location = function.source_location(); @@ -1256,11 +1245,11 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } - else if(identifier==CPROVER_PREFIX "fence") + else if(identifier == CPROVER_PREFIX "fence") { if(arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have at least one argument" << eom; throw 0; @@ -1273,15 +1262,15 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_other(fence, function.source_location())); } - else if(identifier=="__builtin_prefetch") + else if(identifier == "__builtin_prefetch") { // does nothing } - else if(identifier=="__builtin_unreachable") + else if(identifier == "__builtin_unreachable") { // says something like UNREACHABLE; } - else if(identifier==ID_gcc_builtin_va_arg) + else if(identifier == ID_gcc_builtin_va_arg) { // This does two things. // 1) Return value of argument. @@ -1289,14 +1278,14 @@ void goto_convertt::do_function_call_symbol( // 2) Move list pointer to next argument. // This is just an increment. - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } - exprt list_arg=make_va_list(arguments[0]); + exprt list_arg = make_va_list(arguments[0]); if(lhs.is_not_nil()) { @@ -1309,10 +1298,10 @@ void goto_convertt::do_function_call_symbol( typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))}; } - typet t=pointer_type(lhs.type()); + typet t = pointer_type(lhs.type()); dereference_exprt rhs{ typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}}; - rhs.add_source_location()=function.source_location(); + rhs.add_source_location() = function.source_location(); dest.add( goto_programt::make_assignment(lhs, rhs, function.source_location())); } @@ -1324,21 +1313,21 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assignment( std::move(assign), function.source_location())); } - else if(identifier=="__builtin_va_copy") + else if(identifier == "__builtin_va_copy") { - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } - exprt dest_expr=make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0]); const typecast_exprt src_expr(arguments[1], dest_expr.type()); if(!is_assignable(dest_expr)) { - error().source_location=dest_expr.find_source_location(); + error().source_location = dest_expr.find_source_location(); error() << "va_copy argument expected to be lvalue" << eom; throw 0; } @@ -1350,18 +1339,18 @@ void goto_convertt::do_function_call_symbol( { // Set the list argument to be the address of the // parameter argument. - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } - exprt dest_expr=make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0]); if(!is_assignable(dest_expr)) { - error().source_location=dest_expr.find_source_location(); + error().source_location = dest_expr.find_source_location(); error() << "va_start argument expected to be lvalue" << eom; throw 0; } @@ -1382,21 +1371,21 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assignment( std::move(dest_expr), std::move(rhs), function.source_location())); } - else if(identifier=="__builtin_va_end") + else if(identifier == "__builtin_va_end") { // Invalidates the argument. We do so by setting it to NULL. - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } - exprt dest_expr=make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0]); if(!is_assignable(dest_expr)) { - error().source_location=dest_expr.find_source_location(); + error().source_location = dest_expr.find_source_location(); error() << "va_end argument expected to be lvalue" << eom; throw 0; } @@ -1420,22 +1409,23 @@ void goto_convertt::do_function_call_symbol( { // these support two double or two float arguments; we call the // appropriate internal version - if(arguments.size()!=2 || - (arguments[0].type()!=double_type() && - arguments[0].type()!=float_type()) || - (arguments[1].type()!=double_type() && - arguments[1].type()!=float_type())) + if( + arguments.size() != 2 || + (arguments[0].type() != double_type() && + arguments[0].type() != float_type()) || + (arguments[1].type() != double_type() && + arguments[1].type() != float_type())) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two float/double arguments" << eom; throw 0; } - exprt::operandst new_arguments=arguments; + exprt::operandst new_arguments = arguments; - bool use_double=arguments[0].type()==double_type(); - if(arguments[0].type()!=arguments[1].type()) + bool use_double = arguments[0].type() == double_type(); + if(arguments[0].type() != arguments[1].type()) { if(use_double) { @@ -1446,31 +1436,31 @@ void goto_convertt::do_function_call_symbol( { new_arguments[0] = typecast_exprt(new_arguments[0], arguments[1].type()); - use_double=true; + use_double = true; } } - code_typet f_type=to_code_type(function.type()); + code_typet f_type = to_code_type(function.type()); f_type.remove_ellipsis(); - const typet &a_t=new_arguments[0].type(); - f_type.parameters()= + const typet &a_t = new_arguments[0].type(); + f_type.parameters() = code_typet::parameterst(2, code_typet::parametert(a_t)); // replace __builtin_ by CPROVER_PREFIX - std::string name=CPROVER_PREFIX+id2string(identifier).substr(10); + std::string name = CPROVER_PREFIX + id2string(identifier).substr(10); // append d or f for double/float - name+=use_double?'d':'f'; + name += use_double ? 'd' : 'f'; DATA_INVARIANT( ns.lookup(name).type == f_type, "builtin declaration should match constructed type"); - symbol_exprt new_function=function; + symbol_exprt new_function = function; new_function.set_identifier(name); - new_function.type()=f_type; + new_function.type() = f_type; code_function_callt function_call(lhs, new_function, new_arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); copy(function_call, FUNCTION_CALL, dest); } @@ -1486,7 +1476,7 @@ void goto_convertt::do_function_call_symbol( // use symbol->symbol_expr() to ensure we use the type from the symbol table code_function_callt function_call( lhs, symbol->symbol_expr().with_source_location(function), arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); // remove void-typed assignments, which may have been created when the // front-end was unable to detect them in type checking for a lack of diff --git a/src/ansi-c/goto-conversion/destructor.cpp b/src/ansi-c/goto-conversion/destructor.cpp index 2ecc88dfa7a..3ac1d4298b7 100644 --- a/src/ansi-c/goto-conversion/destructor.cpp +++ b/src/ansi-c/goto-conversion/destructor.cpp @@ -11,22 +11,20 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" -#include - #include #include -code_function_callt get_destructor( - const namespacet &ns, - const typet &type) +#include + +code_function_callt get_destructor(const namespacet &ns, const typet &type) { if(type.id() == ID_struct_tag) { return get_destructor(ns, ns.follow_tag(to_struct_tag_type(type))); } - else if(type.id()==ID_struct) + else if(type.id() == ID_struct) { - const exprt &methods=static_cast(type.find(ID_methods)); + const exprt &methods = static_cast(type.find(ID_methods)); for(const auto &op : methods.operands()) { @@ -34,10 +32,11 @@ code_function_callt get_destructor( { const code_typet &code_type = to_code_type(op.type()); - if(code_type.return_type().id()==ID_destructor && - code_type.parameters().size()==1) + if( + code_type.return_type().id() == ID_destructor && + code_type.parameters().size() == 1) { - const typet &arg_type=code_type.parameters().front().type(); + const typet &arg_type = code_type.parameters().front().type(); if( arg_type.id() == ID_pointer && diff --git a/src/ansi-c/goto-conversion/destructor.h b/src/ansi-c/goto-conversion/destructor.h index 8c887a2426b..7cfbb594a61 100644 --- a/src/ansi-c/goto-conversion/destructor.h +++ b/src/ansi-c/goto-conversion/destructor.h @@ -15,8 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; class typet; -class code_function_callt get_destructor( - const namespacet &ns, - const typet &type); +class code_function_callt +get_destructor(const namespacet &ns, const typet &type); #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H diff --git a/src/ansi-c/goto-conversion/format_strings.cpp b/src/ansi-c/goto-conversion/format_strings.cpp index ecbf78e5fe5..8ed4d1671a1 100644 --- a/src/ansi-c/goto-conversion/format_strings.cpp +++ b/src/ansi-c/goto-conversion/format_strings.cpp @@ -18,57 +18,56 @@ Author: CM Wintersteiger #include -void parse_flags( - std::string::const_iterator &it, - format_tokent &curtok) +void parse_flags(std::string::const_iterator &it, format_tokent &curtok) { - while(*it=='#' || *it=='0' || - *it=='-' || *it==' ' || *it=='+') + while(*it == '#' || *it == '0' || *it == '-' || *it == ' ' || *it == '+') { switch(*it) { - case '#': - curtok.flags.push_back(format_tokent::flag_typet::ALTERNATE); break; - case '0': - curtok.flags.push_back(format_tokent::flag_typet::ZERO_PAD); break; - case '-': - curtok.flags.push_back(format_tokent::flag_typet::LEFT_ADJUST); break; - case ' ': - curtok.flags.push_back(format_tokent::flag_typet::SIGNED_SPACE); break; - case '+': - curtok.flags.push_back(format_tokent::flag_typet::SIGN); break; - default: - throw unsupported_operation_exceptiont( - std::string("unsupported format specifier flag: '") + *it + "'"); + case '#': + curtok.flags.push_back(format_tokent::flag_typet::ALTERNATE); + break; + case '0': + curtok.flags.push_back(format_tokent::flag_typet::ZERO_PAD); + break; + case '-': + curtok.flags.push_back(format_tokent::flag_typet::LEFT_ADJUST); + break; + case ' ': + curtok.flags.push_back(format_tokent::flag_typet::SIGNED_SPACE); + break; + case '+': + curtok.flags.push_back(format_tokent::flag_typet::SIGN); + break; + default: + throw unsupported_operation_exceptiont( + std::string("unsupported format specifier flag: '") + *it + "'"); } it++; } } -void parse_field_width( - std::string::const_iterator &it, - format_tokent &curtok) +void parse_field_width(std::string::const_iterator &it, format_tokent &curtok) { - if(*it=='*') + if(*it == '*') { curtok.flags.push_back(format_tokent::flag_typet::ASTERISK); it++; } std::string tmp; - for( ; isdigit(*it); it++) tmp+=*it; - curtok.field_width=string2integer(tmp); + for(; isdigit(*it); it++) + tmp += *it; + curtok.field_width = string2integer(tmp); } -void parse_precision( - std::string::const_iterator &it, - format_tokent &curtok) +void parse_precision(std::string::const_iterator &it, format_tokent &curtok) { - if(*it=='.') + if(*it == '.') { it++; - if(*it=='*') + if(*it == '*') { curtok.flags.push_back(format_tokent::flag_typet::ASTERISK); it++; @@ -76,8 +75,9 @@ void parse_precision( else { std::string tmp; - for( ; isdigit(*it); it++) tmp+=*it; - curtok.precision=string2integer(tmp); + for(; isdigit(*it); it++) + tmp += *it; + curtok.precision = string2integer(tmp); } } } @@ -86,31 +86,31 @@ void parse_length_modifier( std::string::const_iterator &it, format_tokent &curtok) { - if(*it=='h') + if(*it == 'h') { it++; - if(*it=='h') + if(*it == 'h') it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_h; } - else if(*it=='l') + else if(*it == 'l') { it++; - if(*it=='l') + if(*it == 'l') it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_l; } - else if(*it=='L') + else if(*it == 'L') { it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_L; } - else if(*it=='j') + else if(*it == 'j') { it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_j; } - else if(*it=='t') + else if(*it == 't') { it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_L; @@ -124,61 +124,77 @@ void parse_conversion_specifier( { switch(*it) { - case 'd': - case 'i': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::SIGNED_DEC; - break; - case 'o': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::UNSIGNED_OCT; - break; - case 'u': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::UNSIGNED_DEC; - break; - case 'x': - case 'X': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::UNSIGNED_HEX; - break; - case 'e': - case 'E': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'f': - case 'F': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'g': - case 'G': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'a': - case 'A': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'c': curtok.type=format_tokent::token_typet::CHAR; break; - case 's': curtok.type=format_tokent::token_typet::STRING; break; - case 'p': curtok.type=format_tokent::token_typet::POINTER; break; - case '%': - curtok.type=format_tokent::token_typet::TEXT; - curtok.value="%"; - break; - case '[': // pattern matching in, e.g., fscanf. + case 'd': + case 'i': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::SIGNED_DEC; + break; + case 'o': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::UNSIGNED_OCT; + break; + case 'u': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::UNSIGNED_DEC; + break; + case 'x': + case 'X': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::UNSIGNED_HEX; + break; + case 'e': + case 'E': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'f': + case 'F': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'g': + case 'G': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'a': + case 'A': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'c': + curtok.type = format_tokent::token_typet::CHAR; + break; + case 's': + curtok.type = format_tokent::token_typet::STRING; + break; + case 'p': + curtok.type = format_tokent::token_typet::POINTER; + break; + case '%': + curtok.type = format_tokent::token_typet::TEXT; + curtok.value = "%"; + break; + case '[': // pattern matching in, e.g., fscanf. + { + std::string tmp; + it++; + if(*it == '^') // if it's there, it must be first { - std::string tmp; + tmp += '^'; it++; - if(*it=='^') // if it's there, it must be first + if(*it == ']') // if it's there, it must be here { - tmp+='^'; it++; - if(*it==']') // if it's there, it must be here - { - tmp+=']'; it++; - } + tmp += ']'; + it++; } + } - for( ; it!=arg_string.end() && *it!=']'; it++) - tmp+=*it; + for(; it != arg_string.end() && *it != ']'; it++) + tmp += *it; - break; - } + break; + } - default: - throw unsupported_operation_exceptiont( - std::string("unsupported format conversion specifier: '") + *it + "'"); + default: + throw unsupported_operation_exceptiont( + std::string("unsupported format conversion specifier: '") + *it + "'"); } it++; } @@ -187,14 +203,14 @@ format_token_listt parse_format_string(const std::string &arg_string) { format_token_listt token_list; - std::string::const_iterator it=arg_string.begin(); + std::string::const_iterator it = arg_string.begin(); - while(it!=arg_string.end()) + while(it != arg_string.end()) { - if(*it=='%') + if(*it == '%') { token_list.push_back(format_tokent()); - format_tokent &curtok=token_list.back(); + format_tokent &curtok = token_list.back(); it++; parse_flags(it, curtok); @@ -205,20 +221,21 @@ format_token_listt parse_format_string(const std::string &arg_string) } else { - if(token_list.empty() || - token_list.back().type!=format_tokent::token_typet::TEXT) + if( + token_list.empty() || + token_list.back().type != format_tokent::token_typet::TEXT) token_list.push_back(format_tokent(format_tokent::token_typet::TEXT)); std::string tmp; - for( ; it!=arg_string.end() && *it!='%'; it++) - tmp+=*it; + for(; it != arg_string.end() && *it != '%'; it++) + tmp += *it; INVARIANT( !token_list.empty() && - token_list.back().type == format_tokent::token_typet::TEXT, + token_list.back().type == format_tokent::token_typet::TEXT, "must already have a TEXT token at the back of the token list"); - token_list.back().value=tmp; + token_list.back().value = tmp; } } @@ -233,25 +250,25 @@ std::optional get_type(const format_tokent &token) switch(token.length_modifier) { case format_tokent::length_modifierst::LEN_h: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_char_type(); else return unsigned_char_type(); case format_tokent::length_modifierst::LEN_hh: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_short_int_type(); else return unsigned_short_int_type(); case format_tokent::length_modifierst::LEN_l: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_long_int_type(); else return unsigned_long_int_type(); case format_tokent::length_modifierst::LEN_ll: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_long_long_int_type(); else return unsigned_long_long_int_type(); @@ -260,7 +277,7 @@ std::optional get_type(const format_tokent &token) case format_tokent::length_modifierst::LEN_j: case format_tokent::length_modifierst::LEN_L: case format_tokent::length_modifierst::LEN_undef: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_int_type(); else return unsigned_int_type(); @@ -269,8 +286,10 @@ std::optional get_type(const format_tokent &token) case format_tokent::token_typet::FLOAT: switch(token.length_modifier) { - case format_tokent::length_modifierst::LEN_l: return double_type(); - case format_tokent::length_modifierst::LEN_L: return long_double_type(); + case format_tokent::length_modifierst::LEN_l: + return double_type(); + case format_tokent::length_modifierst::LEN_L: + return long_double_type(); case format_tokent::length_modifierst::LEN_h: case format_tokent::length_modifierst::LEN_hh: case format_tokent::length_modifierst::LEN_j: @@ -283,7 +302,8 @@ std::optional get_type(const format_tokent &token) case format_tokent::token_typet::CHAR: switch(token.length_modifier) { - case format_tokent::length_modifierst::LEN_l: return wchar_t_type(); + case format_tokent::length_modifierst::LEN_l: + return wchar_t_type(); case format_tokent::length_modifierst::LEN_h: case format_tokent::length_modifierst::LEN_hh: case format_tokent::length_modifierst::LEN_j: diff --git a/src/ansi-c/goto-conversion/format_strings.h b/src/ansi-c/goto-conversion/format_strings.h index 7e77c032cae..667bc17552d 100644 --- a/src/ansi-c/goto-conversion/format_strings.h +++ b/src/ansi-c/goto-conversion/format_strings.h @@ -28,9 +28,9 @@ class format_tokent { UNKNOWN, TEXT, - INT, // d, i, o, u, x - FLOAT, // a, e, f, g - CHAR, // c + INT, // d, i, o, u, x + FLOAT, // a, e, f, g + CHAR, // c STRING, // s POINTER // p }; @@ -70,13 +70,14 @@ class format_tokent : type(_type), length_modifier(length_modifierst::LEN_undef), representation(representationt::SIGNED_undef) - { } - format_tokent(): - type(token_typet::UNKNOWN), - length_modifier(length_modifierst::LEN_undef), - representation(representationt::SIGNED_undef) - { } - + { + } + format_tokent() + : type(token_typet::UNKNOWN), + length_modifier(length_modifierst::LEN_undef), + representation(representationt::SIGNED_undef) + { + } token_typet type; std::list flags; diff --git a/src/ansi-c/goto-conversion/goto_asm.cpp b/src/ansi-c/goto-conversion/goto_asm.cpp index 63492b5d9ce..9b85ff0cb7f 100644 --- a/src/ansi-c/goto-conversion/goto_asm.cpp +++ b/src/ansi-c/goto-conversion/goto_asm.cpp @@ -11,9 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" -void goto_convertt::convert_asm( - const code_asmt &code, - goto_programt &dest) +void goto_convertt::convert_asm(const code_asmt &code, goto_programt &dest) { // copy as OTHER copy(code, OTHER, dest); diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 39451755393..036845ff8a8 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -36,11 +36,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include -#include - #include class goto_check_ct @@ -1169,11 +1168,10 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard) isinf_exprt(to_binary_expr(expr).op1()), not_exprt(isinf_exprt(expr))); - std::string kind = expr.id() == ID_plus - ? "addition" - : expr.id() == ID_minus - ? "subtraction" - : expr.id() == ID_mult ? "multiplication" : ""; + std::string kind = expr.id() == ID_plus ? "addition" + : expr.id() == ID_minus ? "subtraction" + : expr.id() == ID_mult ? "multiplication" + : ""; add_guarded_property( std::move(overflow_check), diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index 2c9e1f32f4f..f8de1cff1ed 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -22,7 +22,7 @@ symbol_exprt goto_convertt::make_compound_literal( goto_programt &dest, const irep_idt &mode) { - const source_locationt source_location=expr.find_source_location(); + const source_locationt source_location = expr.find_source_location(); symbolt &new_symbol = get_fresh_aux_symbol( expr.type(), @@ -32,13 +32,13 @@ symbol_exprt goto_convertt::make_compound_literal( mode, symbol_table); new_symbol.is_static_lifetime = lifetime != lifetimet::AUTOMATIC_LOCAL; - new_symbol.value=expr; + new_symbol.value = expr; // The value might depend on a variable, thus // generate code for this. - symbol_exprt result=new_symbol.symbol_expr(); - result.add_source_location()=source_location; + symbol_exprt result = new_symbol.symbol_expr(); + result.add_source_location() = source_location; // The lifetime of compound literals is really that of // the block they are in. @@ -46,7 +46,7 @@ symbol_exprt goto_convertt::make_compound_literal( copy(code_declt(result), DECL, dest); code_assignt code_assign(result, expr); - code_assign.add_source_location()=source_location; + code_assign.add_source_location() = source_location; convert(code_assign, dest, mode); // now create a 'dead' instruction @@ -87,7 +87,7 @@ bool goto_convertt::needs_cleaning(const exprt &expr) // g1 = (i == 0) // g2 = (i > 10) // forall (i : int) (g1 || g2) - if(expr.id()==ID_forall || expr.id()==ID_exists) + if(expr.id() == ID_forall || expr.id() == ID_exists) return false; for(const auto &op : expr.operands()) @@ -115,10 +115,11 @@ void goto_convertt::rewrite_boolean(exprt &expr) // re-write "a ==> b" into a?b:1 if(auto implies = expr_try_dynamic_cast(expr)) { - expr = if_exprt{std::move(implies->lhs()), - std::move(implies->rhs()), - true_exprt{}, - bool_typet{}}; + expr = if_exprt{ + std::move(implies->lhs()), + std::move(implies->rhs()), + true_exprt{}, + bool_typet{}}; return; } @@ -127,27 +128,25 @@ void goto_convertt::rewrite_boolean(exprt &expr) exprt tmp; - if(expr.id()==ID_and) - tmp=true_exprt(); + if(expr.id() == ID_and) + tmp = true_exprt(); else // ID_or - tmp=false_exprt(); + tmp = false_exprt(); - exprt::operandst &ops=expr.operands(); + exprt::operandst &ops = expr.operands(); // start with last one - for(exprt::operandst::reverse_iterator - it=ops.rbegin(); - it!=ops.rend(); + for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend(); ++it) { - exprt &op=*it; + exprt &op = *it; DATA_INVARIANT_WITH_DIAGNOSTICS( op.is_boolean(), "boolean operators must have only boolean operands", expr.find_source_location()); - if(expr.id()==ID_and) + if(expr.id() == ID_and) { if_exprt if_e(op, tmp, false_exprt()); tmp.swap(if_e); @@ -191,27 +190,28 @@ void goto_convertt::clean_expr( clean_expr(expr, dest, mode, result_is_used); return; } - else if(expr.id()==ID_if) + else if(expr.id() == ID_if) { // first clean condition clean_expr(to_if_expr(expr).cond(), dest, mode, true); // possibly done now - if(!needs_cleaning(to_if_expr(expr).true_case()) && - !needs_cleaning(to_if_expr(expr).false_case())) + if( + !needs_cleaning(to_if_expr(expr).true_case()) && + !needs_cleaning(to_if_expr(expr).false_case())) return; // copy expression - if_exprt if_expr=to_if_expr(expr); + if_exprt if_expr = to_if_expr(expr); DATA_INVARIANT_WITH_DIAGNOSTICS( if_expr.cond().is_boolean(), "condition for an 'if' must be boolean", if_expr.find_source_location()); - const source_locationt source_location=expr.find_source_location(); + const source_locationt source_location = expr.find_source_location(); - #if 0 +#if 0 // We do some constant-folding here, to mimic // what typical compilers do. { @@ -230,7 +230,7 @@ void goto_convertt::clean_expr( return; } } - #endif +#endif goto_programt tmp_true; clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used); @@ -244,19 +244,19 @@ void goto_convertt::clean_expr( new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode); code_assignt assignment_true; - assignment_true.lhs()=new_symbol.symbol_expr(); - assignment_true.rhs()=if_expr.true_case(); - assignment_true.add_source_location()=source_location; + assignment_true.lhs() = new_symbol.symbol_expr(); + assignment_true.rhs() = if_expr.true_case(); + assignment_true.add_source_location() = source_location; convert(assignment_true, tmp_true, mode); code_assignt assignment_false; - assignment_false.lhs()=new_symbol.symbol_expr(); - assignment_false.rhs()=if_expr.false_case(); - assignment_false.add_source_location()=source_location; + assignment_false.lhs() = new_symbol.symbol_expr(); + assignment_false.rhs() = if_expr.false_case(); + assignment_false.add_source_location() = source_location; convert(assignment_false, tmp_false, mode); // overwrites expr - expr=new_symbol.symbol_expr(); + expr = new_symbol.symbol_expr(); } else { @@ -279,7 +279,7 @@ void goto_convertt::clean_expr( convert(code_expression, tmp_false, mode); } - expr=nil_exprt(); + expr = nil_exprt(); } // generate guard for argument side-effects @@ -295,7 +295,7 @@ void goto_convertt::clean_expr( return; } - else if(expr.id()==ID_comma) + else if(expr.id() == ID_comma) { if(result_is_used) { @@ -303,7 +303,7 @@ void goto_convertt::clean_expr( Forall_operands(it, expr) { - bool last=(it==--expr.operands().end()); + bool last = (it == --expr.operands().end()); // special treatment for last one if(last) @@ -334,12 +334,12 @@ void goto_convertt::clean_expr( convert(code_expressiont(*it), dest, mode); } - expr=nil_exprt(); + expr = nil_exprt(); } return; } - else if(expr.id()==ID_typecast) + else if(expr.id() == ID_typecast) { typecast_exprt &typecast = to_typecast_expr(expr); @@ -351,18 +351,18 @@ void goto_convertt::clean_expr( return; } - else if(expr.id()==ID_side_effect) + else if(expr.id() == ID_side_effect) { // some of the side-effects need special treatment! - const irep_idt statement=to_side_effect_expr(expr).get_statement(); + const irep_idt statement = to_side_effect_expr(expr).get_statement(); - if(statement==ID_gcc_conditional_expression) + if(statement == ID_gcc_conditional_expression) { // need to do separately remove_gcc_conditional_expression(expr, dest, mode); return; } - else if(statement==ID_statement_expression) + else if(statement == ID_statement_expression) { // need to do separately to prevent that // the operands of expr get 'cleaned' @@ -370,7 +370,7 @@ void goto_convertt::clean_expr( to_side_effect_expr(expr), dest, mode, result_is_used); return; } - else if(statement==ID_assign) + else if(statement == ID_assign) { // we do a special treatment for x=f(...) INVARIANT( @@ -402,7 +402,7 @@ void goto_convertt::clean_expr( exprt new_rhs = typecast_exprt::conditional_cast( side_effect_assign.rhs(), new_lhs.type()); code_assignt assignment(std::move(new_lhs), new_rhs); - assignment.add_source_location()=expr.source_location(); + assignment.add_source_location() = expr.source_location(); convert_assign(assignment, dest, mode); if(result_is_used) @@ -413,13 +413,13 @@ void goto_convertt::clean_expr( } } } - else if(expr.id()==ID_forall || expr.id()==ID_exists) + else if(expr.id() == ID_forall || expr.id() == ID_exists) { DATA_INVARIANT( !has_subexpr(expr, ID_side_effect), "the front-end should check quantified expressions for side-effects"); } - else if(expr.id()==ID_address_of) + else if(expr.id() == ID_address_of) { address_of_exprt &addr = to_address_of_expr(expr); clean_expr_address_of(addr.object(), dest, mode); @@ -431,12 +431,12 @@ void goto_convertt::clean_expr( Forall_operands(it, expr) clean_expr(*it, dest, mode); - if(expr.id()==ID_side_effect) + if(expr.id() == ID_side_effect) { remove_side_effect( to_side_effect_expr(expr), dest, mode, result_is_used, false); } - else if(expr.id()==ID_compound_literal) + else if(expr.id() == ID_compound_literal) { // This is simply replaced by the literal DATA_INVARIANT( @@ -453,30 +453,30 @@ void goto_convertt::clean_expr_address_of( // The address of object constructors can be taken, // which is re-written into the address of a variable. - if(expr.id()==ID_compound_literal) + if(expr.id() == ID_compound_literal) { DATA_INVARIANT( expr.operands().size() == 1, "ID_compound_literal has a single operand"); clean_expr(to_unary_expr(expr).op(), dest, mode); expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode); } - else if(expr.id()==ID_string_constant) + else if(expr.id() == ID_string_constant) { // Leave for now, but long-term these might become static symbols. // LLVM appears to do precisely that. } - else if(expr.id()==ID_index) + else if(expr.id() == ID_index) { index_exprt &index_expr = to_index_expr(expr); clean_expr_address_of(index_expr.array(), dest, mode); clean_expr(index_expr.index(), dest, mode); } - else if(expr.id()==ID_dereference) + else if(expr.id() == ID_dereference) { dereference_exprt &deref_expr = to_dereference_expr(expr); clean_expr(deref_expr.pointer(), dest, mode); } - else if(expr.id()==ID_comma) + else if(expr.id() == ID_comma) { // Yes, one can take the address of a comma expression. // Treatment is similar to clean_expr() above. @@ -485,7 +485,7 @@ void goto_convertt::clean_expr_address_of( Forall_operands(it, expr) { - bool last=(it==--expr.operands().end()); + bool last = (it == --expr.operands().end()); // special treatment for last one if(last) diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 2a79ffd9f35..f7e2961a1e6 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Program Transformation -#include "destructor.h" #include "goto_convert.h" #include "goto_convert_class.h" @@ -27,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "destructor.h" + static bool is_empty(const goto_programt &goto_program) { forall_goto_program_instructions(it, goto_program) @@ -67,7 +68,7 @@ static void finish_catch_push_targets(goto_programt &dest) if(instruction.targets.empty()) { - bool handler_added=true; + bool handler_added = true; const code_push_catcht::exception_listt &handler_list = to_code_push_catch(instruction.code()).exception_list(); @@ -75,9 +76,9 @@ static void finish_catch_push_targets(goto_programt &dest) { // some handlers may not have been converted (if there was no // exception to be caught); in such a situation we abort - if(label_targets.find(handler.get_label())==label_targets.end()) + if(label_targets.find(handler.get_label()) == label_targets.end()) { - handler_added=false; + handler_added = false; break; } } @@ -245,7 +246,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) for(const auto &g_it : targets.gotos) { - goto_programt::instructiont &i=*(g_it.first); + goto_programt::instructiont &i = *(g_it.first); if(i.is_start_thread()) { @@ -346,7 +347,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) { for(auto &g_it : targets.computed_gotos) { - goto_programt::instructiont &i=*g_it; + goto_programt::instructiont &i = *g_it; dereference_exprt destination = to_dereference_expr(i.code().op0()); const exprt pointer = destination.pointer(); @@ -455,7 +456,7 @@ void goto_convertt::convert_label( const irep_idt &mode) { // grab the label - const irep_idt &label=code.get_label(); + const irep_idt &label = code.get_label(); goto_programt tmp; @@ -474,14 +475,14 @@ void goto_convertt::convert_label( // thread block (START_THREAD...END_THREAD). code_blockt thread_body; thread_body.add(to_code_label(code).code()); - thread_body.add_source_location()=code.source_location(); + thread_body.add_source_location() = code.source_location(); generate_thread_block(thread_body, dest, mode); } else { convert(to_code_label(code).code(), tmp, mode); - goto_programt::targett target=tmp.instructions.begin(); + goto_programt::targett target = tmp.instructions.begin(); dest.destructive_append(tmp); targets.labels.insert( @@ -490,9 +491,7 @@ void goto_convertt::convert_label( } } -void goto_convertt::convert_gcc_local_label( - const codet &, - goto_programt &) +void goto_convertt::convert_gcc_local_label(const codet &, goto_programt &) { // ignore for now } @@ -505,7 +504,7 @@ void goto_convertt::convert_switch_case( goto_programt tmp; convert(code.code(), tmp, mode); - goto_programt::targett target=tmp.instructions.begin(); + goto_programt::targett target = tmp.instructions.begin(); dest.destructive_append(tmp); // is a default target given? @@ -516,15 +515,16 @@ void goto_convertt::convert_switch_case( { // cases? - cases_mapt::iterator cases_entry=targets.cases_map.find(target); - if(cases_entry==targets.cases_map.end()) + cases_mapt::iterator cases_entry = targets.cases_map.find(target); + if(cases_entry == targets.cases_map.end()) { targets.cases.push_back(std::make_pair(target, caset())); - cases_entry=targets.cases_map.insert(std::make_pair( - target, --targets.cases.end())).first; + cases_entry = + targets.cases_map.insert(std::make_pair(target, --targets.cases.end())) + .first; } - exprt::operandst &case_op_dest=cases_entry->second->second; + exprt::operandst &case_op_dest = cases_entry->second->second; case_op_dest.push_back(code.case_op()); // make sure we have a source location in the case operand as otherwise we // end up with a GOTO instruction without a source location @@ -571,9 +571,9 @@ void goto_convertt::convert_gcc_switch_case_range( } // create a skeleton for case_guard - cases_entry->second->second.push_back( - and_exprt{binary_relation_exprt{code.lower(), ID_le, nil_exprt{}}, - binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}}); + cases_entry->second->second.push_back(and_exprt{ + binary_relation_exprt{code.lower(), ID_le, nil_exprt{}}, + binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}}); } /// converts 'code' and appends the result to 'dest' @@ -582,83 +582,82 @@ void goto_convertt::convert( goto_programt &dest, const irep_idt &mode) { - const irep_idt &statement=code.get_statement(); + const irep_idt &statement = code.get_statement(); - if(statement==ID_block) + if(statement == ID_block) convert_block(to_code_block(code), dest, mode); - else if(statement==ID_decl) + else if(statement == ID_decl) convert_frontend_decl(to_code_frontend_decl(code), dest, mode); - else if(statement==ID_decl_type) + else if(statement == ID_decl_type) convert_decl_type(code, dest); - else if(statement==ID_expression) + else if(statement == ID_expression) convert_expression(to_code_expression(code), dest, mode); - else if(statement==ID_assign) + else if(statement == ID_assign) convert_assign(to_code_assign(code), dest, mode); - else if(statement==ID_assert) + else if(statement == ID_assert) convert_assert(to_code_assert(code), dest, mode); - else if(statement==ID_assume) + else if(statement == ID_assume) convert_assume(to_code_assume(code), dest, mode); - else if(statement==ID_function_call) + else if(statement == ID_function_call) convert_function_call(to_code_function_call(code), dest, mode); - else if(statement==ID_label) + else if(statement == ID_label) convert_label(to_code_label(code), dest, mode); - else if(statement==ID_gcc_local_label) + else if(statement == ID_gcc_local_label) convert_gcc_local_label(code, dest); - else if(statement==ID_switch_case) + else if(statement == ID_switch_case) convert_switch_case(to_code_switch_case(code), dest, mode); - else if(statement==ID_gcc_switch_case_range) + else if(statement == ID_gcc_switch_case_range) convert_gcc_switch_case_range( to_code_gcc_switch_case_range(code), dest, mode); - else if(statement==ID_for) + else if(statement == ID_for) convert_for(to_code_for(code), dest, mode); - else if(statement==ID_while) + else if(statement == ID_while) convert_while(to_code_while(code), dest, mode); - else if(statement==ID_dowhile) + else if(statement == ID_dowhile) convert_dowhile(to_code_dowhile(code), dest, mode); - else if(statement==ID_switch) + else if(statement == ID_switch) convert_switch(to_code_switch(code), dest, mode); - else if(statement==ID_break) + else if(statement == ID_break) convert_break(to_code_break(code), dest, mode); - else if(statement==ID_return) + else if(statement == ID_return) convert_return(to_code_frontend_return(code), dest, mode); - else if(statement==ID_continue) + else if(statement == ID_continue) convert_continue(to_code_continue(code), dest, mode); - else if(statement==ID_goto) + else if(statement == ID_goto) convert_goto(to_code_goto(code), dest); - else if(statement==ID_gcc_computed_goto) + else if(statement == ID_gcc_computed_goto) convert_gcc_computed_goto(code, dest); - else if(statement==ID_skip) + else if(statement == ID_skip) convert_skip(code, dest); - else if(statement==ID_ifthenelse) + else if(statement == ID_ifthenelse) convert_ifthenelse(to_code_ifthenelse(code), dest, mode); - else if(statement==ID_start_thread) + else if(statement == ID_start_thread) convert_start_thread(code, dest); - else if(statement==ID_end_thread) + else if(statement == ID_end_thread) convert_end_thread(code, dest); - else if(statement==ID_atomic_begin) + else if(statement == ID_atomic_begin) convert_atomic_begin(code, dest); - else if(statement==ID_atomic_end) + else if(statement == ID_atomic_end) convert_atomic_end(code, dest); - else if(statement==ID_cpp_delete || - statement=="cpp_delete[]") + else if(statement == ID_cpp_delete || statement == "cpp_delete[]") convert_cpp_delete(code, dest); - else if(statement==ID_msc_try_except) + else if(statement == ID_msc_try_except) convert_msc_try_except(code, dest, mode); - else if(statement==ID_msc_try_finally) + else if(statement == ID_msc_try_finally) convert_msc_try_finally(code, dest, mode); - else if(statement==ID_msc_leave) + else if(statement == ID_msc_leave) convert_msc_leave(code, dest, mode); - else if(statement==ID_try_catch) // C++ try/catch + else if(statement == ID_try_catch) // C++ try/catch convert_try_catch(code, dest, mode); - else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade + else if(statement == ID_CPROVER_try_catch) // CPROVER-homemade convert_CPROVER_try_catch(code, dest, mode); - else if(statement==ID_CPROVER_throw) // CPROVER-homemade + else if(statement == ID_CPROVER_throw) // CPROVER-homemade convert_CPROVER_throw(code, dest, mode); - else if(statement==ID_CPROVER_try_finally) + else if(statement == ID_CPROVER_try_finally) convert_CPROVER_try_finally(code, dest, mode); - else if(statement==ID_asm) + else if(statement == ID_asm) convert_asm(to_code_asm(code), dest); - else if(statement==ID_static_assert) + else if(statement == ID_static_assert) { PRECONDITION(code.operands().size() == 2); exprt assertion = @@ -669,16 +668,16 @@ void goto_convertt::convert( "static assertion " + id2string(get_string_constant(code.op1())), code.op0().find_source_location()); } - else if(statement==ID_dead) + else if(statement == ID_dead) copy(code, DEAD, dest); - else if(statement==ID_decl_block) + else if(statement == ID_decl_block) { for(const auto &op : code.operands()) convert(to_code(op), dest, mode); } - else if(statement==ID_push_catch || - statement==ID_pop_catch || - statement==ID_exception_landingpad) + else if( + statement == ID_push_catch || statement == ID_pop_catch || + statement == ID_exception_landingpad) copy(code, CATCH, dest); else copy(code, OTHER, dest); @@ -695,7 +694,7 @@ void goto_convertt::convert_block( goto_programt &dest, const irep_idt &mode) { - const source_locationt &end_location=code.end_location(); + const source_locationt &end_location = code.end_location(); // this saves the index of the destructor stack node_indext old_stack_top = targets.scope_stack.get_current_node(); @@ -726,18 +725,18 @@ void goto_convertt::convert_expression( { exprt expr = code.expression(); - if(expr.id()==ID_if) + if(expr.id() == ID_if) { // We do a special treatment for c?t:f // by compiling to if(c) t; else f; - const if_exprt &if_expr=to_if_expr(expr); + const if_exprt &if_expr = to_if_expr(expr); code_ifthenelset tmp_code( if_expr.cond(), code_expressiont(if_expr.true_case()), code_expressiont(if_expr.false_case())); - tmp_code.add_source_location()=expr.source_location(); - tmp_code.then_case().add_source_location()=expr.source_location(); - tmp_code.else_case().add_source_location()=expr.source_location(); + tmp_code.add_source_location() = expr.source_location(); + tmp_code.then_case().add_source_location() = expr.source_location(); + tmp_code.else_case().add_source_location() = expr.source_location(); convert_ifthenelse(tmp_code, dest, mode); } else @@ -748,9 +747,9 @@ void goto_convertt::convert_expression( // We keep it to add checks later. if(expr.is_not_nil()) { - codet tmp=code; - tmp.op0()=expr; - tmp.add_source_location()=expr.source_location(); + codet tmp = code; + tmp.op0() = expr; + tmp.add_source_location() = expr.source_location(); copy(tmp, OTHER, dest); } } @@ -765,8 +764,7 @@ void goto_convertt::convert_frontend_decl( const symbolt &symbol = ns.lookup(identifier); - if(symbol.is_static_lifetime || - symbol.type.id()==ID_code) + if(symbol.is_static_lifetime || symbol.type.id() == ID_code) return; // this is a SKIP! const goto_programt::targett declaration_iterator = [&]() { @@ -778,7 +776,7 @@ void goto_convertt::convert_frontend_decl( exprt initializer = code.op1(); - codet tmp=code; + codet tmp = code; tmp.operands().resize(1); // hide this declaration-without-initializer step in the goto trace tmp.add_source_location().set_hide(); @@ -814,7 +812,7 @@ void goto_convertt::convert_frontend_decl( } // do destructor - code_function_callt destructor=get_destructor(ns, symbol.type); + code_function_callt destructor = get_destructor(ns, symbol.type); if(destructor.is_not_nil()) { @@ -826,9 +824,7 @@ void goto_convertt::convert_frontend_decl( } } -void goto_convertt::convert_decl_type( - const codet &, - goto_programt &) +void goto_convertt::convert_decl_type(const codet &, goto_programt &) { // we remove these } @@ -838,13 +834,11 @@ void goto_convertt::convert_assign( goto_programt &dest, const irep_idt &mode) { - exprt lhs=code.lhs(), - rhs=code.rhs(); + exprt lhs = code.lhs(), rhs = code.rhs(); clean_expr(lhs, dest, mode); - if(rhs.id()==ID_side_effect && - rhs.get(ID_statement)==ID_function_call) + if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call) { const auto &rhs_function_call = to_side_effect_expr_function_call(rhs); @@ -863,9 +857,9 @@ void goto_convertt::convert_assign( dest, mode); } - else if(rhs.id()==ID_side_effect && - (rhs.get(ID_statement)==ID_cpp_new || - rhs.get(ID_statement)==ID_cpp_new_array)) + else if( + rhs.id() == ID_side_effect && (rhs.get(ID_statement) == ID_cpp_new || + rhs.get(ID_statement) == ID_cpp_new_array)) { Forall_operands(it, rhs) clean_expr(*it, dest, mode); @@ -898,8 +892,8 @@ void goto_convertt::convert_assign( clean_expr(*it, dest, mode); code_assignt new_assign(code); - new_assign.lhs()=lhs; - new_assign.rhs()=rhs; + new_assign.lhs() = lhs; + new_assign.rhs() = rhs; copy(new_assign, ASSIGN, dest); } @@ -909,51 +903,49 @@ void goto_convertt::convert_assign( clean_expr(rhs, dest, mode); code_assignt new_assign(code); - new_assign.lhs()=lhs; - new_assign.rhs()=rhs; + new_assign.lhs() = lhs; + new_assign.rhs() = rhs; copy(new_assign, ASSIGN, dest); } } -void goto_convertt::convert_cpp_delete( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().size() == 1, "cpp_delete statement takes one operand", code.find_source_location()); - exprt tmp_op=code.op0(); + exprt tmp_op = code.op0(); clean_expr(tmp_op, dest, ID_cpp); // we call the destructor, and then free - const exprt &destructor= + const exprt &destructor = static_cast(code.find(ID_destructor)); irep_idt delete_identifier; - if(code.get_statement()==ID_cpp_delete_array) - delete_identifier="__delete_array"; - else if(code.get_statement()==ID_cpp_delete) - delete_identifier="__delete"; + if(code.get_statement() == ID_cpp_delete_array) + delete_identifier = "__delete_array"; + else if(code.get_statement() == ID_cpp_delete) + delete_identifier = "__delete"; else UNREACHABLE; if(destructor.is_not_nil()) { - if(code.get_statement()==ID_cpp_delete_array) + if(code.get_statement() == ID_cpp_delete_array) { // build loop } - else if(code.get_statement()==ID_cpp_delete) + else if(code.get_statement() == ID_cpp_delete) { // just one object const dereference_exprt deref_op(tmp_op); - codet tmp_code=to_code(destructor); + codet tmp_code = to_code(destructor); replace_new_object(deref_op, tmp_code); convert(tmp_code, dest, ID_cpp); } @@ -962,18 +954,18 @@ void goto_convertt::convert_cpp_delete( } // now do "free" - exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr(); + exprt delete_symbol = ns.lookup(delete_identifier).symbol_expr(); DATA_INVARIANT( to_code_type(delete_symbol.type()).parameters().size() == 1, "delete statement takes 1 parameter"); - typet arg_type= + typet arg_type = to_code_type(delete_symbol.type()).parameters().front().type(); code_function_callt delete_call( delete_symbol, {typecast_exprt(tmp_op, arg_type)}); - delete_call.add_source_location()=code.source_location(); + delete_call.add_source_location() = code.source_location(); convert(delete_call, dest, ID_cpp); } @@ -983,7 +975,7 @@ void goto_convertt::convert_assert( goto_programt &dest, const irep_idt &mode) { - exprt cond=code.assertion(); + exprt cond = code.assertion(); clean_expr(cond, dest, mode); @@ -992,9 +984,7 @@ void goto_convertt::convert_assert( dest.add(goto_programt::make_assertion(cond, annotated_location)); } -void goto_convertt::convert_skip( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_skip(const codet &code, goto_programt &dest) { dest.add(goto_programt::instructiont( code, code.source_location(), SKIP, nil_exprt(), {})); @@ -1005,7 +995,7 @@ void goto_convertt::convert_assume( goto_programt &dest, const irep_idt &mode) { - exprt op=code.assumption(); + exprt op = code.assumption(); clean_expr(op, dest, mode); @@ -1074,7 +1064,7 @@ void goto_convertt::convert_for( if(code.init().is_not_nil()) convert(to_code(code.init()), dest, mode); - exprt cond=code.cond(); + exprt cond = code.cond(); goto_programt sideeffects; clean_expr(cond, sideeffects, mode); @@ -1083,7 +1073,7 @@ void goto_convertt::convert_for( break_continue_targetst old_targets(targets); // do the u label - goto_programt::targett u=sideeffects.instructions.begin(); + goto_programt::targett u = sideeffects.instructions.begin(); // do the v label goto_programt tmp_v; @@ -1103,7 +1093,7 @@ void goto_convertt::convert_for( } else { - exprt tmp_B=code.iter(); + exprt tmp_B = code.iter(); clean_expr(tmp_B, tmp_x, mode, false); @@ -1113,7 +1103,7 @@ void goto_convertt::convert_for( // optimize the v label if(sideeffects.instructions.empty()) - u=v; + u = v; // set the targets targets.set_break(z); @@ -1151,8 +1141,8 @@ void goto_convertt::convert_while( goto_programt &dest, const irep_idt &mode) { - const exprt &cond=code.cond(); - const source_locationt &source_location=code.source_location(); + const exprt &cond = code.cond(); + const source_locationt &source_location = code.source_location(); // while(c) P; //-------------------- @@ -1175,7 +1165,7 @@ void goto_convertt::convert_while( boolean_negate(cond), z, source_location, tmp_branch, mode); // do the v label - goto_programt::targett v=tmp_branch.instructions.begin(); + goto_programt::targett v = tmp_branch.instructions.begin(); // y: goto v; goto_programt tmp_y; @@ -1213,9 +1203,9 @@ void goto_convertt::convert_dowhile( code.find_source_location()); // save source location - source_locationt condition_location=code.cond().find_source_location(); + source_locationt condition_location = code.cond().find_source_location(); - exprt cond=code.cond(); + exprt cond = code.cond(); goto_programt sideeffects; clean_expr(cond, sideeffects, mode); @@ -1243,9 +1233,9 @@ void goto_convertt::convert_dowhile( // do the x label goto_programt::targett x; if(sideeffects.instructions.empty()) - x=y; + x = y; else - x=sideeffects.instructions.begin(); + x = sideeffects.instructions.begin(); // set the targets targets.set_break(z); @@ -1254,7 +1244,7 @@ void goto_convertt::convert_dowhile( // do the w label goto_programt tmp_w; convert(code.body(), tmp_w, mode); - goto_programt::targett w=tmp_w.instructions.begin(); + goto_programt::targett w = tmp_w.instructions.begin(); // y: if(c) goto w; y->complete_goto(w); @@ -1327,13 +1317,13 @@ void goto_convertt::convert_switch( // get the location of the end of the body, but // default to location of switch, if none - source_locationt body_end_location= - code.body().get_statement()==ID_block? - to_code_block(code.body()).end_location(): - code.source_location(); + source_locationt body_end_location = + code.body().get_statement() == ID_block + ? to_code_block(code.body()).end_location() + : code.source_location(); // do the value we switch over - exprt argument=code.value(); + exprt argument = code.value(); goto_programt sideeffects; clean_expr(argument, sideeffects, mode); @@ -1390,20 +1380,20 @@ void goto_convertt::convert_switch( // case 10: // case_number 3 // ...; // } - size_t case_number=1; + size_t case_number = 1; for(auto &case_pair : targets.cases) { - const caset &case_ops=case_pair.second; + const caset &case_ops = case_pair.second; - if (case_ops.empty()) + if(case_ops.empty()) continue; - exprt guard_expr=case_guard(argument, case_ops); + exprt guard_expr = case_guard(argument, case_ops); - source_locationt source_location=case_ops.front().find_source_location(); + source_locationt source_location = case_ops.front().find_source_location(); source_location.set_case_number(std::to_string(case_number)); case_number++; - guard_expr.add_source_location()=source_location; + guard_expr.add_source_location() = source_location; tmp_cases.add(goto_programt::make_goto( case_pair.first, std::move(guard_expr), source_location)); @@ -1458,8 +1448,7 @@ void goto_convertt::convert_return( if(new_code.has_return_value()) { - bool result_is_used= - new_code.return_value().type().id()!=ID_empty; + bool result_is_used = new_code.return_value().type().id() != ID_empty; goto_programt sideeffects; clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); @@ -1539,9 +1528,7 @@ void goto_convertt::convert_gcc_computed_goto( targets.computed_gotos.push_back(t); } -void goto_convertt::convert_start_thread( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_start_thread(const codet &code, goto_programt &dest) { goto_programt::targett start_thread = dest.add(goto_programt::instructiont( code, code.source_location(), START_THREAD, nil_exprt(), {})); @@ -1551,9 +1538,7 @@ void goto_convertt::convert_start_thread( start_thread, targets.scope_stack.get_current_node()); } -void goto_convertt::convert_end_thread( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_end_thread(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().empty(), @@ -1563,9 +1548,7 @@ void goto_convertt::convert_end_thread( copy(code, END_THREAD, dest); } -void goto_convertt::convert_atomic_begin( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_atomic_begin(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().empty(), @@ -1575,9 +1558,7 @@ void goto_convertt::convert_atomic_begin( copy(code, ATOMIC_BEGIN, dest); } -void goto_convertt::convert_atomic_end( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_atomic_end(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().empty(), @@ -1594,10 +1575,9 @@ void goto_convertt::convert_ifthenelse( { DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body"); - bool has_else= - !code.else_case().is_nil(); + bool has_else = !code.else_case().is_nil(); - const source_locationt &source_location=code.source_location(); + const source_locationt &source_location = code.source_location(); // We do a bit of special treatment for && in the condition // in case cleaning would be needed otherwise. @@ -1636,7 +1616,7 @@ void goto_convertt::convert_ifthenelse( : code.else_case().source_location(); } - exprt tmp_guard=code.cond(); + exprt tmp_guard = code.cond(); clean_expr(tmp_guard, dest, mode); generate_ifthenelse( @@ -1655,7 +1635,7 @@ void goto_convertt::collect_operands( const irep_idt &id, std::list &dest) { - if(expr.id()!=id) + if(expr.id() != id) { dest.push_back(expr); } @@ -1673,7 +1653,7 @@ void goto_convertt::collect_operands( static inline bool is_size_one(const goto_programt &g) { return (!g.instructions.empty()) && - ++g.instructions.begin()==g.instructions.end(); + ++g.instructions.begin() == g.instructions.end(); } /// if(guard) true_case; else false_case; @@ -1687,8 +1667,7 @@ void goto_convertt::generate_ifthenelse( goto_programt &dest, const irep_idt &mode) { - if(is_empty(true_case) && - is_empty(false_case)) + if(is_empty(true_case) && is_empty(false_case)) { // hmpf. Useless branch. goto_programt tmp_z; @@ -1765,7 +1744,7 @@ void goto_convertt::generate_ifthenelse( mode); } - bool has_else=!is_empty(false_case); + bool has_else = !is_empty(false_case); // if(c) P; //-------------------- @@ -1797,7 +1776,7 @@ void goto_convertt::generate_ifthenelse( if(has_else) { tmp_y.swap(false_case); - y=tmp_y.instructions.begin(); + y = tmp_y.instructions.begin(); } // v: if(!c) goto z/y; @@ -1849,7 +1828,7 @@ static bool has_and_or(const exprt &expr) return true; } - if(expr.id()==ID_and || expr.id()==ID_or) + if(expr.id() == ID_and || expr.id() == ID_or) return true; return false; @@ -1881,7 +1860,7 @@ void goto_convertt::generate_conditional_branch( else { // simple branch - exprt cond=guard; + exprt cond = guard; clean_expr(cond, dest, mode); dest.add(goto_programt::make_goto(target_true, cond, source_location)); @@ -1897,7 +1876,7 @@ void goto_convertt::generate_conditional_branch( goto_programt &dest, const irep_idt &mode) { - if(guard.id()==ID_not) + if(guard.id() == ID_not) { // simply swap targets generate_conditional_branch( @@ -1910,7 +1889,7 @@ void goto_convertt::generate_conditional_branch( return; } - if(guard.id()==ID_and) + if(guard.id() == ID_and) { // turn // if(a && b) goto target_true; else goto target_false; @@ -1930,7 +1909,7 @@ void goto_convertt::generate_conditional_branch( return; } - else if(guard.id()==ID_or) + else if(guard.id() == ID_or) { // turn // if(a || b) goto target_true; else goto target_false; @@ -1953,7 +1932,7 @@ void goto_convertt::generate_conditional_branch( return; } - exprt cond=guard; + exprt cond = guard; clean_expr(cond, dest, mode); // true branch @@ -1963,9 +1942,7 @@ void goto_convertt::generate_conditional_branch( dest.add(goto_programt::make_goto(target_false, source_location)); } -bool goto_convertt::get_string_constant( - const exprt &expr, - irep_idt &value) +bool goto_convertt::get_string_constant(const exprt &expr, irep_idt &value) { if(expr.id() == ID_typecast) return get_string_constant(to_typecast_expr(expr).op(), value); @@ -1978,12 +1955,12 @@ bool goto_convertt::get_string_constant( get_constant(to_index_expr(to_address_of_expr(expr).object()).array()); simplify(index_op, ns); - if(index_op.id()==ID_string_constant) + if(index_op.id() == ID_string_constant) { value = to_string_constant(index_op).value(); return false; } - else if(index_op.id()==ID_array) + else if(index_op.id() == ID_array) { std::string result; for(const auto &op : as_const(index_op).operands()) @@ -1999,11 +1976,11 @@ bool goto_convertt::get_string_constant( } } - return value=result, false; + return value = result, false; } } - if(expr.id()==ID_string_constant) + if(expr.id() == ID_string_constant) { value = to_string_constant(expr).value(); return false; @@ -2028,20 +2005,19 @@ irep_idt goto_convertt::get_string_constant(const exprt &expr) exprt goto_convertt::get_constant(const exprt &expr) { - if(expr.id()==ID_symbol) + if(expr.id() == ID_symbol) { - const symbolt &symbol= - ns.lookup(to_symbol_expr(expr)); + const symbolt &symbol = ns.lookup(to_symbol_expr(expr)); return symbol.value; } - else if(expr.id()==ID_member) + else if(expr.id() == ID_member) { auto tmp = to_member_expr(expr); tmp.compound() = get_constant(tmp.compound()); return std::move(tmp); } - else if(expr.id()==ID_index) + else if(expr.id() == ID_index) { auto tmp = to_index_expr(expr); tmp.op0() = get_constant(tmp.op0()); @@ -2069,7 +2045,7 @@ symbolt &goto_convertt::new_tmp_symbol( symbol_table); code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=source_location; + decl.add_source_location() = source_location; convert_frontend_decl(decl, dest, mode); return new_symbol; @@ -2081,19 +2057,19 @@ void goto_convertt::make_temp_symbol( goto_programt &dest, const irep_idt &mode) { - const source_locationt source_location=expr.find_source_location(); + const source_locationt source_location = expr.find_source_location(); symbolt &new_symbol = new_tmp_symbol(expr.type(), suffix, dest, source_location, mode); code_assignt assignment; - assignment.lhs()=new_symbol.symbol_expr(); - assignment.rhs()=expr; - assignment.add_source_location()=source_location; + assignment.lhs() = new_symbol.symbol_expr(); + assignment.rhs() = expr; + assignment.add_source_location() = source_location; convert(assignment, dest, mode); - expr=new_symbol.symbol_expr(); + expr = new_symbol.symbol_expr(); } void goto_convert( @@ -2121,7 +2097,7 @@ void goto_convert( DATA_INVARIANT( s_it != symbol_table.symbols.end(), "failed to find main symbol"); - const symbolt &symbol=s_it->second; + const symbolt &symbol = s_it->second; ::goto_convert( to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode); diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index b23f569b692..3a8a741476b 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -17,20 +17,20 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include -#include +#include "scope_tree.h" #include #include #include -#include "scope_tree.h" - class side_effect_expr_overflowt; struct build_declaration_hops_inputst; -class goto_convertt:public messaget +class goto_convertt : public messaget { public: void @@ -38,11 +38,11 @@ class goto_convertt:public messaget goto_convertt( symbol_table_baset &_symbol_table, - message_handlert &_message_handler): - messaget(_message_handler), - symbol_table(_symbol_table), - ns(_symbol_table), - tmp_symbol_prefix("goto_convertt") + message_handlert &_message_handler) + : messaget(_message_handler), + symbol_table(_symbol_table), + ns(_symbol_table), + tmp_symbol_prefix("goto_convertt") { } @@ -141,17 +141,13 @@ class goto_convertt:public messaget side_effect_exprt &expr, goto_programt &dest, bool result_is_used); - void remove_cpp_delete( - side_effect_exprt &expr, - goto_programt &dest); + void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest); void remove_malloc( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_temporary_object( - side_effect_exprt &expr, - goto_programt &dest); + void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); void remove_statement_expression( side_effect_exprt &expr, goto_programt &dest, @@ -182,9 +178,7 @@ class goto_convertt:public messaget const side_effect_exprt &rhs, goto_programt &dest); - static void replace_new_object( - const exprt &object, - exprt &dest); + static void replace_new_object(const exprt &object, exprt &dest); void cpp_new_initializer( const exprt &lhs, @@ -376,14 +370,12 @@ class goto_convertt:public messaget void finish_computed_gotos(goto_programt &dest); void optimize_guarded_gotos(goto_programt &dest); - typedef std::map> + typedef std::map> labelst; - typedef std::list> - gotost; + typedef std::list> gotost; typedef std::list computed_gotost; typedef exprt::operandst caset; - typedef std::list > casest; + typedef std::list> casest; typedef std::map< goto_programt::targett, casest::iterator, @@ -395,8 +387,8 @@ class goto_convertt:public messaget goto_programt *prefix = nullptr; goto_programt *suffix = nullptr; - bool return_set, has_return_value, break_set, continue_set, - default_set, throw_set, leave_set; + bool return_set, has_return_value, break_set, continue_set, default_set, + throw_set, leave_set; labelst labels; gotost gotos; @@ -410,60 +402,60 @@ class goto_convertt:public messaget default_target, throw_target, leave_target; node_indext break_stack_node, continue_stack_node, throw_stack_node, - leave_stack_node; - - targetst(): - return_set(false), - has_return_value(false), - break_set(false), - continue_set(false), - default_set(false), - throw_set(false), - leave_set(false), - break_stack_node(), - continue_stack_node(), - throw_stack_node(), - leave_stack_node() + leave_stack_node; + + targetst() + : return_set(false), + has_return_value(false), + break_set(false), + continue_set(false), + default_set(false), + throw_set(false), + leave_set(false), + break_stack_node(), + continue_stack_node(), + throw_stack_node(), + leave_stack_node() { } void set_break(goto_programt::targett _break_target) { - break_set=true; - break_target=_break_target; + break_set = true; + break_target = _break_target; break_stack_node = scope_stack.get_current_node(); } void set_continue(goto_programt::targett _continue_target) { - continue_set=true; - continue_target=_continue_target; + continue_set = true; + continue_target = _continue_target; continue_stack_node = scope_stack.get_current_node(); } void set_default(goto_programt::targett _default_target) { - default_set=true; - default_target=_default_target; + default_set = true; + default_target = _default_target; } void set_return(goto_programt::targett _return_target) { - return_set=true; - return_target=_return_target; + return_set = true; + return_target = _return_target; } void set_throw(goto_programt::targett _throw_target) { - throw_set=true; - throw_target=_throw_target; + throw_set = true; + throw_target = _throw_target; throw_stack_node = scope_stack.get_current_node(); } void set_leave(goto_programt::targett _leave_target) { - leave_set=true; - leave_target=_leave_target; + leave_set = true; + leave_target = _leave_target; leave_stack_node = scope_stack.get_current_node(); } } targets; @@ -474,18 +466,18 @@ class goto_convertt:public messaget explicit break_continue_targetst(const targetst &targets) { - break_set=targets.break_set; - continue_set=targets.continue_set; - break_target=targets.break_target; - continue_target=targets.continue_target; + break_set = targets.break_set; + continue_set = targets.continue_set; + break_target = targets.break_target; + continue_target = targets.continue_target; } void restore(targetst &targets) { - targets.break_set=break_set; - targets.continue_set=continue_set; - targets.break_target=break_target; - targets.continue_target=continue_target; + targets.break_set = break_set; + targets.continue_set = continue_set; + targets.break_target = break_target; + targets.continue_target = continue_target; } goto_programt::targett break_target; @@ -499,23 +491,23 @@ class goto_convertt:public messaget explicit break_switch_targetst(const targetst &targets) { - break_set=targets.break_set; - default_set=targets.default_set; - break_target=targets.break_target; - default_target=targets.default_target; + break_set = targets.break_set; + default_set = targets.default_set; + break_target = targets.break_target; + default_target = targets.default_target; break_stack_node = targets.scope_stack.get_current_node(); - cases=targets.cases; - cases_map=targets.cases_map; + cases = targets.cases; + cases_map = targets.cases_map; } void restore(targetst &targets) { - targets.break_set=break_set; - targets.default_set=default_set; - targets.break_target=break_target; - targets.default_target=default_target; - targets.cases=cases; - targets.cases_map=cases_map; + targets.break_set = break_set; + targets.default_set = default_set; + targets.break_target = break_target; + targets.default_target = default_target; + targets.cases = cases; + targets.cases_map = cases_map; } goto_programt::targett break_target; @@ -533,15 +525,15 @@ class goto_convertt:public messaget explicit throw_targett(const targetst &targets) { - throw_set=targets.throw_set; - throw_target=targets.throw_target; + throw_set = targets.throw_set; + throw_target = targets.throw_target; throw_stack_node = targets.scope_stack.get_current_node(); } void restore(targetst &targets) { - targets.throw_set=throw_set; - targets.throw_target=throw_target; + targets.throw_set = throw_set; + targets.throw_target = throw_target; } goto_programt::targett throw_target; @@ -555,15 +547,15 @@ class goto_convertt:public messaget explicit leave_targett(const targetst &targets) { - leave_set=targets.leave_set; - leave_target=targets.leave_target; + leave_set = targets.leave_set; + leave_target = targets.leave_target; leave_stack_node = targets.scope_stack.get_current_node(); } void restore(targetst &targets) { - targets.leave_set=leave_set; - targets.leave_target=leave_target; + targets.leave_set = leave_set; + targets.leave_target = leave_target; } goto_programt::targett leave_target; @@ -571,9 +563,7 @@ class goto_convertt:public messaget node_indext leave_stack_node; }; - exprt case_guard( - const exprt &value, - const caset &case_op); + exprt case_guard(const exprt &value, const caset &case_op); // if(cond) { true_case } else { false_case } void generate_ifthenelse( diff --git a/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp b/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp index cc42054c27d..f7a87a0554c 100644 --- a/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp @@ -101,7 +101,7 @@ void goto_convertt::convert_try_catch( // the CATCH-push instruction is annotated with a list of IDs, // one per target - code_push_catcht::exception_listt &exception_list= + code_push_catcht::exception_listt &exception_list = push_catch_code.exception_list(); // add a SKIP target for the end of everything @@ -119,9 +119,9 @@ void goto_convertt::convert_try_catch( // add a goto to the end of the 'try' block dest.add(goto_programt::make_goto(end_target)); - for(std::size_t i=1; icomplete_goto(y); @@ -151,7 +151,7 @@ void goto_convertt::do_function_call_other( { // don't know what to do with it code_function_callt function_call(lhs, function, arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); dest.add(goto_programt::make_function_call( function_call, function.source_location())); } diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.cpp b/src/ansi-c/goto-conversion/goto_convert_functions.cpp index c12dd711bf7..07a3c3713e1 100644 --- a/src/ansi-c/goto-conversion/goto_convert_functions.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_functions.cpp @@ -13,10 +13,10 @@ Date: June 2003 #include #include -#include - #include +#include + goto_convert_functionst::goto_convert_functionst( symbol_table_baset &_symbol_table, message_handlert &_message_handler) diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.h b/src/ansi-c/goto-conversion/goto_convert_functions.h index b19d9008fa5..70d1f856f66 100644 --- a/src/ansi-c/goto-conversion/goto_convert_functions.h +++ b/src/ansi-c/goto-conversion/goto_convert_functions.h @@ -27,9 +27,7 @@ void goto_convert( message_handlert &); // convert it all! -void goto_convert( - goto_modelt &, - message_handlert &); +void goto_convert(goto_modelt &, message_handlert &); // just convert a specific function void goto_convert( @@ -38,7 +36,7 @@ void goto_convert( goto_functionst &functions, message_handlert &); -class goto_convert_functionst:public goto_convertt +class goto_convert_functionst : public goto_convertt { public: void goto_convert(goto_functionst &functions); diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index 6c76fcbb271..b5720722e68 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -29,11 +29,11 @@ void goto_convertt::remove_assignment( bool address_taken, const irep_idt &mode) { - const irep_idt statement=expr.get_statement(); + const irep_idt statement = expr.get_statement(); std::optional replacement_expr_opt; - if(statement==ID_assign) + if(statement == ID_assign) { auto &old_assignment = to_side_effect_expr_assign(expr); exprt new_lhs = skip_typecast(old_assignment.lhs()); @@ -56,17 +56,13 @@ void goto_convertt::remove_assignment( convert_assign(new_assignment, dest, mode); } - else if(statement==ID_assign_plus || - statement==ID_assign_minus || - statement==ID_assign_mult || - statement==ID_assign_div || - statement==ID_assign_mod || - statement==ID_assign_shl || - statement==ID_assign_ashr || - statement==ID_assign_lshr || - statement==ID_assign_bitand || - statement==ID_assign_bitxor || - statement==ID_assign_bitor) + else if( + statement == ID_assign_plus || statement == ID_assign_minus || + statement == ID_assign_mult || statement == ID_assign_div || + statement == ID_assign_mod || statement == ID_assign_shl || + statement == ID_assign_ashr || statement == ID_assign_lshr || + statement == ID_assign_bitand || statement == ID_assign_bitxor || + statement == ID_assign_bitor) { INVARIANT_WITH_DIAGNOSTICS( expr.operands().size() == 2, @@ -75,28 +71,28 @@ void goto_convertt::remove_assignment( irep_idt new_id; - if(statement==ID_assign_plus) - new_id=ID_plus; - else if(statement==ID_assign_minus) - new_id=ID_minus; - else if(statement==ID_assign_mult) - new_id=ID_mult; - else if(statement==ID_assign_div) - new_id=ID_div; - else if(statement==ID_assign_mod) - new_id=ID_mod; - else if(statement==ID_assign_shl) - new_id=ID_shl; - else if(statement==ID_assign_ashr) - new_id=ID_ashr; - else if(statement==ID_assign_lshr) - new_id=ID_lshr; - else if(statement==ID_assign_bitand) - new_id=ID_bitand; - else if(statement==ID_assign_bitxor) - new_id=ID_bitxor; - else if(statement==ID_assign_bitor) - new_id=ID_bitor; + if(statement == ID_assign_plus) + new_id = ID_plus; + else if(statement == ID_assign_minus) + new_id = ID_minus; + else if(statement == ID_assign_mult) + new_id = ID_mult; + else if(statement == ID_assign_div) + new_id = ID_div; + else if(statement == ID_assign_mod) + new_id = ID_mod; + else if(statement == ID_assign_shl) + new_id = ID_shl; + else if(statement == ID_assign_ashr) + new_id = ID_ashr; + else if(statement == ID_assign_lshr) + new_id = ID_lshr; + else if(statement == ID_assign_bitand) + new_id = ID_bitand; + else if(statement == ID_assign_bitxor) + new_id = ID_bitxor; + else if(statement == ID_assign_bitor) + new_id = ID_bitor; else { UNREACHABLE; @@ -125,7 +121,7 @@ void goto_convertt::remove_assignment( rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type()); rhs.add_source_location() = expr.source_location(); code_assignt assignment(new_lhs, rhs); - assignment.add_source_location()=expr.source_location(); + assignment.add_source_location() = expr.source_location(); convert(assignment, dest, mode); } @@ -177,7 +173,7 @@ void goto_convertt::remove_pre( "preincrement/predecrement must have one operand", expr.find_source_location()); - const irep_idt statement=expr.get_statement(); + const irep_idt statement = expr.get_statement(); DATA_INVARIANT( statement == ID_preincrement || statement == ID_predecrement, @@ -235,7 +231,7 @@ void goto_convertt::remove_pre( make_temp_symbol(rhs, "pre", dest, mode); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=expr.find_source_location(); + assignment.add_source_location() = expr.find_source_location(); convert(assignment, dest, mode); @@ -272,7 +268,7 @@ void goto_convertt::remove_post( "postincrement/postdecrement must have one operand", expr.find_source_location()); - const irep_idt statement=expr.get_statement(); + const irep_idt statement = expr.get_statement(); DATA_INVARIANT( statement == ID_postincrement || statement == ID_postdecrement, @@ -314,7 +310,7 @@ void goto_convertt::remove_post( rhs.add_source_location() = expr.source_location(); code_assignt assignment(op, rhs); - assignment.add_source_location()=expr.find_source_location(); + assignment.add_source_location() = expr.find_source_location(); convert(assignment, tmp2, mode); @@ -349,7 +345,7 @@ void goto_convertt::remove_function_call( if(!result_is_used) { code_function_callt call(expr.function(), expr.arguments()); - call.add_source_location()=expr.source_location(); + call.add_source_location() = expr.source_location(); convert_function_call(call, dest, mode); expr.make_nil(); return; @@ -365,8 +361,8 @@ void goto_convertt::remove_function_call( to_symbol_expr(expr.function()).get_identifier(); const symbolt &symbol = ns.lookup(identifier); - new_base_name+='_'; - new_base_name+=id2string(symbol.base_name); + new_base_name += '_'; + new_base_name += id2string(symbol.base_name); new_symbol_mode = symbol.mode; } @@ -380,7 +376,7 @@ void goto_convertt::remove_function_call( { code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=new_symbol.location; + decl.add_source_location() = new_symbol.location; convert_frontend_decl(decl, dest, mode); } @@ -388,19 +384,17 @@ void goto_convertt::remove_function_call( goto_programt tmp_program2; code_function_callt call( new_symbol.symbol_expr(), expr.function(), expr.arguments()); - call.add_source_location()=new_symbol.location; + call.add_source_location() = new_symbol.location; convert_function_call(call, dest, mode); } - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); } -void goto_convertt::replace_new_object( - const exprt &object, - exprt &dest) +void goto_convertt::replace_new_object(const exprt &object, exprt &dest) { - if(dest.id()=="new_object") - dest=object; + if(dest.id() == "new_object") + dest = object; else Forall_operands(it, dest) replace_new_object(object, *it); @@ -420,13 +414,13 @@ void goto_convertt::remove_cpp_new( symbol_table); code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=new_symbol.location; + decl.add_source_location() = new_symbol.location; convert_frontend_decl(decl, dest, ID_cpp); const code_assignt call(new_symbol.symbol_expr(), expr); if(result_is_used) - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); else expr.make_nil(); @@ -440,7 +434,7 @@ void goto_convertt::remove_cpp_delete( DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand"); codet tmp(expr.get_statement()); - tmp.add_source_location()=expr.source_location(); + tmp.add_source_location() = expr.source_location(); tmp.copy_to_operands(to_unary_expr(expr).op()); tmp.set(ID_destructor, expr.find(ID_destructor)); @@ -466,13 +460,13 @@ void goto_convertt::remove_malloc( symbol_table); code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=new_symbol.location; + decl.add_source_location() = new_symbol.location; convert_frontend_decl(decl, dest, mode); code_assignt call(new_symbol.symbol_expr(), expr); - call.add_source_location()=expr.source_location(); + call.add_source_location() = expr.source_location(); - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); convert(call, dest, mode); } @@ -492,10 +486,10 @@ void goto_convertt::remove_temporary_object( "temporary_object takes zero or one operands", expr.find_source_location()); - symbolt &new_symbol = new_tmp_symbol( - expr.type(), "obj", dest, expr.find_source_location(), mode); + symbolt &new_symbol = + new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location(), mode); - if(expr.operands().size()==1) + if(expr.operands().size() == 1) { const code_assignt assignment( new_symbol.symbol_expr(), to_unary_expr(expr).op()); @@ -509,13 +503,13 @@ void goto_convertt::remove_temporary_object( expr.operands().empty(), "temporary_object takes zero operands", expr.find_source_location()); - exprt initializer=static_cast(expr.find(ID_initializer)); + exprt initializer = static_cast(expr.find(ID_initializer)); replace_new_object(new_symbol.symbol_expr(), initializer); convert(to_code(initializer), dest, mode); } - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); } void goto_convertt::remove_statement_expression( @@ -549,28 +543,28 @@ void goto_convertt::remove_statement_expression( expr.find_source_location()); // get last statement from block, following labels - codet &last=to_code_block(code).find_last_statement(); + codet &last = to_code_block(code).find_last_statement(); - source_locationt source_location=last.find_source_location(); + source_locationt source_location = last.find_source_location(); symbolt &new_symbol = new_tmp_symbol( expr.type(), "statement_expression", dest, source_location, mode); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); - tmp_symbol_expr.add_source_location()=source_location; + tmp_symbol_expr.add_source_location() = source_location; - if(last.get(ID_statement)==ID_expression) + if(last.get(ID_statement) == ID_expression) { // we turn this into an assignment - exprt e=to_code_expression(last).expression(); - last=code_assignt(tmp_symbol_expr, e); - last.add_source_location()=source_location; + exprt e = to_code_expression(last).expression(); + last = code_assignt(tmp_symbol_expr, e); + last.add_source_location() = source_location; } - else if(last.get(ID_statement)==ID_assign) + else if(last.get(ID_statement) == ID_assign) { - exprt e=to_code_assign(last).lhs(); + exprt e = to_code_assign(last).lhs(); code_assignt assignment(tmp_symbol_expr, e); - assignment.add_source_location()=source_location; + assignment.add_source_location() = source_location; code.operands().push_back(assignment); } else @@ -584,7 +578,7 @@ void goto_convertt::remove_statement_expression( dest.destructive_append(tmp); } - static_cast(expr)=tmp_symbol_expr; + static_cast(expr) = tmp_symbol_expr; } void goto_convertt::remove_overflow( @@ -621,12 +615,10 @@ void goto_convertt::remove_overflow( else { const typet &arith_type = to_pointer_type(result.type()).base_type(); - irep_idt arithmetic_operation = - statement == ID_overflow_plus - ? ID_plus - : statement == ID_overflow_minus - ? ID_minus - : statement == ID_overflow_mult ? ID_mult : ID_nil; + irep_idt arithmetic_operation = statement == ID_overflow_plus ? ID_plus + : statement == ID_overflow_minus ? ID_minus + : statement == ID_overflow_mult ? ID_mult + : ID_nil; CHECK_RETURN(arithmetic_operation != ID_nil); exprt overflow_with_result = overflow_result_exprt{ typecast_exprt::conditional_cast(lhs, arith_type), @@ -666,51 +658,42 @@ void goto_convertt::remove_side_effect( bool result_is_used, bool address_taken) { - const irep_idt &statement=expr.get_statement(); + const irep_idt &statement = expr.get_statement(); - if(statement==ID_function_call) + if(statement == ID_function_call) remove_function_call( to_side_effect_expr_function_call(expr), dest, mode, result_is_used); - else if(statement==ID_assign || - statement==ID_assign_plus || - statement==ID_assign_minus || - statement==ID_assign_mult || - statement==ID_assign_div || - statement==ID_assign_bitor || - statement==ID_assign_bitxor || - statement==ID_assign_bitand || - statement==ID_assign_lshr || - statement==ID_assign_ashr || - statement==ID_assign_shl || - statement==ID_assign_mod) + else if( + statement == ID_assign || statement == ID_assign_plus || + statement == ID_assign_minus || statement == ID_assign_mult || + statement == ID_assign_div || statement == ID_assign_bitor || + statement == ID_assign_bitxor || statement == ID_assign_bitand || + statement == ID_assign_lshr || statement == ID_assign_ashr || + statement == ID_assign_shl || statement == ID_assign_mod) remove_assignment(expr, dest, result_is_used, address_taken, mode); - else if(statement==ID_postincrement || - statement==ID_postdecrement) + else if(statement == ID_postincrement || statement == ID_postdecrement) remove_post(expr, dest, mode, result_is_used); - else if(statement==ID_preincrement || - statement==ID_predecrement) + else if(statement == ID_preincrement || statement == ID_predecrement) remove_pre(expr, dest, result_is_used, address_taken, mode); - else if(statement==ID_cpp_new || - statement==ID_cpp_new_array) + else if(statement == ID_cpp_new || statement == ID_cpp_new_array) remove_cpp_new(expr, dest, result_is_used); - else if(statement==ID_cpp_delete || - statement==ID_cpp_delete_array) + else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array) remove_cpp_delete(expr, dest); - else if(statement==ID_allocate) + else if(statement == ID_allocate) remove_malloc(expr, dest, mode, result_is_used); - else if(statement==ID_temporary_object) + else if(statement == ID_temporary_object) remove_temporary_object(expr, dest); - else if(statement==ID_statement_expression) + else if(statement == ID_statement_expression) remove_statement_expression(expr, dest, mode, result_is_used); - else if(statement==ID_nondet) + else if(statement == ID_nondet) { // these are fine } - else if(statement==ID_skip) + else if(statement == ID_skip) { expr.make_nil(); } - else if(statement==ID_throw) + else if(statement == ID_throw) { codet code = code_expressiont(side_effect_expr_throwt( expr.find(ID_exception_list), expr.type(), expr.source_location())); diff --git a/src/ansi-c/goto-conversion/link_to_library.cpp b/src/ansi-c/goto-conversion/link_to_library.cpp index b66fe9fec93..cc814e1965a 100644 --- a/src/ansi-c/goto-conversion/link_to_library.cpp +++ b/src/ansi-c/goto-conversion/link_to_library.cpp @@ -11,12 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "link_to_library.h" -#include - #include #include #include +#include + #include "goto_convert_functions.h" /// Try to add \p missing_function from \p library to \p goto_model. diff --git a/src/ansi-c/goto-conversion/link_to_library.h b/src/ansi-c/goto-conversion/link_to_library.h index 8ddf2d3b0b8..4420fa4b725 100644 --- a/src/ansi-c/goto-conversion/link_to_library.h +++ b/src/ansi-c/goto-conversion/link_to_library.h @@ -12,11 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H #define CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H +#include + #include #include -#include - class goto_modelt; class message_handlert; class symbol_tablet; diff --git a/src/ansi-c/goto-conversion/string_instrumentation.cpp b/src/ansi-c/goto-conversion/string_instrumentation.cpp index 84138e98d4c..873dee0006e 100644 --- a/src/ansi-c/goto-conversion/string_instrumentation.cpp +++ b/src/ansi-c/goto-conversion/string_instrumentation.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "string_instrumentation.h" -#include - #include #include #include @@ -25,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "format_strings.h" +#include + exprt is_zero_string(const exprt &what, bool write) { unary_exprt result{"is_zero_string", what, c_bool_type()}; @@ -33,9 +33,7 @@ exprt is_zero_string(const exprt &what, bool write) return notequal_exprt{result, from_integer(0, c_bool_type())}; } -exprt zero_string_length( - const exprt &what, - bool write) +exprt zero_string_length(const exprt &what, bool write) { exprt result("zero_string_length", size_type()); result.copy_to_operands(what); @@ -67,7 +65,7 @@ class string_instrumentationt void make_type(exprt &dest, const typet &type) { - if(ns.follow(dest.type())!=ns.follow(type)) + if(ns.follow(dest.type()) != ns.follow(type)) dest = typecast_exprt(dest, type); } @@ -177,16 +175,13 @@ void string_instrumentation( void string_instrumentation(goto_modelt &goto_model) { - string_instrumentation( - goto_model.symbol_table, - goto_model.goto_functions); + string_instrumentation(goto_model.symbol_table, goto_model.goto_functions); } void string_instrumentationt::operator()(goto_functionst &dest) { - for(goto_functionst::function_mapt::iterator - it=dest.function_map.begin(); - it!=dest.function_map.end(); + for(goto_functionst::function_mapt::iterator it = dest.function_map.begin(); + it != dest.function_map.end(); it++) { (*this)(it->second.body); @@ -215,41 +210,40 @@ void string_instrumentationt::do_function_call( const exprt &function = as_const(*target).call_function(); const auto &arguments = as_const(*target).call_arguments(); - if(function.id()==ID_symbol) + if(function.id() == ID_symbol) { - const irep_idt &identifier= - to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).get_identifier(); - if(identifier=="strcoll") + if(identifier == "strcoll") { } - else if(identifier=="strncmp") + else if(identifier == "strncmp") do_strncmp(dest, target, lhs, arguments); - else if(identifier=="strxfrm") + else if(identifier == "strxfrm") { } - else if(identifier=="strchr") + else if(identifier == "strchr") do_strchr(dest, target, lhs, arguments); - else if(identifier=="strcspn") + else if(identifier == "strcspn") { } - else if(identifier=="strpbrk") + else if(identifier == "strpbrk") { } - else if(identifier=="strrchr") + else if(identifier == "strrchr") do_strrchr(dest, target, lhs, arguments); - else if(identifier=="strspn") + else if(identifier == "strspn") { } - else if(identifier=="strerror") + else if(identifier == "strerror") do_strerror(dest, target, lhs, arguments); - else if(identifier=="strstr") + else if(identifier == "strstr") do_strstr(dest, target, lhs, arguments); - else if(identifier=="strtok") + else if(identifier == "strtok") do_strtok(dest, target, lhs, arguments); - else if(identifier=="sprintf") + else if(identifier == "sprintf") do_sprintf(dest, target, lhs, arguments); - else if(identifier=="snprintf") + else if(identifier == "snprintf") do_snprintf(dest, target, lhs, arguments); else if(identifier == "fscanf" || identifier == "__isoc99_fscanf") do_fscanf(dest, target, lhs, arguments); @@ -264,7 +258,7 @@ void string_instrumentationt::do_sprintf( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()<2) + if(arguments.size() < 2) { throw invalid_source_file_exceptiont( "sprintf expected to have two or more arguments", @@ -300,7 +294,7 @@ void string_instrumentationt::do_snprintf( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()<3) + if(arguments.size() < 3) { throw invalid_source_file_exceptiont( "snprintf expected to have three or more arguments", @@ -337,7 +331,7 @@ void string_instrumentationt::do_fscanf( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()<2) + if(arguments.size() < 2) { throw invalid_source_file_exceptiont( "fscanf expected to have two or more arguments", @@ -368,7 +362,7 @@ void string_instrumentationt::do_format_string_read( std::size_t argument_start_inx, const std::string &function_name) { - const exprt &format_arg=arguments[format_string_inx]; + const exprt &format_arg = arguments[format_string_inx]; if( format_arg.id() == ID_address_of && @@ -381,22 +375,22 @@ void string_instrumentationt::do_format_string_read( to_index_expr(to_address_of_expr(format_arg).object()).array()) .value())); - std::size_t args=0; + std::size_t args = 0; for(const auto &token : token_list) { - if(token.type==format_tokent::token_typet::STRING) + if(token.type == format_tokent::token_typet::STRING) { - const exprt &arg=arguments[argument_start_inx+args]; + const exprt &arg = arguments[argument_start_inx + args]; - if(arg.id()!=ID_string_constant) // we don't need to check constants + if(arg.id() != ID_string_constant) // we don't need to check constants { exprt temp(arg); if(arg.type().id() != ID_pointer) { index_exprt index(temp, from_integer(0, c_index_type())); - temp=address_of_exprt(index); + temp = address_of_exprt(index); } source_locationt annotated_location = target->source_location(); @@ -409,14 +403,16 @@ void string_instrumentationt::do_format_string_read( } } - if(token.type!=format_tokent::token_typet::TEXT && - token.type!=format_tokent::token_typet::UNKNOWN) args++; + if( + token.type != format_tokent::token_typet::TEXT && + token.type != format_tokent::token_typet::UNKNOWN) + args++; - if(find( - token.flags.begin(), - token.flags.end(), - format_tokent::flag_typet::ASTERISK)!= - token.flags.end()) + if( + find( + token.flags.begin(), + token.flags.end(), + format_tokent::flag_typet::ASTERISK) != token.flags.end()) args++; // just eat the additional argument } } @@ -429,9 +425,9 @@ void string_instrumentationt::do_format_string_read( dest.add(goto_programt::make_assertion( is_zero_string(arguments[1]), annotated_location)); - for(std::size_t i=2; isource_location(); @@ -462,7 +458,7 @@ void string_instrumentationt::do_format_string_write( std::size_t argument_start_inx, const std::string &function_name) { - const exprt &format_arg=arguments[format_string_inx]; + const exprt &format_arg = arguments[format_string_inx]; if( format_arg.id() == ID_address_of && @@ -475,96 +471,94 @@ void string_instrumentationt::do_format_string_write( to_index_expr(to_address_of_expr(format_arg).object()).array()) .value())); - std::size_t args=0; + std::size_t args = 0; for(const auto &token : token_list) { - if(find( - token.flags.begin(), - token.flags.end(), - format_tokent::flag_typet::ASTERISK)!= - token.flags.end()) + if( + find( + token.flags.begin(), + token.flags.end(), + format_tokent::flag_typet::ASTERISK) != token.flags.end()) continue; // asterisk means `ignore this' switch(token.type) { - case format_tokent::token_typet::STRING: + case format_tokent::token_typet::STRING: + { + const exprt &argument = arguments[argument_start_inx + args]; + const typet &arg_type = argument.type(); + + exprt condition; + + if(token.field_width != 0) { - const exprt &argument=arguments[argument_start_inx+args]; - const typet &arg_type = argument.type(); + exprt fwidth = from_integer(token.field_width, unsigned_int_type()); + exprt one = from_integer(1, unsigned_int_type()); + const plus_exprt fw_1(fwidth, one); // +1 for 0-char - exprt condition; + exprt fw_lt_bs; - if(token.field_width!=0) - { - exprt fwidth=from_integer(token.field_width, unsigned_int_type()); - exprt one=from_integer(1, unsigned_int_type()); - const plus_exprt fw_1(fwidth, one); // +1 for 0-char - - exprt fw_lt_bs; - - if(arg_type.id()==ID_pointer) - fw_lt_bs= - binary_relation_exprt(fw_1, ID_le, buffer_size(argument)); - else - { - const index_exprt index( - argument, from_integer(0, unsigned_int_type())); - address_of_exprt aof(index); - fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof)); - } - - condition = fw_lt_bs; - } + if(arg_type.id() == ID_pointer) + fw_lt_bs = + binary_relation_exprt(fw_1, ID_le, buffer_size(argument)); else { - // this is a possible overflow. - condition = false_exprt(); + const index_exprt index( + argument, from_integer(0, unsigned_int_type())); + address_of_exprt aof(index); + fw_lt_bs = binary_relation_exprt(fw_1, ID_le, buffer_size(aof)); } - source_locationt annotated_location = target->source_location(); - annotated_location.set_property_class("string"); - std::string comment("format string buffer overflow in "); - comment += function_name; - annotated_location.set_comment(comment); - dest.add( - goto_programt::make_assertion(condition, annotated_location)); - - // now kill the contents - invalidate_buffer( - dest, target, argument, arg_type, token.field_width); - - args++; - break; + condition = fw_lt_bs; } - case format_tokent::token_typet::TEXT: - case format_tokent::token_typet::UNKNOWN: + else { - // nothing - break; + // this is a possible overflow. + condition = false_exprt(); } - case format_tokent::token_typet::POINTER: - case format_tokent::token_typet::CHAR: - case format_tokent::token_typet::FLOAT: - case format_tokent::token_typet::INT: - { - const exprt &argument=arguments[argument_start_inx+args]; - const dereference_exprt lhs{argument}; - side_effect_expr_nondett rhs(lhs.type(), target->source_location()); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + std::string comment("format string buffer overflow in "); + comment += function_name; + annotated_location.set_comment(comment); + dest.add(goto_programt::make_assertion(condition, annotated_location)); - dest.add(goto_programt::make_assignment( - lhs, rhs, target->source_location())); + // now kill the contents + invalidate_buffer(dest, target, argument, arg_type, token.field_width); - args++; - break; - } + args++; + break; + } + case format_tokent::token_typet::TEXT: + case format_tokent::token_typet::UNKNOWN: + { + // nothing + break; + } + case format_tokent::token_typet::POINTER: + case format_tokent::token_typet::CHAR: + case format_tokent::token_typet::FLOAT: + case format_tokent::token_typet::INT: + { + const exprt &argument = arguments[argument_start_inx + args]; + const dereference_exprt lhs{argument}; + + side_effect_expr_nondett rhs(lhs.type(), target->source_location()); + + dest.add( + goto_programt::make_assignment(lhs, rhs, target->source_location())); + + args++; + break; + } } } } else // non-const format string { - for(std::size_t i=argument_start_inx; isource_location()); @@ -637,7 +631,7 @@ void string_instrumentationt::do_strrchr( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()!=2) + if(arguments.size() != 2) { throw invalid_source_file_exceptiont( "strrchr expected to have two arguments", target->source_location()); @@ -660,7 +654,7 @@ void string_instrumentationt::do_strstr( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()!=2) + if(arguments.size() != 2) { throw invalid_source_file_exceptiont( "strstr expected to have two arguments", target->source_location()); @@ -691,7 +685,7 @@ void string_instrumentationt::do_strtok( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()!=2) + if(arguments.size() != 2) { throw invalid_source_file_exceptiont( "strtok expected to have two arguments", target->source_location()); @@ -728,32 +722,32 @@ void string_instrumentationt::do_strerror( return; } - irep_idt identifier_buf="__strerror_buffer"; - irep_idt identifier_size="__strerror_buffer_size"; + irep_idt identifier_buf = "__strerror_buffer"; + irep_idt identifier_size = "__strerror_buffer_size"; - if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end()) + if(symbol_table.symbols.find(identifier_buf) == symbol_table.symbols.end()) { symbolt new_symbol_size{identifier_size, size_type(), ID_C}; new_symbol_size.base_name = identifier_size; - new_symbol_size.pretty_name=new_symbol_size.base_name; - new_symbol_size.is_state_var=true; - new_symbol_size.is_lvalue=true; - new_symbol_size.is_static_lifetime=true; + new_symbol_size.pretty_name = new_symbol_size.base_name; + new_symbol_size.is_state_var = true; + new_symbol_size.is_lvalue = true; + new_symbol_size.is_static_lifetime = true; array_typet type(char_type(), new_symbol_size.symbol_expr()); symbolt new_symbol_buf{identifier_buf, type, ID_C}; - new_symbol_buf.is_state_var=true; - new_symbol_buf.is_lvalue=true; - new_symbol_buf.is_static_lifetime=true; + new_symbol_buf.is_state_var = true; + new_symbol_buf.is_lvalue = true; + new_symbol_buf.is_static_lifetime = true; new_symbol_buf.base_name = identifier_buf; - new_symbol_buf.pretty_name=new_symbol_buf.base_name; + new_symbol_buf.pretty_name = new_symbol_buf.base_name; symbol_table.insert(std::move(new_symbol_buf)); symbol_table.insert(std::move(new_symbol_size)); } - const symbolt &symbol_size=ns.lookup(identifier_size); - const symbolt &symbol_buf=ns.lookup(identifier_buf); + const symbolt &symbol_size = ns.lookup(identifier_size); + const symbolt &symbol_buf = ns.lookup(identifier_buf); goto_programt tmp; @@ -786,7 +780,7 @@ void string_instrumentationt::do_strerror( // assign address { - exprt rhs=ptr; + exprt rhs = ptr; make_type(rhs, lhs.type()); tmp.add(goto_programt::make_assignment( code_assignt(lhs, rhs), it->source_location())); @@ -803,21 +797,21 @@ void string_instrumentationt::invalidate_buffer( const typet &buf_type, const mp_integer &limit) { - irep_idt cntr_id="string_instrumentation::$counter"; + irep_idt cntr_id = "string_instrumentation::$counter"; - if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end()) + if(symbol_table.symbols.find(cntr_id) == symbol_table.symbols.end()) { symbolt new_symbol{cntr_id, size_type(), ID_C}; - new_symbol.base_name="$counter"; - new_symbol.pretty_name=new_symbol.base_name; - new_symbol.is_state_var=true; - new_symbol.is_lvalue=true; - new_symbol.is_static_lifetime=true; + new_symbol.base_name = "$counter"; + new_symbol.pretty_name = new_symbol.base_name; + new_symbol.is_state_var = true; + new_symbol.is_lvalue = true; + new_symbol.is_static_lifetime = true; symbol_table.insert(std::move(new_symbol)); } - const symbolt &cntr_sym=ns.lookup(cntr_id); + const symbolt &cntr_sym = ns.lookup(cntr_id); // create a loop that runs over the buffer // and invalidates every element @@ -829,20 +823,20 @@ void string_instrumentationt::invalidate_buffer( exprt bufp; - if(buf_type.id()==ID_pointer) - bufp=buffer; + if(buf_type.id() == ID_pointer) + bufp = buffer; else { index_exprt index( buffer, from_integer(0, c_index_type()), to_type_with_subtype(buf_type).subtype()); - bufp=address_of_exprt(index); + bufp = address_of_exprt(index); } exprt condition; - if(limit==0) + if(limit == 0) condition = binary_relation_exprt(cntr_sym.symbol_expr(), ID_ge, buffer_size(bufp)); else diff --git a/src/ansi-c/goto-conversion/string_instrumentation.h b/src/ansi-c/goto-conversion/string_instrumentation.h index 646f803e3c8..fd57d0306d6 100644 --- a/src/ansi-c/goto-conversion/string_instrumentation.h +++ b/src/ansi-c/goto-conversion/string_instrumentation.h @@ -25,7 +25,7 @@ void string_instrumentation(symbol_table_baset &, goto_functionst &); void string_instrumentation(goto_modelt &); exprt is_zero_string(const exprt &what, bool write = false); -exprt zero_string_length(const exprt &what, bool write=false); +exprt zero_string_length(const exprt &what, bool write = false); exprt buffer_size(const exprt &what); #endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H diff --git a/src/ansi-c/printf_formatter.h b/src/ansi-c/printf_formatter.h index ab8dda2d9f5..45968da45ba 100644 --- a/src/ansi-c/printf_formatter.h +++ b/src/ansi-c/printf_formatter.h @@ -19,16 +19,12 @@ Author: Daniel Kroening, kroening@kroening.com class printf_formattert { public: - void operator()( - const std::string &format, - const std::list &_operands); + void operator()(const std::string &format, const std::list &_operands); void print(std::ostream &out); std::string as_string(); - explicit printf_formattert(const namespacet &_ns): - ns(_ns), - format_pos(0) + explicit printf_formattert(const namespacet &_ns) : ns(_ns), format_pos(0) { } @@ -38,9 +34,14 @@ class printf_formattert std::list operands; std::list::const_iterator next_operand; unsigned format_pos; - bool eol() const { return format_pos>=format.size(); } + bool eol() const + { + return format_pos >= format.size(); + } - class eol_exceptiont { }; + class eol_exceptiont + { + }; char next() { diff --git a/unit/ansi-c/allocate_objects.cpp b/unit/ansi-c/allocate_objects.cpp index 8f4a97f6d09..3f33bede78e 100644 --- a/unit/ansi-c/allocate_objects.cpp +++ b/unit/ansi-c/allocate_objects.cpp @@ -6,11 +6,10 @@ Author: Diffblue Ltd \*******************************************************************/ -#include - #include #include +#include #include TEST_CASE(