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

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

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

revision 93596 by julian, Sat Nov 23 07:32:23 2013 UTC revision 93597 by julian, Tue Dec 3 00:48:44 2013 UTC
# Line 106  feature -- Translation Line 106  feature -- Translation
106                  do                  do
107                          check a_feature.has_return_value end                          check a_feature.has_return_value end
108    
109                          if helper.is_feature_status (a_feature, "ghost") then                          translation_pool.add_functional_feature (a_feature, current_target_type)
110                                  translation_pool.add_ghost_function (a_feature, current_target_type)                          l_name := name_translator.boogie_name_for_functional_feature (a_feature, current_target_type)
                                 l_name := name_translator.boogie_name_for_feature (a_feature, current_target_type)  
                         else  
                                 translation_pool.add_functional_feature (a_feature, current_target_type)  
                                 l_name := name_translator.boogie_name_for_functional_feature (a_feature, current_target_type)  
                         end  
111    
112                          create l_call.make (                          create l_call.make (
113                                  l_name,                                  l_name,

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

  ViewVC Help
Powered by ViewVC 1.1.23