/[eiffelstudio]/branches/eth/eve/Src/Eiffel/interface/tty/ewb_boogie_verification.e
ViewVC logotype

Contents of /branches/eth/eve/Src/Eiffel/interface/tty/ewb_boogie_verification.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: 10420 byte(s)
AutoProof: special translation for lemma and functional
1 note
2 description: "Command line command for Boogie verification"
3 date: "$Date$"
4 revision: "$Revision$"
5
6 class
7 EWB_BOOGIE_VERIFICATION
8
9 inherit
10
11 EWB_CMD
12 rename
13 messages as ewb_messages
14 end
15
16 SHARED_ERROR_HANDLER
17 export {NONE} all end
18
19 COMPILER_EXPORTER
20
21 INTERNAL_COMPILER_STRING_EXPORTER
22
23 E2B_SHARED_CONTEXT
24
25 create
26 make_with_arguments
27
28 feature {NONE} -- Initialization
29
30 make_with_arguments (a_arguments: LINKED_LIST [STRING])
31 -- Initialize with `a_arguments'.
32 require
33 a_arguments_attached: a_arguments /= Void
34 do
35 create user_options.make
36 user_options.compare_objects
37 create selection.make
38 from
39 a_arguments.start
40 until
41 a_arguments.after
42 loop
43 if a_arguments.item.starts_with ("-") then
44 user_options.extend (a_arguments.item)
45 a_arguments.forth
46 if not a_arguments.after and a_arguments.item.is_integer then
47 user_options.extend (a_arguments.item)
48 a_arguments.forth
49 end
50 else
51 selection.extend (a_arguments.item)
52 a_arguments.forth
53 end
54 end
55 end
56
57 feature -- Access
58
59 autoproof: E2B_AUTOPROOF
60 -- Autoproof.
61
62 user_options: LINKED_LIST [STRING]
63 -- Option arguments to Boogie command line.
64
65 selection: LINKED_LIST [STRING]
66 -- Class and feature selection arguments to Boogie command line.
67
68 name: STRING
69 do
70 Result := "Boogie Verification"
71 end
72
73 help_message: STRING_GENERAL
74 do
75 Result := "Verify project using Boogie verifier"
76 end
77
78 abbreviation: CHARACTER
79 do
80 Result := 'b'
81 end
82
83 feature -- Execution
84
85 execute
86 -- <Precursor>
87 local
88 html_writer: E2B_HTML_OUTPUT
89 do
90 create autoproof.make
91 -- Load options
92 if user_options.has ("-twostep") then
93 options.set_two_step_verification_enabled (True)
94 elseif user_options.has ("-notwostep") then
95 options.set_two_step_verification_enabled (False)
96 end
97 if user_options.has ("-overflow") then
98 options.set_checking_overflow (True)
99 elseif user_options.has ("-nooverflow") then
100 options.set_checking_overflow (False)
101 end
102 if user_options.has ("-autounroll") then
103 options.set_automatic_loop_unrolling_enabled (True)
104 elseif user_options.has ("-noautounroll") then
105 options.set_automatic_loop_unrolling_enabled (False)
106 end
107 if user_options.has ("-unrolldepth") then
108 options.set_loop_unrolling_depth (option_argument ("-unrolldepth", options.loop_unrolling_depth))
109 end
110 if user_options.has ("-autoinline") then
111 options.set_automatic_inlining_enabled (True)
112 elseif user_options.has ("-noautoinline") then
113 options.set_automatic_inlining_enabled (False)
114 end
115 if user_options.has ("-inlinedepth") then
116 options.set_max_recursive_inlining_depth (option_argument ("-inlinedepth", options.max_recursive_inlining_depth))
117 end
118 if user_options.has ("-ownership") then
119 options.set_ownership_enabled (True)
120 elseif user_options.has ("-noownership") then
121 options.set_ownership_enabled (False)
122 end
123
124 if user_options.has ("-timeout") then
125 options.set_is_enforcing_timeout (True)
126 options.set_timeout (option_argument ("-timeout", options.timeout))
127 end
128
129 if selection.is_empty then
130 load_universe
131 else
132 load_selection
133 end
134 if user_options.has ("-html") then
135 create html_writer
136 autoproof.add_notification (agent html_writer.print_verification_result (?))
137 else
138 autoproof.add_notification (agent print_result (?))
139 end
140 autoproof.verify
141 end
142
143 option_argument (a_option: STRING; a_default: INTEGER): INTEGER
144 require
145 user_options.has (a_option)
146 local
147 l_index: INTEGER
148 do
149 l_index := user_options.index_of (a_option, 1)
150 if l_index > 0 and then user_options.i_th (l_index + 1).is_integer then
151 Result := user_options.i_th (l_index + 1).to_integer
152 else
153 Result := a_default
154 end
155 end
156
157 feature {NONE} -- Printing console
158
159 print_result (a_result: E2B_RESULT)
160 -- Print results to output.
161 do
162 across a_result.autoproof_errors as i loop
163 output_window.add ("AutoProof Error: " + i.item.type)
164 output_window.add_new_line
165 output_window.add (i.item.multi_line_message)
166 output_window.add_new_line
167 end
168 across a_result.procedure_results as i loop
169 output_window.add ("======================================%N")
170 if attached {E2B_SUCCESSFUL_VERIFICATION} i.item as l_success then
171 print_successful_verification (l_success)
172 elseif attached {E2B_FAILED_VERIFICATION} i.item as l_failure then
173 print_failed_verification (l_failure)
174 else
175 check False end
176 end
177 end
178 end
179
180 print_successful_verification (a_success: E2B_SUCCESSFUL_VERIFICATION)
181 -- Print successful verification information.
182 do
183 print_feature_information (a_success)
184 if a_success.original_errors = Void or else a_success.original_errors.is_empty then
185 output_window.add ("Successfully verified.%N")
186 else
187 -- Two-step verification result
188 output_window.add ("Successfully verified after inlining.%N")
189 output_window.add ("Original errors:%N")
190 across a_success.original_errors as i loop
191 if i.cursor_index = 1 then
192 output_window.add_new_line
193 else
194 output_window.add ("--------------------------------------%N")
195 end
196 i.item.multi_line_message (output_window)
197 output_window.add_new_line
198 end
199 end
200 end
201
202 print_failed_verification (a_failure: E2B_FAILED_VERIFICATION)
203 -- Print failed verifcation information.
204 do
205 print_feature_information (a_failure)
206 output_window.add ("Verification failed.%N")
207 across a_failure.errors as i loop
208 if i.cursor_index = 1 then
209 output_window.add_new_line
210 else
211 output_window.add ("--------------------------------------%N")
212 end
213 i.item.multi_line_message (output_window)
214 output_window.add_new_line
215 end
216 end
217
218 print_feature_information (a_proc: E2B_PROCEDURE_RESULT)
219 -- Print feature information.
220 do
221 output_window.add_class (a_proc.eiffel_class.original_class)
222 output_window.add (".")
223 output_window.add_feature (a_proc.eiffel_feature.e_feature, a_proc.eiffel_feature.feature_name_32)
224 output_window.add_new_line
225 end
226
227
228 feature {NONE} -- Implementation
229
230 load_universe
231 -- Load all classes from universe.
232 local
233 l_groups: LIST [CONF_GROUP]
234 do
235 from
236 l_groups := eiffel_universe.groups
237 l_groups.start
238 until
239 l_groups.after
240 loop
241 -- Only load top-level clusters, as they are loaded recursively afterwards
242 if attached {CLUSTER_I} l_groups.item_for_iteration as l_cluster and then l_cluster.parent_cluster = Void then
243 load_cluster (l_cluster)
244 end
245 l_groups.forth
246 end
247 end
248
249 load_selection
250 -- Load classes and features from selection.
251 local
252 l_item: STRING
253 l_parts: LIST [STRING]
254 l_classes: LIST [CLASS_I]
255 do
256 from
257 selection.start
258 until
259 selection.after
260 loop
261 l_item := selection.item
262 if l_item.has ('.') then
263 -- It's an individual feature
264 l_parts := l_item.split ('.')
265 l_classes := universe.classes_with_name (l_parts.i_th (1))
266 if l_classes /= Void and then not l_classes.is_empty then
267 load_feature (l_classes.first, l_parts.i_th (2))
268 else
269 print ("Class " + selection.item + " not found (skipped).%N")
270 end
271 else
272 -- It's a class
273 l_classes := universe.classes_with_name (selection.item)
274 if l_classes /= Void and then not l_classes.is_empty then
275 load_class (l_classes.first)
276 else
277 print ("Class " + selection.item + " not found (skipped).%N")
278 end
279 end
280 selection.forth
281 end
282 end
283
284 load_feature (a_class: CLASS_I; a_feature_name: STRING)
285 -- Load `a_feature' for verification.
286 local
287 l_feature: FEATURE_I
288 do
289 if a_class.is_compiled then
290 l_feature := a_class.compiled_class.feature_named (a_feature_name)
291 if l_feature /= Void then
292 autoproof.add_feature (l_feature)
293 else
294 print ("Feature " + a_class.name + "." + a_feature_name + " not found (skipped).%N")
295 end
296 else
297 print ("Class " + a_class.name + " not compiled (skipped).%N")
298 end
299 end
300
301 load_class (a_class: CLASS_I)
302 -- Load `a_class' for verification.
303 local
304 l_class_c: CLASS_C
305 do
306 if a_class.is_compiled then
307 l_class_c := a_class.compiled_class
308 check l_class_c /= Void end
309 autoproof.add_class (l_class_c)
310 else
311 print ("Class " + a_class.name + " not compiled (skipped).%N")
312 end
313 end
314
315 load_cluster (a_cluster: CLUSTER_I)
316 -- Load `a_cluster' for verification.
317 require
318 a_cluster_not_void: a_cluster /= Void
319 local
320 l_conf_class: CONF_CLASS
321 l_class_i: CLASS_I
322 do
323 from
324 a_cluster.classes.start
325 until
326 a_cluster.classes.after
327 loop
328 l_conf_class := a_cluster.classes.item_for_iteration
329 l_class_i := eiffel_universe.class_named (l_conf_class.name, a_cluster)
330 load_class (l_class_i)
331 a_cluster.classes.forth
332 end
333 if a_cluster.sub_clusters /= Void then
334 from
335 a_cluster.sub_clusters.start
336 until
337 a_cluster.sub_clusters.after
338 loop
339 load_cluster (a_cluster.sub_clusters.item_for_iteration)
340 a_cluster.sub_clusters.forth
341 end
342 end
343 end
344
345 note
346 copyright: "Copyright (c) 1984-2013, Eiffel Software"
347 license: "GPL version 2 (see http://www.eiffel.com/licensing/gpl.txt)"
348 licensing_options: "http://www.eiffel.com/licensing"
349 copying: "[
350 This file is part of Eiffel Software's Eiffel Development Environment.
351
352 Eiffel Software's Eiffel Development Environment is free
353 software; you can redistribute it and/or modify it under
354 the terms of the GNU General Public License as published
355 by the Free Software Foundation, version 2 of the License
356 (available at the URL listed under "license" above).
357
358 Eiffel Software's Eiffel Development Environment is
359 distributed in the hope that it will be useful, but
360 WITHOUT ANY WARRANTY; without even the implied warranty
361 of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
362 See the GNU General Public License for more details.
363
364 You should have received a copy of the GNU General Public
365 License along with Eiffel Software's Eiffel Development
366 Environment; if not, write to the Free Software Foundation,
367 Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
368 ]"
369 source: "[
370 Eiffel Software
371 5949 Hollister Ave., Goleta, CA 93117 USA
372 Telephone 805-685-1006, Fax 805-685-6869
373 Website http://www.eiffel.com
374 Customer support http://support.eiffel.com
375 ]"
376 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23