From 54d581bcf2227c27a515717e3316e70d7128ab3d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 23:15:41 +0000 Subject: [PATCH 01/16] Allow disabling optimized assertion conversion Cannot be used with incremental loop unwinding. --- src/goto-symex/symex_target_equation.cpp | 5 +++-- src/goto-symex/symex_target_equation.h | 6 +++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index affa572a95e..fdfd856fafb 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -451,7 +451,8 @@ void symex_target_equationt::convert_constraints( } void symex_target_equationt::convert_assertions( - decision_proceduret &decision_procedure) + decision_proceduret &decision_procedure, + bool optimized_for_single_assertions) { // we find out if there is only _one_ assertion, // which allows for a simpler formula @@ -461,7 +462,7 @@ void symex_target_equationt::convert_assertions( if(number_of_assertions==0) return; - if(number_of_assertions==1) + if(number_of_assertions == 1 && optimized_for_single_assertions) { for(auto &step : SSA_steps) { diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 1106d1001f1..4a0c9de3ca7 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -194,7 +194,11 @@ class symex_target_equationt:public symex_targett /// Converts assertions: build a disjunction of negated assertions. /// \param decision_procedure: A handle to a decision procedure interface - void convert_assertions(decision_proceduret &decision_procedure); + /// \param optimized_for_single_assertions: Use an optimized encoding for + /// single assertions (unsound for incremental conversions) + void convert_assertions( + decision_proceduret &decision_procedure, + bool optimized_for_single_assertions = true); /// Converts constraints: set the represented condition to _True_. /// \param decision_procedure: A handle to a decision procedure interface From 452b524c23e721428c8f1c39491b1b728a21a691 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 23:16:15 +0000 Subject: [PATCH 02/16] Hidden field is used for hiding in trace not 'ignore' (which is used for slicing). --- src/goto-symex/symex_target_equation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index fdfd856fafb..c3f3283d9b1 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -468,7 +468,7 @@ void symex_target_equationt::convert_assertions( { // ignore already converted assertions in the error trace if(step.is_assert() && step.converted) - step.ignore = true; + step.hidden = true; if(step.is_assert() && !step.ignore && !step.converted) { @@ -495,7 +495,7 @@ void symex_target_equationt::convert_assertions( { // ignore already converted assertions in the error trace if(step.is_assert() && step.converted) - step.ignore = true; + step.hidden = true; if(step.is_assert() && !step.ignore && !step.converted) { From 1fb7d2d1642e5606b9caadae8d058a23c2124bc1 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 3 Feb 2019 14:56:44 +0000 Subject: [PATCH 03/16] Allow symex to temporarily ignore assertions Allows ignoring assertions until a certain condition is satisfied (e.g. a certain unwinding is reached). Used for implementation of ignore-assertions-before-unwind-min. --- src/goto-symex/goto_symex.h | 4 ++++ src/goto-symex/symex_main.cpp | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 12be632efb2..e0c1c6b8888 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -197,6 +197,10 @@ class goto_symext /// symbolic execution from that state. bool should_pause_symex; + /// If this flag is set to true then assertions will be temporarily ignored + /// by the symbolic executions. + bool ignore_assertions = false; + protected: /// The configuration to use for this symbolic execution const symex_configt symex_config; diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index fab1cb1bbf7..cbe35e3158c 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -566,7 +566,7 @@ void goto_symext::execute_next_instruction( break; case ASSERT: - if(!state.guard.is_false()) + if(!state.guard.is_false() && !ignore_assertions) symex_assert(instruction, state); symex_transition(state); break; From 73fb826eb9dfd47e8a2f318c7f6859f7c23bd427 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 3 Feb 2019 17:09:50 +0000 Subject: [PATCH 04/16] Allow symex_target_equationt to separately convert assertions This enables the caller to handle assertion conversion differently, e.g. for incremental loop unwinding. --- src/goto-symex/symex_target_equation.cpp | 13 +++++++++++++ src/goto-symex/symex_target_equation.h | 9 +++++++++ 2 files changed, 22 insertions(+) diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index c3f3283d9b1..3841b6acba3 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -321,6 +321,19 @@ void symex_target_equationt::constraint( merge_ireps(SSA_step); } +void symex_target_equationt::convert_without_assertions( + decision_proceduret &decision_procedure) +{ + convert_guards(decision_procedure); + convert_assignments(decision_procedure); + convert_decls(decision_procedure); + convert_assumptions(decision_procedure); + convert_goto_instructions(decision_procedure); + convert_function_calls(decision_procedure); + convert_io(decision_procedure); + convert_constraints(decision_procedure); +} + void symex_target_equationt::convert(decision_proceduret &decision_procedure) { convert_guards(decision_procedure); diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index 4a0c9de3ca7..2fd897f814c 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -177,6 +177,15 @@ class symex_target_equationt:public symex_targett /// \param decision_procedure: A handle to a decision procedure interface void convert(decision_proceduret &decision_procedure); + /// Interface method to initiate the conversion into a decision procedure + /// format. The method iterates over the equation, i.e. over the SSA steps and + /// converts each type of step separately, except assertions. + /// This enables the caller to handle assertion conversion differently, + /// e.g. for incremental solving. + /// \param decision_procedure: A handle to a particular decision procedure + /// interface + void convert_without_assertions(decision_proceduret &decision_procedure); + /// Converts assignments: set the equality _lhs==rhs_ to _True_. /// \param decision_procedure: A handle to a decision procedure /// interface From 41d3864bf70e6208135aecee20ead1aa0e9efa87 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 23:12:01 +0000 Subject: [PATCH 05/16] Use only remaining properties in property decider We can ignore already failed properties. --- src/goto-checker/goto_symex_property_decider.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index 432cb7e2d2c..5515529a79e 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -43,6 +43,8 @@ exprt goto_symex_property_decidert::goalt::as_expr() const void goto_symex_property_decidert:: update_properties_goals_from_symex_target_equation(propertiest &properties) { + goal_map.clear(); + for(symex_target_equationt::SSA_stepst::iterator it = equation.SSA_steps.begin(); it != equation.SSA_steps.end(); From 7fbc6b030f41efd207e35c5ef9eb4bd31ed7902d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 11:23:19 +0000 Subject: [PATCH 06/16] Add callback to decide on interrupting goto-symex Required for incremental loop unwinding. --- src/goto-symex/goto_symex.h | 7 +++++++ src/goto-symex/symex_goto.cpp | 17 +++++++++++++++++ 2 files changed, 24 insertions(+) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index e0c1c6b8888..19f31641b87 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -201,6 +201,13 @@ class goto_symext /// by the symbolic executions. bool ignore_assertions = false; + virtual bool check_break( + const irep_idt &id, + bool is_function, + statet &state, + const exprt &cond, + unsigned unwind); + protected: /// The configuration to use for this symbolic execution const symex_configt symex_config; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index cd019962740..ddf3d0cd358 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -288,6 +288,7 @@ void goto_symext::symex_goto(statet &state) if(should_stop_unwind(state.source, state.call_stack(), unwind)) { + // we break the loop loop_bound_exceeded(state, new_guard); // next instruction @@ -297,6 +298,11 @@ void goto_symext::symex_goto(statet &state) if(new_guard.is_true()) { + // we continue executing the loop + if(check_break(loop_id, false, state, new_guard, unwind)) + { + should_pause_symex = true; + } symex_transition(state, goto_target, true); return; // nothing else to do } @@ -516,6 +522,17 @@ void goto_symext::symex_goto(statet &state) } } +bool goto_symext::check_break( + const irep_idt &id, + bool is_function, + statet &state, + const exprt &cond, + unsigned unwind) +{ + // dummy implementation + return false; +} + void goto_symext::merge_gotos(statet &state) { framet &frame = state.call_stack().top(); From 2a7b16c125a04302b8d5831d4371c47444eba742 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 11:23:58 +0000 Subject: [PATCH 07/16] Add symex BMC incremental one loop Implement callback that decides on when to interrupt goto-symex during incremental unwinding. --- src/goto-checker/Makefile | 1 + .../symex_bmc_incremental_one_loop.cpp | 133 ++++++++++++++++++ .../symex_bmc_incremental_one_loop.h | 54 +++++++ 3 files changed, 188 insertions(+) create mode 100644 src/goto-checker/symex_bmc_incremental_one_loop.cpp create mode 100644 src/goto-checker/symex_bmc_incremental_one_loop.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index c96f85066e3..06bdd1357e2 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -15,6 +15,7 @@ SRC = bmc_util.cpp \ solver_factory.cpp \ symex_coverage.cpp \ symex_bmc.cpp \ + symex_bmc_incremental_one_loop.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp new file mode 100644 index 00000000000..1c3a9750096 --- /dev/null +++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp @@ -0,0 +1,133 @@ +/*******************************************************************\ + +Module: Incremental Bounded Model Checking for ANSI-C + +Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include + +#include +#include + +#include "symex_bmc_incremental_one_loop.h" + +symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt( + message_handlert &message_handler, + const symbol_tablet &outer_symbol_table, + symex_target_equationt &target, + const optionst &options, + path_storaget &path_storage, + guard_managert &guard_manager) + : symex_bmct( + message_handler, + outer_symbol_table, + target, + options, + path_storage, + guard_manager), + incr_loop_id(options.get_option("incremental-loop")), + incr_max_unwind( + options.is_set("unwind-max") ? options.get_signed_int_option("unwind-max") + : std::numeric_limits::max()), + incr_min_unwind( + options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min") + : 0) +{ +} + +bool symex_bmc_incremental_one_loopt::should_stop_unwind( + const symex_targett::sourcet &source, + const call_stackt &context, + unsigned unwind) +{ + const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc); + + tvt abort_unwind_decision; + unsigned this_loop_limit = std::numeric_limits::max(); + + // use the incremental limits if it is the specified incremental loop + if(id == incr_loop_id) + { + this_loop_limit = incr_max_unwind; + if(unwind + 1 >= incr_min_unwind) + ignore_assertions = false; + abort_unwind_decision = tvt(unwind >= this_loop_limit); + } + else + { + for(auto handler : loop_unwind_handlers) + { + abort_unwind_decision = + handler(context, source.pc->loop_number, unwind, this_loop_limit); + if(abort_unwind_decision.is_known()) + break; + } + + // If no handler gave an opinion, use standard command-line --unwindset + // / --unwind options to decide: + if(abort_unwind_decision.is_unknown()) + { + auto limit = unwindset.get_limit(id, source.thread_nr); + + if(!limit.has_value()) + abort_unwind_decision = tvt(false); + else + abort_unwind_decision = tvt(unwind >= *limit); + } + } + + INVARIANT( + abort_unwind_decision.is_known(), "unwind decision should be taken by now"); + bool abort = abort_unwind_decision.is_true(); + + log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id + << " iteration " << unwind; + + if(this_loop_limit != std::numeric_limits::max()) + log.statistics() << " (" << this_loop_limit << " max)"; + + log.statistics() << " " << source.pc->source_location << " thread " + << source.thread_nr << log.eom; + + return abort; +} + +/// Defines condition for interrupting symbolic execution for incremental BMC +/// \return True if the back edge encountered during symbolic execution +/// corresponds to the given loop (incr_loop_id) +bool symex_bmc_incremental_one_loopt::check_break( + const irep_idt &id, + bool is_function, + statet &state, + const exprt &cond, + unsigned unwind) +{ + if(unwind < incr_min_unwind) + return false; + + // loop specified by incremental-loop + return (id == incr_loop_id); +} + +bool symex_bmc_incremental_one_loopt::from_entry_point_of( + const get_goto_functiont &get_goto_function, + symbol_tablet &new_symbol_table) +{ + state = initialize_entry_point_state(get_goto_function); + + symex_with_state(*state, get_goto_function, new_symbol_table); + + return should_pause_symex; +} + +bool symex_bmc_incremental_one_loopt::resume( + const get_goto_functiont &get_goto_function) +{ + should_pause_symex = false; + + symex_with_state(*state, get_goto_function, state->symbol_table); + + return should_pause_symex; +} diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.h b/src/goto-checker/symex_bmc_incremental_one_loop.h new file mode 100644 index 00000000000..e3aed2eee3e --- /dev/null +++ b/src/goto-checker/symex_bmc_incremental_one_loop.h @@ -0,0 +1,54 @@ +/*******************************************************************\ + + Module: Incremental Bounded Model Checking for ANSI-C + + Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H +#define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H + +#include "symex_bmc.h" + +class symex_bmc_incremental_one_loopt : public symex_bmct +{ +public: + symex_bmc_incremental_one_loopt( + message_handlert &, + const symbol_tablet &outer_symbol_table, + symex_target_equationt &, + const optionst &, + path_storaget &, + guard_managert &); + + /// Return true if symex can be resumed + bool from_entry_point_of( + const get_goto_functiont &get_goto_function, + symbol_tablet &new_symbol_table); + + /// Return true if symex can be resumed + bool resume(const get_goto_functiont &get_goto_function); + +protected: + const irep_idt incr_loop_id; + const unsigned incr_max_unwind; + const unsigned incr_min_unwind; + + std::unique_ptr state; + + // returns true if the symbolic execution is to be interrupted for checking + bool check_break( + const irep_idt &id, + bool is_function, + goto_symext::statet &state, + const exprt &cond, + unsigned unwind) override; + + bool should_stop_unwind( + const symex_targett::sourcet &source, + const call_stackt &context, + unsigned unwind) override; +}; + +#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H From cef212c5cac4396193a30793c37d4a5696206d53 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 2 Feb 2019 22:58:41 +0000 Subject: [PATCH 08/16] Add single-loop incremental symex checker Checks the assertions after each iteration of a specified loop. --- src/goto-checker/Makefile | 1 + .../single_loop_incremental_symex_checker.cpp | 227 ++++++++++++++++++ .../single_loop_incremental_symex_checker.h | 65 +++++ 3 files changed, 293 insertions(+) create mode 100644 src/goto-checker/single_loop_incremental_symex_checker.cpp create mode 100644 src/goto-checker/single_loop_incremental_symex_checker.h diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index 06bdd1357e2..cb8243ecbc1 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -10,6 +10,7 @@ SRC = bmc_util.cpp \ multi_path_symex_only_checker.cpp \ properties.cpp \ report_util.cpp \ + single_loop_incremental_symex_checker.cpp \ single_path_symex_checker.cpp \ single_path_symex_only_checker.cpp \ solver_factory.cpp \ diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp new file mode 100644 index 00000000000..2c473d2aff7 --- /dev/null +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -0,0 +1,227 @@ +/*******************************************************************\ + +Module: Goto Checker using Multi-Path Symbolic Execution + with Incremental Unwinding of a specified Loop + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using multi-path symbolic execution with incremental +/// unwinding of a specified loop + +#include "single_loop_incremental_symex_checker.h" + +#include + +#include + +#include "bmc_util.h" +#include "counterexample_beautification.h" + +single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model) + : incremental_goto_checkert(options, ui_message_handler), + goto_model(goto_model), + ns(goto_model.get_symbol_table(), symex_symbol_table), + equation(ui_message_handler), + symex( + ui_message_handler, + goto_model.get_symbol_table(), + equation, + options, + path_storage, + guard_manager), + property_decider(options, ui_message_handler, equation, ns) +{ + setup_symex(symex, ns, options, ui_message_handler); + + // Freeze all symbols if we are using a prop_conv_solvert + prop_conv_solvert *prop_conv_solver = dynamic_cast( + &property_decider.get_stack_decision_procedure()); + if(prop_conv_solver != nullptr) + prop_conv_solver->set_all_frozen(); +} + +incremental_goto_checkert::resultt single_loop_incremental_symex_checkert:: +operator()(propertiest &properties) +{ + resultt result(resultt::progresst::DONE); + + std::chrono::duration solver_runtime(0); + + // we haven't got an equation yet + if(!initial_equation_generated) + { + full_equation_generated = !symex.from_entry_point_of( + goto_symext::get_goto_function(goto_model), symex_symbol_table); + + // This might add new properties such as unwinding assertions, for instance. + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, equation); + + initial_equation_generated = true; + } + + while(has_properties_to_check(properties)) + { + // There are NOT_CHECKED or UNKNOWN properties. + + if(count_properties(properties, property_statust::UNKNOWN) > 0) + { + // We have UNKNOWN properties, i.e. properties that we can check + // on the current equation. + + log.status() + << "Passing problem to " + << property_decider.get_decision_procedure().decision_procedure_text() + << messaget::eom; + + const auto solver_start = std::chrono::steady_clock::now(); + + if(!current_equation_converted) + { + postprocess_equation(symex, equation, options, ns, ui_message_handler); + + log.status() << "converting SSA" << messaget::eom; + equation.convert_without_assertions( + property_decider.get_decision_procedure()); + + property_decider.update_properties_goals_from_symex_target_equation( + properties); + + // We convert the assertions in a new context. + property_decider.get_stack_decision_procedure().push(); + equation.convert_assertions( + property_decider.get_decision_procedure(), false); + property_decider.convert_goals(); + + current_equation_converted = true; + } + + property_decider.add_constraint_from_goals( + [&properties](const irep_idt &property_id) { + return is_property_to_check(properties.at(property_id).status); + }); + + log.status() + << "Running " + << property_decider.get_decision_procedure().decision_procedure_text() + << messaget::eom; + + decision_proceduret::resultt dec_result = property_decider.solve(); + + property_decider.update_properties_status_from_goals( + properties, result.updated_properties, dec_result, false); + + const auto solver_stop = std::chrono::steady_clock::now(); + solver_runtime += + std::chrono::duration(solver_stop - solver_start); + log.status() << "Runtime decision procedure: " << solver_runtime.count() + << "s" << messaget::eom; + + result.progress = + dec_result == decision_proceduret::resultt::D_SATISFIABLE + ? resultt::progresst::FOUND_FAIL + : resultt::progresst::DONE; + + // We've got a trace to report. + if(result.progress == resultt::progresst::FOUND_FAIL) + break; + + // Nothing else to do with the current set of assertions. + // Let's pop them. + property_decider.get_stack_decision_procedure().pop(); + } + + // Now we are finally done. + if(full_equation_generated) + { + // For now, we assume that UNKNOWN properties are PASS. + update_status_of_unknown_properties( + properties, result.updated_properties); + + // For now, we assume that NOT_REACHED properties are PASS. + update_status_of_not_checked_properties( + properties, result.updated_properties); + + break; + } + + // We continue symbolic execution + full_equation_generated = + !symex.resume(goto_symext::get_goto_function(goto_model)); + revert_slice(equation); + + // This might add new properties such as unwinding assertions, for instance. + update_properties_status_from_symex_target_equation( + properties, result.updated_properties, equation); + + current_equation_converted = false; + } + + return result; +} + +goto_tracet single_loop_incremental_symex_checkert::build_full_trace() const +{ + goto_tracet goto_trace; + build_goto_trace( + equation, + equation.SSA_steps.end(), + property_decider.get_decision_procedure(), + ns, + goto_trace); + + return goto_trace; +} + +goto_tracet single_loop_incremental_symex_checkert::build_shortest_trace() const +{ + if(options.get_bool_option("beautify")) + { + // NOLINTNEXTLINE(whitespace/braces) + counterexample_beautificationt{ui_message_handler}( + dynamic_cast(property_decider.get_stack_decision_procedure()), + equation); + } + + goto_tracet goto_trace; + build_goto_trace( + equation, property_decider.get_decision_procedure(), ns, goto_trace); + + return goto_trace; +} + +goto_tracet single_loop_incremental_symex_checkert::build_trace( + const irep_idt &property_id) const +{ + goto_tracet goto_trace; + build_goto_trace( + equation, + ssa_step_matches_failing_property(property_id), + property_decider.get_decision_procedure(), + ns, + goto_trace); + + return goto_trace; +} + +const namespacet &single_loop_incremental_symex_checkert::get_namespace() const +{ + return ns; +} + +void single_loop_incremental_symex_checkert::output_proof() +{ + output_graphml(equation, ns, options); +} + +void single_loop_incremental_symex_checkert::output_error_witness( + const goto_tracet &error_trace) +{ + output_graphml(error_trace, ns, options); +} diff --git a/src/goto-checker/single_loop_incremental_symex_checker.h b/src/goto-checker/single_loop_incremental_symex_checker.h new file mode 100644 index 00000000000..69883a7486d --- /dev/null +++ b/src/goto-checker/single_loop_incremental_symex_checker.h @@ -0,0 +1,65 @@ +/*******************************************************************\ + +Module: Goto Checker using Multi-Path Symbolic Execution + with Incremental Unwinding of a specified Loop + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Goto Checker using multi-path symbolic execution with incremental +/// unwinding of a specified loop + +#ifndef CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H +#define CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H + +#include "goto_symex_property_decider.h" +#include "goto_trace_provider.h" +#include "incremental_goto_checker.h" +#include "symex_bmc_incremental_one_loop.h" +#include "witness_provider.h" + +/// Performs a multi-path symbolic execution using goto-symex +/// that incrementally unwinds a given loop +/// and calls a SAT/SMT solver to check the status of the properties +/// after each iteration. +class single_loop_incremental_symex_checkert : public incremental_goto_checkert, + public goto_trace_providert, + public witness_providert +{ +public: + single_loop_incremental_symex_checkert( + const optionst &options, + ui_message_handlert &ui_message_handler, + abstract_goto_modelt &goto_model); + + /// \copydoc incremental_goto_checkert::operator()(propertiest &properties) + /// + /// Note: This operator can handle shrinking and expanding sets of properties + /// in repeated invocations. + resultt operator()(propertiest &) override; + + goto_tracet build_full_trace() const override; + goto_tracet build_trace(const irep_idt &) const override; + goto_tracet build_shortest_trace() const override; + const namespacet &get_namespace() const override; + + void output_error_witness(const goto_tracet &) override; + void output_proof() override; + +protected: + abstract_goto_modelt &goto_model; + symbol_tablet symex_symbol_table; + namespacet ns; + symex_target_equationt equation; + path_fifot path_storage; // should go away + guard_managert guard_manager; + symex_bmc_incremental_one_loopt symex; + bool initial_equation_generated = false; + bool full_equation_generated = false; + bool current_equation_converted = false; + goto_symex_property_decidert property_decider; +}; + +#endif // CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H From 4e894a4f2d2ad582cac66b440f2c434ec4f85b53 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 3 Feb 2019 14:28:36 +0000 Subject: [PATCH 09/16] Add options for incremental one-loop BMC for incremental unwinding and assertion checking of a specified loop. --- src/goto-checker/bmc_util.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 3eaf779efdd..586bb2ecd6c 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -188,7 +188,10 @@ void run_property_decider( "(unwind):" \ "(unwindset):" \ "(graphml-witness):" \ - "(unwindset):" + "(incremental-loop):" \ + "(unwind-min):" \ + "(unwind-max):" \ + "(ignore-properties-before-unwind-min)" #define HELP_BMC \ " --paths [strategy] explore paths one at a time\n" \ @@ -201,6 +204,14 @@ void run_property_decider( " --unwind nr unwind nr times\n" \ " --unwindset L:B,... unwind loop L with a bound of B\n" \ " (use --show-loops to get the loop IDs)\n" \ + " --incremental-loop L check properties after each unwinding\n" \ + " of loop L\n" \ + " (use --show-loops to get the loop IDs)\n" \ + " --unwind-min nr start incremental-loop after nr unwindings\n" \ + " --unwind-max nr stop incremental-loop after nr unwindings\n" \ + " --ignore-properties-before-unwind-min\n" \ + " do not check properties before unwind-min\n" \ + " when using incremental-loop\n" \ " --show-vcc show the verification conditions\n" \ " --slice-formula remove assignments unrelated to property\n" \ " --unwinding-assertions generate unwinding assertions (cannot be\n" \ From d7581bd3eb10dd7c09e8eaef67624ffe3dd83fb8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 3 Feb 2019 15:57:44 +0000 Subject: [PATCH 10/16] Add --incremental-loop to CBMC for incremental unwinding and assertion checking of a specified loop. --- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + src/cbmc/cbmc_parse_options.cpp | 42 ++++++++++++++++++++++++++++++++- 3 files changed, 43 insertions(+), 1 deletion(-) diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index a32af852c52..501432e6433 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -31,6 +31,7 @@ add_subdirectory(goto-instrument) add_subdirectory(cpp) add_subdirectory(cbmc-concurrency) add_subdirectory(cbmc-cover) +add_subdirectory(cbmc-incr-oneloop) add_subdirectory(goto-instrument-typedef) add_subdirectory(smt2_solver) add_subdirectory(smt2_strings) diff --git a/regression/Makefile b/regression/Makefile index e4bb8dde0ca..203c0ebec97 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -9,6 +9,7 @@ DIRS = cbmc \ cpp \ cbmc-concurrency \ cbmc-cover \ + cbmc-incr-oneloop \ goto-instrument-typedef \ smt2_solver \ smt2_strings \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a978de62730..7b63dada9b3 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -42,6 +42,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -341,6 +342,30 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) "max-node-refinement", cmdline.get_value("max-node-refinement")); + if(cmdline.isset("incremental-loop")) + { + options.set_option( + "incremental-loop", cmdline.get_value("incremental-loop")); + options.set_option("refine", true); + options.set_option("refine-arrays", true); + + if(cmdline.isset("unwind-min")) + options.set_option("unwind-min", cmdline.get_value("unwind-min")); + + if(cmdline.isset("unwind-max")) + options.set_option("unwind-max", cmdline.get_value("unwind-max")); + + if(cmdline.isset("ignore-properties-before-unwind-min")) + options.set_option("ignore-properties-before-unwind-min", true); + + if(cmdline.isset("paths")) + { + log.error() << "--paths not supported with --incremental-loop" + << messaget::eom; + exit(CPROVER_EXIT_USAGE_ERROR); + } + } + // SMT Options if(cmdline.isset("smt1")) @@ -630,7 +655,22 @@ int cbmc_parse_optionst::doit() std::unique_ptr verifier = nullptr; - if( + if(options.is_set("incremental-loop")) + { + if(options.get_bool_option("stop-on-fail")) + { + verifier = util_make_unique< + stop_on_fail_verifiert>( + options, ui_message_handler, goto_model); + } + else + { + verifier = util_make_unique>( + options, ui_message_handler, goto_model); + } + } + else if( options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { verifier = From 30ca9861282de23ea05eb5cdd6c4c27dcf269c90 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 23:08:55 +0000 Subject: [PATCH 11/16] Fix quoting in test command Otherwise single quotes get incorrectly stripped off. --- regression/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 501432e6433..d47f7a6cd87 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl") macro(add_test_pl_profile name cmdline flag profile) add_test( NAME "${name}-${profile}" - COMMAND ${test_pl_path} -e -p -c ${cmdline} ${flag} ${ARGN} + COMMAND ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN} WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" ) set_tests_properties("${name}-${profile}" PROPERTIES From aa1389b8213d4690526c31da4242ea3ec16aa3ed Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Mar 2019 18:18:40 +0000 Subject: [PATCH 12/16] Make sure output buffers are flushed before writing exit code This seems to work when calling bash again. Otherwise, we can get something like: This is half a liEXIT=123 --- regression/test.pl | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/regression/test.pl b/regression/test.pl index afc080c7b10..7ef8c35df37 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -53,10 +53,7 @@ ($$$$$) } } - open my $FH, ">>$name/$output"; - print $FH "EXIT=$exit_value\n"; - print $FH "SIGNAL=$signal_num\n"; - close $FH; + system("bash", "-c", "cd '$name' ; echo '\nEXIT=$exit_value\nSIGNAL=$signal_num\n' >> '$output'"); if($signal_num == 2) { print "\nProgram under test interrupted; stopping\n"; From 657a899bd92577eec04a3a48ef332c141436b0d3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 9 Feb 2019 11:50:55 +0000 Subject: [PATCH 13/16] Clean up cbmc-incr-oneloop tests Option name has changed. --- regression/cbmc-incr-oneloop/CMakeLists.txt | 3 ++ regression/cbmc-incr-oneloop/Makefile | 4 +-- regression/cbmc-incr-oneloop/alarm1/test.desc | 2 +- regression/cbmc-incr-oneloop/alarm2/test.desc | 2 +- regression/cbmc-incr-oneloop/alarm3/test.desc | 2 +- .../cbmc-incr-oneloop/arrays2/test.desc | 2 +- .../cbmc-incr-oneloop/arrays3/test.desc | 2 +- .../cbmc-incr-oneloop/arrays4/test.desc | 2 +- .../cbmc-incr-oneloop/arrays5/test.desc | 2 +- .../assertion-after-loop1/test.desc | 2 +- .../assertion-after-loop2/test.desc | 2 +- .../cbmc-incr-oneloop/cruise1/test.desc | 2 +- .../cbmc-incr-oneloop/cruise2/test.desc | 2 +- .../cbmc-incr-oneloop/induction1/test.desc | 2 +- .../cbmc-incr-oneloop/induction2/test.desc | 2 +- .../cbmc-incr-oneloop/minmaxunwind1/test.desc | 2 +- .../cbmc-incr-oneloop/minmaxunwind2/test.desc | 2 +- .../cbmc-incr-oneloop/minmaxunwind3/test.desc | 2 +- .../cbmc-incr-oneloop/minmaxunwind4/test.desc | 2 +- .../cbmc-incr-oneloop/minmaxunwind5/test.desc | 2 +- .../cbmc-incr-oneloop/moreasserts1/test.desc | 2 +- .../cbmc-incr-oneloop/nestedloop1/main.c | 4 +-- .../cbmc-incr-oneloop/nestedloop1/test.desc | 2 +- .../no-unwinding-assertion1/test.desc | 2 +- .../cbmc-incr-oneloop/simpleloop1/test.desc | 2 +- .../cbmc-incr-oneloop/simpleloop2/test.desc | 2 +- .../cbmc-incr-oneloop/simpleloop3/test.desc | 2 +- .../simpleloopmax1/test.desc | 2 +- .../simpleloopmax2/test.desc | 2 +- .../cbmc-incr-oneloop/simplifier1/test.desc | 2 +- .../cbmc-incr-oneloop/simplifier2/test.desc | 2 +- .../cbmc-incr-oneloop/simplifier3/test.desc | 2 +- .../cbmc-incr-oneloop/unwind-forever1/main.c | 4 +-- .../unwind-forever1/test.desc | 9 ++++-- .../cbmc-incr-oneloop/unwind-forever2/main.c | 3 +- .../unwind-forever2/test.desc | 10 +++++-- .../unwind-more-loops1/main.c | 16 +++++++++++ .../unwind-more-loops1/test.desc | 11 ++++++++ .../unwinding-assertion1/test.desc | 2 +- .../unwindset-more-loops1/main.c | 28 +++++++++++++++++++ .../unwindset-more-loops1/test.desc | 13 +++++++++ 41 files changed, 122 insertions(+), 43 deletions(-) create mode 100644 regression/cbmc-incr-oneloop/CMakeLists.txt create mode 100644 regression/cbmc-incr-oneloop/unwind-more-loops1/main.c create mode 100644 regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc create mode 100644 regression/cbmc-incr-oneloop/unwindset-more-loops1/main.c create mode 100644 regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc diff --git a/regression/cbmc-incr-oneloop/CMakeLists.txt b/regression/cbmc-incr-oneloop/CMakeLists.txt new file mode 100644 index 00000000000..96b0b3752b5 --- /dev/null +++ b/regression/cbmc-incr-oneloop/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "perl -e 'alarm shift @ARGV; exec @ARGV' 8 $ --slice-formula" +) diff --git a/regression/cbmc-incr-oneloop/Makefile b/regression/cbmc-incr-oneloop/Makefile index 00c5ea25db4..6773ae30f00 100644 --- a/regression/cbmc-incr-oneloop/Makefile +++ b/regression/cbmc-incr-oneloop/Makefile @@ -1,10 +1,10 @@ default: tests.log test: - @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula" + @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula" tests.log: ../test.pl - @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula" + @../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula" show: @for dir in *; do \ diff --git a/regression/cbmc-incr-oneloop/alarm1/test.desc b/regression/cbmc-incr-oneloop/alarm1/test.desc index 60fffddc0f1..70a9179b47d 100644 --- a/regression/cbmc-incr-oneloop/alarm1/test.desc +++ b/regression/cbmc-incr-oneloop/alarm1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 25 --no-unwinding-assertions +--incremental-loop main.0 --unwind-max 15 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index 24d03b681e1..817773abe11 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-min 5 --unwind-max 10 --no-unwinding-assertions +--incremental-loop main.0 --unwind-min 5 --unwind-max 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/alarm3/test.desc b/regression/cbmc-incr-oneloop/alarm3/test.desc index a0f2422aed8..b16aa422ea9 100644 --- a/regression/cbmc-incr-oneloop/alarm3/test.desc +++ b/regression/cbmc-incr-oneloop/alarm3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 +--incremental-loop main.0 --unwind-max 15 --unwinding-assertions ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/arrays2/test.desc b/regression/cbmc-incr-oneloop/arrays2/test.desc index 38db436af85..3eb87deeff5 100644 --- a/regression/cbmc-incr-oneloop/arrays2/test.desc +++ b/regression/cbmc-incr-oneloop/arrays2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions --arrays-uf-always +--incremental-loop main.0 --unwind-max 5 --arrays-uf-always ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/arrays3/test.desc b/regression/cbmc-incr-oneloop/arrays3/test.desc index a30ed0ce8ca..0aac0af59f1 100644 --- a/regression/cbmc-incr-oneloop/arrays3/test.desc +++ b/regression/cbmc-incr-oneloop/arrays3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --no-unwinding-assertions --arrays-uf-always +--incremental-loop main.0 --arrays-uf-always ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/arrays4/test.desc b/regression/cbmc-incr-oneloop/arrays4/test.desc index a30ed0ce8ca..0aac0af59f1 100644 --- a/regression/cbmc-incr-oneloop/arrays4/test.desc +++ b/regression/cbmc-incr-oneloop/arrays4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --no-unwinding-assertions --arrays-uf-always +--incremental-loop main.0 --arrays-uf-always ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/arrays5/test.desc b/regression/cbmc-incr-oneloop/arrays5/test.desc index be9a157500d..2ce7fd6f126 100644 --- a/regression/cbmc-incr-oneloop/arrays5/test.desc +++ b/regression/cbmc-incr-oneloop/arrays5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions --arrays-uf-always +--incremental-loop main.0 --unwind-max 5 --arrays-uf-always ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/assertion-after-loop1/test.desc b/regression/cbmc-incr-oneloop/assertion-after-loop1/test.desc index ede388a6053..c090ea9d5e9 100644 --- a/regression/cbmc-incr-oneloop/assertion-after-loop1/test.desc +++ b/regression/cbmc-incr-oneloop/assertion-after-loop1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-max 10 --incremental-check main.0 +--unwind-max 10 --incremental-loop main.0 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/assertion-after-loop2/test.desc b/regression/cbmc-incr-oneloop/assertion-after-loop2/test.desc index b93239c7cd6..fb2b8088599 100644 --- a/regression/cbmc-incr-oneloop/assertion-after-loop2/test.desc +++ b/regression/cbmc-incr-oneloop/assertion-after-loop2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-max 10 --incremental-check main.0 +--unwind-max 10 --incremental-loop main.0 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/cruise1/test.desc b/regression/cbmc-incr-oneloop/cruise1/test.desc index 8c8e072de04..19e1f90f4c4 100644 --- a/regression/cbmc-incr-oneloop/cruise1/test.desc +++ b/regression/cbmc-incr-oneloop/cruise1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 10 --no-unwinding-assertions +--incremental-loop main.0 --unwind-max 10 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/cruise2/test.desc b/regression/cbmc-incr-oneloop/cruise2/test.desc index a0f2422aed8..c990fab7e06 100644 --- a/regression/cbmc-incr-oneloop/cruise2/test.desc +++ b/regression/cbmc-incr-oneloop/cruise2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 +--incremental-loop main.0 --unwind-max 10 --unwinding-assertions ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/induction1/test.desc b/regression/cbmc-incr-oneloop/induction1/test.desc index f5b70e5960d..d5669341585 100644 --- a/regression/cbmc-incr-oneloop/induction1/test.desc +++ b/regression/cbmc-incr-oneloop/induction1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --stop-when-unsat --no-unwinding-assertions +--incremental-loop main.0 --stop-when-unsat ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/induction2/test.desc b/regression/cbmc-incr-oneloop/induction2/test.desc index f5b70e5960d..d5669341585 100644 --- a/regression/cbmc-incr-oneloop/induction2/test.desc +++ b/regression/cbmc-incr-oneloop/induction2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --stop-when-unsat --no-unwinding-assertions +--incremental-loop main.0 --stop-when-unsat ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind1/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind1/test.desc index edddedee357..b0e06380fb6 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind1/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-min 4 --unwind-max 6 --incremental-check main.0 +--unwind-min 4 --unwind-max 6 --incremental-loop main.0 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind2/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind2/test.desc index 0ff1bda9ea3..2f48e896848 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind2/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-min 5 --unwind-max 5 --incremental-check main.0 +--unwind-min 5 --unwind-max 5 --incremental-loop main.0 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc index 23166b0008b..72879e32fe5 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-min 2 --unwind-max 4 --incremental-check main.0 +--unwind-min 2 --unwind-max 4 --incremental-loop main.0 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc index 1e1f7c33111..bf0f6adb768 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-min 6 --unwind-max 8 --incremental-check main.0 +--unwind-min 6 --unwind-max 8 --incremental-loop main.0 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/minmaxunwind5/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind5/test.desc index c06f1862229..21470cb0a0c 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind5/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-min 4 --unwind-max 6 --incremental-check main.1 +--unwind-min 4 --unwind-max 6 --incremental-loop main.1 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/moreasserts1/test.desc b/regression/cbmc-incr-oneloop/moreasserts1/test.desc index a0f2422aed8..a5d9b3bd58a 100644 --- a/regression/cbmc-incr-oneloop/moreasserts1/test.desc +++ b/regression/cbmc-incr-oneloop/moreasserts1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 +--incremental-loop main.0 --unwinding-assertions --stop-on-fail ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/nestedloop1/main.c b/regression/cbmc-incr-oneloop/nestedloop1/main.c index d8662458577..7d13f71803d 100644 --- a/regression/cbmc-incr-oneloop/nestedloop1/main.c +++ b/regression/cbmc-incr-oneloop/nestedloop1/main.c @@ -3,9 +3,9 @@ int main() { int x = nondet_int(); __CPROVER_assume(0<=x && x<=1); - while(x<4) { + while(x<4) { // main.1 int y = 5; - while(y>2) y-=2; + while(y>2) y-=2; // main.0 x=x+y; assert(x<4); } diff --git a/regression/cbmc-incr-oneloop/nestedloop1/test.desc b/regression/cbmc-incr-oneloop/nestedloop1/test.desc index a0f2422aed8..1a08157fa07 100644 --- a/regression/cbmc-incr-oneloop/nestedloop1/test.desc +++ b/regression/cbmc-incr-oneloop/nestedloop1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 +--incremental-loop main.1 --unwinding-assertions ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc b/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc index b93239c7cd6..fb2b8088599 100644 --- a/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc +++ b/regression/cbmc-incr-oneloop/no-unwinding-assertion1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-max 10 --incremental-check main.0 +--unwind-max 10 --incremental-loop main.0 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/simpleloop1/test.desc b/regression/cbmc-incr-oneloop/simpleloop1/test.desc index a0f2422aed8..6830df4a700 100644 --- a/regression/cbmc-incr-oneloop/simpleloop1/test.desc +++ b/regression/cbmc-incr-oneloop/simpleloop1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 +--incremental-loop main.0 --unwinding-assertions ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/simpleloop2/test.desc b/regression/cbmc-incr-oneloop/simpleloop2/test.desc index 025a452508a..6cf5c97ea86 100644 --- a/regression/cbmc-incr-oneloop/simpleloop2/test.desc +++ b/regression/cbmc-incr-oneloop/simpleloop2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 6 --no-unwinding-assertions +--incremental-loop main.0 --unwind-max 6 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/simpleloop3/test.desc b/regression/cbmc-incr-oneloop/simpleloop3/test.desc index 526aa55e1b8..7120d6f2af3 100644 --- a/regression/cbmc-incr-oneloop/simpleloop3/test.desc +++ b/regression/cbmc-incr-oneloop/simpleloop3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --no-unwinding-assertions +--incremental-loop main.0 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/simpleloopmax1/test.desc b/regression/cbmc-incr-oneloop/simpleloopmax1/test.desc index ede388a6053..c090ea9d5e9 100644 --- a/regression/cbmc-incr-oneloop/simpleloopmax1/test.desc +++ b/regression/cbmc-incr-oneloop/simpleloopmax1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-max 10 --incremental-check main.0 +--unwind-max 10 --incremental-loop main.0 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/simpleloopmax2/test.desc b/regression/cbmc-incr-oneloop/simpleloopmax2/test.desc index b93239c7cd6..fb2b8088599 100644 --- a/regression/cbmc-incr-oneloop/simpleloopmax2/test.desc +++ b/regression/cbmc-incr-oneloop/simpleloopmax2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---no-unwinding-assertions --unwind-max 10 --incremental-check main.0 +--unwind-max 10 --incremental-loop main.0 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/simplifier1/test.desc b/regression/cbmc-incr-oneloop/simplifier1/test.desc index fadc2375302..709e207fdab 100644 --- a/regression/cbmc-incr-oneloop/simplifier1/test.desc +++ b/regression/cbmc-incr-oneloop/simplifier1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions +--incremental-loop main.0 --unwind-max 5 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/simplifier2/test.desc b/regression/cbmc-incr-oneloop/simplifier2/test.desc index ebb2f587b1f..3ad5bec6bce 100644 --- a/regression/cbmc-incr-oneloop/simplifier2/test.desc +++ b/regression/cbmc-incr-oneloop/simplifier2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 3 --no-unwinding-assertions +--incremental-loop main.0 --unwind-max 3 --stop-on-fail ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/simplifier3/test.desc b/regression/cbmc-incr-oneloop/simplifier3/test.desc index fadc2375302..709e207fdab 100644 --- a/regression/cbmc-incr-oneloop/simplifier3/test.desc +++ b/regression/cbmc-incr-oneloop/simplifier3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---incremental-check main.0 --unwind-max 5 --no-unwinding-assertions +--incremental-loop main.0 --unwind-max 5 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-incr-oneloop/unwind-forever1/main.c b/regression/cbmc-incr-oneloop/unwind-forever1/main.c index 874425968ef..cedd8a2f1ea 100644 --- a/regression/cbmc-incr-oneloop/unwind-forever1/main.c +++ b/regression/cbmc-incr-oneloop/unwind-forever1/main.c @@ -3,9 +3,9 @@ int main() { int x = nondet_int(); __CPROVER_assume(0<=x && x<=1); - //no error within loop => will unwind forever if no loop bound is given + // no error within loop => will unwind forever if no loop bound is given while(x<4) { x=x+1; } - assert(x<4); + assert(x < 4); // goto-symex never gets here unless it detects the loop bound } diff --git a/regression/cbmc-incr-oneloop/unwind-forever1/test.desc b/regression/cbmc-incr-oneloop/unwind-forever1/test.desc index 5d03502707e..cbc671c2329 100644 --- a/regression/cbmc-incr-oneloop/unwind-forever1/test.desc +++ b/regression/cbmc-incr-oneloop/unwind-forever1/test.desc @@ -1,7 +1,10 @@ -CORE +THOROUGH main.c - --incremental-check main.0 -^EXIT=142$ +--incremental-loop main.0 --unwinding-assertions +^EXIT=(142|14)$ ^SIGNAL=0$ -- ^warning: ignoring +-- +Tests whether goto-symex does not stop early. +Mac OS exit code is 14 diff --git a/regression/cbmc-incr-oneloop/unwind-forever2/main.c b/regression/cbmc-incr-oneloop/unwind-forever2/main.c index 9f06606e5fe..d38e78f98c9 100644 --- a/regression/cbmc-incr-oneloop/unwind-forever2/main.c +++ b/regression/cbmc-incr-oneloop/unwind-forever2/main.c @@ -3,9 +3,10 @@ int main() { int x = nondet_int(); __CPROVER_assume(0<=x && x<=1); - //no error within loop => will unwind forever if no loop bound is given + // no error within loop => will unwind forever if no loop bound is given while(x<4) { x=x+1; assert(x<=4); } + assert(x < 4); // goto-symex never gets here unless it detects the loop bound } diff --git a/regression/cbmc-incr-oneloop/unwind-forever2/test.desc b/regression/cbmc-incr-oneloop/unwind-forever2/test.desc index 920f3890da5..ca4e95cf4e6 100644 --- a/regression/cbmc-incr-oneloop/unwind-forever2/test.desc +++ b/regression/cbmc-incr-oneloop/unwind-forever2/test.desc @@ -1,7 +1,11 @@ -CORE +THOROUGH main.c ---incremental-check main.0 -^EXIT=142$ +--incremental-loop main.0 --unwinding-assertions +^EXIT=(142|14)$ ^SIGNAL=0$ -- ^warning: ignoring +-- +Tests whether goto-symex does not stop early when it cannot figure out the +loop bound and there is no error in the loop. +Mac OS exit code is 14 diff --git a/regression/cbmc-incr-oneloop/unwind-more-loops1/main.c b/regression/cbmc-incr-oneloop/unwind-more-loops1/main.c new file mode 100644 index 00000000000..39d85c35ac2 --- /dev/null +++ b/regression/cbmc-incr-oneloop/unwind-more-loops1/main.c @@ -0,0 +1,16 @@ +extern int nondet_int(); +int main() +{ + int x = nondet_int(); + __CPROVER_assume(0 <= x && x <= 1); + while(1) // main.0 + { + if(nondet_int()) + break; + } + while(x < 4) // main.1 + { + x = x + 1; + assert(x < 4); + } +} diff --git a/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc b/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc new file mode 100644 index 00000000000..10ec962c79c --- /dev/null +++ b/regression/cbmc-incr-oneloop/unwind-more-loops1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--incremental-loop main.1 --unwind 2 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^Not unwinding loop main\.0 iteration 2 +^Unwinding loop main\.1 iteration 3 +-- +^warning: ignoring +-- diff --git a/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc b/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc index 330d653e34c..83fa9618b2c 100644 --- a/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc +++ b/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind-max 10 --incremental-check main.0 +--unwind-max 10 --incremental-loop main.0 --unwinding-assertions ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/unwindset-more-loops1/main.c b/regression/cbmc-incr-oneloop/unwindset-more-loops1/main.c new file mode 100644 index 00000000000..3e2f53a88a2 --- /dev/null +++ b/regression/cbmc-incr-oneloop/unwindset-more-loops1/main.c @@ -0,0 +1,28 @@ +extern int nondet_int(); +int main() +{ + int x = nondet_int(); + __CPROVER_assume(0 <= x && x <= 1); + int y = 0; + while(y < 5) // main.0 + { + y++; + if(nondet_int()) + break; + } + while(1) // main.1 + { + if(nondet_int()) + break; + } + while(x < 4) // main.3 + { + while(1) // main.2 + { + if(nondet_int()) + break; + } + x = x + 1; + assert(x < 4); + } +} diff --git a/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc b/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc new file mode 100644 index 00000000000..6709bbcaa3b --- /dev/null +++ b/regression/cbmc-incr-oneloop/unwindset-more-loops1/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--incremental-loop main.3 --unwindset main.1:2,main.2:8 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^Unwinding loop main\.0 iteration 5 +^Not unwinding loop main\.1 iteration 2 +^Not unwinding loop main\.2 iteration 8 +^Unwinding loop main\.3 iteration 3 +-- +^warning: ignoring +^Unwinding loop main\.0 iteration 6 \ No newline at end of file From cc60ab3c28e17eab0563dbf14b06cb5b3b2a3bbe Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Feb 2019 10:33:35 +0000 Subject: [PATCH 14/16] Set induction tests to FUTURE These require more options that have not been implemented yet. --- regression/cbmc-incr-oneloop/induction1/test.desc | 7 +++++-- regression/cbmc-incr-oneloop/induction2/test.desc | 7 +++++-- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-incr-oneloop/induction1/test.desc b/regression/cbmc-incr-oneloop/induction1/test.desc index d5669341585..59ade7f6832 100644 --- a/regression/cbmc-incr-oneloop/induction1/test.desc +++ b/regression/cbmc-incr-oneloop/induction1/test.desc @@ -1,8 +1,11 @@ -CORE +FUTURE main.c ---incremental-loop main.0 --stop-when-unsat +--incremental-loop main.0 --stop-when-pass ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +-- +Step case of k-induction for a single loop: +incrementally try for increasing k as long as there are failing assertions. diff --git a/regression/cbmc-incr-oneloop/induction2/test.desc b/regression/cbmc-incr-oneloop/induction2/test.desc index d5669341585..59ade7f6832 100644 --- a/regression/cbmc-incr-oneloop/induction2/test.desc +++ b/regression/cbmc-incr-oneloop/induction2/test.desc @@ -1,8 +1,11 @@ -CORE +FUTURE main.c ---incremental-loop main.0 --stop-when-unsat +--incremental-loop main.0 --stop-when-pass ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +-- +Step case of k-induction for a single loop: +incrementally try for increasing k as long as there are failing assertions. From f1af977ce0020bc4d9d1f4fa0b4648b9d6f8a1ec Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Feb 2019 10:45:19 +0000 Subject: [PATCH 15/16] Clang-format cbmc-incr-oneloop tests --- regression/cbmc-incr-oneloop/alarm1/main.c | 775 ++++++++++-------- regression/cbmc-incr-oneloop/alarm2/main.c | 774 +++++++++-------- regression/cbmc-incr-oneloop/alarm3/main.c | 775 ++++++++++-------- regression/cbmc-incr-oneloop/arrays2/main.c | 11 +- regression/cbmc-incr-oneloop/arrays3/main.c | 12 +- regression/cbmc-incr-oneloop/arrays4/main.c | 11 +- regression/cbmc-incr-oneloop/arrays5/main.c | 7 +- .../assertion-after-loop1/main.c | 9 +- .../assertion-after-loop2/main.c | 9 +- regression/cbmc-incr-oneloop/cruise1/main.c | 138 +++- regression/cbmc-incr-oneloop/cruise2/main.c | 138 +++- .../cbmc-incr-oneloop/induction1/main.c | 10 +- .../cbmc-incr-oneloop/induction2/main.c | 28 +- .../cbmc-incr-oneloop/minmaxunwind1/main.c | 9 +- .../cbmc-incr-oneloop/minmaxunwind2/main.c | 9 +- .../cbmc-incr-oneloop/minmaxunwind3/main.c | 9 +- .../cbmc-incr-oneloop/minmaxunwind4/main.c | 9 +- .../cbmc-incr-oneloop/minmaxunwind5/main.c | 14 +- .../cbmc-incr-oneloop/moreasserts1/main.c | 26 +- .../cbmc-incr-oneloop/nestedloop1/main.c | 12 +- .../no-unwinding-assertion1/main.c | 9 +- .../cbmc-incr-oneloop/simpleloop1/main.c | 9 +- .../cbmc-incr-oneloop/simpleloop2/main.c | 5 +- .../cbmc-incr-oneloop/simpleloop3/main.c | 5 +- .../cbmc-incr-oneloop/simpleloopmax1/main.c | 9 +- .../cbmc-incr-oneloop/simpleloopmax2/main.c | 9 +- .../cbmc-incr-oneloop/simplifier1/main.c | 40 +- .../cbmc-incr-oneloop/simplifier2/main.c | 31 +- .../cbmc-incr-oneloop/simplifier3/main.c | 7 +- .../cbmc-incr-oneloop/unwind-forever1/main.c | 7 +- .../cbmc-incr-oneloop/unwind-forever2/main.c | 9 +- .../unwinding-assertion1/main.c | 9 +- 32 files changed, 1759 insertions(+), 1175 deletions(-) diff --git a/regression/cbmc-incr-oneloop/alarm1/main.c b/regression/cbmc-incr-oneloop/alarm1/main.c index 4c485d71988..53932eadca8 100644 --- a/regression/cbmc-incr-oneloop/alarm1/main.c +++ b/regression/cbmc-incr-oneloop/alarm1/main.c @@ -28,7 +28,6 @@ typedef float SINGLE; typedef unsigned char BOOL; - /* Function-like macros */ /* Conversion to the BOOL type */ @@ -36,361 +35,497 @@ typedef unsigned char BOOL; /* Type declarations */ -typedef struct { - INT32 Counter; - BOOL InitSystem_OPEN; - BOOL VehicleOpen_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterStart_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterPlus_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterEnd_OPEN; - BOOL AlarmWillBeArmedAfter20sec_OPEN; - BOOL AlarmOnlyOptical_CounterPlus_OPEN; - BOOL AlarmOnlyOptical_CounterStart_OPEN; - BOOL AlarmOnlyOptical_CounterEnd_OPEN; - BOOL AlarmOnlyOptical_OPEN; - BOOL AlarmAcousticAndOptical_CounterStart_OPEN; - BOOL AlarmAcousticAndOptical_CounterPlus_OPEN; - BOOL AlarmAcousticAndOptical_CounterEnd_OPEN; - BOOL AlarmAcousticAndOptical_OPEN; - BOOL AlarmArmed_OPEN; - BOOL Alarm_system_OPEN; +typedef struct +{ + INT32 Counter; + BOOL InitSystem_OPEN; + BOOL VehicleOpen_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterStart_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterPlus_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterEnd_OPEN; + BOOL AlarmWillBeArmedAfter20sec_OPEN; + BOOL AlarmOnlyOptical_CounterPlus_OPEN; + BOOL AlarmOnlyOptical_CounterStart_OPEN; + BOOL AlarmOnlyOptical_CounterEnd_OPEN; + BOOL AlarmOnlyOptical_OPEN; + BOOL AlarmAcousticAndOptical_CounterStart_OPEN; + BOOL AlarmAcousticAndOptical_CounterPlus_OPEN; + BOOL AlarmAcousticAndOptical_CounterEnd_OPEN; + BOOL AlarmAcousticAndOptical_OPEN; + BOOL AlarmArmed_OPEN; + BOOL Alarm_system_OPEN; } t_Alarm_system_state; -typedef struct { - BOOL OpticalAlarm; - BOOL AlarmSensor; - BOOL VehLocked; - BOOL AcousticAlarm; - BOOL AlarmArmed; +typedef struct +{ + BOOL OpticalAlarm; + BOOL AlarmSensor; + BOOL VehLocked; + BOOL AcousticAlarm; + BOOL AlarmArmed; } t_Alarm_system_io; /* Named Constants */ #define ALARM_SYSTEM_TICK 0 -void Alarm_system_init(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) { - _io_->OpticalAlarm = FALSE; - _io_->AlarmSensor = FALSE; - _io_->VehLocked = FALSE; - _io_->AcousticAlarm = FALSE; - _io_->AlarmArmed = FALSE; - _state_->Counter = 0; - _state_->InitSystem_OPEN = 0; - _state_->VehicleOpen_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_OPEN = 0; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = 0; - _state_->AlarmOnlyOptical_CounterStart_OPEN = 0; - _state_->AlarmOnlyOptical_CounterEnd_OPEN = 0; - _state_->AlarmOnlyOptical_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = 0; - _state_->AlarmAcousticAndOptical_OPEN = 0; - _state_->AlarmArmed_OPEN = 0; - _state_->Alarm_system_OPEN = 0; +void Alarm_system_init(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) +{ + _io_->OpticalAlarm = FALSE; + _io_->AlarmSensor = FALSE; + _io_->VehLocked = FALSE; + _io_->AcousticAlarm = FALSE; + _io_->AlarmArmed = FALSE; + _state_->Counter = 0; + _state_->InitSystem_OPEN = 0; + _state_->VehicleOpen_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_OPEN = 0; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = 0; + _state_->AlarmOnlyOptical_CounterStart_OPEN = 0; + _state_->AlarmOnlyOptical_CounterEnd_OPEN = 0; + _state_->AlarmOnlyOptical_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = 0; + _state_->AlarmAcousticAndOptical_OPEN = 0; + _state_->AlarmArmed_OPEN = 0; + _state_->Alarm_system_OPEN = 0; } -void Alarm_system_compute(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) { - UINT16 activeEvent = ALARM_SYSTEM_TICK; - if (!_state_->Alarm_system_OPEN) { - /* Open the chart */ - _state_->Alarm_system_OPEN = TRUE; - /* Enter the chart's composition */ - /* Enter state InitSystem */ - _state_->InitSystem_OPEN = TRUE; - } else { - /* Execute an open chart */ - if (_state_->InitSystem_OPEN) { - /* Execute state InitSystem */ - if (_io_->VehLocked == 1) { - _state_->InitSystem_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; - /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ - /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - _state_->InitSystem_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state InitSystem */ - _io_->AlarmArmed = TO_BOOL(1); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); +void Alarm_system_compute( + t_Alarm_system_io *_io_, + t_Alarm_system_state *_state_) +{ + UINT16 activeEvent = ALARM_SYSTEM_TICK; + if(!_state_->Alarm_system_OPEN) + { + /* Open the chart */ + _state_->Alarm_system_OPEN = TRUE; + /* Enter the chart's composition */ + /* Enter state InitSystem */ + _state_->InitSystem_OPEN = TRUE; + } + else + { + /* Execute an open chart */ + if(_state_->InitSystem_OPEN) + { + /* Execute state InitSystem */ + if(_io_->VehLocked == 1) + { + _state_->InitSystem_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; + /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ + /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->Counter = 1; + } + else + { + if(_io_->VehLocked == 0) + { + _state_->InitSystem_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state InitSystem */ + _io_->AlarmArmed = TO_BOOL(1); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + } + else + { + if(_state_->VehicleOpen_OPEN) + { + /* Execute state VehicleOpen */ + if(_io_->VehLocked == 1) + { + _state_->VehicleOpen_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; + /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ + /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->Counter = 1; + } + else + { + /* Perform during and on-event actions of state VehicleOpen */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec */ + if(_state_->Counter == 0 && _io_->VehLocked == 1) + { + /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; } + } } - } else { - if (_state_->VehicleOpen_OPEN) { - /* Execute state VehicleOpen */ - if (_io_->VehLocked == 1) { - _state_->VehicleOpen_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; - /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ - /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->Counter = 1; - } else { - /* Perform during and on-event actions of state VehicleOpen */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); + _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; + _state_->AlarmArmed_OPEN = TRUE; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state AlarmWillBeArmedAfter20sec */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec.CounterPlus */ + if(_state_->Counter < TIMEOUT1 || _io_->VehLocked == 0) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = + FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = + FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterEnd */ + _state_->Counter = 0; + } + } + } + } + } + } + else + { + if(_state_->AlarmOnlyOptical_OPEN) + { + /* Execute state AlarmOnlyOptical */ + if(_state_->Counter == 0) + { + /* Close the inner composition of state AlarmOnlyOptical */ + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterEnd_OPEN) + { + _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; + } } - } else { - if (_state_->AlarmWillBeArmedAfter20sec_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec */ - if (_state_->Counter == 0 && _io_->VehLocked == 1) { - /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; - _state_->AlarmArmed_OPEN = TRUE; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state AlarmWillBeArmedAfter20sec */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec.CounterPlus */ - if (_state_->Counter < TIMEOUT1 || _io_->VehLocked == 0) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterEnd */ - _state_->Counter = 0; - } - } - } - } + } + _state_->AlarmOnlyOptical_OPEN = FALSE; + _state_->AlarmArmed_OPEN = TRUE; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmOnlyOptical */ + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterEnd_OPEN) + { + _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmOnlyOptical_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state AlarmOnlyOptical */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(1); + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + /* Execute state AlarmOnlyOptical.CounterPlus */ + if(_state_->Counter < TIMEOUT3 && _io_->VehLocked == 1) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterEnd */ + _state_->Counter = 0; + } + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + /* Execute state AlarmOnlyOptical.CounterStart */ + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + } + } + } + } + else + { + if(_state_->AlarmAcousticAndOptical_OPEN) + { + /* Execute state AlarmAcousticAndOptical */ + if(_state_->Counter == 0) + { + /* Close the inner composition of state AlarmAcousticAndOptical */ + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmAcousticAndOptical_OPEN = FALSE; + _state_->AlarmOnlyOptical_OPEN = TRUE; + /* Open the inner composition of state AlarmOnlyOptical */ + /* Enter state AlarmOnlyOptical.CounterStart */ + _state_->AlarmOnlyOptical_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterStart */ + _state_->Counter = 1; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmAcousticAndOptical */ + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = + FALSE; + } } - } else { - if (_state_->AlarmOnlyOptical_OPEN) { - /* Execute state AlarmOnlyOptical */ - if (_state_->Counter == 0) { - /* Close the inner composition of state AlarmOnlyOptical */ - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterEnd_OPEN) { - _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmOnlyOptical_OPEN = FALSE; - _state_->AlarmArmed_OPEN = TRUE; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmOnlyOptical */ - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterEnd_OPEN) { - _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmOnlyOptical_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state AlarmOnlyOptical */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(1); - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - /* Execute state AlarmOnlyOptical.CounterPlus */ - if (_state_->Counter < TIMEOUT3 && _io_->VehLocked == 1) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterEnd */ - _state_->Counter = 0; - } - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - /* Execute state AlarmOnlyOptical.CounterStart */ - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } - } - } - } - } else { - if (_state_->AlarmAcousticAndOptical_OPEN) { - /* Execute state AlarmAcousticAndOptical */ - if (_state_->Counter == 0) { - /* Close the inner composition of state AlarmAcousticAndOptical */ - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) { - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmAcousticAndOptical_OPEN = FALSE; - _state_->AlarmOnlyOptical_OPEN = TRUE; - /* Open the inner composition of state AlarmOnlyOptical */ - /* Enter state AlarmOnlyOptical.CounterStart */ - _state_->AlarmOnlyOptical_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmAcousticAndOptical */ - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) { - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmAcousticAndOptical_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //BUG does not work - } else { - /* Perform during and on-event actions of state AlarmAcousticAndOptical */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(1); - _io_->OpticalAlarm = TO_BOOL(1); - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - /* Execute state AlarmAcousticAndOptical.CounterStart */ - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - /* Execute state AlarmAcousticAndOptical.CounterPlus */ - if (_state_->Counter < TIMEOUT2 && _io_->VehLocked == 1) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterEnd */ - _state_->Counter = 0; - } - } - } - } - } - } else { - if (_state_->AlarmArmed_OPEN) { - /* Execute state AlarmArmed */ - if (_io_->AlarmSensor == 1) { - _state_->AlarmArmed_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_OPEN = TRUE; //BUG does not work - /* Open the inner composition of state AlarmAcousticAndOptical */ - /* Enter state AlarmAcousticAndOptical.CounterStart */ - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - _state_->AlarmArmed_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //BUG does not work - } else { - /* Perform during and on-event actions of state AlarmArmed */ - _io_->AlarmArmed = TO_BOOL(1); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); - } - } - } - } + } + _state_->AlarmAcousticAndOptical_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //BUG does not work + } + else + { + /* Perform during and on-event actions of state AlarmAcousticAndOptical */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(1); + _io_->OpticalAlarm = TO_BOOL(1); + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + /* Execute state AlarmAcousticAndOptical.CounterStart */ + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + /* Execute state AlarmAcousticAndOptical.CounterPlus */ + if(_state_->Counter < TIMEOUT2 && _io_->VehLocked == 1) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + FALSE; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + FALSE; + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterEnd */ + _state_->Counter = 0; + } } + } + } + } + } + else + { + if(_state_->AlarmArmed_OPEN) + { + /* Execute state AlarmArmed */ + if(_io_->AlarmSensor == 1) + { + _state_->AlarmArmed_OPEN = FALSE; + _state_->AlarmAcousticAndOptical_OPEN = + TRUE; //BUG does not work + /* Open the inner composition of state AlarmAcousticAndOptical */ + /* Enter state AlarmAcousticAndOptical.CounterStart */ + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterStart */ + _state_->Counter = 1; } + else + { + if(_io_->VehLocked == 0) + { + _state_->AlarmArmed_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //BUG does not work + } + else + { + /* Perform during and on-event actions of state AlarmArmed */ + _io_->AlarmArmed = TO_BOOL(1); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + } } + } } + } } + } } extern int nondet_int(); -t_Alarm_system_io havocIO() { +t_Alarm_system_io havocIO() +{ t_Alarm_system_io _io_; _io_.VehLocked = nondet_int(); _io_.AlarmSensor = nondet_int(); - __CPROVER_assume(0<=_io_.VehLocked && _io_.VehLocked<=1 && - 0<=_io_.AlarmSensor && _io_.AlarmSensor<=1); + __CPROVER_assume( + 0 <= _io_.VehLocked && _io_.VehLocked <= 1 && 0 <= _io_.AlarmSensor && + _io_.AlarmSensor <= 1); return _io_; } -int main() { - int k=0; +int main() +{ + int k = 0; t_Alarm_system_state _state_; t_Alarm_system_state _state_old; t_Alarm_system_io _io_; - Alarm_system_init(&_io_,&_state_); - while(1) { + Alarm_system_init(&_io_, &_state_); + while(1) + { _state_old = _state_; _io_ = havocIO(); - Alarm_system_compute(&_io_,&_state_); - if(_state_old.AlarmArmed_OPEN && _io_.AlarmSensor) { + Alarm_system_compute(&_io_, &_state_); + if(_state_old.AlarmArmed_OPEN && _io_.AlarmSensor) + { assert(_state_.AlarmAcousticAndOptical_OPEN); } - if(!_state_.InitSystem_OPEN && _state_old.Counter!=0 && !_io_.AlarmSensor && !_io_.VehLocked) assert(_state_.VehicleOpen_OPEN); + if( + !_state_.InitSystem_OPEN && _state_old.Counter != 0 && + !_io_.AlarmSensor && !_io_.VehLocked) + assert(_state_.VehicleOpen_OPEN); } return 0; } diff --git a/regression/cbmc-incr-oneloop/alarm2/main.c b/regression/cbmc-incr-oneloop/alarm2/main.c index c5b62d3037e..022793142bc 100644 --- a/regression/cbmc-incr-oneloop/alarm2/main.c +++ b/regression/cbmc-incr-oneloop/alarm2/main.c @@ -28,7 +28,6 @@ typedef float SINGLE; typedef unsigned char BOOL; - /* Function-like macros */ /* Conversion to the BOOL type */ @@ -36,361 +35,496 @@ typedef unsigned char BOOL; /* Type declarations */ -typedef struct { - INT32 Counter; - BOOL InitSystem_OPEN; - BOOL VehicleOpen_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterStart_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterPlus_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterEnd_OPEN; - BOOL AlarmWillBeArmedAfter20sec_OPEN; - BOOL AlarmOnlyOptical_CounterPlus_OPEN; - BOOL AlarmOnlyOptical_CounterStart_OPEN; - BOOL AlarmOnlyOptical_CounterEnd_OPEN; - BOOL AlarmOnlyOptical_OPEN; - BOOL AlarmAcousticAndOptical_CounterStart_OPEN; - BOOL AlarmAcousticAndOptical_CounterPlus_OPEN; - BOOL AlarmAcousticAndOptical_CounterEnd_OPEN; - BOOL AlarmAcousticAndOptical_OPEN; - BOOL AlarmArmed_OPEN; - BOOL Alarm_system_OPEN; +typedef struct +{ + INT32 Counter; + BOOL InitSystem_OPEN; + BOOL VehicleOpen_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterStart_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterPlus_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterEnd_OPEN; + BOOL AlarmWillBeArmedAfter20sec_OPEN; + BOOL AlarmOnlyOptical_CounterPlus_OPEN; + BOOL AlarmOnlyOptical_CounterStart_OPEN; + BOOL AlarmOnlyOptical_CounterEnd_OPEN; + BOOL AlarmOnlyOptical_OPEN; + BOOL AlarmAcousticAndOptical_CounterStart_OPEN; + BOOL AlarmAcousticAndOptical_CounterPlus_OPEN; + BOOL AlarmAcousticAndOptical_CounterEnd_OPEN; + BOOL AlarmAcousticAndOptical_OPEN; + BOOL AlarmArmed_OPEN; + BOOL Alarm_system_OPEN; } t_Alarm_system_state; -typedef struct { - BOOL OpticalAlarm; - BOOL AlarmSensor; - BOOL VehLocked; - BOOL AcousticAlarm; - BOOL AlarmArmed; +typedef struct +{ + BOOL OpticalAlarm; + BOOL AlarmSensor; + BOOL VehLocked; + BOOL AcousticAlarm; + BOOL AlarmArmed; } t_Alarm_system_io; /* Named Constants */ #define ALARM_SYSTEM_TICK 0 -void Alarm_system_init(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) { - _io_->OpticalAlarm = FALSE; - _io_->AlarmSensor = FALSE; - _io_->VehLocked = FALSE; - _io_->AcousticAlarm = FALSE; - _io_->AlarmArmed = FALSE; - _state_->Counter = 0; - _state_->InitSystem_OPEN = 0; - _state_->VehicleOpen_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_OPEN = 0; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = 0; - _state_->AlarmOnlyOptical_CounterStart_OPEN = 0; - _state_->AlarmOnlyOptical_CounterEnd_OPEN = 0; - _state_->AlarmOnlyOptical_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = 0; - _state_->AlarmAcousticAndOptical_OPEN = 0; - _state_->AlarmArmed_OPEN = 0; - _state_->Alarm_system_OPEN = 0; +void Alarm_system_init(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) +{ + _io_->OpticalAlarm = FALSE; + _io_->AlarmSensor = FALSE; + _io_->VehLocked = FALSE; + _io_->AcousticAlarm = FALSE; + _io_->AlarmArmed = FALSE; + _state_->Counter = 0; + _state_->InitSystem_OPEN = 0; + _state_->VehicleOpen_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_OPEN = 0; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = 0; + _state_->AlarmOnlyOptical_CounterStart_OPEN = 0; + _state_->AlarmOnlyOptical_CounterEnd_OPEN = 0; + _state_->AlarmOnlyOptical_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = 0; + _state_->AlarmAcousticAndOptical_OPEN = 0; + _state_->AlarmArmed_OPEN = 0; + _state_->Alarm_system_OPEN = 0; } -void Alarm_system_compute(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) { - UINT16 activeEvent = ALARM_SYSTEM_TICK; - if (!_state_->Alarm_system_OPEN) { - /* Open the chart */ - _state_->Alarm_system_OPEN = TRUE; - /* Enter the chart's composition */ - /* Enter state InitSystem */ - _state_->InitSystem_OPEN = TRUE; - } else { - /* Execute an open chart */ - if (_state_->InitSystem_OPEN) { - /* Execute state InitSystem */ - if (_io_->VehLocked == 1) { - _state_->InitSystem_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; - /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ - /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - _state_->InitSystem_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state InitSystem */ - _io_->AlarmArmed = TO_BOOL(1); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); +void Alarm_system_compute( + t_Alarm_system_io *_io_, + t_Alarm_system_state *_state_) +{ + UINT16 activeEvent = ALARM_SYSTEM_TICK; + if(!_state_->Alarm_system_OPEN) + { + /* Open the chart */ + _state_->Alarm_system_OPEN = TRUE; + /* Enter the chart's composition */ + /* Enter state InitSystem */ + _state_->InitSystem_OPEN = TRUE; + } + else + { + /* Execute an open chart */ + if(_state_->InitSystem_OPEN) + { + /* Execute state InitSystem */ + if(_io_->VehLocked == 1) + { + _state_->InitSystem_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; + /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ + /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->Counter = 1; + } + else + { + if(_io_->VehLocked == 0) + { + _state_->InitSystem_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state InitSystem */ + _io_->AlarmArmed = TO_BOOL(1); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + } + else + { + if(_state_->VehicleOpen_OPEN) + { + /* Execute state VehicleOpen */ + if(_io_->VehLocked == 1) + { + _state_->VehicleOpen_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; + /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ + /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->Counter = 1; + } + else + { + /* Perform during and on-event actions of state VehicleOpen */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec */ + if(_state_->Counter == 0 && _io_->VehLocked == 1) + { + /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; } + } } - } else { - if (_state_->VehicleOpen_OPEN) { - /* Execute state VehicleOpen */ - if (_io_->VehLocked == 1) { - _state_->VehicleOpen_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; - /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ - /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->Counter = 1; - } else { - /* Perform during and on-event actions of state VehicleOpen */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); + _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; + _state_->AlarmArmed_OPEN = TRUE; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state AlarmWillBeArmedAfter20sec */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec.CounterPlus */ + if(_state_->Counter < TIMEOUT1 || _io_->VehLocked == 0) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = + FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = + FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterEnd */ + _state_->Counter = 0; + } + } + } + } + } + } + else + { + if(_state_->AlarmOnlyOptical_OPEN) + { + /* Execute state AlarmOnlyOptical */ + if(_state_->Counter == 0) + { + /* Close the inner composition of state AlarmOnlyOptical */ + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterEnd_OPEN) + { + _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; + } } - } else { - if (_state_->AlarmWillBeArmedAfter20sec_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec */ - if (_state_->Counter == 0 && _io_->VehLocked == 1) { - /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; - _state_->AlarmArmed_OPEN = TRUE; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state AlarmWillBeArmedAfter20sec */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec.CounterPlus */ - if (_state_->Counter < TIMEOUT1 || _io_->VehLocked == 0) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterEnd */ - _state_->Counter = 0; - } - } - } - } + } + _state_->AlarmOnlyOptical_OPEN = FALSE; + _state_->AlarmArmed_OPEN = TRUE; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmOnlyOptical */ + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterEnd_OPEN) + { + _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmOnlyOptical_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state AlarmOnlyOptical */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(1); + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + /* Execute state AlarmOnlyOptical.CounterPlus */ + if(_state_->Counter < TIMEOUT3 && _io_->VehLocked == 1) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterEnd */ + _state_->Counter = 0; + } + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + /* Execute state AlarmOnlyOptical.CounterStart */ + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + } + } + } + } + else + { + if(_state_->AlarmAcousticAndOptical_OPEN) + { + /* Execute state AlarmAcousticAndOptical */ + if(_state_->Counter == 0) + { + /* Close the inner composition of state AlarmAcousticAndOptical */ + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmAcousticAndOptical_OPEN = FALSE; + _state_->AlarmOnlyOptical_OPEN = TRUE; + /* Open the inner composition of state AlarmOnlyOptical */ + /* Enter state AlarmOnlyOptical.CounterStart */ + _state_->AlarmOnlyOptical_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterStart */ + _state_->Counter = 1; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmAcousticAndOptical */ + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = + FALSE; + } } - } else { - if (_state_->AlarmOnlyOptical_OPEN) { - /* Execute state AlarmOnlyOptical */ - if (_state_->Counter == 0) { - /* Close the inner composition of state AlarmOnlyOptical */ - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterEnd_OPEN) { - _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmOnlyOptical_OPEN = FALSE; - _state_->AlarmArmed_OPEN = TRUE; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmOnlyOptical */ - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterEnd_OPEN) { - _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmOnlyOptical_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state AlarmOnlyOptical */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(1); - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - /* Execute state AlarmOnlyOptical.CounterPlus */ - if (_state_->Counter < TIMEOUT3 && _io_->VehLocked == 1) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterEnd */ - _state_->Counter = 0; - } - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - /* Execute state AlarmOnlyOptical.CounterStart */ - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } - } - } - } - } else { - if (_state_->AlarmAcousticAndOptical_OPEN) { - /* Execute state AlarmAcousticAndOptical */ - if (_state_->Counter == 0) { - /* Close the inner composition of state AlarmAcousticAndOptical */ - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) { - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmAcousticAndOptical_OPEN = FALSE; - _state_->AlarmOnlyOptical_OPEN = TRUE; - /* Open the inner composition of state AlarmOnlyOptical */ - /* Enter state AlarmOnlyOptical.CounterStart */ - _state_->AlarmOnlyOptical_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmAcousticAndOptical */ - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) { - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmAcousticAndOptical_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //BUG does not work - } else { - /* Perform during and on-event actions of state AlarmAcousticAndOptical */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(1); - _io_->OpticalAlarm = TO_BOOL(1); - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - /* Execute state AlarmAcousticAndOptical.CounterStart */ - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - /* Execute state AlarmAcousticAndOptical.CounterPlus */ - if (_state_->Counter < TIMEOUT2 && _io_->VehLocked == 1) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterEnd */ - _state_->Counter = 0; - } - } - } - } - } - } else { - if (_state_->AlarmArmed_OPEN) { - /* Execute state AlarmArmed */ - if (_io_->AlarmSensor == 1) { - _state_->AlarmArmed_OPEN = FALSE; - //BUG _state_->AlarmAcousticAndOptical_OPEN = TRUE; //BUG does not work - /* Open the inner composition of state AlarmAcousticAndOptical */ - /* Enter state AlarmAcousticAndOptical.CounterStart */ - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - _state_->AlarmArmed_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //BUG does not work - } else { - /* Perform during and on-event actions of state AlarmArmed */ - _io_->AlarmArmed = TO_BOOL(1); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); - } - } - } - } + } + _state_->AlarmAcousticAndOptical_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //BUG does not work + } + else + { + /* Perform during and on-event actions of state AlarmAcousticAndOptical */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(1); + _io_->OpticalAlarm = TO_BOOL(1); + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + /* Execute state AlarmAcousticAndOptical.CounterStart */ + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + /* Execute state AlarmAcousticAndOptical.CounterPlus */ + if(_state_->Counter < TIMEOUT2 && _io_->VehLocked == 1) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + FALSE; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + FALSE; + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterEnd */ + _state_->Counter = 0; + } } + } + } + } + } + else + { + if(_state_->AlarmArmed_OPEN) + { + /* Execute state AlarmArmed */ + if(_io_->AlarmSensor == 1) + { + _state_->AlarmArmed_OPEN = FALSE; + //BUG _state_->AlarmAcousticAndOptical_OPEN = TRUE; //BUG does not work + /* Open the inner composition of state AlarmAcousticAndOptical */ + /* Enter state AlarmAcousticAndOptical.CounterStart */ + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterStart */ + _state_->Counter = 1; } + else + { + if(_io_->VehLocked == 0) + { + _state_->AlarmArmed_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //BUG does not work + } + else + { + /* Perform during and on-event actions of state AlarmArmed */ + _io_->AlarmArmed = TO_BOOL(1); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + } } + } } + } } + } } extern int nondet_int(); -t_Alarm_system_io havocIO() { +t_Alarm_system_io havocIO() +{ t_Alarm_system_io _io_; _io_.VehLocked = nondet_int(); _io_.AlarmSensor = nondet_int(); - __CPROVER_assume(0<=_io_.VehLocked && _io_.VehLocked<=1 && - 0<=_io_.AlarmSensor && _io_.AlarmSensor<=1); + __CPROVER_assume( + 0 <= _io_.VehLocked && _io_.VehLocked <= 1 && 0 <= _io_.AlarmSensor && + _io_.AlarmSensor <= 1); return _io_; } -int main() { - int k=0; +int main() +{ + int k = 0; t_Alarm_system_state _state_; t_Alarm_system_state _state_old; t_Alarm_system_io _io_; - Alarm_system_init(&_io_,&_state_); - while(1) { + Alarm_system_init(&_io_, &_state_); + while(1) + { _state_old = _state_; _io_ = havocIO(); - Alarm_system_compute(&_io_,&_state_); - if(_state_old.AlarmArmed_OPEN && _io_.AlarmSensor) { + Alarm_system_compute(&_io_, &_state_); + if(_state_old.AlarmArmed_OPEN && _io_.AlarmSensor) + { assert(_state_.AlarmAcousticAndOptical_OPEN); } - if(!_state_.InitSystem_OPEN && _state_old.Counter!=0 && !_io_.AlarmSensor && !_io_.VehLocked) assert(_state_.VehicleOpen_OPEN); + if( + !_state_.InitSystem_OPEN && _state_old.Counter != 0 && + !_io_.AlarmSensor && !_io_.VehLocked) + assert(_state_.VehicleOpen_OPEN); } return 0; } diff --git a/regression/cbmc-incr-oneloop/alarm3/main.c b/regression/cbmc-incr-oneloop/alarm3/main.c index 1df007abbc7..d2cde9cc3e2 100644 --- a/regression/cbmc-incr-oneloop/alarm3/main.c +++ b/regression/cbmc-incr-oneloop/alarm3/main.c @@ -28,7 +28,6 @@ typedef float SINGLE; typedef unsigned char BOOL; - /* Function-like macros */ /* Conversion to the BOOL type */ @@ -36,361 +35,497 @@ typedef unsigned char BOOL; /* Type declarations */ -typedef struct { - INT32 Counter; - BOOL InitSystem_OPEN; - BOOL VehicleOpen_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterStart_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterPlus_OPEN; - BOOL AlarmWillBeArmedAfter20sec_CounterEnd_OPEN; - BOOL AlarmWillBeArmedAfter20sec_OPEN; - BOOL AlarmOnlyOptical_CounterPlus_OPEN; - BOOL AlarmOnlyOptical_CounterStart_OPEN; - BOOL AlarmOnlyOptical_CounterEnd_OPEN; - BOOL AlarmOnlyOptical_OPEN; - BOOL AlarmAcousticAndOptical_CounterStart_OPEN; - BOOL AlarmAcousticAndOptical_CounterPlus_OPEN; - BOOL AlarmAcousticAndOptical_CounterEnd_OPEN; - BOOL AlarmAcousticAndOptical_OPEN; - BOOL AlarmArmed_OPEN; - BOOL Alarm_system_OPEN; +typedef struct +{ + INT32 Counter; + BOOL InitSystem_OPEN; + BOOL VehicleOpen_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterStart_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterPlus_OPEN; + BOOL AlarmWillBeArmedAfter20sec_CounterEnd_OPEN; + BOOL AlarmWillBeArmedAfter20sec_OPEN; + BOOL AlarmOnlyOptical_CounterPlus_OPEN; + BOOL AlarmOnlyOptical_CounterStart_OPEN; + BOOL AlarmOnlyOptical_CounterEnd_OPEN; + BOOL AlarmOnlyOptical_OPEN; + BOOL AlarmAcousticAndOptical_CounterStart_OPEN; + BOOL AlarmAcousticAndOptical_CounterPlus_OPEN; + BOOL AlarmAcousticAndOptical_CounterEnd_OPEN; + BOOL AlarmAcousticAndOptical_OPEN; + BOOL AlarmArmed_OPEN; + BOOL Alarm_system_OPEN; } t_Alarm_system_state; -typedef struct { - BOOL OpticalAlarm; - BOOL AlarmSensor; - BOOL VehLocked; - BOOL AcousticAlarm; - BOOL AlarmArmed; +typedef struct +{ + BOOL OpticalAlarm; + BOOL AlarmSensor; + BOOL VehLocked; + BOOL AcousticAlarm; + BOOL AlarmArmed; } t_Alarm_system_io; /* Named Constants */ #define ALARM_SYSTEM_TICK 0 -void Alarm_system_init(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) { - _io_->OpticalAlarm = FALSE; - _io_->AlarmSensor = FALSE; - _io_->VehLocked = FALSE; - _io_->AcousticAlarm = FALSE; - _io_->AlarmArmed = FALSE; - _state_->Counter = 0; - _state_->InitSystem_OPEN = 0; - _state_->VehicleOpen_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = 0; - _state_->AlarmWillBeArmedAfter20sec_OPEN = 0; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = 0; - _state_->AlarmOnlyOptical_CounterStart_OPEN = 0; - _state_->AlarmOnlyOptical_CounterEnd_OPEN = 0; - _state_->AlarmOnlyOptical_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = 0; - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = 0; - _state_->AlarmAcousticAndOptical_OPEN = 0; - _state_->AlarmArmed_OPEN = 0; - _state_->Alarm_system_OPEN = 0; +void Alarm_system_init(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) +{ + _io_->OpticalAlarm = FALSE; + _io_->AlarmSensor = FALSE; + _io_->VehLocked = FALSE; + _io_->AcousticAlarm = FALSE; + _io_->AlarmArmed = FALSE; + _state_->Counter = 0; + _state_->InitSystem_OPEN = 0; + _state_->VehicleOpen_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = 0; + _state_->AlarmWillBeArmedAfter20sec_OPEN = 0; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = 0; + _state_->AlarmOnlyOptical_CounterStart_OPEN = 0; + _state_->AlarmOnlyOptical_CounterEnd_OPEN = 0; + _state_->AlarmOnlyOptical_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = 0; + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = 0; + _state_->AlarmAcousticAndOptical_OPEN = 0; + _state_->AlarmArmed_OPEN = 0; + _state_->Alarm_system_OPEN = 0; } -void Alarm_system_compute(t_Alarm_system_io *_io_, t_Alarm_system_state *_state_) { - UINT16 activeEvent = ALARM_SYSTEM_TICK; - if (!_state_->Alarm_system_OPEN) { - /* Open the chart */ - _state_->Alarm_system_OPEN = TRUE; - /* Enter the chart's composition */ - /* Enter state InitSystem */ - _state_->InitSystem_OPEN = TRUE; - } else { - /* Execute an open chart */ - if (_state_->InitSystem_OPEN) { - /* Execute state InitSystem */ - if (_io_->VehLocked == 1) { - _state_->InitSystem_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; - /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ - /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - _state_->InitSystem_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state InitSystem */ - _io_->AlarmArmed = TO_BOOL(1); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); +void Alarm_system_compute( + t_Alarm_system_io *_io_, + t_Alarm_system_state *_state_) +{ + UINT16 activeEvent = ALARM_SYSTEM_TICK; + if(!_state_->Alarm_system_OPEN) + { + /* Open the chart */ + _state_->Alarm_system_OPEN = TRUE; + /* Enter the chart's composition */ + /* Enter state InitSystem */ + _state_->InitSystem_OPEN = TRUE; + } + else + { + /* Execute an open chart */ + if(_state_->InitSystem_OPEN) + { + /* Execute state InitSystem */ + if(_io_->VehLocked == 1) + { + _state_->InitSystem_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; + /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ + /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->Counter = 1; + } + else + { + if(_io_->VehLocked == 0) + { + _state_->InitSystem_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state InitSystem */ + _io_->AlarmArmed = TO_BOOL(1); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + } + else + { + if(_state_->VehicleOpen_OPEN) + { + /* Execute state VehicleOpen */ + if(_io_->VehLocked == 1) + { + _state_->VehicleOpen_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; + /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ + /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->Counter = 1; + } + else + { + /* Perform during and on-event actions of state VehicleOpen */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec */ + if(_state_->Counter == 0 && _io_->VehLocked == 1) + { + /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; } + } } - } else { - if (_state_->VehicleOpen_OPEN) { - /* Execute state VehicleOpen */ - if (_io_->VehLocked == 1) { - _state_->VehicleOpen_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_OPEN = TRUE; - /* Open the inner composition of state AlarmWillBeArmedAfter20sec */ - /* Enter state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->Counter = 1; - } else { - /* Perform during and on-event actions of state VehicleOpen */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); + _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; + _state_->AlarmArmed_OPEN = TRUE; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) + { + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state AlarmWillBeArmedAfter20sec */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + if(_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec.CounterStart */ + _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + if(_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) + { + /* Execute state AlarmWillBeArmedAfter20sec.CounterPlus */ + if(_state_->Counter < TIMEOUT1 || _io_->VehLocked == 0) + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = + FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = + FALSE; + _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterEnd */ + _state_->Counter = 0; + } + } + } + } + } + } + else + { + if(_state_->AlarmOnlyOptical_OPEN) + { + /* Execute state AlarmOnlyOptical */ + if(_state_->Counter == 0) + { + /* Close the inner composition of state AlarmOnlyOptical */ + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterEnd_OPEN) + { + _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; + } } - } else { - if (_state_->AlarmWillBeArmedAfter20sec_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec */ - if (_state_->Counter == 0 && _io_->VehLocked == 1) { - /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; - _state_->AlarmArmed_OPEN = TRUE; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmWillBeArmedAfter20sec */ - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN) { - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmWillBeArmedAfter20sec_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state AlarmWillBeArmedAfter20sec */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); - if (_state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec.CounterStart */ - _state_->AlarmWillBeArmedAfter20sec_CounterStart_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - if (_state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN) { - /* Execute state AlarmWillBeArmedAfter20sec.CounterPlus */ - if (_state_->Counter < TIMEOUT1 || _io_->VehLocked == 0) { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmWillBeArmedAfter20sec_CounterPlus_OPEN = FALSE; - _state_->AlarmWillBeArmedAfter20sec_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmWillBeArmedAfter20sec.CounterEnd */ - _state_->Counter = 0; - } - } - } - } + } + _state_->AlarmOnlyOptical_OPEN = FALSE; + _state_->AlarmArmed_OPEN = TRUE; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmOnlyOptical */ + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmOnlyOptical_CounterEnd_OPEN) + { + _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmOnlyOptical_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //possible BUG + } + else + { + /* Perform during and on-event actions of state AlarmOnlyOptical */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(1); + if(_state_->AlarmOnlyOptical_CounterPlus_OPEN) + { + /* Execute state AlarmOnlyOptical.CounterPlus */ + if(_state_->Counter < TIMEOUT3 && _io_->VehLocked == 1) + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterEnd */ + _state_->Counter = 0; + } + } + else + { + if(_state_->AlarmOnlyOptical_CounterStart_OPEN) + { + /* Execute state AlarmOnlyOptical.CounterStart */ + _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; + _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + } + } + } + } + else + { + if(_state_->AlarmAcousticAndOptical_OPEN) + { + /* Execute state AlarmAcousticAndOptical */ + if(_state_->Counter == 0) + { + /* Close the inner composition of state AlarmAcousticAndOptical */ + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; + } + } + } + _state_->AlarmAcousticAndOptical_OPEN = FALSE; + _state_->AlarmOnlyOptical_OPEN = TRUE; + /* Open the inner composition of state AlarmOnlyOptical */ + /* Enter state AlarmOnlyOptical.CounterStart */ + _state_->AlarmOnlyOptical_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmOnlyOptical.CounterStart */ + _state_->Counter = 1; + } + else + { + if(_io_->VehLocked == 0) + { + /* Close the inner composition of state AlarmAcousticAndOptical */ + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) + { + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = + FALSE; + } } - } else { - if (_state_->AlarmOnlyOptical_OPEN) { - /* Execute state AlarmOnlyOptical */ - if (_state_->Counter == 0) { - /* Close the inner composition of state AlarmOnlyOptical */ - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterEnd_OPEN) { - _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmOnlyOptical_OPEN = FALSE; - _state_->AlarmArmed_OPEN = TRUE; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmOnlyOptical */ - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmOnlyOptical_CounterEnd_OPEN) { - _state_->AlarmOnlyOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmOnlyOptical_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //possible BUG - } else { - /* Perform during and on-event actions of state AlarmOnlyOptical */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(1); - if (_state_->AlarmOnlyOptical_CounterPlus_OPEN) { - /* Execute state AlarmOnlyOptical.CounterPlus */ - if (_state_->Counter < TIMEOUT3 && _io_->VehLocked == 1) { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmOnlyOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterEnd */ - _state_->Counter = 0; - } - } else { - if (_state_->AlarmOnlyOptical_CounterStart_OPEN) { - /* Execute state AlarmOnlyOptical.CounterStart */ - _state_->AlarmOnlyOptical_CounterStart_OPEN = FALSE; - _state_->AlarmOnlyOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } - } - } - } - } else { - if (_state_->AlarmAcousticAndOptical_OPEN) { - /* Execute state AlarmAcousticAndOptical */ - if (_state_->Counter == 0) { - /* Close the inner composition of state AlarmAcousticAndOptical */ - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) { - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmAcousticAndOptical_OPEN = FALSE; - _state_->AlarmOnlyOptical_OPEN = TRUE; - /* Open the inner composition of state AlarmOnlyOptical */ - /* Enter state AlarmOnlyOptical.CounterStart */ - _state_->AlarmOnlyOptical_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmOnlyOptical.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - /* Close the inner composition of state AlarmAcousticAndOptical */ - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - } else { - if (_state_->AlarmAcousticAndOptical_CounterEnd_OPEN) { - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = FALSE; - } - } - } - _state_->AlarmAcousticAndOptical_OPEN = FALSE; - //BUG _state_->VehicleOpen_OPEN = TRUE; //BUG does not work - } else { - /* Perform during and on-event actions of state AlarmAcousticAndOptical */ - _io_->AlarmArmed = TO_BOOL(0); - _io_->AcousticAlarm = TO_BOOL(1); - _io_->OpticalAlarm = TO_BOOL(1); - if (_state_->AlarmAcousticAndOptical_CounterStart_OPEN) { - /* Execute state AlarmAcousticAndOptical.CounterStart */ - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - if (_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) { - /* Execute state AlarmAcousticAndOptical.CounterPlus */ - if (_state_->Counter < TIMEOUT2 && _io_->VehLocked == 1) { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ - _state_->Counter = _state_->Counter + 1; - } else { - _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterEnd */ - _state_->Counter = 0; - } - } - } - } - } - } else { - if (_state_->AlarmArmed_OPEN) { - /* Execute state AlarmArmed */ - if (_io_->AlarmSensor == 1) { - _state_->AlarmArmed_OPEN = FALSE; - _state_->AlarmAcousticAndOptical_OPEN = TRUE; //BUG does not work - /* Open the inner composition of state AlarmAcousticAndOptical */ - /* Enter state AlarmAcousticAndOptical.CounterStart */ - _state_->AlarmAcousticAndOptical_CounterStart_OPEN = TRUE; - /* Perform entry actions of state AlarmAcousticAndOptical.CounterStart */ - _state_->Counter = 1; - } else { - if (_io_->VehLocked == 0) { - _state_->AlarmArmed_OPEN = FALSE; - _state_->VehicleOpen_OPEN = TRUE; //BUG does not work - } else { - /* Perform during and on-event actions of state AlarmArmed */ - _io_->AlarmArmed = TO_BOOL(1); - _io_->AcousticAlarm = TO_BOOL(0); - _io_->OpticalAlarm = TO_BOOL(0); - } - } - } - } + } + _state_->AlarmAcousticAndOptical_OPEN = FALSE; + //BUG _state_->VehicleOpen_OPEN = TRUE; //BUG does not work + } + else + { + /* Perform during and on-event actions of state AlarmAcousticAndOptical */ + _io_->AlarmArmed = TO_BOOL(0); + _io_->AcousticAlarm = TO_BOOL(1); + _io_->OpticalAlarm = TO_BOOL(1); + if(_state_->AlarmAcousticAndOptical_CounterStart_OPEN) + { + /* Execute state AlarmAcousticAndOptical.CounterStart */ + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = FALSE; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + if(_state_->AlarmAcousticAndOptical_CounterPlus_OPEN) + { + /* Execute state AlarmAcousticAndOptical.CounterPlus */ + if(_state_->Counter < TIMEOUT2 && _io_->VehLocked == 1) + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + FALSE; + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterPlus */ + _state_->Counter = _state_->Counter + 1; + } + else + { + _state_->AlarmAcousticAndOptical_CounterPlus_OPEN = + FALSE; + _state_->AlarmAcousticAndOptical_CounterEnd_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterEnd */ + _state_->Counter = 0; + } } + } + } + } + } + else + { + if(_state_->AlarmArmed_OPEN) + { + /* Execute state AlarmArmed */ + if(_io_->AlarmSensor == 1) + { + _state_->AlarmArmed_OPEN = FALSE; + _state_->AlarmAcousticAndOptical_OPEN = + TRUE; //BUG does not work + /* Open the inner composition of state AlarmAcousticAndOptical */ + /* Enter state AlarmAcousticAndOptical.CounterStart */ + _state_->AlarmAcousticAndOptical_CounterStart_OPEN = TRUE; + /* Perform entry actions of state AlarmAcousticAndOptical.CounterStart */ + _state_->Counter = 1; } + else + { + if(_io_->VehLocked == 0) + { + _state_->AlarmArmed_OPEN = FALSE; + _state_->VehicleOpen_OPEN = TRUE; //BUG does not work + } + else + { + /* Perform during and on-event actions of state AlarmArmed */ + _io_->AlarmArmed = TO_BOOL(1); + _io_->AcousticAlarm = TO_BOOL(0); + _io_->OpticalAlarm = TO_BOOL(0); + } + } + } } + } } + } } + } } extern int nondet_int(); -t_Alarm_system_io havocIO() { +t_Alarm_system_io havocIO() +{ t_Alarm_system_io _io_; _io_.VehLocked = nondet_int(); _io_.AlarmSensor = nondet_int(); - __CPROVER_assume(0<=_io_.VehLocked && _io_.VehLocked<=1 && - 0<=_io_.AlarmSensor && _io_.AlarmSensor<=1); + __CPROVER_assume( + 0 <= _io_.VehLocked && _io_.VehLocked <= 1 && 0 <= _io_.AlarmSensor && + _io_.AlarmSensor <= 1); return _io_; } -int main() { - int k=0; +int main() +{ + int k = 0; t_Alarm_system_state _state_; t_Alarm_system_state _state_old; t_Alarm_system_io _io_; - Alarm_system_init(&_io_,&_state_); - while(1) { + Alarm_system_init(&_io_, &_state_); + while(1) + { _state_old = _state_; _io_ = havocIO(); - Alarm_system_compute(&_io_,&_state_); - if(_state_old.AlarmArmed_OPEN && _io_.AlarmSensor) { + Alarm_system_compute(&_io_, &_state_); + if(_state_old.AlarmArmed_OPEN && _io_.AlarmSensor) + { assert(_state_.AlarmAcousticAndOptical_OPEN); } - if(!_state_.InitSystem_OPEN && _state_old.Counter!=0 && !_io_.AlarmSensor && !_io_.VehLocked) assert(_state_.VehicleOpen_OPEN); + if( + !_state_.InitSystem_OPEN && _state_old.Counter != 0 && + !_io_.AlarmSensor && !_io_.VehLocked) + assert(_state_.VehicleOpen_OPEN); } return 0; } diff --git a/regression/cbmc-incr-oneloop/arrays2/main.c b/regression/cbmc-incr-oneloop/arrays2/main.c index 5297bf1ed44..801a4be809f 100644 --- a/regression/cbmc-incr-oneloop/arrays2/main.c +++ b/regression/cbmc-incr-oneloop/arrays2/main.c @@ -2,10 +2,13 @@ int main() { int a[5], b[5]; int x; - for(unsigned i = 0;i<5;i++) { + for(unsigned i = 0; i < 5; i++) + { a[i] = b[i]; - if(i==3) b[i] = x; - if(i>0) assert(a[i-1]==b[i-1]); + if(i == 3) + b[i] = x; + if(i > 0) + assert(a[i - 1] == b[i - 1]); } - assert(a[4]==b[4]); + assert(a[4] == b[4]); } diff --git a/regression/cbmc-incr-oneloop/arrays3/main.c b/regression/cbmc-incr-oneloop/arrays3/main.c index 7d21e2d16dc..06615d7d416 100644 --- a/regression/cbmc-incr-oneloop/arrays3/main.c +++ b/regression/cbmc-incr-oneloop/arrays3/main.c @@ -1,12 +1,14 @@ int main() { int a[5], b[5]; - int x,z; + int x, z; unsigned y; - __CPROVER_assume(2<=y && y<=3); - for(unsigned i = 0;i<5;i++) { + __CPROVER_assume(2 <= y && y <= 3); + for(unsigned i = 0; i < 5; i++) + { a[i] = b[i]; - if(z) a[y] = x; - assert(a[i]==b[i] || a[i]==x); + if(z) + a[y] = x; + assert(a[i] == b[i] || a[i] == x); } } diff --git a/regression/cbmc-incr-oneloop/arrays4/main.c b/regression/cbmc-incr-oneloop/arrays4/main.c index 2cc6a4aec4e..d6cd3687566 100644 --- a/regression/cbmc-incr-oneloop/arrays4/main.c +++ b/regression/cbmc-incr-oneloop/arrays4/main.c @@ -2,13 +2,14 @@ int main() { int a[10], b[10]; int x; - unsigned y,z; - __CPROVER_assume(2<=y && y<=4); - __CPROVER_assume(6<=z && z<=8); + unsigned y, z; + __CPROVER_assume(2 <= y && y <= 4); + __CPROVER_assume(6 <= z && z <= 8); b[y] = x; b[z] = x; - for(unsigned i = 0;i<10;i++) { + for(unsigned i = 0; i < 10; i++) + { a[i] = b[i]; } - assert(a[y]==a[z]); + assert(a[y] == a[z]); } diff --git a/regression/cbmc-incr-oneloop/arrays5/main.c b/regression/cbmc-incr-oneloop/arrays5/main.c index 3da4be5001c..056b801921e 100644 --- a/regression/cbmc-incr-oneloop/arrays5/main.c +++ b/regression/cbmc-incr-oneloop/arrays5/main.c @@ -3,10 +3,11 @@ int a[5], b[5]; int main() { unsigned x; - __CPROVER_assume(0<=x && x<=4); + __CPROVER_assume(0 <= x && x <= 4); b[x] = x; - for(unsigned i=0;i<5;i++) { + for(unsigned i = 0; i < 5; i++) + { a[i] = b[i]; } - assert(a[x]==b[x]); + assert(a[x] == b[x]); } diff --git a/regression/cbmc-incr-oneloop/assertion-after-loop1/main.c b/regression/cbmc-incr-oneloop/assertion-after-loop1/main.c index 115c392b84e..daa17f0439b 100644 --- a/regression/cbmc-incr-oneloop/assertion-after-loop1/main.c +++ b/regression/cbmc-incr-oneloop/assertion-after-loop1/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<4) { - x=x+1; + __CPROVER_assume(0 <= x && x <= 1); + while(x < 4) + { + x = x + 1; } - assert(x<4); + assert(x < 4); } diff --git a/regression/cbmc-incr-oneloop/assertion-after-loop2/main.c b/regression/cbmc-incr-oneloop/assertion-after-loop2/main.c index 8072647d664..cd778b85774 100644 --- a/regression/cbmc-incr-oneloop/assertion-after-loop2/main.c +++ b/regression/cbmc-incr-oneloop/assertion-after-loop2/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<4) { - x=x+1; + __CPROVER_assume(0 <= x && x <= 1); + while(x < 4) + { + x = x + 1; } - assert(x<=4); + assert(x <= 4); } diff --git a/regression/cbmc-incr-oneloop/cruise1/main.c b/regression/cbmc-incr-oneloop/cruise1/main.c index 436b0f029b9..5c877d33a2e 100644 --- a/regression/cbmc-incr-oneloop/cruise1/main.c +++ b/regression/cbmc-incr-oneloop/cruise1/main.c @@ -10,11 +10,12 @@ LNCS Volume 8254, 2013, pp 133-148 */ /*******************************************************************************/ +#include #include #include -#include -typedef struct state { +typedef struct state +{ int mode; int speed; int button; @@ -26,65 +27,126 @@ typedef struct state { #define I_GAS 4 #define I_BRAKE 5 -typedef struct input { +typedef struct input +{ int signal; } t_input; -void init(t_state *s) { +void init(t_state *s) +{ s->mode = 0; s->speed = 0; s->button = 0; } -void compute(t_input* i, t_state *s) { - if((s->mode==0) && (s->speed==0) && (s->button==0)) { - if((i->signal==I_ACC)||(i->signal==I_GAS)) s->speed=1; - else if(i->signal==I_BUTTON) s->button=1; +void compute(t_input *i, t_state *s) +{ + if((s->mode == 0) && (s->speed == 0) && (s->button == 0)) + { + if((i->signal == I_ACC) || (i->signal == I_GAS)) + s->speed = 1; + else if(i->signal == I_BUTTON) + s->button = 1; } - else if((s->mode==0) && (s->speed==1) && (s->button==0)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) s->speed=0; - else if((i->signal==I_GAS)||(i->signal==I_ACC)) s->speed=2; - else if(i->signal==I_BUTTON) { s->button=1; s->mode=1; } + else if((s->mode == 0) && (s->speed == 1) && (s->button == 0)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + s->speed = 0; + else if((i->signal == I_GAS) || (i->signal == I_ACC)) + s->speed = 2; + else if(i->signal == I_BUTTON) + { + s->button = 1; + s->mode = 1; + } } - else if((s->mode==0) && (s->speed==0) && (s->button==1)) { - if((i->signal==I_GAS)||(i->signal==I_ACC)) {s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) s->button=0; + else if((s->mode == 0) && (s->speed == 0) && (s->button == 1)) + { + if((i->signal == I_GAS) || (i->signal == I_ACC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + s->button = 0; } - else if((s->mode==1) && (s->speed==1) && (s->button==1)) { - if(i->signal==I_GAS) { s->speed=2; s->mode=2; } - else if(i->signal==I_BRAKE) { s->speed=0; s->mode=2; } - else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; } + else if((s->mode == 1) && (s->speed == 1) && (s->button == 1)) + { + if(i->signal == I_GAS) + { + s->speed = 2; + s->mode = 2; + } + else if(i->signal == I_BRAKE) + { + s->speed = 0; + s->mode = 2; + } + else if(i->signal == I_BUTTON) + { + s->mode = 0; + s->button = 0; + } } - else if((s->mode==2) && (s->speed==2) && (s->button==1)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) { s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; } + else if((s->mode == 2) && (s->speed == 2) && (s->button == 1)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + { + s->mode = 0; + s->button = 0; + } } - else if((s->mode==2) && (s->speed==0) && (s->button==1)) { - if((i->signal==I_GAS)||(i->signal==I_ACC)) { s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; } + else if((s->mode == 2) && (s->speed == 0) && (s->button == 1)) + { + if((i->signal == I_GAS) || (i->signal == I_ACC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + { + s->mode = 0; + s->button = 0; + } } - else if((s->mode==0) && (s->speed==2) && (s->button==0)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) s->speed=1; - else if(i->signal==I_BUTTON) s->button=1; + else if((s->mode == 0) && (s->speed == 2) && (s->button == 0)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + s->speed = 1; + else if(i->signal == I_BUTTON) + s->button = 1; } - else if((s->mode==0) && (s->speed==2) && (s->button==1)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) { s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) s->button=0; + else if((s->mode == 0) && (s->speed == 2) && (s->button == 1)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + s->button = 0; } } - extern t_input nondet_input(); -void main() { +void main() +{ t_state s; init(&s); - while(1) { + while(1) + { t_input i = nondet_input(); - __CPROVER_assume((1<=i.signal) && (i.signal<=5)); + __CPROVER_assume((1 <= i.signal) && (i.signal <= 5)); t_state s_old = s; - compute(&i,&s); - assert(!(s_old.mode==2 && s_old.speed==2 && i.signal==I_DEC) || - s.mode==1); + compute(&i, &s); + assert( + !(s_old.mode == 2 && s_old.speed == 2 && i.signal == I_DEC) || + s.mode == 1); } } diff --git a/regression/cbmc-incr-oneloop/cruise2/main.c b/regression/cbmc-incr-oneloop/cruise2/main.c index 26d397c06eb..1fc6bd2488e 100644 --- a/regression/cbmc-incr-oneloop/cruise2/main.c +++ b/regression/cbmc-incr-oneloop/cruise2/main.c @@ -10,11 +10,12 @@ LNCS Volume 8254, 2013, pp 133-148 */ /*******************************************************************************/ +#include #include #include -#include -typedef struct state { +typedef struct state +{ int mode; int speed; int button; @@ -26,65 +27,126 @@ typedef struct state { #define I_GAS 4 #define I_BRAKE 5 -typedef struct input { +typedef struct input +{ int signal; } t_input; -void init(t_state *s) { +void init(t_state *s) +{ s->mode = 0; s->speed = 0; s->button = 0; } -void compute(t_input* i, t_state *s) { - if((s->mode==0) && (s->speed==0) && (s->button==0)) { - if((i->signal==I_ACC)||(i->signal==I_GAS)) s->speed=1; - else if(i->signal==I_BUTTON) s->button=1; +void compute(t_input *i, t_state *s) +{ + if((s->mode == 0) && (s->speed == 0) && (s->button == 0)) + { + if((i->signal == I_ACC) || (i->signal == I_GAS)) + s->speed = 1; + else if(i->signal == I_BUTTON) + s->button = 1; } - else if((s->mode==0) && (s->speed==1) && (s->button==0)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) s->speed=0; - else if((i->signal==I_GAS)||(i->signal==I_ACC)) s->speed=2; - else if(i->signal==I_BUTTON) { s->button=1; s->mode=1; } + else if((s->mode == 0) && (s->speed == 1) && (s->button == 0)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + s->speed = 0; + else if((i->signal == I_GAS) || (i->signal == I_ACC)) + s->speed = 2; + else if(i->signal == I_BUTTON) + { + s->button = 1; + s->mode = 1; + } } - else if((s->mode==0) && (s->speed==0) && (s->button==1)) { - if((i->signal==I_GAS)||(i->signal==I_ACC)) {s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) s->button=0; + else if((s->mode == 0) && (s->speed == 0) && (s->button == 1)) + { + if((i->signal == I_GAS) || (i->signal == I_ACC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + s->button = 0; } - else if((s->mode==1) && (s->speed==1) && (s->button==1)) { - if(i->signal==I_GAS) { s->speed=2; s->mode=2; } - else if(i->signal==I_BRAKE) { s->speed=0; s->mode=2; } - else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; } + else if((s->mode == 1) && (s->speed == 1) && (s->button == 1)) + { + if(i->signal == I_GAS) + { + s->speed = 2; + s->mode = 2; + } + else if(i->signal == I_BRAKE) + { + s->speed = 0; + s->mode = 2; + } + else if(i->signal == I_BUTTON) + { + s->mode = 0; + s->button = 0; + } } - else if((s->mode==2) && (s->speed==2) && (s->button==1)) { - if((i->signal==I_BRAKE)/*||(i->signal==I_DEC)*/) { s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; } + else if((s->mode == 2) && (s->speed == 2) && (s->button == 1)) + { + if((i->signal == I_BRAKE) /*||(i->signal==I_DEC)*/) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + { + s->mode = 0; + s->button = 0; + } } - else if((s->mode==2) && (s->speed==0) && (s->button==1)) { - if((i->signal==I_GAS)||(i->signal==I_ACC)) { s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; } + else if((s->mode == 2) && (s->speed == 0) && (s->button == 1)) + { + if((i->signal == I_GAS) || (i->signal == I_ACC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + { + s->mode = 0; + s->button = 0; + } } - else if((s->mode==0) && (s->speed==2) && (s->button==0)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) s->speed=1; - else if(i->signal==I_BUTTON) s->button=1; + else if((s->mode == 0) && (s->speed == 2) && (s->button == 0)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + s->speed = 1; + else if(i->signal == I_BUTTON) + s->button = 1; } - else if((s->mode==0) && (s->speed==2) && (s->button==1)) { - if((i->signal==I_BRAKE)||(i->signal==I_DEC)) { s->speed=1; s->mode=1; } - else if(i->signal==I_BUTTON) s->button=0; + else if((s->mode == 0) && (s->speed == 2) && (s->button == 1)) + { + if((i->signal == I_BRAKE) || (i->signal == I_DEC)) + { + s->speed = 1; + s->mode = 1; + } + else if(i->signal == I_BUTTON) + s->button = 0; } } - extern t_input nondet_input(); -void main() { +void main() +{ t_state s; init(&s); - while(1) { + while(1) + { t_input i = nondet_input(); - __CPROVER_assume((1<=i.signal) && (i.signal<=5)); + __CPROVER_assume((1 <= i.signal) && (i.signal <= 5)); t_state s_old = s; - compute(&i,&s); - assert(!(s_old.mode==2 && s_old.speed==2 && i.signal==I_DEC) || - s.mode==1); + compute(&i, &s); + assert( + !(s_old.mode == 2 && s_old.speed == 2 && i.signal == I_DEC) || + s.mode == 1); } } diff --git a/regression/cbmc-incr-oneloop/induction1/main.c b/regression/cbmc-incr-oneloop/induction1/main.c index 2cc849ab513..abb8711cae4 100644 --- a/regression/cbmc-incr-oneloop/induction1/main.c +++ b/regression/cbmc-incr-oneloop/induction1/main.c @@ -2,14 +2,14 @@ int main() { - signed x,y; + signed x, y; while(1) { - __CPROVER_assume(x>=10); + __CPROVER_assume(x >= 10); signed t = x; - if((long)x+y<=INT_MAX) - x = x+y; + if((long)x + y <= INT_MAX) + x = x + y; y = t; - assert(x>=10); + assert(x >= 10); } } diff --git a/regression/cbmc-incr-oneloop/induction2/main.c b/regression/cbmc-incr-oneloop/induction2/main.c index 12946f5ad41..d893eaaa0cb 100644 --- a/regression/cbmc-incr-oneloop/induction2/main.c +++ b/regression/cbmc-incr-oneloop/induction2/main.c @@ -1,18 +1,18 @@ int main() { - int a, b, c, x, i, temp; - a = 1; - b = 2; - c = 3; - x = 0; + int a, b, c, x, i, temp; + a = 1; + b = 2; + c = 3; + x = 0; - while(1) - { - __CPROVER_assume(x == 0); - temp = a; - a = b; - b = c; - c = temp; - assert(x == 0); - } + while(1) + { + __CPROVER_assume(x == 0); + temp = a; + a = b; + b = c; + c = temp; + assert(x == 0); + } } diff --git a/regression/cbmc-incr-oneloop/minmaxunwind1/main.c b/regression/cbmc-incr-oneloop/minmaxunwind1/main.c index 1da993eca70..f3296613642 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind1/main.c +++ b/regression/cbmc-incr-oneloop/minmaxunwind1/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<10) { - x=x+1; - assert(x<6); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 10) + { + x = x + 1; + assert(x < 6); } } diff --git a/regression/cbmc-incr-oneloop/minmaxunwind2/main.c b/regression/cbmc-incr-oneloop/minmaxunwind2/main.c index 1da993eca70..f3296613642 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind2/main.c +++ b/regression/cbmc-incr-oneloop/minmaxunwind2/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<10) { - x=x+1; - assert(x<6); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 10) + { + x = x + 1; + assert(x < 6); } } diff --git a/regression/cbmc-incr-oneloop/minmaxunwind3/main.c b/regression/cbmc-incr-oneloop/minmaxunwind3/main.c index 1da993eca70..f3296613642 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind3/main.c +++ b/regression/cbmc-incr-oneloop/minmaxunwind3/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<10) { - x=x+1; - assert(x<6); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 10) + { + x = x + 1; + assert(x < 6); } } diff --git a/regression/cbmc-incr-oneloop/minmaxunwind4/main.c b/regression/cbmc-incr-oneloop/minmaxunwind4/main.c index 1da993eca70..f3296613642 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind4/main.c +++ b/regression/cbmc-incr-oneloop/minmaxunwind4/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<10) { - x=x+1; - assert(x<6); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 10) + { + x = x + 1; + assert(x < 6); } } diff --git a/regression/cbmc-incr-oneloop/minmaxunwind5/main.c b/regression/cbmc-incr-oneloop/minmaxunwind5/main.c index 0a3c6de1a3c..1290ced14e6 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind5/main.c +++ b/regression/cbmc-incr-oneloop/minmaxunwind5/main.c @@ -2,11 +2,13 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<10) { - int i=-10; - for(;i<1;i++); - x=x+i; - assert(x<6); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 10) + { + int i = -10; + for(; i < 1; i++) + ; + x = x + i; + assert(x < 6); } } diff --git a/regression/cbmc-incr-oneloop/moreasserts1/main.c b/regression/cbmc-incr-oneloop/moreasserts1/main.c index 5a4e73bda8a..96f9aaf87cb 100644 --- a/regression/cbmc-incr-oneloop/moreasserts1/main.c +++ b/regression/cbmc-incr-oneloop/moreasserts1/main.c @@ -1,20 +1,22 @@ -#include +#include extern int nondet_int(); int main() { - int z=nondet_int(); - int x=0; - __CPROVER_assume(z<0 && z>-10); - while(x<100) { - assert(z -10); + while(x < 100) + { + assert(z < x); int y = nondet_int(); - __CPROVER_assume(y>0 && y<10); - x=x+y; - z=z-x; - assert(x<150); - if(z<-100) z=-z; - assert(z 0 && y < 10); + x = x + y; + z = z - x; + assert(x < 150); + if(z < -100) + z = -z; + assert(z < x); } } diff --git a/regression/cbmc-incr-oneloop/nestedloop1/main.c b/regression/cbmc-incr-oneloop/nestedloop1/main.c index 7d13f71803d..88d6d5fd73d 100644 --- a/regression/cbmc-incr-oneloop/nestedloop1/main.c +++ b/regression/cbmc-incr-oneloop/nestedloop1/main.c @@ -2,11 +2,13 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<4) { // main.1 + __CPROVER_assume(0 <= x && x <= 1); + while(x < 4) // main.1 + { int y = 5; - while(y>2) y-=2; // main.0 - x=x+y; - assert(x<4); + while(y > 2) // main.0 + y -= 2; + x = x + y; + assert(x < 4); } } diff --git a/regression/cbmc-incr-oneloop/no-unwinding-assertion1/main.c b/regression/cbmc-incr-oneloop/no-unwinding-assertion1/main.c index 69ca6220d57..fa663afd989 100644 --- a/regression/cbmc-incr-oneloop/no-unwinding-assertion1/main.c +++ b/regression/cbmc-incr-oneloop/no-unwinding-assertion1/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<15) { - x=x+1; - assert(x<15); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 15) + { + x = x + 1; + assert(x < 15); } } diff --git a/regression/cbmc-incr-oneloop/simpleloop1/main.c b/regression/cbmc-incr-oneloop/simpleloop1/main.c index 7639f34cea3..31dc10313bb 100644 --- a/regression/cbmc-incr-oneloop/simpleloop1/main.c +++ b/regression/cbmc-incr-oneloop/simpleloop1/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<4) { - x=x+1; - assert(x<4); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 4) + { + x = x + 1; + assert(x < 4); } } diff --git a/regression/cbmc-incr-oneloop/simpleloop2/main.c b/regression/cbmc-incr-oneloop/simpleloop2/main.c index edd256c11f0..5d5e32183c5 100644 --- a/regression/cbmc-incr-oneloop/simpleloop2/main.c +++ b/regression/cbmc-incr-oneloop/simpleloop2/main.c @@ -1,6 +1,7 @@ int main() { int x; - for(unsigned i = 0;i<5;i++) x--; - assert(x!=0); + for(unsigned i = 0; i < 5; i++) + x--; + assert(x != 0); } diff --git a/regression/cbmc-incr-oneloop/simpleloop3/main.c b/regression/cbmc-incr-oneloop/simpleloop3/main.c index 9dbd6f810bf..7cded2de097 100644 --- a/regression/cbmc-incr-oneloop/simpleloop3/main.c +++ b/regression/cbmc-incr-oneloop/simpleloop3/main.c @@ -1,6 +1,7 @@ int main() { int x; - for(unsigned i = 0;i<=5;i++) x--; - assert(x!=0); + for(unsigned i = 0; i <= 5; i++) + x--; + assert(x != 0); } diff --git a/regression/cbmc-incr-oneloop/simpleloopmax1/main.c b/regression/cbmc-incr-oneloop/simpleloopmax1/main.c index 7639f34cea3..31dc10313bb 100644 --- a/regression/cbmc-incr-oneloop/simpleloopmax1/main.c +++ b/regression/cbmc-incr-oneloop/simpleloopmax1/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<4) { - x=x+1; - assert(x<4); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 4) + { + x = x + 1; + assert(x < 4); } } diff --git a/regression/cbmc-incr-oneloop/simpleloopmax2/main.c b/regression/cbmc-incr-oneloop/simpleloopmax2/main.c index ba320cd5c9b..86b95806645 100644 --- a/regression/cbmc-incr-oneloop/simpleloopmax2/main.c +++ b/regression/cbmc-incr-oneloop/simpleloopmax2/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<4) { - x=x+1; - assert(x<=4); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 4) + { + x = x + 1; + assert(x <= 4); } } diff --git a/regression/cbmc-incr-oneloop/simplifier1/main.c b/regression/cbmc-incr-oneloop/simplifier1/main.c index fe64405ac9f..a999a5ad168 100644 --- a/regression/cbmc-incr-oneloop/simplifier1/main.c +++ b/regression/cbmc-incr-oneloop/simplifier1/main.c @@ -3,21 +3,35 @@ int main() { int x = 0; int y; - __CPROVER_assume(0<=y && y<=1); - while(1) { - switch(x) { - case 0 : - if(y<=2) { - if(nondet()) x=1; - else y++; + __CPROVER_assume(0 <= y && y <= 1); + while(1) + { + switch(x) + { + case 0: + if(y <= 2) + { + if(nondet()) + x = 1; + else + y++; } - else x=2; + else + x = 2; + break; + case 1: + x = 3; + break; + case 2: + x = 3; + break; + case 3: + if(y < 5) + y++; + break; + default: break; - case 1 : x=3; break; - case 2 : x=3; break; - case 3 : if(y<5) y++; break; - default: break; } - assert(x<=3 && y<=5); + assert(x <= 3 && y <= 5); } } diff --git a/regression/cbmc-incr-oneloop/simplifier2/main.c b/regression/cbmc-incr-oneloop/simplifier2/main.c index c2976ece37d..144aa3ed9b9 100644 --- a/regression/cbmc-incr-oneloop/simplifier2/main.c +++ b/regression/cbmc-incr-oneloop/simplifier2/main.c @@ -1,16 +1,29 @@ int main() { int x; - __CPROVER_assume(0<=x && x<=1); + __CPROVER_assume(0 <= x && x <= 1); int y; - __CPROVER_assume(0<=y && y<=1); - while(1) { - switch(x) { - case 0 : x++; y++; break; - case 1 : x++; break; - case 2 : if(y>10) x=10; else x++; break; - default: break; + __CPROVER_assume(0 <= y && y <= 1); + while(1) + { + switch(x) + { + case 0: + x++; + y++; + break; + case 1: + x++; + break; + case 2: + if(y > 10) + x = 10; + else + x++; + break; + default: + break; } - assert(x<=4); + assert(x <= 4); } } diff --git a/regression/cbmc-incr-oneloop/simplifier3/main.c b/regression/cbmc-incr-oneloop/simplifier3/main.c index f161329c079..c2321dd743b 100644 --- a/regression/cbmc-incr-oneloop/simplifier3/main.c +++ b/regression/cbmc-incr-oneloop/simplifier3/main.c @@ -2,9 +2,10 @@ extern int nondet(); int main() { int x; - __CPROVER_assume(0<=x && x<=1); - while(x<3) { + __CPROVER_assume(0 <= x && x <= 1); + while(x < 3) + { x++; - assert(x<=3); + assert(x <= 3); } } diff --git a/regression/cbmc-incr-oneloop/unwind-forever1/main.c b/regression/cbmc-incr-oneloop/unwind-forever1/main.c index cedd8a2f1ea..ef5351fedc0 100644 --- a/regression/cbmc-incr-oneloop/unwind-forever1/main.c +++ b/regression/cbmc-incr-oneloop/unwind-forever1/main.c @@ -2,10 +2,11 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); + __CPROVER_assume(0 <= x && x <= 1); // no error within loop => will unwind forever if no loop bound is given - while(x<4) { - x=x+1; + while(x < 4) + { + x = x + 1; } assert(x < 4); // goto-symex never gets here unless it detects the loop bound } diff --git a/regression/cbmc-incr-oneloop/unwind-forever2/main.c b/regression/cbmc-incr-oneloop/unwind-forever2/main.c index d38e78f98c9..26565f30d1c 100644 --- a/regression/cbmc-incr-oneloop/unwind-forever2/main.c +++ b/regression/cbmc-incr-oneloop/unwind-forever2/main.c @@ -2,11 +2,12 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); + __CPROVER_assume(0 <= x && x <= 1); // no error within loop => will unwind forever if no loop bound is given - while(x<4) { - x=x+1; - assert(x<=4); + while(x < 4) + { + x = x + 1; + assert(x <= 4); } assert(x < 4); // goto-symex never gets here unless it detects the loop bound } diff --git a/regression/cbmc-incr-oneloop/unwinding-assertion1/main.c b/regression/cbmc-incr-oneloop/unwinding-assertion1/main.c index 69ca6220d57..fa663afd989 100644 --- a/regression/cbmc-incr-oneloop/unwinding-assertion1/main.c +++ b/regression/cbmc-incr-oneloop/unwinding-assertion1/main.c @@ -2,9 +2,10 @@ extern int nondet_int(); int main() { int x = nondet_int(); - __CPROVER_assume(0<=x && x<=1); - while(x<15) { - x=x+1; - assert(x<15); + __CPROVER_assume(0 <= x && x <= 1); + while(x < 15) + { + x = x + 1; + assert(x < 15); } } From 20613e80d95e029d1cd94fab8bc7cad5f93aadcc Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Feb 2019 10:23:40 +0000 Subject: [PATCH 16/16] Ignore properties before unwind min Allows to check assertions only between unwind-min and unwind-max iterations of a specified loop. --- regression/cbmc-incr-oneloop/minmaxunwind4/test.desc | 4 +++- src/goto-checker/symex_bmc_incremental_one_loop.cpp | 2 ++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc index bf0f6adb768..c52e8ccd2bb 100644 --- a/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc +++ b/regression/cbmc-incr-oneloop/minmaxunwind4/test.desc @@ -1,8 +1,10 @@ CORE main.c ---unwind-min 6 --unwind-max 8 --incremental-loop main.0 +--unwind-min 6 --unwind-max 8 --incremental-loop main.0 --ignore-properties-before-unwind-min ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ +^Generated 1 VCC\(s\), \d+ remaining after simplification$ -- +^Generated 6 VCC\(s\), \d+ remaining after simplification$ ^warning: ignoring diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp index 1c3a9750096..73f3dca6c07 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp +++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp @@ -35,6 +35,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt( options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min") : 0) { + ignore_assertions = + options.get_bool_option("ignore-properties-before-unwind-min"); } bool symex_bmc_incremental_one_loopt::should_stop_unwind(