note description: "[ TODO ]" date: "$Date$" revision: "$Revision$" frozen class E2B_OPTIONS create make feature {NONE} -- Initialization make -- Initialize default options. do is_two_step_verification_enabled := False is_inlining_enabled := True is_automatic_inlining_enabled := False is_automatic_loop_unrolling_enabled := False is_sound_loop_unrolling_enabled := True is_postcondition_predicate_enabled := False is_checking_overflow := False is_generating_triggers := False is_triggering_on_arithmetic := False is_arithmetic_extracted := False is_inv_check_independent := True is_ignoring_nonvariant := False is_ownership_enabled := True is_ownership_defaults_enabled := True loop_unrolling_depth := 7 max_recursive_inlining_depth := 4 is_postcondition_mutation_enabled := False is_coupled_mutations_enabled := True is_aging_enabled := False is_uncoupled_mutations_enabled := False is_trace_enabled := False is_generating_trivial_loop_variants := True is_bulk_verification_enabled := True max_parallel_boogies := 3 is_print_time := True end feature -- Inlining verification step is_two_step_verification_enabled: BOOLEAN -- Is a verification with inlining done in case of failed verifications? set_two_step_verification_enabled (a_value: BOOLEAN) -- Set `is_two_step_verification_enabled' to `a_value'. do is_two_step_verification_enabled := a_value end feature --Postcondition mutation step is_postcondition_mutation_enabled: BOOLEAN -- Should postcondition mutation be executed? set_postcondition_mutation_enabled (a_value: BOOLEAN) -- Set `is_postcondition_mutation_enabled' to `a_value'. do is_postcondition_mutation_enabled := a_value end is_coupled_mutations_enabled : BOOLEAN -- Execute postcondition mutation with coupled mutations? -- This is usually the minimum, but can be turned off if uncoupled is used instead. set_coupled_mutations_enabled (a_value: BOOLEAN) -- Set `is_coupled_mutations_enabled' to `a_value'. do is_coupled_mutations_enabled := a_value end is_uncoupled_mutations_enabled: BOOLEAN -- Execute postcondition mutation with uncoupled mutations? set_uncoupled_mutations_enabled(a_value: BOOLEAN) -- Set `is_uncoupled_mutations_enabled' to `a_value'. do is_uncoupled_mutations_enabled := a_value end is_aging_enabled : BOOLEAN -- Execute postcondition mutation with variable aging? set_aging_enabled (a_value: BOOLEAN) -- Set `is_aging_enabled' to `a_value'. do is_aging_enabled := a_value end feature -- Inlining options is_inlining_enabled: BOOLEAN -- Is inlining enabled? inlining_depth: INTEGER -- Current inlining depth. max_recursive_inlining_depth: INTEGER -- Maximum inlining depth for inlining recursive features. set_max_recursive_inlining_depth (a_value: INTEGER) -- Set `max_recursive_inlining_depth' to `a_value'. do max_recursive_inlining_depth := a_value end set_inlining_depth (a_value: INTEGER) -- Set `inlining_depth' to `a_value'. do inlining_depth := a_value end is_automatic_inlining_enabled: BOOLEAN -- Is automatic inlining of certain routines enabled? set_automatic_inlining_enabled (a_value: BOOLEAN) -- Set `is_automatic_inlining_enabled' to `a_value'. do is_automatic_inlining_enabled := a_value end routines_to_inline: LINKED_LIST [INTEGER] -- Routines to inline. once create Result.make end feature -- Loop unrolling loop_unrolling_depth: INTEGER -- Loop unrolling depth. set_loop_unrolling_depth (a_value: INTEGER) -- Set `loop_unrolling_depth' to `a_value'. do loop_unrolling_depth := a_value end is_automatic_loop_unrolling_enabled: BOOLEAN -- Is automatic unrolling of certain loops enabled? set_automatic_loop_unrolling_enabled (a_value: BOOLEAN) -- Set `is_automatic_loop_unrolling_enabled' to `a_value'. do is_automatic_loop_unrolling_enabled := a_value end is_sound_loop_unrolling_enabled: BOOLEAN -- Is loop unrolling being done in a sound way? set_sound_loop_unrolling_enabled (a_value: BOOLEAN) -- Set `is_sound_loop_unrolling_enabled' to `a_value'. do is_sound_loop_unrolling_enabled := a_value end feature -- Precondition and postcondition predicates is_postcondition_predicate_enabled: BOOLEAN -- Is generation of postcondition predicates enabled? set_postcondition_predicate_enabled (a_value: BOOLEAN) -- Set `is_postcondition_predicate_enabled' to `a_value'. do is_postcondition_predicate_enabled := a_value end feature -- Arithmetic operations is_checking_overflow: BOOLEAN -- Is checking of overflow enabled? set_checking_overflow (a_value: BOOLEAN) -- Set `is_checking_overflow' to `a_value'. do is_checking_overflow := a_value end feature -- Quantifiers is_generating_triggers: BOOLEAN -- Should AutoProof add triggers to quantified expressions? set_generating_triggers (a_value: BOOLEAN) -- Set `is_generating_triggers' to `a_value'. do is_generating_triggers := a_value end is_triggering_on_arithmetic: BOOLEAN -- Should arithmetic operations inside quantifiers be translated as functions, -- so that they can be used in triggers? set_triggering_on_arithmetic (a_value: BOOLEAN) -- Set `is_triggering_on_arithmetic' to `a_value'. do is_triggering_on_arithmetic := a_value end is_arithmetic_extracted: BOOLEAN -- Should arithmetic operations in function/map arguments inside quantifiers -- be extracted into fresh bound variables? set_arithmetic_extracted (a_value: BOOLEAN) -- Set `is_arithmetic_extracted' to `a_value'. do is_arithmetic_extracted := a_value end is_inv_check_independent: BOOLEAN -- Should each invariant clause be checked independently? set_inv_check_independent (a_value: BOOLEAN) -- Set `is_inv_check_independent' to `a_value'. do is_inv_check_independent := a_value end is_ignoring_nonvariant: BOOLEAN -- Should the "nonvariant" annotation be ignored? set_ignoring_nonvariant (a_value: BOOLEAN) -- Set `is_ignoring_nonvariant' to `a_value'. do is_ignoring_nonvariant := a_value end feature -- Framing is_ownership_enabled: BOOLEAN -- Is ownership enabled? set_ownership_enabled (a_value: BOOLEAN) -- Set `is_ownership_enabled' to `a_value'. do is_ownership_enabled := a_value end is_ownership_defaults_enabled: BOOLEAN -- Is ownership enabled? set_ownership_defaults_enabled (a_value: BOOLEAN) -- Set `is_ownership_defaults_enabled' to `a_value'. do is_ownership_defaults_enabled := a_value end feature -- Boogie/Z3 is_enforcing_timeout: BOOLEAN -- Is timeout enforced? set_is_enforcing_timeout (a_value: BOOLEAN) -- Set `is_enforcing_timeout' to `a_value'. do is_enforcing_timeout := a_value end timeout: INTEGER -- Timeout of z3 in seconds. set_timeout (a_value: INTEGER) -- Set `timeout' to `a_value'. do timeout := a_value end is_trace_enabled: BOOLEAN -- Are trace statements printed? set_is_trace_enabled (a_value: BOOLEAN) -- Set `is_trace_enabled' to `a_value'. do is_trace_enabled := a_value end feature -- Output is_print_time: BOOLEAN -- Is verification time output to the console? set_print_time (a_value: BOOLEAN) -- Set `is_time_output' to `a_value'. do is_print_time := a_value end feature -- Other is_generating_trivial_loop_variants: BOOLEAN -- Are trivially false loop variants generated? is_bulk_verification_enabled: BOOLEAN -- Are classes verified in bulk or by individual routines? set_bulk_verification_enabled (a_value: BOOLEAN) -- Set `is_bulk_verification_enabled' to `a_value'. do is_bulk_verification_enabled := a_value end max_parallel_boogies: INTEGER -- Maximum number of parallel Boogie instances. set_max_parallel_boogies (a_value: INTEGER) -- Set `max_parallel_boogies' to `a_value'. do max_parallel_boogies := a_value end end