Error VC0031

Message: '<type>' does not contain a definition for '<field>'

You get this message when trying to access non-structural type using field syntax or when referencing a non-existing field of a structural type.
See the following example for an error of the first kind:

#include "vcc.h"

struct Y { int y; };

struct X {
    struct Y *y;
    invariant(y.y==42) // fails
    // You get: 'Y*' does not contain a definition for 'y'. Correctly you
    // should have written -> instead of ., i.e., invariant(y->y==42)
    invariant(set_in(y,owns(this)))
};

(Because the faulty access is inside an annotation, you do not get a message by cl.exe as is usually the case.)

Error VC9600

Message: OOPS: <msg>

Error VC9601

Message: pointer types in subtraction differ

Error VC9602

Message: function pointer casts are only allowed in non-pure context

Error VC9603

Message: function pointers: different number of parameters

Error VC9604

Message: function pointers: different types of parameters

Error VC9605

Message: function pointers: different return types

Error VC9608

Message: expressions are not the same: <expr> !== <expr>

Error VC9610

Message: don't know how to take address of <expr>

Error VC9611

Message: assignment used in pure context

Error VC9612

Message: don't know how to write to <expr>

Error VC9613

Message: void-call used in pure context

Error VC9614

Message: expression with side effects used in pure context <expr>

Error VC9615

Message: expecting more arguments in call to <function-name>

Error VC9616

Message: <type> is not a pointer

Error VC9617

Message: unsupported thing passed to writes check

Error VC9618

Message: unsupported writes clause <expr>

Error VC9619

Message: non-pointer reads clauses are not supported

Error VC9620

Message: need at least one physical field in structure, got only spec fields

Error VC9621

Message: call to wrap(...) with a improper type: <type>

Error VC9622

Message: the admissibility check function expects a single pointer parameter

Error VC9623

Message: writes specified on a pure function

Error VC9624

Message: custom admissibility checks are not allowed to have explicit requires/ensures/writes

Error VC9625

Message: this function should be called on atomically-updated object

Error VC9626

Message: claim(...) cannot be used inside atomic update/read

Error VC9626

Message: <special-function-name>(...) cannot be used inside atomic update/read

Error VC9627

Message: ordinary functions like <function-name>(...) cannot be used inside atomic update/read

Error VC9628

Message: by_claim(...) expects field or embedded array reference as a second parameter

Error VC9629

Message: by_claim(...) can only refer to a non-volatile field

Error VC9630

Message: Cannot have union type '<union-name>' on backing path '<path>'

Error VC9631

Message: Cannot have backing path '<path>' end in a bitfield

Error VC9632

Message: fields of map type must be declared as specification fields

Error VC9633

Message: '<field-name>' cannot be used as a backing member for '<type-name>'

Error VC9634

Message: Cannot eliminate path '<path>' because its type '<type-name>' has invariants

Error VC9635

Message: function '<function-name>' used in pure context, but not marked with 'ispure'

Error VC9636

Message: wrong number of arguments in call to function '<function-name>'; was <n>, should be <m>

Error VC9637

Message: the pure function '<function-name>' calls '<function-name>' which is not pure

Error VC9638

Message: cycle in pure function calls: <function-name> -> <function-name> -> ...

Error VC9639

Message: function '<function-name>' pretends to be several read checks at once

Error VC9640

Message: the reads check cannot specify additional contract

Error VC9641

Message: the reads check and the function checked have different number of parameters

Error VC9642

Message: the reads check and function checked differ on type of parameter '<parm-name>'

Error VC9643

Message: function '<function-name>' is nowhere to be found (for reads check)

Error VC9644

Message: the admissibility check is required to have a body

Error VC9645

Message: the reads check is required to have a body

Error VC9646

Message: cannot handle val-struct <expr>

Error VC9647

Message: void* and obj_t are not supported in reads clauses

Error VC9648

Message: non-pointers are not supported in reads clauses

Error VC9649

Message: field '<field-name>' of structured type is removed due to union flattening. Refer to its fields instead.

Error VC9650

Message: the specification refers to memory, but function is missing a reads clause

We used to get (0): verification: undeclared identifier: #s before instead of this error.

Fix: specify reads(...), might be reads(set_universe()).

Error VC9651

Message: gemb(...) applied to non-global

gemb(...) can be only applied to global variable or primitive or primitive array type.