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

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

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

revision 93596 by polikarn, Fri Nov 29 18:50:14 2013 UTC revision 93597 by julian, Tue Dec 3 00:48:44 2013 UTC
# Line 22  feature {NONE} -- Initialization Line 22  feature {NONE} -- Initialization
22                  do                  do
23                  end                  end
24    
25  feature -- Basic operations  feature -- Translation: Signature
26    
27          translate_routine_signature (a_feature: FEATURE_I; a_type: TYPE_A)          translate_routine_signature (a_feature: FEATURE_I; a_type: TYPE_A)
28                          -- Translate signature of feature `a_feature' of type `a_type'.                          -- Translate signature of feature `a_feature' of type `a_type'.
29                    require
30                            not_attribute: not a_feature.is_attribute
31                  do                  do
32                          translate_signature (a_feature, a_type, False)                          if helper.is_functional (a_feature) then
33                                    translate_functional_feature (a_feature, a_type)
34                            else
35                                    translate_signature (a_feature, a_type, False)
36                            end
37                  end                  end
38    
39          translate_creator_signature (a_feature: FEATURE_I; a_type: TYPE_A)          translate_creator_signature (a_feature: FEATURE_I; a_type: TYPE_A)
# Line 77  feature -- Basic operations Line 83  feature -- Basic operations
83                          add_result_with_property                          add_result_with_property
84    
85                                  -- Modifies                                  -- Modifies
86                          create l_modifies.make ("Heap")                          if helper.is_lemma (a_feature) then
87                          current_boogie_procedure.add_contract (l_modifies)                                          -- Lemmas do not modify the heap
88                            else
89                                    create l_modifies.make ("Heap")
90                                    current_boogie_procedure.add_contract (l_modifies)
91                            end
92    
93                                  -- Pre- and postconditions                                  -- Pre- and postconditions
94                          l_contracts := contracts_of (current_feature, current_type)                          l_contracts := contracts_of (current_feature, current_type)
# Line 99  feature -- Basic operations Line 109  feature -- Basic operations
109    
110                                  -- Framing                                  -- Framing
111                          if options.is_ownership_enabled then                          if options.is_ownership_enabled then
112                                  add_ownership_contracts (a_for_creator)                                  if not helper.is_lemma (a_feature) then
113                                            add_ownership_contracts (a_for_creator)
114                                    end
115                          else                          else
116                                  if helper.feature_note_values (current_feature, "framing").has ("False") then                                  if helper.feature_note_values (current_feature, "framing").has ("False") then
117                                                  -- No frame condition                                                  -- No frame condition
# Line 265  feature -- Basic operations Line 277  feature -- Basic operations
277                          Result := l_forall                          Result := l_forall
278                  end                  end
279    
280            translate_functional_feature (a_feature: FEATURE_I; a_context_type: TYPE_A)
281                            -- Translate feature `a_feature' of `a_context_type' as a functional feature.
282                    require
283                            is_functional: helper.is_functional (a_feature)
284                    local
285                            l_function: IV_FUNCTION
286                            l_expr_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR
287                    do
288                            set_context (a_feature, a_context_type)
289                            helper.set_up_byte_context (a_feature, a_context_type)
290    
291                            if a_feature.has_return_value then
292                                            -- Create IV_FUNCTION
293                                    create l_function.make (
294                                            name_translator.boogie_name_for_functional_feature (a_feature, a_context_type),
295                                            types.for_type_in_context (a_feature.type, a_context_type))
296                                    boogie_universe.add_declaration (l_function)
297    
298                                            -- Set up arguments
299                                    l_function.add_argument ("heap", types.heap_type)
300                                    l_function.add_argument ("current", types.ref)
301                                    across arguments_of_current_feature as i loop
302                                            l_function.add_argument (i.item.name, i.item.boogie_type)
303                                    end
304                            end
305    
306                            if
307                                    not a_feature.has_return_value or else
308                                    not a_feature.is_routine or else
309                                    not attached Context.byte_code or else
310                                    not attached Context.byte_code.compound or else
311                                    not attached Context.byte_code.compound.count = 1 or else
312                                    not attached {ASSIGN_B} Context.byte_code.compound.first as l_assign_b or else
313                                    not attached {RESULT_B} l_assign_b.target
314                            then
315                                    if not a_feature.is_function or not a_feature.is_routine then
316                                            helper.add_semantic_error (current_feature, messages.functional_feature_not_function)
317                                    else
318                                            helper.add_semantic_error (current_feature, messages.functional_feature_not_single_assignment)
319                                    end
320                            else
321                                            -- Translate expression
322                                    create l_expr_translator.make
323                                    l_expr_translator.entity_mapping.set_heap (create {IV_ENTITY}.make ("heap", types.heap))
324                                    l_expr_translator.entity_mapping.set_current (create {IV_ENTITY}.make ("current", types.ref))
325                                    l_expr_translator.set_context (a_feature, a_context_type)
326                                    l_assign_b.source.process (l_expr_translator)
327                                    l_function.set_body (l_expr_translator.last_expression)
328                            end
329                    end
330    
331    feature -- Translation: Implementation
332    
333          translate_routine_implementation (a_feature: FEATURE_I; a_type: TYPE_A)          translate_routine_implementation (a_feature: FEATURE_I; a_type: TYPE_A)
334                          -- Translate implementation of feature `a_feature' of type `a_type'.                          -- Translate implementation of feature `a_feature' of type `a_type'.
335                  require                  require
336                          routine: a_feature.is_routine                          routine: a_feature.is_routine
337                  do                  do
338                          translate_implementation (a_feature, a_type, False)                          if helper.is_functional (a_feature) then
339                                    translate_functional_check (a_feature, a_type)
340                            else
341                                    translate_implementation (a_feature, a_type, False)
342                            end
343                  end                  end
344    
345          translate_creator_implementation (a_feature: FEATURE_I; a_type: TYPE_A)          translate_creator_implementation (a_feature: FEATURE_I; a_type: TYPE_A)
# Line 281  feature -- Basic operations Line 350  feature -- Basic operations
350    
351          translate_implementation (a_feature: FEATURE_I; a_type: TYPE_A; a_for_creator: BOOLEAN)          translate_implementation (a_feature: FEATURE_I; a_type: TYPE_A; a_for_creator: BOOLEAN)
352                          -- Translate implementation of feature `a_feature' of type `a_type'.                          -- Translate implementation of feature `a_feature' of type `a_type'.
353                    require
354                            not_functional: not helper.is_functional (a_feature)
355                  local                  local
356                          l_procedure: IV_PROCEDURE                          l_procedure: IV_PROCEDURE
357                          l_implementation: IV_IMPLEMENTATION                          l_implementation: IV_IMPLEMENTATION
# Line 334  feature -- Basic operations Line 405  feature -- Basic operations
405                                  end                                  end
406                          end                          end
407                                  -- OWNERSHIP: start of routine body                                  -- OWNERSHIP: start of routine body
408                          if options.is_ownership_enabled then                          if options.is_ownership_enabled and not helper.is_lemma (a_feature) then
409                                  if a_for_creator then                                  if a_for_creator then
410                                                  -- Add creator initialization for ownership                                                  -- Add creator initialization for ownership
411                                          create l_assign.make (factory.heap_current_access (l_translator.entity_mapping, "owns", types.set (types.ref)), factory.function_call ("Set#Empty", <<>>, types.set (types.ref)))                                          create l_assign.make (factory.heap_current_access (l_translator.entity_mapping, "owns", types.set (types.ref)), factory.function_call ("Set#Empty", <<>>, types.set (types.ref)))
# Line 369  feature -- Basic operations Line 440  feature -- Basic operations
440                                  end                                  end
441                          end                          end
442    
                         if a_for_creator then  
 --                                      -- Creator finalizer: set "initialized" to true  
 --                              create l_assign.make (factory.heap_current_initialized (l_translator.entity_mapping), factory.true_)  
 --                              l_implementation.body.add_statement (l_assign)  
                         end  
   
