Style guidelines

  • Keep to the column width of the language you are writing assertions for. The verifier’s assertion language is generally whitespace-insensitive.

  • Test scripts should be short and check for one specific language feature. When in doubt, write a separate script.

  • Test scripts should not exhaustively check for all possible graph objects that a code segment should emit. Related features should be grouped together and assertions made about them in separate scripts.

  • Use short, meaningful names for EVars.

Avoid quotation marks in offset specifications, unless they are needed.

Quotes for most tokens are unnecessary (C++)
//- @"f" defines/binding _
void f(int x) { }

is less clear than

Less noise is better (C++)
//- @f defines/binding _
void f(int x) { }

Avoid the more complicated offset specifications when possible.

It is better to change code snippets than to use complicated offset specifications.

f is ambiguous (C++)
//- @#0f defines/binding _
void f(float x) { }

is less clear than

fn is not ambiguous (C++)
//- @fn defines/binding _
void fn(float x) { }

Do not bind dangling EVars.

VarX is otherwise unconstrained (C++)
//- @x defines/binding VarX
int x;

is less clear than

We only care that there exists an edge of a certain kind (C++)
//- @x defines/binding _
int x;

Put shorter assertion blocks about anchors close to those anchors.

Long distances between anchors and assertions (C++)
//- @x defines/binding VarX
int x;
//- @y defines/binding VarY
float y;

//- VarX.node/kind variable
//- VarY.node/kind variable

is less clear than

Short distances between anchors and assertions (C++)
//- @x defines/binding VarX
//- VarX.node/kind variable
int x;
//- @y defines/binding VarY
//- VarY.node/kind variable
float y;

Prefer repeating @ specifications for short anchors to binding EVars.

Unnecessary binding to anchors (C++)
void f() {
//- FCallAnchor=@"f()" ref/call FnF
//- FCallAnchor childof FnF
  f();
}

is less clear than

Repeating offset specifications (C++)
void f() {
//- @"f()" ref/call FnF
//- @"f()" childof FnF
  f();
}

Minimize use of explicit unification.

Explicit unification is important in those cases where you want to check whether you are generating a particular VName. In most test scripts, you should make use of the verifier’s graph search algorithm to discover VNames during execution. This makes verification tests easier to read and less brittle in the face of changing implementations for opaque identifiers.

Testing whether a type generates a specific name (C++)
//- @int ref vname("int#builtin","","","","c++")
using Int = int;

is reasonable; however,

Testing whether two variables have the same type (C++)
//- @int ref IntType=vname("int#builtin","","","","c++")
int x;
//- @int ref SecondIntType=vname("int#builtin","","","","c++")
int y;

is less clear than

Testing whether two variables have the same type (C++)
//- @int ref IntType
int x;
//- @int ref IntType
int y;