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

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

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

revision 93596 by julian, Thu Nov 28 16:42:09 2013 UTC revision 93597 by julian, Tue Dec 3 00:48:44 2013 UTC
# Line 137  feature -- Feature status helpers Line 137  feature -- Feature status helpers
137                          Result := is_feature_status (a_feature, "ghost")                          Result := is_feature_status (a_feature, "ghost")
138                  end                  end
139    
140            is_functional (a_feature: FEATURE_I): BOOLEAN
141                            -- Is `a_feature' a ghost feature?
142                    do
143                            Result := is_feature_status (a_feature, "functional")
144                    end
145    
146            is_lemma (a_feature: FEATURE_I): BOOLEAN
147                            -- Is `a_feature' a ghost feature?
148                    do
149                            Result := is_feature_status (a_feature, "lemma")
150                    end
151    
152          is_public (a_feature: FEATURE_I): BOOLEAN          is_public (a_feature: FEATURE_I): BOOLEAN
153                          -- Is `a_feature' a public feature?                          -- Is `a_feature' a public feature?
154                  do                  do
# Line 361  feature -- Other Line 373  feature -- Other
373                          autoproof_errors.extend (l_error)                          autoproof_errors.extend (l_error)
374                  end                  end
375    
376          add_semantic_error (a_class: CLASS_C; a_feature: FEATURE_I; a_message: STRING)          add_semantic_error (a_class_or_feature: ANY; a_message: STRING)
377                          -- Add AutoProof error about unsupported construct.                          -- Add AutoProof error about unsupported construct.
378                          -- If `a_class' is set, the error will be associated with the class.                          -- If `a_class' is set, the error will be associated with the class.
379                          -- If `a_feature' is set, the error will be associated with the feature and its written class.                          -- If `a_feature' is set, the error will be associated with the feature and its written class.
380                  require                  require
381                          not_class_and_feature: a_class = Void or a_feature = Void                          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)
382                          message_set: a_message /= Void and then not a_message.is_empty                          message_set: a_message /= Void and then not a_message.is_empty
383                  local                  local
384                          l_error: E2B_AUTOPROOF_ERROR                          l_error: E2B_AUTOPROOF_ERROR
# Line 374  feature -- Other Line 386  feature -- Other
386                          create l_error                          create l_error
387                          l_error.set_type ("Error")                          l_error.set_type ("Error")
388                          l_error.set_single_line_message (a_message)                          l_error.set_single_line_message (a_message)
389                          if a_feature /= Void then                          if attached {FEATURE_I} a_class_or_feature as x then
390                                  l_error.set_eiffel_feature (a_feature)                                  l_error.set_eiffel_feature (x)
391                          elseif a_class /= Void then                          elseif attached {CLASS_C} a_class_or_feature as x then
392                                  l_error.set_eiffel_class (a_class)                                  l_error.set_eiffel_class (x)
393                          end                          end
394                          autoproof_errors.extend (l_error)                          autoproof_errors.extend (l_error)
395                  end                  end

Legend:
Removed from v.93596  
changed lines
  Added in v.93597

  ViewVC Help
Powered by ViewVC 1.1.23