/[eiffelstudio]/branches/eth/eve/Src/framework/program_analysis/contract/epa_feature_contract_remover.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/program_analysis/contract/epa_feature_contract_remover.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 98118 - (show annotations)
Thu Nov 19 13:59:02 2015 UTC (3 years, 10 months ago) by maxpei
File size: 9977 byte(s)
Fixed a fault in AutoFix. Due to the fault, violated contract expression may not be used as a fixing target.
1 note
2 description: "Summary description for {EPA_FEATURE_CONTRACT_REMOVER}."
3 author: ""
4 date: "$Date$"
5 revision: "$Revision$"
6
7 class
8 EPA_FEATURE_CONTRACT_REMOVER
9
10 inherit
11 AST_ITERATOR
12 redefine
13 process_check_as
14 end
15
16 SHARED_SERVER
17
18 EPA_UTILITY
19
20 feature -- Basic operation
21
22 remove_contracts_of_features (a_features: DS_HASH_TABLE [DS_HASH_SET [EPA_FEATURE_WITH_CONTEXT_CLASS], BOOLEAN])
23 local
24 l_class_texts: DS_HASH_TABLE [STRING, STRING]
25 do
26 reset
27 initialize_features_with_declarations (a_features)
28 l_class_texts := class_texts_with_feature_contracts_removed
29 save_class_texts (l_class_texts)
30 end
31
32 undo_last_removal
33 local
34 l_cursor: DS_ARRAYED_LIST_CURSOR [PATH]
35 l_file: PLAIN_TEXT_FILE
36 do
37 if last_generated_new_class_paths /= Void and then not last_generated_new_class_paths.is_empty then
38 from
39 l_cursor := last_generated_new_class_paths.new_cursor
40 l_cursor.start
41 until
42 l_cursor.after
43 loop
44 create l_file.make_with_path (l_cursor.item)
45 if l_file.exists then
46 l_file.delete
47 end
48 l_cursor.forth
49 end
50
51 last_generated_new_class_paths := Void
52 end
53 end
54
55 feature -- Status report
56
57 is_last_removal_successful: BOOLEAN
58 -- Is last removal successful?
59
60 feature{NONE} -- Access
61
62 last_generated_new_class_paths: DS_ARRAYED_LIST [PATH]
63
64 features_with_declarations: DS_HASH_TABLE [DS_HASH_TABLE [DS_HASH_SET [FEATURE_I], BOOLEAN], CLASS_C]
65 -- Features whose contracts are to be removed.
66 --
67 -- Key: class
68 -- Sub-key: True for precondition and False for postcondition
69 -- Val: set of features whose contracts to be removed
70 do
71 if features_with_declarations_cache = Void then
72 create features_with_declarations_cache.make_equal (10)
73 end
74 Result := features_with_declarations_cache
75 end
76
77 feature{NONE} -- Implementation
78
79 reset
80 -- Reset the remover.
81 do
82 features_with_declarations_cache := Void
83 end
84
85 initialize_features_with_declarations (a_features: DS_HASH_TABLE [DS_HASH_SET [EPA_FEATURE_WITH_CONTEXT_CLASS], BOOLEAN])
86 local
87 l_table_cursor: DS_HASH_TABLE_CURSOR [DS_HASH_SET [EPA_FEATURE_WITH_CONTEXT_CLASS], BOOLEAN]
88 l_change_type: BOOLEAN
89 l_features: DS_HASH_SET [EPA_FEATURE_WITH_CONTEXT_CLASS]
90 l_features_with_declarations: like features_with_declarations
91 l_feature_cursor: DS_HASH_SET_CURSOR [EPA_FEATURE_WITH_CONTEXT_CLASS]
92 l_feature: EPA_FEATURE_WITH_CONTEXT_CLASS
93 l_classes_with_feature_declarations: DS_ARRAYED_LIST [CLASS_C]
94 l_precursors: DS_HASH_SET [FEATURE_I]
95 l_class_cursor: DS_ARRAYED_LIST_CURSOR [CLASS_C]
96 l_class: CLASS_C
97 l_features_by_change_type: DS_HASH_TABLE [DS_HASH_SET [FEATURE_I], BOOLEAN]
98 do
99 l_features_with_declarations := features_with_declarations
100
101 from
102 l_table_cursor := a_features.new_cursor
103 l_table_cursor.start
104 until
105 l_table_cursor.after
106 loop
107 l_change_type := l_table_cursor.key
108 l_features := l_table_cursor.item
109
110 from
111 l_feature_cursor := l_features.new_cursor
112 l_feature_cursor.start
113 until
114 l_feature_cursor.after
115 loop
116 l_feature := l_feature_cursor.item
117 -- All classes where `l_feature' is (re)defined.
118 create l_classes_with_feature_declarations.make_equal (10)
119 if attached l_feature.feature_.e_feature.precursors as lt_supers then
120 lt_supers.do_all (agent l_classes_with_feature_declarations.force_last)
121 end
122 l_classes_with_feature_declarations.force_last (l_feature.written_class)
123
124 -- All (re)definitions of `l_feature'.
125 from
126 l_class_cursor := l_classes_with_feature_declarations.new_cursor
127 l_class_cursor.start
128 until
129 l_class_cursor.after
130 loop
131 l_class := l_class_cursor.item
132 create l_precursors.make_equal (l_classes_with_feature_declarations.count + 1)
133 if attached l_class.feature_of_rout_id_set (l_feature.feature_.rout_id_set) as lt_feat then
134 l_precursors.force (lt_feat)
135 end
136
137 if not l_precursors.is_empty then
138 if l_features_with_declarations.has (l_class) then
139 if l_features_with_declarations.item (l_class).has (l_change_type) then
140 l_features_with_declarations.item (l_class).item (l_change_type).merge (l_precursors)
141 else
142 l_features_with_declarations.item (l_class).force (l_precursors, l_change_type)
143 end
144 else
145 create l_features_by_change_type.make_equal (2)
146 l_features_by_change_type.force (l_precursors, l_change_type)
147 l_features_with_declarations.force (l_features_by_change_type, l_class)
148 end
149 end
150 l_class_cursor.forth
151 end
152
153 l_feature_cursor.forth
154 end
155
156 l_table_cursor.forth
157 end
158
159 end
160
161 class_texts_with_feature_contracts_removed: DS_HASH_TABLE [STRING, STRING]
162 --
163 local
164 l_table_cursor: DS_HASH_TABLE_CURSOR [DS_HASH_TABLE [DS_HASH_SET [FEATURE_I], BOOLEAN], CLASS_C]
165 l_change_type: BOOLEAN
166 l_table_for_class: DS_HASH_TABLE [DS_HASH_SET [FEATURE_I], BOOLEAN]
167 l_table_for_class_cursor: DS_HASH_TABLE_CURSOR [DS_HASH_SET [FEATURE_I], BOOLEAN]
168
169 l_class: CLASS_C
170 l_class_file_name, l_class_text: STRING
171 l_features: DS_HASH_SET [FEATURE_I]
172 l_feature_cursor: DS_HASH_SET_CURSOR [FEATURE_I]
173 l_feature: FEATURE_I
174 l_asts_to_set_true: DS_ARRAYED_LIST [TAGGED_AS]
175 l_ast_cursor: DS_ARRAYED_LIST_CURSOR [TAGGED_AS]
176 l_match_list: LEAF_AS_LIST
177 do
178 create Result.make_equal (10)
179 from
180 l_table_cursor := features_with_declarations.new_cursor
181 l_table_cursor.start
182 until
183 l_table_cursor.after
184 loop
185 l_class := l_table_cursor.key
186 l_class_file_name := l_class.name_in_upper.as_lower
187 l_table_for_class := l_table_cursor.item
188
189 create l_class_text.make (4096)
190 create l_asts_to_set_true.make_equal (10)
191
192 from
193 l_table_for_class_cursor := l_table_for_class.new_cursor
194 l_table_for_class_cursor.start
195 until
196 l_table_for_class_cursor.after
197 loop
198 l_change_type := l_table_for_class_cursor.key
199 l_features := l_table_for_class_cursor.item
200
201 -- All asts to set true in `l_class'.
202 from
203 l_feature_cursor := l_features.new_cursor
204 l_feature_cursor.start
205 until
206 l_feature_cursor.after
207 loop
208 l_feature := l_feature_cursor.item
209 l_asts_to_set_true.append_last (contract_asts_from_feature (l_feature, l_change_type))
210
211 l_feature_cursor.forth
212 end
213
214 l_table_for_class_cursor.forth
215 end
216
217 l_match_list := Match_list_server.item (l_class.class_id)
218 from
219 l_ast_cursor := l_asts_to_set_true.new_cursor
220 l_ast_cursor.start
221 until
222 l_ast_cursor.after
223 loop
224 l_ast_cursor.item.replace_text ("True", l_match_list)
225 l_ast_cursor.forth
226 end
227 Result.force (l_class.ast.text (l_match_list).twin, l_class_file_name)
228 l_match_list.remove_modifications
229
230 l_table_cursor.forth
231 end
232 end
233
234 add_all_tagged_as (a_eiffel_list: EIFFEL_LIST [TAGGED_AS]; a_list_of_as: DS_ARRAYED_LIST [TAGGED_AS])
235 --
236 local
237 l_cursor: INDEXABLE_ITERATION_CURSOR [TAGGED_AS]
238 do
239 from
240 l_cursor := a_eiffel_list.new_cursor
241 l_cursor.start
242 until
243 l_cursor.after
244 loop
245 a_list_of_as.force_last (l_cursor.item)
246 l_cursor.forth
247 end
248 end
249
250 contract_asts_from_feature (a_feature: FEATURE_I; a_change_type: BOOLEAN): DS_ARRAYED_LIST [TAGGED_AS]
251 -- List of AST nodes from the text of `a_feature' that are contract clauses.
252 --
253 -- At most one node for "require/require else", one node for "ensure/ensure then",
254 -- and one node for each check instruction.
255 require
256 feature_attached: a_feature /= Void
257 local
258 do
259 create Result.make (4)
260 if attached a_feature.e_feature.ast.body.as_routine as l_rout then
261 if a_change_type and then l_rout.precondition /= Void and then l_rout.precondition.assertions /= Void then
262 add_all_tagged_as (l_rout.precondition.assertions, Result)
263 end
264 if not a_change_type and then l_rout.postcondition /= Void and then l_rout.postcondition.assertions /= Void then
265 add_all_tagged_as (l_rout.postcondition.assertions, Result)
266 end
267 collect_checks_from_feature (a_feature)
268 Result.append_last (check_lists)
269 end
270 end
271
272 save_class_texts (a_class_texts: DS_HASH_TABLE [STRING, STRING])
273 --
274 local
275 l_path: PATH
276 l_dir: DIRECTORY
277 l_table_cursor: DS_HASH_TABLE_CURSOR [STRING, STRING]
278 l_class_file_name, l_class_text: STRING
279 l_class_file_path: PATH
280 l_class_file: PLAIN_TEXT_FILE
281 do
282 create last_generated_new_class_paths.make_equal (a_class_texts.count + 1)
283
284 -- Store the new class file into OVERRIDE cluster.
285 l_path := system.eiffel_project.project_directory.path.extended ("override")
286 create l_dir.make_with_path (l_path)
287 if not l_dir.exists then
288 l_dir.recursive_create_dir
289 end
290
291 from
292 l_table_cursor := a_class_texts.new_cursor
293 l_table_cursor.start
294 until
295 l_table_cursor.after
296 loop
297 l_class_file_name := l_table_cursor.key
298 l_class_text := l_table_cursor.item
299
300 l_class_file_path := l_path.extended (l_class_file_name + ".e")
301 last_generated_new_class_paths.force_last (l_class_file_path)
302 create l_class_file.make_with_path (l_class_file_path)
303 l_class_file.open_write
304 l_class_file.put_string (l_class_text)
305 l_class_file.close
306
307 l_table_cursor.forth
308 end
309 end
310
311 feature{NONE} -- Collect check assertions
312
313 check_lists: DS_ARRAYED_LIST [TAGGED_AS]
314
315 collect_checks_from_feature (a_feature: FEATURE_I)
316 -- Collect assertion clauses in CHECK instructions from `a_feature'.
317 -- Make result available in `check_lists'.
318 require
319 feature_attached: a_feature /= Void
320 local
321 do
322 create check_lists.make (10)
323 if attached a_feature.e_feature.ast.body.as_routine as l_rout then
324 l_rout.process (Current)
325 end
326 end
327
328 process_check_as (l_as: CHECK_AS)
329 -- <Precursor>
330 do
331 add_all_tagged_as (l_as.check_list, check_lists)
332 end
333
334 feature{NONE} -- Cache
335
336 features_with_declarations_cache: like features_with_declarations
337
338 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23