/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/exec/e2b_verifier.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/exec/e2b_verifier.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93597 - (show annotations)
Tue Dec 3 00:48:44 2013 UTC (5 years, 10 months ago) by julian
File size: 2390 byte(s)
AutoProof: special translation for lemma and functional
1 note
2 description: "[
3 Interface to run the Boogie verifier.
4
5 Usage:
6 create verifier.make
7 verifier.input.add_boogie_file ("file.bpl")
8 verifier.input.add_custom_content ("some boogie code")
9 verifier.verify
10 verifier.parse_verification_output
11 ]"
12 date: "$Date$"
13 revision: "$Revision$"
14
15 class
16 E2B_VERIFIER
17
18 create
19 make
20
21 feature {NONE} -- Initialization
22
23 make
24 -- Initialize Boogie verifier.
25 do
26 create {E2B_PLATFORM_EXECUTABLE_IMPL} executable
27 create output_parser.make
28 create input.make
29 end
30
31 feature -- Access
32
33 input: E2B_VERIFIER_INPUT
34 -- Input for verifier.
35
36 last_result: detachable E2B_RESULT
37 -- Result of last run of Boogie.
38 do
39 if not attached internal_last_result and then attached last_output then
40 parse_verification_output
41 end
42 Result := internal_last_result
43 end
44
45 last_output: detachable STRING
46 -- Output of last run of Boogie.
47 do
48 Result := executable.last_output
49 end
50
51 feature -- Status report
52
53 is_running: BOOLEAN
54 -- Is Boogie verifier running right now?
55 do
56 Result := executable.is_running
57 end
58
59 feature -- Element change
60
61 set_input (a_input: like input)
62 -- Set `input' to `a_input'.
63 require
64 a_input_attached: attached a_input
65 do
66 input := a_input
67 ensure
68 input_set: input = a_input
69 end
70
71 feature -- Basic operations
72
73 verify
74 -- Launch Boogie verifier on input.
75 do
76 internal_last_result := Void
77 executable.set_input (input)
78 executable.run
79 end
80
81 verify_asynchronous
82 -- Launch Boogie verifier on input, without waiting for Boogie to finish.
83 do
84 internal_last_result := Void
85 executable.set_input (input)
86 executable.run_asynchronous
87 end
88
89 cancel
90 -- Cancel execution of Boogie.
91 do
92 executable.cancel
93 end
94
95 parse_verification_output
96 -- Parse `last_output' and fill `last_result'.
97 require
98 last_output_set: attached last_output
99 local
100 l_boogie_parser: E2B_BOOGIE_OUTPUT_PARSER
101 do
102 create l_boogie_parser.make
103 l_boogie_parser.parse (last_output)
104
105 output_parser.process (last_output)
106 internal_last_result := output_parser.last_result
107 ensure
108 last_result_set: attached last_result
109 end
110
111 feature {NONE} -- Implementation
112
113 executable: attached E2B_EXECUTABLE
114 -- Boogie executable.
115
116 output_parser: attached E2B_OUTPUT_PARSER
117 -- Output parser.
118
119 internal_last_result: detachable E2B_RESULT
120 -- Cached last result.
121
122 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23