/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/master_clock/f_mc_clock_d.e
ViewVC logotype

Diff of /branches/eth/eve/Src/framework/eiffel2boogie/tests/framing/ownership/master_clock/f_mc_clock_d.e

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

revision 93732 by polikarn, Mon Dec 16 09:25:16 2013 UTC revision 93733 by polikarn, Mon Dec 16 12:32:04 2013 UTC
# Line 15  feature {NONE} -- Initialization Line 15  feature {NONE} -- Initialization
15                          status: creator                          status: creator
16                  require                  require
17                          m_exists: m /= Void                          m_exists: m /= Void
                         default_open: is_open  
18                          default_arg_wrapped: m.is_wrapped                          default_arg_wrapped: m.is_wrapped
19                          modify (Current)                          modify (Current)
20                          modify_field (["observers", "closed"], m)                          modify_field (["observers", "closed"], m)

Legend:
Removed from v.93732  
changed lines
  Added in v.93733

  ViewVC Help
Powered by ViewVC 1.1.23