From e9491965a8005ae8a2b4ec3d6184345b39e28fce Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 3 Feb 2017 12:24:25 +0000 Subject: [PATCH 1/3] Extended the coding standard Now cover how source list of Makefiles should be structured (to aid merging). Also explain the decisions me and Micahel discussed on #454 regarding sharing command flags between programs. --- CODING_STANDARD | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/CODING_STANDARD b/CODING_STANDARD index d6c83eaa746..abfd9a9d072 100644 --- a/CODING_STANDARD +++ b/CODING_STANDARD @@ -92,6 +92,35 @@ Header files: of the header file rather than in line - Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc +Make files +- Each source file should appear on a separate line +- The final source file should still be followed by a trailing slash +- The last line should be a comment to not be deleted, i.e. should look like: +``` +SRC = source_file.cpp \ + source_file2.cpp \ + # Empty last line +``` +- This ensures the Makefiles can be easily merged. + +Program Command Line Options +- Each program contains a program_name_parse_optionst class which should + contain a define PROGRAM_NAME_PARSE_OPTIONS which is a string of all the + parse options in brackets (with a colon after the bracket if it takes a + parameter) +- Each parameter should be one per line to yield easy merging +- If parameters are shared between programs, they should be pulled out into + a common file and then included using a define +- The defines should be OPT_FLAG_NAMES which should go into the OPTIONS define +- The defines should include HELP_FLAG_NAMES which should contain the help + output of the format: + ``` + " --flag explanations\n" \ + " --another flag more explanation\n" \ + <-------30 chars------> +- The defines may include PARSE_OPTIONS_FLAG_NAMES which move the options + from the command line into the options + C++ features: - Do not use namespaces. - Prefer use of 'typedef' insted of 'using'. From 6bd56e205497a399df28d621f7823d2c56e9f5bd Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 24 Feb 2017 21:56:42 +0000 Subject: [PATCH 2/3] Add documentation for cpplint pre-commit hook Closes #565 --- CODING_STANDARD | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CODING_STANDARD b/CODING_STANDARD index abfd9a9d072..d079889bb8d 100644 --- a/CODING_STANDARD +++ b/CODING_STANDARD @@ -172,3 +172,13 @@ Output: - Use '\n' instead of std::endl You are allowed to break rules if you have a good reason to do so. + +Pre-commit hook to run cpplint locally +-------------------------------------- +To install the hook +cp .githooks/pre-commit .git/hooks/pre-commit +or use a symbolic link. +Then, when running git commit, you should get the linter output +(if any) before being prompted to enter a commit message. +To bypass the check (e.g. if there was a false positive), +add the option --no-verify. From 4031a0aff61aa1627b696f24d13c3b1999f59456 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 4 Apr 2017 13:53:12 +0100 Subject: [PATCH 3/3] Fixing make files to be one file per line The lines are alphabetical and the final line is a comment. This prevents unnecessary merge conflicts caused by either: addition of two files on the same line or by adding a trailing \ to the final line by two different commits. Fixes #657 --- src/analyses/Makefile | 35 +++-- src/ansi-c/Makefile | 54 +++++--- src/assembler/Makefile | 5 +- src/cbmc/Makefile | 21 ++- src/cegis/Makefile | 239 +++++++++++++++++++++++----------- src/clobber/Makefile | 5 +- src/cpp/Makefile | 66 +++++++--- src/goto-analyzer/Makefile | 10 +- src/goto-cc/Makefile | 24 +++- src/goto-diff/Makefile | 11 +- src/goto-instrument/Makefile | 86 ++++++++---- src/goto-programs/Makefile | 82 ++++++++---- src/goto-symex/Makefile | 44 +++++-- src/java_bytecode/Makefile | 32 +++-- src/jsil/Makefile | 16 ++- src/json/Makefile | 6 +- src/langapi/Makefile | 7 +- src/linking/Makefile | 7 +- src/memory-models/Makefile | 9 +- src/miniz/Makefile | 4 +- src/musketeer/Makefile | 17 ++- src/path-symex/Makefile | 12 +- src/pointer-analysis/Makefile | 29 +++-- src/solvers/Makefile | 145 ++++++++++++++------- src/symex/Makefile | 7 +- src/util/Makefile | 116 +++++++++++++---- src/xmllang/Makefile | 8 +- unit/Makefile | 17 ++- 28 files changed, 798 insertions(+), 316 deletions(-) diff --git a/src/analyses/Makefile b/src/analyses/Makefile index e05d5be0c42..690b119e83c 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -1,13 +1,30 @@ -SRC = natural_loops.cpp is_threaded.cpp dirty.cpp interval_analysis.cpp \ - invariant_set.cpp invariant_set_domain.cpp invariant_propagation.cpp \ - static_analysis.cpp uninitialized_domain.cpp local_may_alias.cpp \ - locals.cpp goto_check.cpp call_graph.cpp interval_domain.cpp \ - goto_rw.cpp reaching_definitions.cpp ai.cpp local_cfg.cpp \ - local_bitvector_analysis.cpp dependence_graph.cpp \ - constant_propagator.cpp replace_symbol_ext.cpp \ - flow_insensitive_analysis.cpp \ - custom_bitvector_analysis.cpp escape_analysis.cpp global_may_alias.cpp \ +SRC = ai.cpp \ + call_graph.cpp \ + constant_propagator.cpp \ + custom_bitvector_analysis.cpp \ + dependence_graph.cpp \ + dirty.cpp \ does_remove_const.cpp \ + escape_analysis.cpp \ + flow_insensitive_analysis.cpp \ + global_may_alias.cpp \ + goto_check.cpp \ + goto_rw.cpp \ + interval_analysis.cpp \ + interval_domain.cpp \ + invariant_propagation.cpp \ + invariant_set.cpp \ + invariant_set_domain.cpp \ + is_threaded.cpp \ + local_bitvector_analysis.cpp \ + local_cfg.cpp \ + local_may_alias.cpp \ + locals.cpp \ + natural_loops.cpp \ + reaching_definitions.cpp \ + replace_symbol_ext.cpp \ + static_analysis.cpp \ + uninitialized_domain.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index bed65d0d7b6..ac509c591dd 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -1,20 +1,44 @@ -SRC = c_typecast.cpp ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_parser.cpp \ - expr2c.cpp ansi_c_language.cpp c_sizeof.cpp ansi_c_scope.cpp \ - c_types.cpp ansi_c_typecheck.cpp \ - c_preprocess.cpp c_storage_spec.cpp \ - c_typecheck_base.cpp c_typecheck_initializer.cpp \ - c_typecheck_typecast.cpp c_typecheck_code.cpp \ - c_typecheck_expr.cpp c_typecheck_type.cpp string_constant.cpp \ - c_qualifiers.cpp c_typecheck_argc_argv.cpp ansi_c_parse_tree.cpp \ - preprocessor_line.cpp ansi_c_convert_type.cpp \ - type2name.cpp cprover_library.cpp anonymous_member.cpp \ - printf_formatter.cpp ansi_c_internal_additions.cpp padding.cpp \ - ansi_c_declaration.cpp designator.cpp ansi_c_entry_point.cpp \ - literals/parse_float.cpp literals/unescape_string.cpp \ - literals/convert_float_literal.cpp \ +SRC = anonymous_member.cpp \ + ansi_c_convert_type.cpp \ + ansi_c_declaration.cpp \ + ansi_c_entry_point.cpp \ + ansi_c_internal_additions.cpp \ + ansi_c_language.cpp \ + ansi_c_lex.yy.cpp \ + ansi_c_parse_tree.cpp \ + ansi_c_parser.cpp \ + ansi_c_scope.cpp \ + ansi_c_typecheck.cpp \ + ansi_c_y.tab.cpp \ + c_misc.cpp \ + c_preprocess.cpp \ + c_qualifiers.cpp \ + c_sizeof.cpp \ + c_storage_spec.cpp \ + c_typecast.cpp \ + c_typecheck_argc_argv.cpp \ + c_typecheck_base.cpp \ + c_typecheck_code.cpp \ + c_typecheck_expr.cpp \ + c_typecheck_initializer.cpp \ + c_typecheck_type.cpp \ + c_typecheck_typecast.cpp \ + c_types.cpp \ + cprover_library.cpp \ + designator.cpp \ + expr2c.cpp \ literals/convert_character_literal.cpp \ + literals/convert_float_literal.cpp \ literals/convert_integer_literal.cpp \ - literals/convert_string_literal.cpp c_misc.cpp + literals/convert_string_literal.cpp \ + literals/parse_float.cpp \ + literals/unescape_string.cpp \ + padding.cpp \ + preprocessor_line.cpp \ + printf_formatter.cpp \ + string_constant.cpp \ + type2name.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/assembler/Makefile b/src/assembler/Makefile index 90b2562f1d4..ab8ac02a9bd 100644 --- a/src/assembler/Makefile +++ b/src/assembler/Makefile @@ -1,5 +1,6 @@ -SRC = assembler_lex.yy.cpp assembler_parser.cpp - +SRC = assembler_lex.yy.cpp \ + assembler_parser.cpp \ + # Empty last line INCLUDES= -I .. include ../config.inc diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 8132097565c..37f8b65eb00 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -1,8 +1,19 @@ -SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \ - cbmc_languages.cpp counterexample_beautification.cpp \ - bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \ - xml_interface.cpp bmc_cover.cpp all_properties.cpp \ - fault_localization.cpp symex_coverage.cpp +SRC = all_properties.cpp \ + bmc.cpp \ + bmc_cover.cpp \ + bv_cbmc.cpp \ + cbmc_dimacs.cpp \ + cbmc_languages.cpp \ + cbmc_main.cpp \ + cbmc_parse_options.cpp \ + cbmc_solvers.cpp \ + counterexample_beautification.cpp \ + fault_localization.cpp \ + show_vcc.cpp \ + symex_bmc.cpp \ + symex_coverage.cpp \ + xml_interface.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/cegis/Makefile b/src/cegis/Makefile index f1a38ce4915..00e4f9d20a1 100644 --- a/src/cegis/Makefile +++ b/src/cegis/Makefile @@ -1,88 +1,175 @@ -SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger/options/danger_program.cpp \ - danger/genetic/dynamic_danger_test_runner.cpp \ - danger/options/danger_program_printer.cpp danger/constraint/danger_constraint_factory.cpp \ - danger/preprocess/danger_preprocessing.cpp danger/preprocess/store_nondet_choices.cpp \ - danger/preprocess/add_ranking_and_skolem_variables.cpp danger/symex/learn/add_variable_refs.cpp \ - danger/symex/learn/add_programs_to_learn.cpp danger/symex/learn/solution_factory.cpp \ - danger/symex/learn/read_x0.cpp danger/symex/learn/add_x0_placeholders.cpp danger/symex/learn/danger_learn_config.cpp \ - danger/symex/learn/encoded_danger_learn_config.cpp danger/symex/verify/insert_candidate.cpp danger/symex/verify/restrict_counterexamples.cpp \ - danger/symex/verify/danger_verify_config.cpp danger/symex/verify/parallel_danger_verifier.cpp \ - danger/symex/verify/parallel_danger_verify_task.cpp danger/symex/fitness/danger_fitness_config.cpp \ - safety/options/safety_program.cpp safety/options/safety_program_printer.cpp safety/preprocessing/safety_preprocessing.cpp \ - safety/genetic/dynamic_safety_test_runner.cpp \ - safety/meta/meta_variable_names.cpp safety/constraint/safety_constraint_factory.cpp \ - safety/symex/learn/safety_learn_config.cpp safety/symex/learn/solution_factory.cpp \ - safety/symex/learn/add_variable_refs.cpp safety/symex/verify/safety_verify_config.cpp \ - safety/symex/learn/encoded_safety_learn_config.cpp safety/symex/learn/add_counterexamples.cpp \ - safety/symex/verify/insert_candidate.cpp safety/facade/safety_runner.cpp \ - safety/symex/fitness/safety_fitness_config.cpp safety/value/safety_goto_ce.cpp \ - safety/value/individual_to_safety_solution_deserialiser.cpp \ - invariant/options/invariant_program.cpp invariant/options/target_copy_helper.cpp \ - invariant/util/copy_instructions.cpp invariant/util/invariant_program_helper.cpp \ - invariant/util/invariant_constraint_variables.cpp \ - invariant/constant/add_constant.cpp invariant/constant/default_constant_strategy.cpp \ - invariant/constant/literals_constant_strategy.cpp invariant/meta/meta_variable_names.cpp \ - invariant/preprocess/add_invariants_and_temp_variables.cpp invariant/preprocess/remove_loops_and_assertion.cpp \ - invariant/symex/learn/add_counterexamples.cpp invariant/symex/learn/add_invariant_programs_to_learn.cpp \ - invariant/symex/learn/instrument_vars.cpp \ - invariant/symex/learn/replace_operators.cpp invariant/symex/verify/extract_counterexample.cpp \ - invariant/symex/verify/insert_constraint.cpp invariant/symex/verify/insert_program.cpp \ - invariant/fitness/concrete_fitness_source_provider.cpp \ - jsa/facade/jsa_runner.cpp jsa/options/jsa_program.cpp jsa/options/jsa_program_info.cpp \ - jsa/preprocessing/jsa_preprocessing.cpp jsa/preprocessing/remove_loop.cpp \ - jsa/preprocessing/add_constraint_meta_variables.cpp jsa/preprocessing/default_jsa_constant_strategy.cpp \ - jsa/preprocessing/create_temp_variables.cpp jsa/preprocessing/collect_variables.cpp jsa/preprocessing/clone_heap.cpp \ - jsa/preprocessing/add_synthesis_library.cpp \ - jsa/learn/jsa_symex_learn.cpp jsa/learn/insert_counterexample.cpp jsa/learn/insert_predicates_and_queries.cpp \ - jsa/learn/instrument_pred_ops.cpp jsa/learn/execute_jsa_programs.cpp jsa/learn/extract_candidate.cpp \ - jsa/verify/jsa_symex_verify.cpp jsa/verify/extract_counterexample.cpp jsa/verify/renondet_inputs.cpp \ - jsa/verify/insert_solution.cpp \ - jsa/constraint/jsa_constraint_factory.cpp \ - jsa/converters/solution.cpp jsa/converters/translate_to_goto_program.cpp jsa/converters/replace_operators.cpp \ - jsa/converters/counterexample.cpp \ - jsa/instrument/jsa_meta_data.cpp jsa/instrument/temps_helper.cpp \ - jsa/value/jsa_solution.cpp jsa/value/jsa_solution_printer.cpp jsa/value/jsa_types.cpp \ - jsa/value/default_solution.cpp jsa/value/jsa_counterexample_printer.cpp \ - jsa/genetic/jsa_source_provider.cpp jsa/genetic/dynamic_jsa_test_runner.cpp jsa/genetic/random_jsa_mutate.cpp \ - jsa/genetic/random_jsa_cross.cpp jsa/genetic/jsa_genetic_convert.cpp jsa/genetic/jsa_random.cpp \ - jsa/genetic/solution_helper.cpp jsa/genetic/jsa_serialiser.cpp jsa/genetic/jsa_paragon_wrapper.cpp \ +SRC = cegis-util/cbmc_runner.cpp \ + cegis-util/constant_width.cpp \ + cegis-util/counterexample_vars.cpp \ + cegis-util/inline_user_program.cpp \ + cegis-util/instruction_iterator.cpp \ + cegis-util/irep_pipe.cpp \ + cegis-util/module_helper.cpp \ + cegis-util/program_helper.cpp \ + cegis-util/string_helper.cpp \ + cegis-util/task_pool.cpp \ + cegis-util/temporary_output_block.cpp \ + cegis-util/type_helper.cpp \ + constant/add_constant.cpp \ + constant/default_cegis_constant_strategy.cpp \ + constant/literals_collector.cpp \ control/facade/control_runner.cpp \ + control/learn/nondet_solution.cpp \ control/learn/print_control_solution.cpp \ - control/learn/rational_solution_configuration.cpp control/learn/vector_solution_configuration.cpp \ - control/preprocessing/control_preprocessing.cpp control/preprocessing/propagate_controller_sizes.cpp \ + control/learn/rational_solution_configuration.cpp \ + control/learn/vector_solution_configuration.cpp \ control/options/control_program.cpp \ - control/learn/nondet_solution.cpp \ + control/preprocessing/control_preprocessing.cpp \ + control/preprocessing/propagate_controller_sizes.cpp \ control/simplify/remove_unused_elements.cpp \ - control/verify/insert_solution.cpp control/verify/zero_solutions.cpp \ - control/value/float_helper.cpp control/value/control_types.cpp \ + control/value/control_types.cpp \ + control/value/float_helper.cpp \ + control/verify/insert_solution.cpp \ + control/verify/zero_solutions.cpp \ + danger/constraint/danger_constraint_factory.cpp \ + danger/facade/danger_runner.cpp \ + danger/genetic/dynamic_danger_test_runner.cpp \ + danger/meta/meta_variable_names.cpp \ + danger/options/danger_program.cpp \ + danger/options/danger_program_printer.cpp \ + danger/preprocess/add_ranking_and_skolem_variables.cpp \ + danger/preprocess/danger_preprocessing.cpp \ + danger/preprocess/store_nondet_choices.cpp \ + danger/symex/fitness/danger_fitness_config.cpp \ + danger/symex/learn/add_programs_to_learn.cpp \ + danger/symex/learn/add_variable_refs.cpp \ + danger/symex/learn/add_x0_placeholders.cpp \ + danger/symex/learn/danger_learn_config.cpp \ + danger/symex/learn/encoded_danger_learn_config.cpp \ + danger/symex/learn/read_x0.cpp \ + danger/symex/learn/solution_factory.cpp \ + danger/symex/verify/danger_verify_config.cpp \ + danger/symex/verify/insert_candidate.cpp \ + danger/symex/verify/parallel_danger_verifier.cpp \ + danger/symex/verify/parallel_danger_verify_task.cpp \ + danger/symex/verify/restrict_counterexamples.cpp \ + genetic/dynamic_test_runner_helper.cpp \ + genetic/genetic_constant_strategy.cpp \ + genetic/genetic_settings.cpp \ + genetic/instruction_set_info_factory.cpp \ + genetic/program_individual_test_runner_helper.cpp \ + genetic/random_cross.cpp \ + genetic/random_individual.cpp \ + genetic/random_mutate.cpp \ + genetic/serialise_individual.cpp \ + instructions/instruction_set_factory.cpp \ + instrument/cegis_library.cpp \ + instrument/find_cprover_initialize.cpp \ + instrument/instrument_var_ops.cpp \ + instrument/meta_variables.cpp \ + invariant/constant/add_constant.cpp \ + invariant/constant/default_constant_strategy.cpp \ + invariant/constant/literals_constant_strategy.cpp \ + invariant/fitness/concrete_fitness_source_provider.cpp \ + invariant/meta/meta_variable_names.cpp \ + invariant/options/invariant_program.cpp \ + invariant/options/target_copy_helper.cpp \ + invariant/preprocess/add_invariants_and_temp_variables.cpp \ + invariant/preprocess/remove_loops_and_assertion.cpp \ + invariant/symex/learn/add_counterexamples.cpp \ + invariant/symex/learn/add_invariant_programs_to_learn.cpp \ + invariant/symex/learn/instrument_vars.cpp \ + invariant/symex/learn/replace_operators.cpp \ + invariant/symex/verify/extract_counterexample.cpp \ + invariant/symex/verify/insert_constraint.cpp \ + invariant/symex/verify/insert_program.cpp \ + invariant/util/copy_instructions.cpp \ + invariant/util/invariant_constraint_variables.cpp \ + invariant/util/invariant_program_helper.cpp \ + jsa/constraint/jsa_constraint_factory.cpp \ + jsa/converters/counterexample.cpp \ + jsa/converters/replace_operators.cpp \ + jsa/converters/solution.cpp \ + jsa/converters/translate_to_goto_program.cpp \ + jsa/facade/jsa_runner.cpp \ + jsa/genetic/dynamic_jsa_test_runner.cpp \ + jsa/genetic/jsa_genetic_convert.cpp \ + jsa/genetic/jsa_paragon_wrapper.cpp \ + jsa/genetic/jsa_random.cpp \ + jsa/genetic/jsa_serialiser.cpp \ + jsa/genetic/jsa_source_provider.cpp \ + jsa/genetic/random_jsa_cross.cpp \ + jsa/genetic/random_jsa_mutate.cpp \ + jsa/genetic/solution_helper.cpp \ + jsa/instrument/jsa_meta_data.cpp \ + jsa/instrument/temps_helper.cpp \ + jsa/learn/execute_jsa_programs.cpp \ + jsa/learn/extract_candidate.cpp \ + jsa/learn/insert_counterexample.cpp \ + jsa/learn/insert_predicates_and_queries.cpp \ + jsa/learn/instrument_pred_ops.cpp \ + jsa/learn/jsa_symex_learn.cpp \ + jsa/options/jsa_program.cpp \ + jsa/options/jsa_program_info.cpp \ + jsa/preprocessing/add_constraint_meta_variables.cpp \ + jsa/preprocessing/add_synthesis_library.cpp \ + jsa/preprocessing/clone_heap.cpp \ + jsa/preprocessing/collect_variables.cpp \ + jsa/preprocessing/create_temp_variables.cpp \ + jsa/preprocessing/default_jsa_constant_strategy.cpp \ + jsa/preprocessing/jsa_preprocessing.cpp \ + jsa/preprocessing/remove_loop.cpp \ + jsa/value/default_solution.cpp \ + jsa/value/jsa_counterexample_printer.cpp \ + jsa/value/jsa_solution.cpp \ + jsa/value/jsa_solution_printer.cpp \ + jsa/value/jsa_types.cpp \ + jsa/verify/extract_counterexample.cpp \ + jsa/verify/insert_solution.cpp \ + jsa/verify/jsa_symex_verify.cpp \ + jsa/verify/renondet_inputs.cpp \ + learn/constraint_helper.cpp \ + learn/insert_counterexample.cpp \ + refactor/constraint/constraint_factory.cpp \ refactor/environment/instrument_state_vars.cpp \ - refactor/instructionset/create_cegis_processor.cpp refactor/instructionset/execute_cegis_program.cpp \ - refactor/instructionset/processor_types.cpp refactor/instructionset/cegis_processor_body_factory.cpp \ - refactor/instructionset/instruction_description.cpp refactor/instructionset/cegis_instruction_factory.cpp \ + refactor/facade/refactor_runner.cpp \ + refactor/instructionset/cegis_instruction_factory.cpp \ + refactor/instructionset/cegis_processor_body_factory.cpp \ + refactor/instructionset/create_cegis_processor.cpp \ + refactor/instructionset/execute_cegis_program.cpp \ + refactor/instructionset/instruction_description.cpp \ refactor/instructionset/processor_symbols.cpp \ - refactor/constraint/constraint_factory.cpp \ - refactor/preprocessing/refactor_preprocessing.cpp refactor/preprocessing/collect_counterexamples.cpp \ - refactor/learn/refactor_symex_learn.cpp refactor/learn/instrument_counterexamples.cpp \ + refactor/instructionset/processor_types.cpp \ + refactor/learn/instrument_counterexamples.cpp \ refactor/learn/refactor_candidate_printer.cpp \ + refactor/learn/refactor_symex_learn.cpp \ + refactor/nullobject/nullable_analysis.cpp \ + refactor/nullobject/range_collector.cpp \ + refactor/options/refactor_program.cpp \ + refactor/options/refactoring_type.cpp \ + refactor/preprocessing/collect_counterexamples.cpp \ + refactor/preprocessing/refactor_preprocessing.cpp \ refactor/verify/refactor_symex_verify.cpp \ - refactor/facade/refactor_runner.cpp \ - refactor/options/refactoring_type.cpp refactor/options/refactor_program.cpp \ - refactor/nullobject/range_collector.cpp refactor/nullobject/nullable_analysis.cpp \ - wordsize/restrict_bv_size.cpp value/program_individual_serialisation.cpp value/assignments_printer.cpp \ + runner/cegis_languages.cpp \ + runner/cegis_main.cpp \ + runner/cegis_parse_options.cpp \ + safety/constraint/safety_constraint_factory.cpp \ + safety/facade/safety_runner.cpp \ + safety/genetic/dynamic_safety_test_runner.cpp \ + safety/meta/meta_variable_names.cpp \ + safety/options/safety_program.cpp \ + safety/options/safety_program_printer.cpp \ + safety/preprocessing/safety_preprocessing.cpp \ + safety/symex/fitness/safety_fitness_config.cpp \ + safety/symex/learn/add_counterexamples.cpp \ + safety/symex/learn/add_variable_refs.cpp \ + safety/symex/learn/encoded_safety_learn_config.cpp \ + safety/symex/learn/safety_learn_config.cpp \ + safety/symex/learn/solution_factory.cpp \ + safety/symex/verify/insert_candidate.cpp \ + safety/symex/verify/safety_verify_config.cpp \ + safety/value/individual_to_safety_solution_deserialiser.cpp \ + safety/value/safety_goto_ce.cpp \ seed/literals_seed.cpp \ - genetic/instruction_set_info_factory.cpp genetic/random_mutate.cpp genetic/random_cross.cpp \ - genetic/random_individual.cpp genetic/genetic_constant_strategy.cpp instructions/instruction_set_factory.cpp \ - genetic/dynamic_test_runner_helper.cpp genetic/genetic_settings.cpp \ - genetic/serialise_individual.cpp genetic/program_individual_test_runner_helper.cpp \ - cegis-util/task_pool.cpp cegis-util/constant_width.cpp cegis-util/irep_pipe.cpp cegis-util/program_helper.cpp \ - cegis-util/temporary_output_block.cpp cegis-util/cbmc_runner.cpp cegis-util/module_helper.cpp \ - cegis-util/inline_user_program.cpp cegis-util/counterexample_vars.cpp cegis-util/string_helper.cpp \ - cegis-util/instruction_iterator.cpp cegis-util/type_helper.cpp \ - learn/insert_counterexample.cpp learn/constraint_helper.cpp \ - constant/add_constant.cpp constant/literals_collector.cpp constant/default_cegis_constant_strategy.cpp \ - instrument/cegis_library.cpp instrument/instrument_var_ops.cpp instrument/meta_variables.cpp \ - instrument/find_cprover_initialize.cpp \ - runner/cegis_parse_options.cpp runner/cegis_main.cpp runner/cegis_languages.cpp + value/assignments_printer.cpp \ + value/program_individual_serialisation.cpp \ + wordsize/restrict_bv_size.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/clobber/Makefile b/src/clobber/Makefile index ee77d22e33a..f3a4c8aed20 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -1,5 +1,6 @@ -SRC = clobber_main.cpp clobber_parse_options.cpp - +SRC = clobber_main.cpp \ + clobber_parse_options.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../linking/linking$(LIBEXT) \ diff --git a/src/cpp/Makefile b/src/cpp/Makefile index f7be0dba3f9..b98e4766b42 100644 --- a/src/cpp/Makefile +++ b/src/cpp/Makefile @@ -1,27 +1,51 @@ -SRC = cpp_id.cpp cpp_language.cpp expr2cpp.cpp cpp_parser.cpp \ - cpp_typecheck.cpp cpp_convert_type.cpp \ - cpp_typecheck_expr.cpp cpp_typecheck_code.cpp \ - cpp_typecheck_type.cpp parse.cpp cpp_parse_tree.cpp \ - cpp_token_buffer.cpp cpp_typecheck_fargs.cpp \ - cpp_typecheck_resolve.cpp cpp_util.cpp cpp_enum_type.cpp \ - cpp_typecheck_function.cpp cpp_typecheck_namespace.cpp \ - cpp_name.cpp cpp_is_pod.cpp cpp_scope.cpp \ - template_map.cpp \ - cpp_scopes.cpp cpp_declarator.cpp cpp_instantiate_template.cpp \ - cpp_internal_additions.cpp cpp_type2name.cpp \ - cpp_typecheck_linkage_spec.cpp \ - cpp_typecheck_template.cpp cpp_typecheck_method_bodies.cpp \ - cpp_typecheck_initializer.cpp cpp_typecheck_compound_type.cpp \ - cpp_constructor.cpp cpp_destructor.cpp \ - cpp_typecheck_conversions.cpp\ - cpp_typecheck_declaration.cpp cpp_declarator_converter.cpp \ - cpp_declaration.cpp cpp_namespace_spec.cpp \ - cpp_typecheck_using.cpp cpp_exception_id.cpp \ - cpp_typecheck_enum_type.cpp cpp_typecheck_bases.cpp \ +SRC = cpp_constructor.cpp \ + cpp_convert_type.cpp \ + cpp_declaration.cpp \ + cpp_declarator.cpp \ + cpp_declarator_converter.cpp \ + cpp_destructor.cpp \ + cpp_enum_type.cpp \ + cpp_exception_id.cpp \ + cpp_id.cpp \ + cpp_instantiate_template.cpp \ + cpp_internal_additions.cpp \ + cpp_is_pod.cpp \ + cpp_language.cpp \ + cpp_name.cpp \ + cpp_namespace_spec.cpp \ + cpp_parse_tree.cpp \ + cpp_parser.cpp \ + cpp_scope.cpp \ + cpp_scopes.cpp \ + cpp_token_buffer.cpp \ + cpp_type2name.cpp \ + cpp_typecheck.cpp \ + cpp_typecheck_bases.cpp \ + cpp_typecheck_code.cpp \ + cpp_typecheck_compound_type.cpp \ cpp_typecheck_constructor.cpp \ + cpp_typecheck_conversions.cpp \ + cpp_typecheck_declaration.cpp \ cpp_typecheck_destructor.cpp \ + cpp_typecheck_enum_type.cpp \ + cpp_typecheck_expr.cpp \ + cpp_typecheck_fargs.cpp \ + cpp_typecheck_function.cpp \ + cpp_typecheck_initializer.cpp \ + cpp_typecheck_linkage_spec.cpp \ + cpp_typecheck_method_bodies.cpp \ + cpp_typecheck_namespace.cpp \ + cpp_typecheck_resolve.cpp \ + cpp_typecheck_static_assert.cpp \ + cpp_typecheck_template.cpp \ + cpp_typecheck_type.cpp \ + cpp_typecheck_using.cpp \ cpp_typecheck_virtual_table.cpp \ - cpp_typecheck_static_assert.cpp + cpp_util.cpp \ + expr2cpp.cpp \ + parse.cpp \ + template_map.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index b27b514bf88..9eb45165f9c 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -1,6 +1,10 @@ -SRC = goto_analyzer_main.cpp goto_analyzer_parse_options.cpp \ - taint_parser.cpp taint_analysis.cpp static_analyzer.cpp \ - unreachable_instructions.cpp +SRC = goto_analyzer_main.cpp \ + goto_analyzer_parse_options.cpp \ + static_analyzer.cpp \ + taint_analysis.cpp \ + taint_parser.cpp \ + unreachable_instructions.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 3079e7ebb00..51ac3f0f9cb 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -1,9 +1,21 @@ -SRC = goto_cc_main.cpp goto_cc_mode.cpp gcc_mode.cpp \ - gcc_cmdline.cpp ms_cl_cmdline.cpp ld_cmdline.cpp \ - compile.cpp armcc_cmdline.cpp \ - goto_cc_languages.cpp goto_cc_cmdline.cpp \ - ms_cl_mode.cpp armcc_mode.cpp cw_mode.cpp bcc_cmdline.cpp \ - as_mode.cpp as_cmdline.cpp as86_cmdline.cpp +SRC = armcc_cmdline.cpp \ + armcc_mode.cpp \ + as86_cmdline.cpp \ + as_cmdline.cpp \ + as_mode.cpp \ + bcc_cmdline.cpp \ + compile.cpp \ + cw_mode.cpp \ + gcc_cmdline.cpp \ + gcc_mode.cpp \ + goto_cc_cmdline.cpp \ + goto_cc_languages.cpp \ + goto_cc_main.cpp \ + goto_cc_mode.cpp \ + ld_cmdline.cpp \ + ms_cl_cmdline.cpp \ + ms_cl_mode.cpp \ + # Empty last line OBJ += ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index fd18897aaea..b11cb008b3a 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -1,6 +1,11 @@ -SRC = goto_diff_main.cpp goto_diff_parse_options.cpp \ - goto_diff_languages.cpp goto_diff_base.cpp syntactic_diff.cpp \ - unified_diff.cpp change_impact.cpp +SRC = change_impact.cpp \ + goto_diff_base.cpp \ + goto_diff_languages.cpp \ + goto_diff_main.cpp \ + goto_diff_parse_options.cpp \ + syntactic_diff.cpp \ + unified_diff.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 3fbaac8620b..4b74d173ff7 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -1,30 +1,66 @@ -SRC = goto_instrument_parse_options.cpp rw_set.cpp \ - document_properties.cpp goto_instrument_languages.cpp \ - uninitialized.cpp full_slicer.cpp k_induction.cpp \ - object_id.cpp show_locations.cpp points_to.cpp \ - alignment_checks.cpp race_check.cpp \ - nondet_volatile.cpp interrupt.cpp function.cpp branch.cpp \ - mmio.cpp stack_depth.cpp nondet_static.cpp \ - concurrency.cpp dump_c.cpp dot.cpp havoc_loops.cpp \ - call_sequences.cpp unwind.cpp function_modifies.cpp \ - accelerate/accelerate.cpp accelerate/polynomial.cpp \ - accelerate/scratch_program.cpp accelerate/polynomial_accelerator.cpp \ - accelerate/util.cpp accelerate/trace_automaton.cpp \ - accelerate/enumerating_loop_acceleration.cpp \ +SRC = accelerate/accelerate.cpp \ + accelerate/acceleration_utils.cpp \ accelerate/all_paths_enumerator.cpp \ - accelerate/sat_path_enumerator.cpp \ + accelerate/cone_of_influence.cpp \ accelerate/disjunctive_polynomial_acceleration.cpp \ - accelerate/cone_of_influence.cpp accelerate/overflow_instrumenter.cpp\ - accelerate/path.cpp accelerate/acceleration_utils.cpp \ - count_eloc.cpp reachability_slicer.cpp goto_program2code.cpp \ - wmm/abstract_event.cpp wmm/fence.cpp wmm/shared_buffers.cpp \ - wmm/cycle_collection.cpp wmm/goto2graph.cpp wmm/weak_memory.cpp \ - wmm/data_dp.cpp wmm/instrumenter_strategies.cpp \ - wmm/event_graph.cpp wmm/pair_collection.cpp \ - goto_instrument_main.cpp horn_encoding.cpp \ - thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \ - code_contracts.cpp cover.cpp model_argc_argv.cpp \ - undefined_functions.cpp + accelerate/enumerating_loop_acceleration.cpp \ + accelerate/overflow_instrumenter.cpp \ + accelerate/path.cpp \ + accelerate/polynomial.cpp \ + accelerate/polynomial_accelerator.cpp \ + accelerate/sat_path_enumerator.cpp \ + accelerate/scratch_program.cpp \ + accelerate/trace_automaton.cpp \ + accelerate/util.cpp \ + alignment_checks.cpp \ + branch.cpp \ + call_sequences.cpp \ + code_contracts.cpp \ + concurrency.cpp \ + count_eloc.cpp \ + cover.cpp \ + document_properties.cpp \ + dot.cpp \ + dump_c.cpp \ + full_slicer.cpp \ + function.cpp \ + function_modifies.cpp \ + goto_instrument_languages.cpp \ + goto_instrument_main.cpp \ + goto_instrument_parse_options.cpp \ + goto_program2code.cpp \ + havoc_loops.cpp \ + horn_encoding.cpp \ + interrupt.cpp \ + k_induction.cpp \ + loop_utils.cpp \ + mmio.cpp \ + model_argc_argv.cpp \ + nondet_static.cpp \ + nondet_volatile.cpp \ + object_id.cpp \ + points_to.cpp \ + race_check.cpp \ + reachability_slicer.cpp \ + rw_set.cpp \ + show_locations.cpp \ + skip_loops.cpp \ + stack_depth.cpp \ + thread_instrumentation.cpp \ + undefined_functions.cpp \ + uninitialized.cpp \ + unwind.cpp \ + wmm/abstract_event.cpp \ + wmm/cycle_collection.cpp \ + wmm/data_dp.cpp \ + wmm/event_graph.cpp \ + wmm/fence.cpp \ + wmm/goto2graph.cpp \ + wmm/instrumenter_strategies.cpp \ + wmm/pair_collection.cpp \ + wmm/shared_buffers.cpp \ + wmm/weak_memory.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index bf6abb39ab6..94fc21b420c 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,27 +1,65 @@ -SRC = goto_convert.cpp goto_convert_function_call.cpp \ - goto_convert_side_effect.cpp goto_program.cpp basic_blocks.cpp \ - goto_convert_exceptions.cpp property_checker.cpp \ - remove_function_pointers.cpp goto_functions.cpp goto_inline.cpp \ - remove_skip.cpp goto_convert_functions.cpp string_instrumentation.cpp \ - builtin_functions.cpp show_properties.cpp set_properties.cpp \ - read_goto_binary.cpp goto_asm.cpp elf_reader.cpp show_symbol_table.cpp \ - string_abstraction.cpp destructor.cpp remove_asm.cpp \ - read_bin_goto_object.cpp goto_program_irep.cpp interpreter.cpp \ - interpreter_evaluate.cpp json_goto_trace.cpp \ - format_strings.cpp loop_ids.cpp pointer_arithmetic.cpp \ - goto_program_template.cpp write_goto_binary.cpp remove_unreachable.cpp \ - remove_unused_functions.cpp remove_vector.cpp \ - wp.cpp goto_clean_expr.cpp safety_checker.cpp parameter_assignments.cpp \ - compute_called_functions.cpp link_to_library.cpp \ - remove_returns.cpp remove_exceptions.cpp osx_fat_reader.cpp \ - remove_complex.cpp goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ - graphml_witness.cpp remove_virtual_functions.cpp \ - class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ - slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \ +SRC = basic_blocks.cpp \ + builtin_functions.cpp \ + class_hierarchy.cpp \ + class_identifier.cpp \ + compute_called_functions.cpp \ + destructor.cpp \ + elf_reader.cpp \ + format_strings.cpp \ + get_goto_model.cpp \ + goto_asm.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_functions.cpp \ + goto_inline.cpp \ + goto_inline_class.cpp \ + goto_program.cpp \ + goto_program_irep.cpp \ + goto_program_template.cpp \ + goto_trace.cpp \ + graphml_witness.cpp \ + interpreter.cpp \ + interpreter_evaluate.cpp \ + json_goto_trace.cpp \ + link_to_library.cpp \ + loop_ids.cpp \ + osx_fat_reader.cpp \ + parameter_assignments.cpp \ + pointer_arithmetic.cpp \ + property_checker.cpp \ + read_bin_goto_object.cpp \ + read_goto_binary.cpp \ + remove_asm.cpp \ + remove_complex.cpp \ + remove_const_function_pointers.cpp \ + remove_exceptions.cpp \ + remove_function_pointers.cpp \ + remove_instanceof.cpp \ + remove_returns.cpp \ + remove_skip.cpp \ + remove_static_init_loops.cpp \ + remove_unreachable.cpp \ + remove_unused_functions.cpp \ + remove_vector.cpp \ + remove_virtual_functions.cpp \ + safety_checker.cpp \ + set_properties.cpp \ + show_goto_functions.cpp \ show_goto_functions_json.cpp \ show_goto_functions_xml.cpp \ - remove_static_init_loops.cpp remove_instanceof.cpp \ - remove_const_function_pointers.cpp \ + show_properties.cpp \ + show_symbol_table.cpp \ + slice_global_inits.cpp \ + string_abstraction.cpp \ + string_instrumentation.cpp \ + vcd_goto_trace.cpp \ + wp.cpp \ + write_goto_binary.cpp \ + xml_goto_trace.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index 801307df858..76f9bb61d91 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -1,14 +1,36 @@ -SRC = symex_target.cpp symex_target_equation.cpp goto_symex.cpp \ - symex_main.cpp build_goto_trace.cpp adjust_float_expressions.cpp \ - symex_function_call.cpp goto_symex_state.cpp symex_dereference.cpp \ - symex_goto.cpp symex_builtin_functions.cpp slice.cpp symex_other.cpp \ - slice_by_trace.cpp symex_decl.cpp symex_dead.cpp rewrite_union.cpp \ - precondition.cpp postcondition.cpp symex_clean_expr.cpp \ - symex_dereference_state.cpp auto_objects.cpp \ - symex_catch.cpp symex_start_thread.cpp symex_assign.cpp \ - symex_throw.cpp symex_atomic_section.cpp memory_model.cpp \ - memory_model_sc.cpp partial_order_concurrency.cpp \ - memory_model_tso.cpp memory_model_pso.cpp +SRC = adjust_float_expressions.cpp \ + auto_objects.cpp \ + build_goto_trace.cpp \ + goto_symex.cpp \ + goto_symex_state.cpp \ + memory_model.cpp \ + memory_model_pso.cpp \ + memory_model_sc.cpp \ + memory_model_tso.cpp \ + partial_order_concurrency.cpp \ + postcondition.cpp \ + precondition.cpp \ + rewrite_union.cpp \ + slice.cpp \ + slice_by_trace.cpp \ + symex_assign.cpp \ + symex_atomic_section.cpp \ + symex_builtin_functions.cpp \ + symex_catch.cpp \ + symex_clean_expr.cpp \ + symex_dead.cpp \ + symex_decl.cpp \ + symex_dereference.cpp \ + symex_dereference_state.cpp \ + symex_function_call.cpp \ + symex_goto.cpp \ + symex_main.cpp \ + symex_other.cpp \ + symex_start_thread.cpp \ + symex_target.cpp \ + symex_target_equation.cpp \ + symex_throw.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index d5d427747c2..3867eb28182 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -1,12 +1,26 @@ -SRC = java_bytecode_language.cpp java_bytecode_parse_tree.cpp \ - java_bytecode_typecheck.cpp expr2java.cpp \ - java_bytecode_convert_class.cpp java_types.cpp java_entry_point.cpp \ - java_bytecode_typecheck_code.cpp java_bytecode_typecheck_expr.cpp \ - java_bytecode_typecheck_type.cpp java_bytecode_internal_additions.cpp \ - java_root_class.cpp java_bytecode_parser.cpp bytecode_info.cpp \ - java_class_loader.cpp jar_file.cpp java_object_factory.cpp \ - java_bytecode_convert_method.cpp java_local_variable_table.cpp \ - java_pointer_casts.cpp java_utils.cpp java_class_loader_limit.cpp +SRC = bytecode_info.cpp \ + expr2java.cpp \ + jar_file.cpp \ + java_bytecode_convert_class.cpp \ + java_bytecode_convert_method.cpp \ + java_bytecode_internal_additions.cpp \ + java_bytecode_language.cpp \ + java_bytecode_parse_tree.cpp \ + java_bytecode_parser.cpp \ + java_bytecode_typecheck.cpp \ + java_bytecode_typecheck_code.cpp \ + java_bytecode_typecheck_expr.cpp \ + java_bytecode_typecheck_type.cpp \ + java_class_loader.cpp \ + java_class_loader_limit.cpp \ + java_entry_point.cpp \ + java_local_variable_table.cpp \ + java_object_factory.cpp \ + java_pointer_casts.cpp \ + java_root_class.cpp \ + java_types.cpp \ + java_utils.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/jsil/Makefile b/src/jsil/Makefile index b1f9cc278e9..60e907197a5 100644 --- a/src/jsil/Makefile +++ b/src/jsil/Makefile @@ -1,7 +1,15 @@ -SRC = jsil_y.tab.cpp jsil_lex.yy.cpp \ - jsil_convert.cpp jsil_language.cpp jsil_parse_tree.cpp jsil_types.cpp \ - jsil_parser.cpp jsil_typecheck.cpp expr2jsil.cpp \ - jsil_entry_point.cpp jsil_internal_additions.cpp +SRC = expr2jsil.cpp \ + jsil_convert.cpp \ + jsil_entry_point.cpp \ + jsil_internal_additions.cpp \ + jsil_language.cpp \ + jsil_lex.yy.cpp \ + jsil_parse_tree.cpp \ + jsil_parser.cpp \ + jsil_typecheck.cpp \ + jsil_types.cpp \ + jsil_y.tab.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/json/Makefile b/src/json/Makefile index 0cf6ae2d8d6..95d6b9bf558 100644 --- a/src/json/Makefile +++ b/src/json/Makefile @@ -1,5 +1,7 @@ -SRC = json_parser.cpp json_y.tab.cpp json_lex.yy.cpp - +SRC = json_lex.yy.cpp \ + json_parser.cpp \ + json_y.tab.cpp \ + # Empty last line INCLUDES= -I .. include ../config.inc diff --git a/src/langapi/Makefile b/src/langapi/Makefile index 1eb5645b2d6..12bc2a2f784 100644 --- a/src/langapi/Makefile +++ b/src/langapi/Makefile @@ -1,5 +1,8 @@ -SRC = mode.cpp language_ui.cpp languages.cpp language_util.cpp - +SRC = language_ui.cpp \ + language_util.cpp \ + languages.cpp \ + mode.cpp \ + # Empty last line INCLUDES= -I .. include ../config.inc diff --git a/src/linking/Makefile b/src/linking/Makefile index b0b44b0b15d..a2030500ec4 100644 --- a/src/linking/Makefile +++ b/src/linking/Makefile @@ -1,5 +1,8 @@ -SRC = linking.cpp zero_initializer.cpp static_lifetime_init.cpp \ - remove_internal_symbols.cpp +SRC = linking.cpp \ + remove_internal_symbols.cpp \ + static_lifetime_init.cpp \ + zero_initializer.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile index a1127d05821..e13309deaae 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -1,5 +1,10 @@ -SRC = mm_y.tab.cpp mm_lex.yy.cpp mmcc_main.cpp mm_parser.cpp \ - mmcc_parse_options.cpp mm2cpp.cpp +SRC = mm2cpp.cpp \ + mm_lex.yy.cpp \ + mm_parser.cpp \ + mm_y.tab.cpp \ + mmcc_main.cpp \ + mmcc_parse_options.cpp \ + # Empty last line OBJ += ../big-int/big-int$(LIBEXT) \ ../ansi-c/ansi-c$(LIBEXT) \ diff --git a/src/miniz/Makefile b/src/miniz/Makefile index 324c9821b91..77258d1f6bc 100644 --- a/src/miniz/Makefile +++ b/src/miniz/Makefile @@ -1,5 +1,5 @@ -SRC = miniz.cpp - +SRC = miniz.cpp \ + # Empty last line INCLUDES= -I .. include ../config.inc diff --git a/src/musketeer/Makefile b/src/musketeer/Makefile index d732a396ebd..be41fa923cc 100644 --- a/src/musketeer/Makefile +++ b/src/musketeer/Makefile @@ -1,7 +1,16 @@ -SRC = languages.cpp fencer.cpp fence_inserter.cpp musketeer_main.cpp \ - musketeer_parse_options.cpp fence_assert.cpp fence_user_def.cpp \ - fence_shared.cpp pensieve.cpp propagate_const_function_pointers.cpp \ - graph_visitor.cpp cycles_visitor.cpp +SRC = cycles_visitor.cpp \ + fence_assert.cpp \ + fence_inserter.cpp \ + fence_shared.cpp \ + fence_user_def.cpp \ + fencer.cpp \ + graph_visitor.cpp \ + languages.cpp \ + musketeer_main.cpp \ + musketeer_parse_options.cpp \ + pensieve.cpp \ + propagate_const_function_pointers.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../linking/linking$(LIBEXT) \ diff --git a/src/path-symex/Makefile b/src/path-symex/Makefile index 579a787b602..111597fb97a 100644 --- a/src/path-symex/Makefile +++ b/src/path-symex/Makefile @@ -1,6 +1,12 @@ -SRC = locs.cpp var_map.cpp path_symex_history.cpp path_symex_state.cpp \ - path_symex.cpp build_goto_trace.cpp path_replay.cpp \ - path_symex_state_read.cpp +SRC = build_goto_trace.cpp \ + locs.cpp \ + path_replay.cpp \ + path_symex.cpp \ + path_symex_history.cpp \ + path_symex_state.cpp \ + path_symex_state_read.cpp \ + var_map.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/pointer-analysis/Makefile b/src/pointer-analysis/Makefile index 6df993586b8..7e9837ac737 100644 --- a/src/pointer-analysis/Makefile +++ b/src/pointer-analysis/Makefile @@ -1,11 +1,24 @@ -SRC = value_set.cpp goto_program_dereference.cpp value_set_analysis.cpp \ - dereference.cpp pointer_offset_sum.cpp add_failed_symbols.cpp \ - show_value_sets.cpp value_set_domain.cpp rewrite_index.cpp \ - value_set_analysis_fi.cpp value_set_fi.cpp value_set_domain_fi.cpp \ - value_set_analysis_fivr.cpp value_set_fivr.cpp value_set_domain_fivr.cpp \ - value_set_analysis_fivrns.cpp value_set_fivrns.cpp \ - value_set_domain_fivrns.cpp value_set_dereference.cpp \ - dereference_callback.cpp +SRC = add_failed_symbols.cpp \ + dereference.cpp \ + dereference_callback.cpp \ + goto_program_dereference.cpp \ + pointer_offset_sum.cpp \ + rewrite_index.cpp \ + show_value_sets.cpp \ + value_set.cpp \ + value_set_analysis.cpp \ + value_set_analysis_fi.cpp \ + value_set_analysis_fivr.cpp \ + value_set_analysis_fivrns.cpp \ + value_set_dereference.cpp \ + value_set_domain.cpp \ + value_set_domain_fi.cpp \ + value_set_domain_fivr.cpp \ + value_set_domain_fivrns.cpp \ + value_set_fi.cpp \ + value_set_fivr.cpp \ + value_set_fivrns.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 95ea7650274..57c74a2e322 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -71,54 +71,109 @@ ifneq ($(LINGELING),) CP_CXXFLAGS += -DHAVE_LINGELING endif -SRC = $(CHAFF_SRC) $(BOOLEFORCE_SRC) $(MINISAT_SRC) $(MINISAT2_SRC) \ - $(SMVSAT_SRC) $(SQUOLEM2_SRC) $(CUDD_SRC) $(GLUCOSE_SRC) \ - $(PRECOSAT_SRC) $(PICOSAT_SRC) $(LINGELING_SRC) \ - sat/cnf.cpp sat/dimacs_cnf.cpp sat/cnf_clause_list.cpp \ - sat/pbs_dimacs_cnf.cpp sat/read_dimacs_cnf.cpp \ - sat/resolution_proof.cpp sat/satcheck.cpp \ - qbf/qdimacs_cnf.cpp qbf/qbf_quantor.cpp \ - qbf/qbf_skizzo.cpp qbf/qdimacs_core.cpp qbf/qbf_qube.cpp \ - qbf/qbf_qube_core.cpp \ - prop/prop.cpp prop/prop_conv.cpp prop/prop_conv_store.cpp \ - prop/cover_goals.cpp prop/literal.cpp \ - prop/aig.cpp prop/aig_prop.cpp prop/minimize.cpp \ - prop/prop_assignment.cpp prop/bdd_expr.cpp \ - cvc/cvc_conv.cpp cvc/cvc_dec.cpp \ - smt1/smt1_dec.cpp smt1/smt1_conv.cpp \ - smt2/smt2_dec.cpp smt2/smt2_conv.cpp smt2/smt2_parser.cpp smt2/smt2irep.cpp \ - flattening/equality.cpp flattening/arrays.cpp \ - flattening/functions.cpp flattening/bv_minimize.cpp \ - flattening/boolbv_width.cpp flattening/boolbv.cpp \ +SRC = $(BOOLEFORCE_SRC) \ + $(CHAFF_SRC) \ + $(CUDD_SRC) \ + $(GLUCOSE_SRC) \ + $(LINGELING_SRC) \ + $(MINISAT2_SRC) \ + $(MINISAT_SRC) \ + $(PICOSAT_SRC) \ + $(PRECOSAT_SRC) \ + $(SMVSAT_SRC) \ + $(SQUOLEM2_SRC) \ + cvc/cvc_conv.cpp \ + cvc/cvc_dec.cpp \ + flattening/arrays.cpp \ + flattening/boolbv.cpp \ + flattening/boolbv_abs.cpp \ + flattening/boolbv_add_sub.cpp \ + flattening/boolbv_array.cpp \ + flattening/boolbv_array_of.cpp \ + flattening/boolbv_bitwise.cpp \ + flattening/boolbv_bv_rel.cpp \ + flattening/boolbv_byte_extract.cpp \ + flattening/boolbv_byte_update.cpp \ + flattening/boolbv_case.cpp \ + flattening/boolbv_complex.cpp \ + flattening/boolbv_concatenation.cpp \ + flattening/boolbv_cond.cpp \ + flattening/boolbv_constant.cpp \ flattening/boolbv_constraint_select_one.cpp \ - flattening/bv_pointers.cpp flattening/bv_utils.cpp \ - flattening/boolbv_abs.cpp flattening/boolbv_with.cpp \ - flattening/boolbv_typecast.cpp flattening/boolbv_index.cpp \ - flattening/boolbv_member.cpp flattening/boolbv_if.cpp \ - flattening/boolbv_byte_extract.cpp flattening/boolbv_add_sub.cpp \ - flattening/boolbv_mult.cpp flattening/boolbv_constant.cpp \ - flattening/boolbv_extractbit.cpp flattening/boolbv_bv_rel.cpp \ - flattening/boolbv_shift.cpp flattening/boolbv_case.cpp \ - flattening/boolbv_cond.cpp flattening/boolbv_concatenation.cpp \ - flattening/boolbv_div.cpp flattening/boolbv_mod.cpp \ - flattening/boolbv_extractbits.cpp flattening/boolbv_replication.cpp \ - flattening/boolbv_reduction.cpp flattening/boolbv_overflow.cpp \ - flattening/boolbv_get.cpp flattening/boolbv_bitwise.cpp \ - flattening/boolbv_equality.cpp flattening/boolbv_unary_minus.cpp \ - flattening/boolbv_ieee_float_rel.cpp flattening/pointer_logic.cpp \ - flattening/boolbv_quantifier.cpp flattening/boolbv_struct.cpp \ - flattening/boolbv_byte_update.cpp flattening/boolbv_array_of.cpp \ - flattening/boolbv_map.cpp flattening/boolbv_type.cpp \ - flattening/boolbv_array.cpp flattening/boolbv_vector.cpp \ - flattening/boolbv_complex.cpp flattening/boolbv_floatbv_op.cpp \ - flattening/boolbv_union.cpp flattening/flatten_byte_operators.cpp \ - flattening/boolbv_update.cpp flattening/c_bit_field_replacement_type.cpp \ - flattening/boolbv_onehot.cpp flattening/boolbv_not.cpp \ + flattening/boolbv_div.cpp \ + flattening/boolbv_equality.cpp \ + flattening/boolbv_extractbit.cpp \ + flattening/boolbv_extractbits.cpp \ + flattening/boolbv_floatbv_op.cpp \ + flattening/boolbv_get.cpp \ + flattening/boolbv_ieee_float_rel.cpp \ + flattening/boolbv_if.cpp \ + flattening/boolbv_index.cpp \ + flattening/boolbv_map.cpp \ + flattening/boolbv_member.cpp \ + flattening/boolbv_mod.cpp \ + flattening/boolbv_mult.cpp \ + flattening/boolbv_not.cpp \ + flattening/boolbv_onehot.cpp \ + flattening/boolbv_overflow.cpp \ flattening/boolbv_power.cpp \ - floatbv/float_utils.cpp floatbv/float_bv.cpp \ - refinement/bv_refinement_loop.cpp refinement/refine_arithmetic.cpp \ + flattening/boolbv_quantifier.cpp \ + flattening/boolbv_reduction.cpp \ + flattening/boolbv_replication.cpp \ + flattening/boolbv_shift.cpp \ + flattening/boolbv_struct.cpp \ + flattening/boolbv_type.cpp \ + flattening/boolbv_typecast.cpp \ + flattening/boolbv_unary_minus.cpp \ + flattening/boolbv_union.cpp \ + flattening/boolbv_update.cpp \ + flattening/boolbv_vector.cpp \ + flattening/boolbv_width.cpp \ + flattening/boolbv_with.cpp \ + flattening/bv_minimize.cpp \ + flattening/bv_pointers.cpp \ + flattening/bv_utils.cpp \ + flattening/c_bit_field_replacement_type.cpp \ + flattening/equality.cpp \ + flattening/flatten_byte_operators.cpp \ + flattening/functions.cpp \ + flattening/pointer_logic.cpp \ + floatbv/float_bv.cpp \ + floatbv/float_utils.cpp \ + miniBDD/miniBDD.cpp \ + prop/aig.cpp \ + prop/aig_prop.cpp \ + prop/bdd_expr.cpp \ + prop/cover_goals.cpp \ + prop/literal.cpp \ + prop/minimize.cpp \ + prop/prop.cpp \ + prop/prop_assignment.cpp \ + prop/prop_conv.cpp \ + prop/prop_conv_store.cpp \ + qbf/qbf_quantor.cpp \ + qbf/qbf_qube.cpp \ + qbf/qbf_qube_core.cpp \ + qbf/qbf_skizzo.cpp \ + qbf/qdimacs_cnf.cpp \ + qbf/qdimacs_core.cpp \ + refinement/bv_refinement_loop.cpp \ + refinement/refine_arithmetic.cpp \ refinement/refine_arrays.cpp \ - miniBDD/miniBDD.cpp + sat/cnf.cpp \ + sat/cnf_clause_list.cpp \ + sat/dimacs_cnf.cpp \ + sat/pbs_dimacs_cnf.cpp \ + sat/read_dimacs_cnf.cpp \ + sat/resolution_proof.cpp \ + sat/satcheck.cpp \ + smt1/smt1_conv.cpp \ + smt1/smt1_dec.cpp \ + smt2/smt2_conv.cpp \ + smt2/smt2_dec.cpp \ + smt2/smt2_parser.cpp \ + smt2/smt2irep.cpp \ + # Empty last line INCLUDES += -I .. \ $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \ diff --git a/src/symex/Makefile b/src/symex/Makefile index e887ca55352..672b2e07fc2 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -1,5 +1,8 @@ -SRC = symex_main.cpp symex_parse_options.cpp path_search.cpp \ - symex_cover.cpp +SRC = path_search.cpp \ + symex_cover.cpp \ + symex_main.cpp \ + symex_parse_options.cpp \ + # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/util/Makefile b/src/util/Makefile index 84aa55afdd4..154792d1331 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -1,29 +1,95 @@ -SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ - expr.cpp expr_util.cpp irep.cpp language.cpp \ - lispexpr.cpp lispirep.cpp source_location.cpp message.cpp language_file.cpp \ - mp_arith.cpp namespace.cpp parse_options.cpp rename.cpp \ - replace_expr.cpp threeval.cpp typecheck.cpp graph.cpp \ - type.cpp pointer_predicates.cpp merge_irep.cpp run.cpp \ - parser.cpp replace_symbol.cpp json.cpp get_base_name.cpp \ - simplify_expr.cpp simplify_expr_floatbv.cpp simplify_expr_int.cpp \ - simplify_expr_array.cpp simplify_expr_struct.cpp \ - simplify_expr_boolean.cpp simplify_expr_pointer.cpp \ - get_module.cpp string_hash.cpp string_container.cpp identifier.cpp \ - rational.cpp options.cpp dstring.cpp \ - find_symbols.cpp rational_tools.cpp ui_message.cpp simplify_utils.cpp \ - time_stopping.cpp symbol.cpp irep_hash_container.cpp cout_message.cpp \ - type_eq.cpp guard.cpp array_name.cpp \ - substitute.cpp decision_procedure.cpp union_find.cpp \ - xml.cpp xml_irep.cpp xml_expr.cpp std_types.cpp std_code.cpp \ - format_constant.cpp find_macros.cpp ref_expr_set.cpp std_expr.cpp \ - irep_serialization.cpp fixedbv.cpp rename_symbol.cpp \ - ieee_float.cpp signal_catcher.cpp pointer_offset_size.cpp \ - bv_arithmetic.cpp tempdir.cpp tempfile.cpp timer.cpp unicode.cpp \ - irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \ - memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \ - ssa_expr.cpp json_irep.cpp json_expr.cpp \ +SRC = arith_tools.cpp \ + array_name.cpp \ + base_type.cpp \ + bv_arithmetic.cpp \ + byte_operators.cpp \ + cmdline.cpp \ + config.cpp \ + cout_message.cpp \ + decision_procedure.cpp \ + dstring.cpp \ + endianness_map.cpp \ + expr.cpp \ + expr_util.cpp \ + file_util.cpp \ + find_macros.cpp \ + find_symbols.cpp \ + fixedbv.cpp \ + format_constant.cpp \ fresh_symbol.cpp \ - string_utils.cpp + get_base_name.cpp \ + get_module.cpp \ + graph.cpp \ + guard.cpp \ + identifier.cpp \ + ieee_float.cpp \ + irep.cpp \ + irep_hash.cpp \ + irep_hash_container.cpp \ + irep_ids.cpp \ + irep_serialization.cpp \ + json.cpp \ + json_expr.cpp \ + json_irep.cpp \ + language.cpp \ + language_file.cpp \ + lispexpr.cpp \ + lispirep.cpp \ + memory_info.cpp \ + merge_irep.cpp \ + message.cpp \ + mp_arith.cpp \ + namespace.cpp \ + options.cpp \ + parse_options.cpp \ + parser.cpp \ + pipe_stream.cpp \ + pointer_offset_size.cpp \ + pointer_predicates.cpp \ + rational.cpp \ + rational_tools.cpp \ + ref_expr_set.cpp \ + rename.cpp \ + rename_symbol.cpp \ + replace_expr.cpp \ + replace_symbol.cpp \ + run.cpp \ + signal_catcher.cpp \ + simplify_expr.cpp \ + simplify_expr_array.cpp \ + simplify_expr_boolean.cpp \ + simplify_expr_floatbv.cpp \ + simplify_expr_int.cpp \ + simplify_expr_pointer.cpp \ + simplify_expr_struct.cpp \ + simplify_utils.cpp \ + source_location.cpp \ + ssa_expr.cpp \ + std_code.cpp \ + std_expr.cpp \ + std_types.cpp \ + string2int.cpp \ + string_container.cpp \ + string_hash.cpp \ + string_utils.cpp \ + substitute.cpp \ + symbol.cpp \ + symbol_table.cpp \ + tempdir.cpp \ + tempfile.cpp \ + threeval.cpp \ + time_stopping.cpp \ + timer.cpp \ + type.cpp \ + type_eq.cpp \ + typecheck.cpp \ + ui_message.cpp \ + unicode.cpp \ + union_find.cpp \ + xml.cpp \ + xml_expr.cpp \ + xml_irep.cpp \ + # Empty last line INCLUDES= -I .. diff --git a/src/xmllang/Makefile b/src/xmllang/Makefile index 81f656b1cca..393890a2c1c 100644 --- a/src/xmllang/Makefile +++ b/src/xmllang/Makefile @@ -1,5 +1,9 @@ -SRC = xml_parser.cpp xml_y.tab.cpp xml_lex.yy.cpp xml_parse_tree.cpp graphml.cpp - +SRC = graphml.cpp \ + xml_lex.yy.cpp \ + xml_parse_tree.cpp \ + xml_parser.cpp \ + xml_y.tab.cpp \ + # Empty last line INCLUDES= -I .. include ../config.inc diff --git a/unit/Makefile b/unit/Makefile index 007ebd3c70d..049d3f84ac0 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,8 +1,17 @@ -SRC = cpp_parser.cpp cpp_scanner.cpp elf_reader.cpp float_utils.cpp \ - ieee_float.cpp json.cpp miniBDD.cpp osx_fat_reader.cpp \ - smt2_parser.cpp wp.cpp string_utils.cpp \ +SRC = cpp_parser.cpp \ + cpp_scanner.cpp \ + elf_reader.cpp \ + float_utils.cpp \ + ieee_float.cpp \ + json.cpp \ + miniBDD.cpp \ + osx_fat_reader.cpp \ sharing_map.cpp \ - sharing_node.cpp + sharing_node.cpp \ + smt2_parser.cpp \ + string_utils.cpp \ + wp.cpp \ + # Empty last line INCLUDES= -I ../src/