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

Diff of /branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_attribute_translator.e

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 94770 by polikarn, Sat Mar 15 14:57:57 2014 UTC revision 94771 by polikarn, Thu Apr 3 12:37:44 2014 UTC
# Line 22  feature -- Basic operations Line 22  feature -- Basic operations
22                          is_attribute: a_feature.is_attribute                          is_attribute: a_feature.is_attribute
23                  local                  local
24                          l_attribute_name, l_old_name: STRING                          l_attribute_name, l_old_name: STRING
25                          l_class_type: CL_TYPE_A                          l_class_type, l_written_type: CL_TYPE_A
26                          l_type_prop, l_expr, l_context_type: IV_EXPRESSION                          l_type_prop, l_expr, l_context_type: IV_EXPRESSION
27                          l_forall: IV_FORALL                          l_forall: IV_FORALL
28                          l_heap, l_o, l_f: IV_ENTITY                          l_heap, l_o, l_f: IV_ENTITY
# Line 49  feature -- Basic operations Line 49  feature -- Basic operations
49    
50                                  -- Add equivalences                                  -- Add equivalences
51                          across previous_versions as prev loop                          across previous_versions as prev loop
52                                          -- Check that properties match                                  if prev.item.is_attribute then
53                                  if helper.is_ghost (prev.item.feat) /= is_ghost then                                                  -- Check that properties match
54                                          helper.add_semantic_error (current_feature, messages.invalid_ghost_status (prev.item.feat.feature_name_32, prev.item.typ.base_class.name_in_upper), -1)                                          if helper.is_ghost (prev.item) /= is_ghost then
55                                  end                                                  helper.add_semantic_error (current_feature, messages.invalid_ghost_status (prev.item.feature_name_32, prev.item.written_class.name_in_upper), -1)
56                                            end
57    
58                                  l_old_name := name_translator.boogie_procedure_for_feature (prev.item.feat, prev.item.typ)                                          l_written_type := helper.class_type_from_class (prev.item.written_class, current_type)
59                                  translation_pool.add_referenced_feature (prev.item.feat, prev.item.typ)                                          l_old_name := name_translator.boogie_procedure_for_feature (prev.item, l_written_type)
60                                  boogie_universe.add_declaration (create {IV_AXIOM}.make (factory.equal (l_f, create {IV_ENTITY}.make (l_old_name, l_f.type))))                                          translation_pool.add_referenced_feature (prev.item, l_written_type)
61                                            boogie_universe.add_declaration (create {IV_AXIOM}.make (factory.equal (l_f, create {IV_ENTITY}.make (l_old_name, l_f.type))))
62                                    end
63                          end                          end
64    
65                                  -- Mark field as a ghost or non-ghost                                  -- Mark field as a ghost or non-ghost
# Line 159  feature -- Basic operations Line 162  feature -- Basic operations
162    
163  feature {NONE} -- Implementation  feature {NONE} -- Implementation
164    
165          previous_versions: LINKED_LIST [TUPLE [feat: FEATURE_I; typ: CL_TYPE_A]]          previous_versions: LINKED_LIST [FEATURE_I]
166                          -- Versions of `current_feature' from ancestors of `current_type' if inherited or redefined.                          -- Versions of `current_feature' from ancestors of `current_type' if inherited or redefined.
                 local  
                         l_written_type: CL_TYPE_A  
                         l_written_feature: FEATURE_I  
                         i: INTEGER  
167                  do                  do
                         create Result.make  
168                          if current_feature.written_in /= current_type.base_class.class_id then                          if current_feature.written_in /= current_type.base_class.class_id then
169                                          -- Inherited attribute: return the class where it is written in                                                                  -- Inherited attribute: return the class where it is written in                        
170                                  l_written_type := helper.class_type_from_class (current_feature.written_class, current_type)                                  create Result.make
171                                  l_written_feature := l_written_type.base_class.feature_of_body_index (current_feature.body_index)                                  Result.extend (current_feature.written_class.feature_of_body_index (current_feature.body_index))
172                                  Result.extend ([l_written_feature, l_written_type])                          else
173                          elseif current_feature.assert_id_set /= Void then                                  Result := helper.all_versions (current_feature)
174                                          -- Redefined attribute: return original versions                                  Result.start
175                                  from                                  Result.remove
                                         i := 1  
                                 until  
                                         i > current_feature.assert_id_set.count  
                                 loop  
                                         l_written_type := helper.class_type_from_class (current_feature.assert_id_set [i].written_class, current_type)  
                                         l_written_feature := l_written_type.base_class.feature_of_body_index (current_feature.assert_id_set [i].body_index)  
                                         if l_written_feature.is_attribute then  
                                                 Result.extend ([l_written_feature, l_written_type])  
                                         end  
                                         i := i + 1  
                                 end  
176                          end                          end
177                  end                  end
178    

Legend:
Removed from v.94770  
changed lines
  Added in v.94771

  ViewVC Help
Powered by ViewVC 1.1.23