note
	description: "Result of verifying a Boogie program."
	date: "$Date$"
	revision: "$Revision$"

class
	E2B_BOOGIE_RESULT

create
	make

feature {NONE} -- Initialization

	make
			-- Initialize result.
		do
			create boogie_errors.make
			create procedure_results.make
		end

feature -- Access

	boogie_version: STRING
			-- Boogie version.

	boogie_errors: LINKED_LIST [STRING]
			-- List of Boogie errors.

	procedure_results: LINKED_LIST [E2B_BOOGIE_PROCEDURE_RESULT]
			-- List of procedure results.

	input_text: LIST [STRING]
			-- Input text to Boogie.

feature -- Element change

	set_boogie_version (a_value: STRING)
			-- Set `boogie_version' to `a_value'.
		do
			boogie_version := a_value.twin
		end

	set_input_text (a_text: LIST [STRING])
			-- Set `input_text' to `a_text'
		do
			input_text := a_text
		end

end