Compiler assertions

Error VC8001

Message: custom admissibility was called

Error VC8002

Message: state was altered after havoc_others()

The error is thrown in custom admissibility check if the state was altered after havoc_others() or if havoc_others() is missing altogether in the custom admissibility check.

Error VC8003

Message: <expr> might overflow (in div/mod case)

Error VC8004

Message: <expr> might overflow

Error VC8005

Message: intercepted call to reads check

Error VC8006

Message: state was altered after reads_havoc()

Error VC8007

Message: the value of '<function-name>' changed (in reads check)

Tip: If you do not need the frameaxiom, then you can always specify reads(set_universe()) to get rid of the reads check.

Error VC8008

Message: <expr> has non-writable ref_cnt and is not listed in atomic(...) (and thus is impossible to claim/unclaim)

Error VC8009

Message: type of object <expr> was not marked with vcc(claimable) -- impossible to claim

Error VC8010

Message: object <expr> might equal <expr> -- in unclaim(c, o1, o2)

Error VC8011

Message: writes clause of the loop might not be included writes clause of the function

Error VC8012

Message: invariant(<expr>) is not admissible

Error VC8013

Message: invariant(<expr>) is not admissible (stuttering)

The invariant fails the following check: inv(old(S), S, p) ==> inv(S, S, p).

Error VC8014

Message: invariant(<expr>) fails on wrap

When wrapping an object you need to make sure its invariant holds. It might be also the case, that while the invariant of the object holds in pre-state of wrap, it does not hold accorss the wrap transition, that is the invariant of the object forbids wrapping at this point.

Error VC8015

Message: invariant(<expr>) fails on unwrap

The invariant of the object being unwrapped does not hold accorss the unwrap transition, that is the invariant of the object forbids unwrapping at this point.

Assertion VC8501

Message: <expr> is typed (in well-formedness check)

Assertion VC8502

Message: <expr> is thread local (in well-formedness check)

Assertion VC8503

Message: <min> <= <expr> && <expr> <= <max> in bitfield assignment

Assertion VC8504

Message: <expr> is valid function pointer -- is typed(...)

Assertion VC8505

Message: inferred assertion: <expr> -- should never fail

Assertion VC8506

Message: <expr> is typed -- in memory write

Assertion VC8507

Message: <expr> is writable -- in memory write

Assertion VC8508

Message: <expr> is a valid claim (in by_claim(<expr>, <expr>))

Assertion VC8509

Message: object <expr> is claimed by <expr> (in by_claim(<expr>, <expr>))

Assertion VC8510

Message: <expr> is writable in call to <expr>

Assertion VC8511

Message: <expr> is typed -- in memory read

Assertion VC8512

Message: <expr> is thread local -- in memory read

Assertion VC8513

Message: invariant(<expr>) of <expr> holds -- before wrap(...)

Assertion VC8514

Message: invariant(<expr>) holds (in admissibility check)

Removed. Will now generate VC8012.

Assertion VC8515

Message: the invariant of <expr> holds -- custom admissibility check

Assertion VC8516

Message: <expr> is mutable (SAL) -- compatibility with vcc1

Assertion VC8517

Message: array <expr> is mutable (SAL) -- compatibility with vcc1

Assertion VC8518

Message: <expr> fits range of <type> -- in type conversion

Assertion VC8519

Message: <expr> != 0 (in division by zero)

Assertion VC8520

Message: chunk <expr> of the claim initially holds

Assertion VC8521

Message: chunk <expr> of the claim holds after a step of the machine

Assertion VC8522

Message: object <expr> was claimed by <expr> -- in unclaim(...)

Assertion VC8523

Message: the disposed claim <expr> is writable

Assertion VC8524

Message: chunk <expr> of invariant of <expr> holds after atomic

Assertion VC8525

Message: invariant of <expr> holds after atomic -- when the exact notation is unknown

Assertion VC8526

Message: claim <expr> is valid

Assertion VC8527

Message: <expr> is closed (for atomic(...))