443                                  -- OWNERSHIP: end of routine body                                  -- OWNERSHIP: end of routine body
444                          if options.is_ownership_enabled then                          if options.is_ownership_enabled and not helper.is_lemma (a_feature) then
445                                  if not helper.is_explicit (current_feature, "wrapping") then                                  if not helper.is_explicit (current_feature, "wrapping") then
446                                          if a_for_creator or helper.is_public (current_feature) and not a_feature.has_return_value then                                          if a_for_creator or helper.is_public (current_feature) and not a_feature.has_return_value then
447                                                  l_implementation.body.add_statement (factory.procedure_call ("wrap", << "Current" >>))                                                  l_implementation.body.add_statement (factory.procedure_call ("wrap", << "Current" >>))
# Line 385  feature -- Basic operations Line 450  feature -- Basic operations
450                          end                          end
451                  end                  end
452    
453            translate_functional_check (a_feature: FEATURE_I; a_type: TYPE_A)
454                            -- Trnslate check that functional feature `a_feature' is well-formed.
455                    require
456                            is_functional: helper.is_functional (a_feature)
457                    do
458                                    -- TODO: implement
459                            check True end
460                    end
461    
462    feature -- Translation: Other
463    
464          translate_functional_representation (a_feature: FEATURE_I; a_type: TYPE_A)          translate_functional_representation (a_feature: FEATURE_I; a_type: TYPE_A)
465                          -- Translate implementation of feature `a_feature' of type `a_type'.                          -- Translate implementation of feature `a_feature' of type `a_type'.

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

  ViewVC Help
Powered by ViewVC 1.1.23