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

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

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

revision 93596 by julian, Sat Nov 23 08:02:05 2013 UTC revision 93597 by julian, Tue Dec 3 00:48:44 2013 UTC
# Line 238  feature -- Translation Line 238  feature -- Translation
238                  local                  local
239                          l_target: IV_EXPRESSION                          l_target: IV_EXPRESSION
240                          l_target_type: TYPE_A                          l_target_type: TYPE_A
241                          l_call: IV_PROCEDURE_CALL                          l_pcall: IV_PROCEDURE_CALL
242                            l_fcall: IV_FUNCTION_CALL
243                  do                  do
244                          if a_for_creator then                          if helper.is_functional (a_feature) then
245                                  translation_pool.add_referenced_creator (a_feature, current_target_type)                                  check not a_for_creator end
                         else  
246                                  translation_pool.add_referenced_feature (a_feature, current_target_type)                                  translation_pool.add_referenced_feature (a_feature, current_target_type)
247                          end                                  if a_feature.has_return_value then
   
                         if a_for_creator then  
                                 create l_call.make (name_translator.boogie_name_for_creation_routine (a_feature, current_target_type))  
                         else  
                                 create l_call.make (name_translator.boogie_name_for_feature (a_feature, current_target_type))  
                         end  
                         l_call.add_argument (current_target)  
248    
249                          process_parameters (a_parameters)                                          create l_fcall.make (name_translator.boogie_name_for_functional_feature (a_feature, current_target_type), types.for_type_a (a_feature.type))
250                          l_call.arguments.append (last_parameters)                                          l_fcall.add_argument (entity_mapping.heap)
251                                            l_fcall.add_argument (current_target)
252                                            process_parameters (a_parameters)
253                                            l_fcall.arguments.append (last_parameters)
254    
255                                  -- Process call                                          last_expression := l_fcall
256                          if a_feature.has_return_value then                                  else
257                                  create_local (a_feature.type.instantiated_in (current_target_type))                                                  -- It's a procedure call, nothing to generate
258                                  l_call.set_target (last_local)                                                  -- There should be an error being reported for this feature
259                                  last_expression := last_local                                          last_expression := Void
260                                    end
261                          else                          else
262                                          -- No expression generated, this has to be a call statement                                  if a_for_creator then
263                                  last_expression := Void                                          translation_pool.add_referenced_creator (a_feature, current_target_type)
264                                            create l_pcall.make (name_translator.boogie_name_for_creation_routine (a_feature, current_target_type))
265                                    else
266                                            translation_pool.add_referenced_feature (a_feature, current_target_type)
267                                            create l_pcall.make (name_translator.boogie_name_for_feature (a_feature, current_target_type))
268                                    end
269                                    l_pcall.add_argument (current_target)
270                                    process_parameters (a_parameters)
271                                    l_pcall.arguments.append (last_parameters)
272    
273                                            -- Process call
274                                    if a_feature.has_return_value then
275                                            create_local (a_feature.type.instantiated_in (current_target_type))
276                                            l_pcall.set_target (last_local)
277                                            last_expression := last_local
278                                    else
279                                                    -- No expression generated, this has to be a call statement
280                                            last_expression := Void
281                                    end
282                                    side_effect.extend (l_pcall)
283                          end                          end
                         side_effect.extend (l_call)  
284                  end                  end
285    
286          process_builtin_routine_call (a_feature: FEATURE_I; a_parameters: BYTE_LIST [PARAMETER_B]; a_builtin_name: STRING)          process_builtin_routine_call (a_feature: FEATURE_I; a_parameters: BYTE_LIST [PARAMETER_B]; a_builtin_name: STRING)

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

  ViewVC Help
Powered by ViewVC 1.1.23