/[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 93377 by julian, Thu Nov 14 08:30:25 2013 UTC revision 93378 by julian, Thu Nov 14 15:57:08 2013 UTC
# Line 239  feature -- Basic operations Line 239  feature -- Basic operations
239                                          create l_post.make (forall_mml_set_property ("observers", "is_wrapped"))                                          create l_post.make (forall_mml_set_property ("observers", "is_wrapped"))
240                                          current_boogie_procedure.add_contract (l_post)                                          current_boogie_procedure.add_contract (l_post)
241                                  elseif helper.is_public (current_feature) then                                  elseif helper.is_public (current_feature) then
242                                          create l_pre.make (factory.function_call ("is_wrapped", << "Heap", "Current" >>, types.bool))                                          if current_feature.has_return_value then
243                                          current_boogie_procedure.add_contract (l_pre)                                                  create l_pre.make (factory.function_call ("!is_open", << "Heap", "Current" >>, types.bool))
244                                          create l_pre.make (forall_mml_set_property ("observers", "is_wrapped"))                                                  current_boogie_procedure.add_contract (l_pre)
245                                          current_boogie_procedure.add_contract (l_pre)                                                  create l_pre.make (forall_mml_set_property ("observers", "!is_open"))
246                                          create l_post.make (factory.function_call ("is_wrapped", << "Heap", "Current" >>, types.bool))                                                  current_boogie_procedure.add_contract (l_pre)
247                                          current_boogie_procedure.add_contract (l_post)                                                  create l_post.make (factory.function_call ("!is_open", << "Heap", "Current" >>, types.bool))
248                                          create l_post.make (forall_mml_set_property ("observers", "is_wrapped"))                                                  current_boogie_procedure.add_contract (l_post)
249                                          current_boogie_procedure.add_contract (l_post)                                                  create l_post.make (forall_mml_set_property ("observers", "!is_open"))
250                                                    current_boogie_procedure.add_contract (l_post)
251                                            else
252                                                    create l_pre.make (factory.function_call ("is_wrapped", << "Heap", "Current" >>, types.bool))
253                                                    current_boogie_procedure.add_contract (l_pre)
254                                                    create l_pre.make (forall_mml_set_property ("observers", "is_wrapped"))
255                                                    current_boogie_procedure.add_contract (l_pre)
256                                                    create l_post.make (factory.function_call ("is_wrapped", << "Heap", "Current" >>, types.bool))
257                                                    current_boogie_procedure.add_contract (l_post)
258                                                    create l_post.make (forall_mml_set_property ("observers", "is_wrapped"))
259                                                    current_boogie_procedure.add_contract (l_post)
260                                            end
261                                  else                                  else
262                                          create l_pre.make (factory.function_call ("is_open", << "Heap", "Current" >>, types.bool))                                          create l_pre.make (factory.function_call ("is_open", << "Heap", "Current" >>, types.bool))
263                                          current_boogie_procedure.add_contract (l_pre)                                          current_boogie_procedure.add_contract (l_pre)

Legend:
Removed from v.93377  
changed lines
  Added in v.93378

  ViewVC Help
Powered by ViewVC 1.1.23