/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_helper.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_helper.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 94771 - (show annotations)
Thu Apr 3 12:37:44 2014 UTC (5 years, 6 months ago) by polikarn
File size: 26804 byte(s)
Bugfix: redefinitions now taken into account when calculating replaced model queries.
1 note
2 description: "[
3 Helper functions for Eiffel to Boogie translation.
4 ]"
5 date: "$Date$"
6 revision: "$Revision$"
7
8 frozen class
9 E2B_HELPER
10
11 inherit
12
13 E2B_SHARED_CONTEXT
14 export {NONE} all end
15
16 SHARED_WORKBENCH
17 export {NONE} all end
18
19 SHARED_BYTE_CONTEXT
20 export {NONE} all end
21
22 SHARED_SERVER
23 export {NONE} all end
24
25 IV_SHARED_TYPES
26 export {NONE} all end
27
28 INTERNAL_COMPILER_STRING_EXPORTER
29 export {NONE} all end
30
31 feature -- Cache control
32
33 reset
34 -- Reset cached data.
35 do
36 map_access_feature_cache.wipe_out
37 flat_model_cache.wipe_out
38 internal_counter.put (0)
39 -- Reset type varibale counter
40 (create {IV_VAR_TYPE}.reset).do_nothing
41 end
42
43 feature -- General note helpers
44
45 class_note_values (a_class: CLASS_C; a_tag: STRING_32): ARRAYED_LIST [STRING_32]
46 -- List of note values of tag `a_tag'.
47 do
48 create Result.make (5)
49 Result.compare_objects
50 if attached a_class.ast as l_ast then
51 if l_ast.top_indexes /= Void then
52 Result.append (note_values (l_ast.top_indexes, a_tag))
53 end
54 if l_ast.bottom_indexes /= Void then
55 Result.append (note_values (l_ast.bottom_indexes, a_tag))
56 end
57 end
58 ensure
59 result_attached: attached Result
60 end
61
62 feature_note_values (a_feature: FEATURE_I; a_tag: STRING_32): ARRAYED_LIST [STRING_32]
63 -- List of note values of tag `a_tag'.
64 do
65 if a_feature.body /= Void and then a_feature.body.indexes /= Void then
66 Result := note_values (a_feature.body.indexes, a_tag)
67 else
68 create Result.make (0)
69 end
70 ensure
71 result_attached: attached Result
72 end
73
74 note_values (a_indexing_clause: INDEXING_CLAUSE_AS; a_tag: STRING_32): ARRAYED_LIST [STRING_32]
75 -- List of note values of tag `a_tag'.
76 local
77 l_values: EIFFEL_LIST [ATOMIC_AS]
78 do
79 create Result.make (3)
80 Result.compare_objects
81 from
82 a_indexing_clause.start
83 until
84 a_indexing_clause.after
85 loop
86 if a_indexing_clause.item.tag.name_32.is_equal (a_tag) then
87 l_values := a_indexing_clause.item.index_list
88 from
89 l_values.start
90 until
91 l_values.after
92 loop
93 if attached {STRING_AS} l_values.item as l_string then
94 Result.extend (l_string.value_32)
95 else
96 Result.extend (l_values.item.string_value_32)
97 end
98 l_values.forth
99 end
100 end
101 a_indexing_clause.forth
102 end
103 end
104
105 boolean_feature_note_value (a_feature: FEATURE_I; a_tag: STRING_32): BOOLEAN
106 -- Value of a boolean feature note tag, False if not present.
107 local
108 l_values: ARRAYED_LIST [STRING_32]
109 do
110 l_values := feature_note_values (a_feature, a_tag)
111 if not l_values.is_empty then
112 Result := l_values.i_th (1).is_case_insensitive_equal ("true")
113 end
114 end
115
116 boolean_class_note_value (a_class: CLASS_C; a_tag: STRING_32): BOOLEAN
117 -- Value of a boolean feature note tag, False if not present.
118 local
119 l_values: ARRAYED_LIST [STRING_32]
120 do
121 l_values := class_note_values (a_class, a_tag)
122 if not l_values.is_empty then
123 Result := l_values.i_th (1).is_case_insensitive_equal ("true")
124 end
125 end
126
127 integer_feature_note_value (a_feature: FEATURE_I; a_tag: STRING_32): INTEGER
128 -- Value of an integer feature note tag, -1 if not present.
129 local
130 l_values: ARRAYED_LIST [STRING_32]
131 do
132 Result := -1
133 l_values := feature_note_values (a_feature, a_tag)
134 if not l_values.is_empty and then l_values.i_th (1).is_integer then
135 Result := l_values.i_th (1).to_integer
136 end
137 end
138
139 string_class_note_value (a_class: CLASS_C; a_tag: STRING_32): STRING
140 -- Value of an string class note tag, empty string if not present.
141 local
142 l_values: ARRAYED_LIST [STRING_32]
143 do
144 Result := ""
145 l_values := class_note_values (a_class, a_tag)
146 if not l_values.is_empty then
147 Result := l_values.i_th (1).as_string_8
148 end
149 end
150
151 string_feature_note_value (a_feature: FEATURE_I; a_tag: STRING_32): STRING
152 -- Value of an string feature note tag, empty string if not present.
153 local
154 l_values: ARRAYED_LIST [STRING_32]
155 do
156 Result := ""
157 l_values := feature_note_values (a_feature, a_tag)
158 if not l_values.is_empty then
159 Result := l_values.i_th (1).as_string_8
160 end
161 end
162
163 feature -- Feature status helpers
164
165 is_feature_status (a_feature: FEATURE_I; a_value: STRING): BOOLEAN
166 -- Does `a_feature' has a feature note with a tag status that contains the value `a_value'?
167 local
168 l_values: ARRAYED_LIST [STRING_32]
169 do
170 l_values := feature_note_values (a_feature, "status")
171 if not l_values.is_empty then
172 Result := across l_values as i some i.item.as_string_8.is_equal (a_value) end
173 end
174 end
175
176 is_ghost (a_feature: FEATURE_I): BOOLEAN
177 -- Is `a_feature' a ghost feature?
178 do
179 Result := is_feature_status (a_feature, "ghost")
180 end
181
182 is_functional (a_feature: FEATURE_I): BOOLEAN
183 -- Is `a_feature' a ghost feature?
184 do
185 Result := is_feature_status (a_feature, "functional")
186 end
187
188 is_lemma (a_feature: FEATURE_I): BOOLEAN
189 -- Is `a_feature' a ghost feature?
190 do
191 Result := is_feature_status (a_feature, "lemma")
192 end
193
194 is_public (a_feature: FEATURE_I): BOOLEAN
195 -- Is `a_feature' a public feature?
196 do
197 Result := a_feature.is_exported_for (system.any_class.compiled_class)
198 end
199
200 is_private (a_feature: FEATURE_I): BOOLEAN
201 -- Is `a_feature' a public feature?
202 do
203 Result := a_feature.export_status.is_none
204 end
205
206 function_for_logical (a_feature: FEATURE_I): STRING
207 -- Boogie function that `a_feature' maps to;
208 -- Void if `a_feature' is not from a logical class.
209 local
210 l_values: ARRAYED_LIST [STRING_32]
211 do
212 if attached a_feature and then is_class_logical (a_feature.written_class) then
213 l_values := feature_note_values (a_feature, "maps_to")
214 if l_values.is_empty then
215 -- Use standard naming scheme
216 Result := type_for_logical (a_feature.written_class) + "#" + to_camel_case (a_feature.feature_name)
217 else
218 Result := l_values.first
219 end
220 end
221 end
222
223 map_access_feature (a_class: CLASS_C): FEATURE_I
224 -- The feature of the logical class `a_class' that maps to map access in Boogie (if any).
225 require
226 logical_class: is_class_logical (a_class)
227 local
228 l_feature: FEATURE_I
229 do
230 if map_access_feature_cache.has_key (a_class.class_id) then
231 Result := map_access_feature_cache.item (a_class.class_id)
232 else
233 from
234 a_class.feature_table.start
235 until
236 Result /= Void or a_class.feature_table.after
237 loop
238 l_feature := a_class.feature_table.item_for_iteration
239 if function_for_logical (l_feature) ~ "[]" then
240 Result := l_feature
241 end
242 a_class.feature_table.forth
243 end
244 map_access_feature_cache.put (Result, a_class.class_id)
245 end
246 end
247
248 feature_with_string_note_value (a_class: CLASS_C; a_tag, a_value: STRING_32): FEATURE_I
249 -- Feature of class `a_class', which has a note where `a_tag' contain `a_value'.
250 local
251 l_feature: FEATURE_I
252 do
253 from
254 a_class.feature_table.start
255 until
256 Result /= Void or a_class.feature_table.after
257 loop
258 l_feature := a_class.feature_table.item_for_iteration
259 if feature_note_values (l_feature, a_tag).has (a_value) then
260 Result := l_feature
261 end
262 a_class.feature_table.forth
263 end
264 end
265
266 has_functional_representation (a_feature: FEATURE_I): BOOLEAN
267 -- Will a Boogie function be generated for `a_feature'?
268 do
269 Result := a_feature.has_return_value and not is_feature_status (a_feature, "impure")
270 end
271
272 feature -- Class status helpers
273
274 is_class_logical (a_class: CLASS_C): BOOLEAN
275 -- Is `a_class' mapped to a logical type in a Boogie theory?
276 local
277 l_values: ARRAYED_LIST [STRING_32]
278 do
279 Result := attached type_for_logical (a_class)
280 end
281
282 type_for_logical (a_class: CLASS_C): STRING
283 -- Boogie type that `a_class' maps to;
284 -- Void if `a_class' is not logical.
285 require
286 a_class_exists: attached a_class
287 local
288 l_values: ARRAYED_LIST [STRING_32]
289 do
290 l_values := class_note_values (a_class, "maps_to")
291 if not l_values.is_empty then
292 Result := l_values.first
293 end
294 end
295
296 feature -- Ownership helpers
297
298 is_class_explicit (a_class: CLASS_C; a_type: STRING): BOOLEAN
299 -- Does `a_class' list `a_type' as explicit?
300 local
301 l_values: ARRAYED_LIST [STRING_32]
302 do
303 l_values := class_note_values (a_class, "explicit")
304 if not l_values.is_empty then
305 Result := across l_values as i some i.item.as_string_8 ~ a_type or i.item.as_string_8 ~ "all" end
306 end
307 end
308
309 is_feature_explicit (a_feature: FEATURE_I; a_type: STRING): BOOLEAN
310 -- Does `a_feature' or list `a_type' as explicit?
311 local
312 l_values: ARRAYED_LIST [STRING_32]
313 do
314 l_values := feature_note_values (a_feature, "explicit")
315 if not l_values.is_empty then
316 Result := across l_values as i some i.item.as_string_8 ~ a_type or i.item.as_string_8 ~ "all" end
317 end
318 end
319
320 is_explicit (a_feature: FEATURE_I; a_type: STRING): BOOLEAN
321 -- Does either of the following hold?
322 -- 1. ownership defaults are disabled
323 -- 2. `a_feature' list `a_type' as explicit
324 -- 3. `a_feature' marks all as explicit
325 -- 4. the class of `a_feature' list `a_type' as explicit
326 -- 5. the class of `a_feature' marks all as explicit
327 do
328 Result := not options.is_ownership_defaults_enabled
329 if not Result then
330 Result := is_feature_explicit (a_feature, a_type)
331 end
332 if not Result then
333 Result := is_class_explicit (a_feature.written_class, a_type)
334 end
335 end
336
337 is_clause_reads (a_clause: ASSERT_B): BOOLEAN
338 -- Is contract clause `a_clause' a reads clause?
339 do
340 Result := attached {FEATURE_B} a_clause.expr as l_call and then (l_call.feature_name ~ "reads" or l_call.feature_name ~ "reads_field" or l_call.feature_name ~ "reads_model")
341 end
342
343 is_clause_modify (a_clause: ASSERT_B): BOOLEAN
344 -- Is contract clause `a_clause' a modify clause?
345 do
346 Result := attached {FEATURE_B} a_clause.expr as l_call and then (l_call.feature_name ~ "modify" or l_call.feature_name ~ "modify_field" or l_call.feature_name ~ "modify_model")
347 end
348
349 is_clause_decreases (a_clause: ASSERT_B): BOOLEAN
350 -- Is contract clause `a_clause' a decreases clause?
351 do
352 Result := attached {FEATURE_B} a_clause.expr as l_call and then l_call.feature_name ~ "decreases"
353 end
354
355 boogie_name_for_attribute (a_feature: FEATURE_I; a_context_type: CL_TYPE_A): STRING_32
356 -- Name of the boogie tranlsation of `a_feature', taking special translation of built-ins into account.
357 local
358 l_name: STRING_32
359 do
360 l_name := a_feature.feature_name_32
361 if translation_mapping.ghost_access.has (l_name) then
362 Result := l_name
363 else
364 Result := name_translator.boogie_procedure_for_feature (a_feature, a_context_type)
365 end
366 end
367
368 guard_for_attribute (a_feature: FEATURE_I): STRING_32
369 -- Update guard for attribute `a_feature'.
370 do
371 Result := string_feature_note_value (a_feature, "guard")
372 end
373
374 attribute_from_string (a_name: STRING; a_type: CL_TYPE_A; a_origin_class: CLASS_C; a_context_feature: FEATURE_I; a_context_line_number: INTEGER): FEATURE_I
375 -- Attribute or built-in ghost access with name `a_name' defined in `a_origin_class' in type `a_type'.
376 local
377 l_old_version: FEATURE_I
378 do
379 l_old_version := a_origin_class.feature_named_32 (a_name)
380 if l_old_version = Void then
381 add_semantic_error (a_context_feature, messages.unknown_attribute (a_name, a_origin_class.name_in_upper), a_context_line_number)
382 else
383 Result := a_type.base_class.feature_of_rout_id_set (l_old_version.rout_id_set)
384 check attached Result end
385 if not l_old_version.is_attribute and not translation_mapping.ghost_access.has (a_name) then
386 add_semantic_error (a_context_feature, messages.unknown_attribute (a_name, a_origin_class.name_in_upper), a_context_line_number)
387 end
388 end
389 end
390
391 field_from_attribute (a_feature: FEATURE_I; a_context_type: CL_TYPE_A): IV_ENTITY
392 -- Boogie field entity that corresponds to attribute (or built-in ghost access) `a_feature' in `a_context_type'.
393 local
394 l_type: CL_TYPE_A
395 do
396 if translation_mapping.ghost_access.has (a_feature.feature_name_32) then
397 -- Handle built-in ANY attributes separately, since they are not really attributes.
398 create Result.make (a_feature.feature_name_32, types.field (translation_mapping.ghost_access_type (a_feature.feature_name_32)))
399 else
400 check a_feature.is_attribute end
401 l_type := class_type_in_context (a_feature.type, a_context_type.base_class, Void, a_context_type)
402 create Result.make (name_translator.boogie_procedure_for_feature (a_feature, a_context_type),
403 types.field (types.for_class_type (l_type)))
404 translation_pool.add_referenced_feature (a_feature, a_context_type)
405 end
406 end
407
408 feature -- Model helpers
409
410 model_queries (a_class: CLASS_C): ARRAYED_LIST [STRING_32]
411 -- Names of model queries declared in class `a_class'.
412 do
413 Result := class_note_values (a_class, "model")
414 end
415
416 flat_model_queries (a_class: CLASS_C): ARRAYED_LIST [FEATURE_I]
417 -- Names of model queries declared in class `a_class' and all its ancestors.
418 local
419 l_new_version: FEATURE_I
420 do
421 if flat_model_cache.has_key (a_class.class_id) then
422 Result := flat_model_cache [a_class.class_id]
423 else
424 create Result.make (5)
425 if a_class.class_id = system.any_id then
426 across translation_mapping.ghost_access as m loop
427 Result.extend (a_class.feature_named_32 (m.item))
428 end
429 else
430 across model_queries (a_class) as m loop
431 Result.extend (a_class.feature_named_32 (m.item))
432 end
433 across a_class.parents_classes as c loop
434 across flat_model_queries (c.item) as q loop
435 l_new_version := a_class.feature_of_rout_id_set (q.item.rout_id_set)
436 if not Result.has (l_new_version) then
437 Result.extend (l_new_version)
438 end
439 end
440 end
441 end
442 flat_model_cache.put (Result, a_class.class_id)
443 end
444 end
445
446 is_model_query (a_class: CLASS_C; a_feature: FEATURE_I): BOOLEAN
447 -- Is `a_feature' an immediate or inherited model query of `a_class'?
448 do
449 Result := across flat_model_queries (a_class) as f some is_same_feature (f.item, a_feature) end
450 end
451
452 replaced_model_queries (a_feature: FEATURE_I; a_descendant: CLASS_C): ARRAYED_LIST [FEATURE_I]
453 -- All features replaced by all version of `a_feature' in `a_type',
454 -- as seen from `a_descendant'.
455 require
456 a_feature_exists: attached a_feature
457 local
458 l_rep_clause: ARRAYED_LIST [STRING_32]
459 l_rep_feature: FEATURE_I
460 do
461 create Result.make (5)
462 across all_versions (a_feature) as vers loop
463 l_rep_clause := feature_note_values (vers.item, "replaces")
464 across l_rep_clause as f loop
465 l_rep_feature := vers.item.written_class.feature_named_32 (f.item)
466 if attached l_rep_feature then
467 Result.extend (a_descendant.feature_of_rout_id_set (l_rep_feature.rout_id_set))
468 across replaced_model_queries (l_rep_feature, a_descendant) as q loop
469 if not Result.has (q.item) then
470 Result.extend (q.item)
471 end
472 end
473 end
474 end
475 end
476 end
477
478 replacing_model_queries (a_feature: FEATURE_I; a_class, a_descendant: CLASS_C): ARRAYED_LIST [FEATURE_I]
479 -- All model queries that represent `a_feature' from `a_class'
480 -- in `a_class' and its descendants down to `a_descendant',
481 -- as seen in `a_descendant'.
482 require
483 class_exists: attached a_class
484 feature_exists: attached a_feature
485 feature_is_model: is_model_query (a_class, a_feature)
486 local
487 l_rep_feature, l_new_version: FEATURE_I
488 do
489 create Result.make (5)
490 Result.extend (a_descendant.feature_of_rout_id_set (a_feature.rout_id_set))
491 across a_class.direct_descendants as d loop
492 if a_descendant.inherits_from (d.item) then
493 l_new_version := d.item.feature_of_rout_id_set (a_feature.rout_id_set)
494 if model_queries (d.item).has (l_new_version.feature_name_32) then
495 l_rep_feature := l_new_version
496 else
497 l_rep_feature := feature_with_string_note_value (d.item, "replaces", l_new_version.feature_name_32)
498 end
499 if attached l_rep_feature then
500 across replacing_model_queries (l_rep_feature, d.item, a_descendant) as q loop
501 if not Result.has (q.item) then
502 Result.extend (q.item)
503 end
504 end
505 end
506 end
507 end
508 end
509
510 feature -- String helpers
511
512 feature_of_type_as_string (a_feature: FEATURE_I; a_type: TYPE_A): STRING
513 do
514 Result := "{" + a_type.name + "}." + a_feature.feature_name_32
515 end
516
517 feature -- Eiffel helpers
518
519 is_same_class (c1, c2: CLASS_C): BOOLEAN
520 -- Are `c1' and `c2' the same class?
521 do
522 Result := c1 = c2 or
523 ((c1 /= Void and c2 /= Void) and then c1.class_id = c2.class_id)
524 end
525
526 is_same_feature (f1, f2: FEATURE_I): BOOLEAN
527 -- Are `f1' and `f2' the same feature?
528 do
529 Result := f1 = f2 or
530 ((f1 /= Void and f2 /= Void) and then (f1.written_in = f2.written_in and f1.rout_id_set.first = f2.rout_id_set.first))
531 end
532
533 is_conforming_or_non_conforming_parent_class (a_child, a_parent: CLASS_C): BOOLEAN
534 -- Does `a_child' inherit conforminlgy or non-conformingly from `a_parent'?
535 do
536 Result := a_child.conform_to (a_parent) or else is_non_conforming_parent_class (a_child, a_parent)
537 end
538
539 is_non_conforming_parent_class (a_child, a_parent: CLASS_C): BOOLEAN
540 -- Does `a_child' inherit non-conformingly from `a_parent'?
541 local
542 l_item: CLASS_C
543 do
544 if a_child.non_conforming_parents_classes /= Void then
545 from
546 a_child.non_conforming_parents_classes.start
547 until
548 a_child.non_conforming_parents_classes.after or Result
549 loop
550 l_item := a_child.non_conforming_parents_classes.item
551 Result := l_item.class_id = a_parent.class_id or else is_conforming_or_non_conforming_parent_class (l_item, a_parent)
552 a_child.non_conforming_parents_classes.forth
553 end
554 end
555 end
556
557 feature_for_call_access (a_node: CALL_ACCESS_B; a_target_type: TYPE_A): FEATURE_I
558 -- Feature represented by `a_node'.
559 do
560 check is_conforming_or_non_conforming_parent_class (a_target_type.associated_class, system.class_of_id (a_node.written_in)) end
561 Result := a_target_type.associated_class.feature_of_name_id (a_node.feature_name_id)
562 -- Result := system.class_of_id (a_node.written_in).feature_of_name_id (a_node.feature_name_id)
563 if Result /= Void then
564 -- Not renamed
565 Result := a_target_type.associated_class.feature_of_name_id (a_node.feature_name_id)
566 else
567 -- Renamed
568 Result := a_target_type.associated_class.feature_of_rout_id (a_node.routine_id)
569 end
570 Result := Result.instantiated (a_target_type)
571 check Result /= Void end
572 end
573
574 class_type_in_context (a_type: TYPE_A; a_written_class: CLASS_C; a_feature: FEATURE_I; a_current_type: CL_TYPE_A): CL_TYPE_A
575 -- Class type of `a_type', which is written in `a_written_class' (with optional `a_feature') as seen from `a_current_type'.
576 require
577 no_formals: not a_current_type.has_formal_generic
578 do
579 if a_type.is_like_current then
580 Result := a_current_type
581 else
582 -- `evaluated_type_in_descendant' switches to the correct feature in case of LIKE_FEATURE types
583 -- `deep_actual_type' gets rid of like types
584 -- `instantiated_in (a_current_type)' instantiates the generics
585 check attached {CL_TYPE_A} a_type.evaluated_type_in_descendant (a_written_class, a_current_type.base_class, a_feature).deep_actual_type.instantiated_in (a_current_type) as t then
586 Result := t
587 end
588 end
589 ensure
590 no_formals: not Result.has_formal_generic
591 end
592
593 class_type_from_class (a_class: CLASS_C; a_context_type: CL_TYPE_A): CL_TYPE_A
594 -- Type of ancetor `a_class' in `a_context_type'.
595 do
596 Result := class_type_in_context (a_class.actual_type, a_class, Void, a_context_type)
597 end
598
599 all_versions (a_feature: FEATURE_I): LINKED_LIST [FEATURE_I]
600 -- All written versions of `a_feature'.
601 local
602 l_written_feature: FEATURE_I
603 i: INTEGER
604 do
605 create Result.make
606 -- Add the written version of the feature
607 l_written_feature := a_feature.written_class.feature_of_body_index (a_feature.body_index)
608 Result.extend (l_written_feature)
609 if a_feature.assert_id_set /= Void then
610 -- Redefined feature: return original versions
611 from
612 i := 1
613 until
614 i > a_feature.assert_id_set.count
615 loop
616 l_written_feature := a_feature.assert_id_set [i].written_class.feature_of_body_index (a_feature.assert_id_set [i].body_index)
617 Result.extend (l_written_feature)
618 i := i + 1
619 end
620 end
621 end
622
623 set_any_type: CL_TYPE_A
624 -- Type MML_SET [ANY] (supplier of ANY).
625 do
626 check attached {CL_TYPE_A} system.any_type.base_class.feature_named_32 ("owns").type as t then
627 Result := t
628 end
629 end
630
631 set_class: CLASS_C
632 -- Class MML_SET.
633 do
634 Result := set_any_type.base_class
635 end
636
637 feature -- Byte context helpers
638
639 set_up_byte_context (a_feature: FEATURE_I; a_type: TYPE_A)
640 -- Set up byte context for `a_feature' of type `a_type'.
641 local
642 l_byte_code: BYTE_CODE
643 do
644 -- Clear byte context
645 if a_feature /= Void then
646 Context.clear_feature_data
647 end
648 Context.clear_class_type_data
649 Context.inherited_assertion.wipe_out
650
651 -- Set up class type
652 if not a_type.has_associated_class_type (Void) then
653 if attached {CL_TYPE_A} a_type as l_cl_type_a then
654 a_type.associated_class.update_types (l_cl_type_a)
655 else
656 check False end
657 end
658 end
659 check a_type.has_associated_class_type (Void) end
660 Context.init (a_type.associated_class_type (Void))
661
662 -- Set up feature data
663 if a_feature /= Void then
664 Context.set_current_feature (a_feature)
665 if byte_server.has (a_feature.body_index) then
666 l_byte_code := byte_server.item (a_feature.body_index)
667 Context.set_byte_code (l_byte_code)
668 end
669 end
670 end
671
672 set_up_byte_context_type (a_type: TYPE_A; a_context: TYPE_A)
673 -- Set up byte context.
674 do
675 -- Set up class type
676 if not a_type.has_associated_class_type (Void) then
677 if attached {CL_TYPE_A} a_type as l_cl_type_a then
678 a_type.associated_class.update_types (l_cl_type_a)
679 else
680 check False end
681 end
682 end
683 check a_type.has_associated_class_type (Void) end
684 Context.init (a_type.associated_class_type (Void))
685
686 -- Set up context type
687 if not a_context.has_associated_class_type (Void) then
688 if attached {CL_TYPE_A} a_context as l_cl_type_a then
689 a_context.associated_class.update_types (l_cl_type_a)
690 else
691 check False end
692 end
693 end
694 check a_context.has_associated_class_type (Void) end
695 Context.change_class_type_context (
696 a_type.associated_class_type (Void), a_type.associated_class_type (Void).type,
697 a_context.associated_class_type (Void), a_context.associated_class_type (Void).type)
698 end
699
700 feature -- IV nodes helper
701
702
703
704
705 feature -- Other
706
707 is_inlining_routine (a_routine: FEATURE_I): BOOLEAN
708 -- Should routine `a_routine' be inlinied?
709 local
710 l_contract_extractor: EPA_CONTRACT_EXTRACTOR
711 do
712 Result := options.is_inlining_enabled and then
713 boolean_feature_note_value (a_routine, "inline_in_caller")
714 if not Result and options.is_automatic_inlining_enabled then
715 create l_contract_extractor
716 Result := l_contract_extractor.all_postconditions (a_routine).is_empty
717 end
718 if not Result then
719 Result := options.routines_to_inline.has (a_routine.body_index)
720 end
721 end
722
723 internal_counter: CELL [INTEGER]
724 -- Internal shared counter.
725 once
726 create Result.put (0)
727 end
728
729 unique_identifier (a_name: STRING): STRING
730 -- Unique identifier with base name `a_name'.
731 do
732 internal_counter.put (internal_counter.item + 1)
733 check internal_counter.item >= 0 end
734 Result := a_name + "_" + internal_counter.item.out
735 end
736
737 add_unsupported_error (a_class: CLASS_C; a_feature: FEATURE_I; a_message: STRING)
738 -- Add AutoProof error about unsupported construct concerning `a_class_or_feature' with message `a_message'.
739 -- Verification will not proceed.
740 require
741 not_class_and_feature: a_class = Void or a_feature = Void
742 message_set: a_message /= Void and then not a_message.is_empty
743 local
744 l_error: E2B_AUTOPROOF_ERROR
745 do
746 create l_error
747 l_error.set_type ("Unsupported")
748 l_error.set_message (a_message)
749 if a_feature /= Void then
750 l_error.set_feature (a_feature)
751 elseif a_class /= Void then
752 l_error.set_class (a_class)
753 end
754 autoproof_errors.extend (l_error)
755 end
756
757 add_semantic_error (a_class_or_feature: ANY; a_message: STRING; a_line_number: INTEGER)
758 -- Add AutoProof validity error concerning `a_class_or_feature' with message `a_message'.
759 -- Verification will not proceed.
760 require
761 class_or_feature_or_void: a_class_or_feature = Void or else (attached {CLASS_C} a_class_or_feature or attached {FEATURE_I} a_class_or_feature)
762 message_set: a_message /= Void and then not a_message.is_empty
763 local
764 l_error: E2B_AUTOPROOF_ERROR
765 do
766 create l_error
767 l_error.set_type ("Validity")
768 l_error.set_message (a_message)
769 if attached {FEATURE_I} a_class_or_feature as x then
770 l_error.set_feature (x)
771 elseif attached {CLASS_C} a_class_or_feature as x then
772 l_error.set_class (x)
773 end
774 l_error.set_line_number (a_line_number)
775 if not autoproof_errors.has (l_error) then
776 autoproof_errors.extend (l_error)
777 end
778 end
779
780 add_semantic_warning (a_class_or_feature: ANY; a_message: STRING; a_line_number: INTEGER)
781 -- Add AutoProof validity warning concerning `a_class_or_feature' with message `a_message'.
782 -- Verification will proceed.
783 require
784 class_or_feature_or_void: a_class_or_feature = Void or else (attached {CLASS_C} a_class_or_feature or attached {FEATURE_I} a_class_or_feature)
785 message_set: a_message /= Void and then not a_message.is_empty
786 local
787 l_error: E2B_AUTOPROOF_ERROR
788 do
789 create l_error
790 l_error.set_type ("Validity")
791 l_error.set_message (a_message)
792 if attached {FEATURE_I} a_class_or_feature as x then
793 l_error.set_feature (x)
794 elseif attached {CLASS_C} a_class_or_feature as x then
795 l_error.set_class (x)
796 end
797 l_error.set_line_number (a_line_number)
798 l_error.set_warning (True)
799 if not autoproof_errors.has (l_error) then
800 autoproof_errors.extend (l_error)
801 end
802 end
803
804 feature {NONE} -- Implementation
805
806 to_camel_case (a_name: STRING): STRING
807 -- Eiffel-style identifier `a_name' converted to camel case.
808 local
809 i: INTEGER
810 do
811 Result := a_name.string
812 from
813 i := 1
814 until
815 not Result.valid_index (i)
816 loop
817 Result.replace_substring (Result.substring (i, i).as_upper, i, i)
818 i := Result.index_of ('_', i)
819 if Result.valid_index (i) then
820 Result.remove (i)
821 end
822 end
823 end
824
825 map_access_feature_cache: HASH_TABLE [FEATURE_I, INTEGER]
826 -- Cache of the feature that translates to map access for each model class.
827 once
828 create Result.make (50)
829 end
830
831 flat_model_cache: HASH_TABLE [ARRAYED_LIST [FEATURE_I], INTEGER]
832 -- Cache of a list of all model queries for each class.
833 once
834 create Result.make (50)
835 end
836
837 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23