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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93378 - (show annotations)
Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File size: 4451 byte(s)
AutoProof: continued ownership implementation.

1 note
2 description: "[
3 Translator for ghost features.
4 ]"
5 date: "$Date$"
6 revision: "$Revision$"
7
8 class
9 E2B_GHOST_TRANSLATOR
10
11 inherit
12
13 E2B_ROUTINE_TRANSLATOR_BASE
14
15 feature -- Basic operations
16
17 translate_ghost_attribute (a_feature: FEATURE_I; a_context_type: TYPE_A)
18 -- Translate ghost attribute `a_feature' of `a_context_type' as a ghost attribute.
19 require
20 is_attribute: a_feature.is_attribute
21 is_ghost: helper.is_ghost (a_feature)
22 local
23 l_attribute_name: STRING
24 do
25 l_attribute_name := name_translator.boogie_name_for_feature (a_feature, a_context_type)
26
27 -- Add field declaration
28 boogie_universe.add_declaration (
29 create {IV_CONSTANT}.make_unique (
30 l_attribute_name,
31 types.field (types.for_type_in_context (a_feature.type, a_context_type))))
32
33 -- Mark field as a ghost field
34 boogie_universe.add_declaration (
35 create {IV_AXIOM}.make (
36 factory.function_call ("IsGhostField", << l_attribute_name >>, types.bool)))
37
38 -- TODO: global field properties
39 if a_feature.type.base_class ~ "MML_SET" then
40
41 end
42
43 -- Add translation references
44 translation_pool.add_type_in_context (a_feature.type, a_context_type)
45 end
46
47 translate_ghost_function (a_feature: FEATURE_I; a_context_type: TYPE_A)
48 -- Translate feature `a_feature' of `a_context_type' as a ghost function.
49 require
50 is_routine: a_feature.is_routine
51 is_function: a_feature.is_function
52 is_ghost: helper.is_ghost (a_feature)
53 local
54 l_function: IV_FUNCTION
55 l_expr_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR
56 do
57 set_context (a_feature, a_context_type)
58 helper.set_up_byte_context (a_feature, a_context_type)
59
60 if
61 not attached Context.byte_code or else
62 not attached Context.byte_code.compound or else
63 not attached Context.byte_code.compound.count = 1 or else
64 not attached {ASSIGN_B} Context.byte_code.compound.first as l_assign_b or else
65 not attached {RESULT_B} l_assign_b.target
66 then
67 -- TODO: error message
68 check False end
69 else
70 -- Create IV_FUNCTION
71 create l_function.make (
72 name_translator.boogie_name_for_feature (a_feature, a_context_type),
73 types.for_type_in_context (a_feature.type, a_context_type))
74 boogie_universe.add_declaration (l_function)
75
76 -- Set up arguments
77 l_function.add_argument ("heap", types.heap_type)
78 l_function.add_argument ("current", types.ref)
79 across arguments_of_current_feature as i loop
80 l_function.add_argument (i.item.name, i.item.boogie_type)
81 end
82
83 -- Translate expression
84 create l_expr_translator.make
85 l_expr_translator.entity_mapping.set_heap (create {IV_ENTITY}.make ("heap", types.heap))
86 l_expr_translator.entity_mapping.set_current (create {IV_ENTITY}.make ("current", types.ref))
87 l_expr_translator.set_context (a_feature, a_context_type)
88 l_assign_b.source.process (l_expr_translator)
89 l_function.set_body (l_expr_translator.last_expression)
90 -- TODO: check safety conditions
91 end
92 end
93
94 translate_ghost_routine_signature (a_feature: FEATURE_I; a_context_type: TYPE_A)
95 -- Translate signature of ghost routine `a_feature' of `a_context_type'.
96 require
97 is_routine: a_feature.is_routine
98 not_function: not a_feature.is_function
99 is_ghost: helper.is_ghost (a_feature)
100 do
101 set_context (a_feature, a_context_type)
102 set_up_boogie_procedure (name_translator.boogie_name_for_feature (a_feature, a_context_type))
103
104 -- Set up arguments
105 add_argument_with_property ("Current", a_context_type, types.ref)
106 across arguments_of_current_feature as i loop
107 add_argument_with_property (i.item.name, i.item.type, i.item.boogie_type)
108 end
109
110 check not current_feature.has_return_value end
111
112 -- Set up contracts (pre/post/inv)
113 -- Set up framing (modify)
114
115 check False end
116 end
117
118 translate_ghost_routine_implementation (a_feature: FEATURE_I; a_context_type: TYPE_A)
119 -- Translate signature of ghost routine `a_feature' of `a_context_type'.
120 require
121 is_routine: a_feature.is_routine
122 not_function: not a_feature.is_function
123 is_ghost: helper.is_ghost (a_feature)
124 local
125 l_impl: IV_IMPLEMENTATION
126 do
127 set_context (a_feature, a_context_type)
128 set_up_boogie_procedure (name_translator.boogie_name_for_feature (a_feature, a_context_type))
129 create l_impl.make (current_boogie_procedure)
130
131 -- Add local variables
132 -- Initialize local variables
133 -- Translate implementation
134
135 check False end
136 end
137
138 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23