note description: "Result of a successful verification." date: "$Date$" revision: "$Revision$" class E2B_SUCCESSFUL_VERIFICATION inherit E2B_VERIFICATION_RESULT feature -- Access original_errors: detachable LINKED_LIST [E2B_VERIFICATION_ERROR] -- Original errors (if any) suggestion: STRING -- Suggestion for user. feature -- Element change add_original_error (a_error: E2B_VERIFICATION_ERROR) -- Add `a_error' to `original_errors'. do if not attached original_errors then create original_errors.make end original_errors.extend (a_error) if attached {E2B_DEFAULT_VERIFICATION_ERROR} a_error as l_default then if l_default.boogie_error.is_precondition_violation then set_suggestion ("You might need to weaken the precondition.") elseif l_default.boogie_error.is_assert_error or l_default.boogie_error.is_postcondition_violation then set_suggestion ("You might need to strenghten the loop invariant or postcondition of called features.") end end end set_suggestion (a_string: STRING) -- Set `suggestion' to `a_string'. do suggestion := a_string.twin end feature -- Display single_line_message (a_formatter: TEXT_FORMATTER) -- do if attached original_errors and then not original_errors.is_empty then a_formatter.add (locale.plural_translation_in_context ("Verification successful after inlining. (See an original error.)", "Verification successful after inlining. (See original errors.)", once "tool.auto_proof.result", original_errors.count)) else a_formatter.add (locale.translation_in_context (once "Verification successful.", once "tool.auto_proof.result")) end end end