--- Comment #2 from 2010-11-19 09:45:30 PST ---
(In reply to comment #1)
> Or alternatively, have the compiler define a debug/version identifier when
> compiled in release mode, and then just use conditional compilation.

In that case the compiler can't enforce this constraint:

> can't be accessed inside static or instance methods of the
> class/struct/union,

The idea is that ghost field may be read/written only inside
pre/post-conditions and invariants.

Configure issuemail:
------- You are receiving this mail because: -------

Reply via email to