Apr 19, 2011 at 10:48 AM

If VCC is giving error that it can't verify is something is writable. Is there some way to let VCC assume for the time being that it is writable and carry on with the code.

something like: assume(writable(some_obj))

Apr 19, 2011 at 8:10 PM


  unfortunately at this time there's no "writable()" predicate. Asserting the mutability can help to a certain extent.

  If you want to ignored write and reads checking, you can also use the "/omitrw" switch.

  Best, Mark

Apr 19, 2011 at 9:19 PM

Thanks Mark