12 Attributes🔗

An attribute is a brace-delimited annotation of the form {:name arg, ...} that can be attached to almost every syntactic category in a Boogie program. This is Boogie 2 calls them tool directives and says (section 11) that “the Boogie language does not assign any formal meaning to the attributes”. That was true in 2008 and is no longer true: the Boogie tool now reads well over sixty distinct attribute names, and several of them change whether a program verifies, how many verification conditions are produced, what the solver is told, and — in the case of :checksum — whether an assertion is checked at all.

There is no complete list of these anywhere in the distribution. Boogie ships a partial one behind boogie /attrHelp. This chapter is that list, built by reading every call site of QKeyValue.FindStringAttribute, FindIntAttribute, FindExprAttribute, FindBoolAttribute, FindAttribute, CheckIntAttribute, CheckUIntAttribute, CheckBooleanAttribute and FindAllAttributes in Source/.

Attributes that belong to Civl (:layer, :yields, :linear and friends) are summarised here and described properly in Civl: concurrency and refinement.

12.1 Syntax🔗

Attributes and triggers share one grammar production, because they are lexically ambiguous until the parser has seen the character after the opening brace:

Attribute<ref QKeyValue kv>

=

AttributeOrTrigger<ref kv, ref trig>

.

AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>

=

"{"

(

":" Ident

[ AttributeParameter { "," AttributeParameter } ]

|

Expression { "," Expression }

)

"}"

.

AttributeParameter<out object o>

=

( string

| Expression

)

.

So a brace group whose first character is : is an attribute; anything else is a trigger. In every position that allows attributes but not triggers — which is every position except the body of a quantifier or lambda — the parser calls Attribute, which is AttributeOrTrigger plus a check:

function f(int): int;

procedure {f(0)} P()

{

assert true;

}

boogie attr-trigger-position.bpl

attr-trigger-position.bpl(3,16): error: only attributes, not triggers, allowed here

1 parse errors detected in attr-trigger-position.bpl

An attribute name is an Ident — ordinary Boogie identifier syntax, so {:my_attr} and {:MyAttr9} are fine but {:my-attr} is not. There is a single flat namespace for attribute names shared by Boogie, Civl, Dafny, GPUVerify, SMACK and anything else that emits Boogie; the paper’s advice (section 11.0) to pick tool-distinctive names is still good advice.

Each argument is either a string literal or an expression. There is no other form: there are no bare identifiers-as-symbols, no nested attributes, no key-value pairs. {:smt_option "a", "b"} is a two-string attribute, not a map.

12.1.1 Attributes chain🔗

Several attributes may be written in a row, and the AST stores them as a singly-linked list (QKeyValue.Next), not as a dictionary. Nothing prevents the same name appearing more than once; what happens then depends on which accessor reads it (see below).

assume {:print "line 22"} {:print "i = ", i} true;

12.1.2 Arguments are resolved and type checked🔗

Expression arguments are real expressions: they are resolved and type checked like any other, so a typo is an error rather than an inert annotation.

procedure P()

{

assert {:myattr undeclared_thing} true;

}

boogie attr-arg-typecheck.bpl

attr-arg-typecheck.bpl(3,18): Error: undeclared identifier: undeclared_thing

1 name resolution errors detected in attr-arg-typecheck.bpl

QKeyValue.Resolve raises the resolution state from one-state to two-state before resolving arguments, so old(...) is legal inside an attribute wherever the attribute itself is legal — including on an assert in the middle of a procedure body, where old is not otherwise allowed:

var g: int;

procedure P()

modifies g;

{

g := 1;

assert {:myattr old(g)} true;

}

boogie attr-two-state.bpl

Boogie program verifier finished with 1 verified, 0 errors

Similarly ICarriesAttributes.TypecheckAttributes clears tc.GlobalAccessOnlyInOld for the duration, so attribute arguments are exempt from the Civl restriction that a pure procedure may mention globals only under old.

Two attributes get extra checks during resolution and type checking, in QKeyValue.Resolve and QKeyValue.Typecheck: :minimize / :maximize and :verified_under (below), plus :layer. Every other attribute is accepted by the front end no matter what it is applied to or what arguments it is given.

12.1.3 Unknown attributes are silently accepted🔗

There is no whitelist. An attribute nobody reads costs nothing and produces no diagnostic:

type {:whatever} T;

const {:no_such_attribute "x", 3, true} c: int;

procedure {:completely_made_up} P()

{

assert {:also_made_up 1, 2, 3} true;

}

boogie attr-unknown.bpl

Boogie program verifier finished with 1 verified, 0 errors

This is the reason the rest of this chapter matters: a misspelt {:subsumption 0} is not an error, it is a no-op.

12.2 How Boogie reads an attribute🔗

Every consumer in the source goes through one of eight accessors. Each accepts a different argument shape, and each has a different failure mode. Knowing which accessor reads a given attribute tells you exactly what you can write.

The split matters: the QKeyValue.Find* statics (and the FindBoolAttribute extension built on them) scan the chain and stop at the first match, while the instance methods on Declaration — FindAttribute, FindExprAttribute, and the CheckIntAttribute / CheckUIntAttribute / CheckBooleanAttribute layered on top of them — scan the whole chain and keep the last. So assert {:subsumption 2} {:subsumption 0} e; takes the 2 (FindIntAttribute, first wins) while procedure {:verify false} {:verify true} P() takes the true (CheckBooleanAttribute, last wins).

Three consequences are worth stating outright.

Malformed attributes are usually silent. FindStringAttribute searches for an occurrence with exactly one string parameter; if your {:msg} has an expression argument instead of a string, the search simply finds nothing and the default behaviour applies. The same holds for :timeLimit ten" and :rlimit true}: both are ill-formed and both are ignored without a word. @bpl{ procedure {:timeLimit ten" {:rlimit true} {:priority "high"} P() { assert true; } }

boogie attr-bad-int.bpl

Boogie program verifier finished with 1 verified, 0 errors

{:name false} does not mean “off” for attributes read by FindBoolAttribute — it means the search will not match, which usually gives the same result. But for attributes read by FindAttribute (presence only), such as :isolate and :linear, writing false turns the feature on. See Splitting the verification condition.

Only CheckBooleanAttribute understands false as a way to disable something. That accessor is used for exactly five attributes: :verify, :identity, :never_pattern, :existential and :vcs_split_on_every_assert.

12.3 Where attributes may be written🔗

The grammar admits attributes in the following places. Each row names the production in Source/Core/BoogiePL.atg.

No attributes may be written on havoc, break, hide, reveal, push or pop, nor on the while keyword itself — a loop carries its attributes on the invariant and measure clauses instead. havoc is the omission that surprises people:

procedure P()

{

var x: int;

havoc {:foo} x;

}

boogie attr-havoc.bpl

attr-havoc.bpl(4,9): error: invalid Ident

1 parse errors detected in attr-havoc.bpl

12.3.1 A procedure with a body has two attribute lists🔗

procedure P() { ... } is sugar for a Procedure plus an Implementation, and the parser gives both of them a clone of the attribute list:

procedure {:myAttr 1} P()

{

assert true;

}

boogie /noVerify /print:- attr-clone.bpl

procedure {:myAttr 1} P();

implementation {:myAttr 1} P()

{

assert true;

}

(Every /print listing in this chapter drops the two // banner comments that /print emits first — one of which contains the absolute solver path — and the trailing Boogie program verifier finished with ... line. Nothing else is changed.)

This matters constantly, because many attributes are read only from the Implementation (:priority, :timeLimit, :rlimit, :random_seed, :smt_option, :msg_if_verifies, :entrypoint, :kInductionDepth, the :vcs_* family) and others only from the Procedure. If you split the declaration and the body apart, an attribute that “worked” can stop working with no diagnostic:

procedure {:smt_option "smt.qi.eager_threshold", "10"} {:timeLimit 17} P();

implementation P()

{

assert true;

}

boogie /proverLog:opts2.smt2 attr-smt-options-proc.bpl

grep set-option opts2.smt2

Boogie program verifier finished with 1 verified, 0 errors

(set-option :print-success false)

(set-option :smt.mbqi false)

(set-option :model.compact false)

(set-option :model.v2 true)

(set-option :pp.bv_literals false)

(set-option :timeout 0)

(set-option :rlimit 0)

(set-option :smt.mbqi false)

(set-option :model.compact false)

(set-option :model.v2 true)

(set-option :pp.bv_literals false)

Neither the SMT option nor the time limit reached the solver. Put the same attributes on the implementation and both appear (see Procedures and implementations).

A visible side-effect of the cloning is that a resolution error inside an attribute on a procedure-with-body is reported twice — once for the procedure and once for the implementation.

12.3.2 Quantifiers: before the bound variables means something else🔗

This is the single most common attribute mistake in Boogie. In

(forall A x: int :: B trigger body)

A is parsed by AttributesIdsTypeWheres and attaches to the bound variable x; B is parsed by QuantifierBody and attaches to the quantifier. Nothing in the syntax hints that the two are read by completely different code. :pool is the only attribute read from position A; :qid, :weight, :add_to_pool and :nopats are read only from position B. (The pretty-printer does round-trip both positions faithfully — BinderExpr.Emit writes the quantifier’s own attributes after the :: and the bound variables’ with the variables — so /print:- will tell you which one you actually wrote.)

function f(int): int;

axiom (forall {:qid "f_def"} {:weight 3} x: int :: {f(x)} f(x) == x + 1);

procedure P() { assert f(0) == 1; }

boogie /proverLog:wrong.smt2 attr-quant-wrong.bpl

The relevant part of wrong.smt2:

(declare-fun f (Int) Int)

(assert (forall ((x Int) ) (! (= (f x) (+ x 1))

:qid |attrquantwrongbpl.2:42|

:skolemid |0|

:pattern ( (f x))

)))

The :qid is the auto-generated file.line:col one and there is no :weight at all. Move both attributes past the :::

function f(int): int;

axiom (forall x: int :: {:qid "f_def"} {:weight 3} {f(x)} f(x) == x + 1);

procedure P() { assert f(0) == 1; }

boogie /proverLog:right.smt2 attr-quant-right.bpl

The relevant part of right.smt2:

(declare-fun f (Int) Int)

(assert (forall ((x Int) ) (! (= (f x) (+ x 1))

:qid f_def

:weight 3

:skolemid |0|

:pattern ( (f x))

)))

12.4 Top-level declarations🔗

12.4.1 {:ignore}🔗

No arguments (FindBoolAttribute). Any top-level declaration.

The declaration is registered (so its name is taken and duplicate-name checking still applies) and then dropped from the program before resolution, in Program.Resolve. It therefore contributes nothing to the solver.

function g(int): int;

axiom {:ignore} (forall x: int :: {g(x)} g(x) == 0);

axiom (forall x: int :: {g(x)} g(x) == 1);

procedure P()

{

assert g(0) == 1;

}

boogie attr-ignore.bpl

Boogie program verifier finished with 1 verified, 0 errors

Boogie also adds {:ignore} itself, to the loser of an :extern clash.

12.4.2 {:extern}🔗

No arguments (FindBoolAttribute). Any top-level declaration, plus axioms carrying :name.

Two declarations of the same name are normally a resolution error:

function f(int): int;

function f(int): int;

boogie attr-extern-dup.bpl

attr-extern-dup.bpl(2,9): Error: more than one declaration of function name: f

1 name resolution errors detected in attr-extern-dup.bpl

If at least one of them carries :extern, ResolutionContext.SelectNonExtern keeps the non-:extern one and prepends :ignore to the other. If both are :extern, it tests the two in an unspecified order and drops whichever it tests first, so which one survives is arbitrary — Boogie’s own /attrHelp says as much. The intent is that a prelude may declare a symbol :extern and a generated program may then redeclare and override it.

function {:extern} f(int): int;

axiom {:extern} {:name "f_def"} (forall x: int :: {f(x)} f(x) == 0);

function f(int): int;

axiom {:name "f_def"} (forall x: int :: {f(x)} f(x) == x);

procedure P(y: int)

{

assert f(y) == y;

}

boogie attr-extern.bpl

Boogie program verifier finished with 1 verified, 0 errors

The non-:extern axiom won, so f(y) == y holds.

12.4.3 {:name "s"}🔗

One string (FindStringAttribute). Axioms only.

Axioms have no names of their own, so this attribute gives one, purely so that the :extern mechanism can apply to axioms. It has no other effect — the name is not used in error messages, in /proc matching, or in pruning. Two axioms with the same :name and no :extern clash:

axiom {:name "a"} true;

axiom {:name "a"} true;

boogie attr-axiom-name.bpl

attr-axiom-name.bpl(2,16): Error: more than one declaration of axiom name: a

1 name resolution errors detected in attr-axiom-name.bpl

12.4.4 {:verboseName "s"}🔗

One string (FindStringAttribute). Any NamedDeclaration.

Overrides the name used when Boogie prints progress, and the name matched by /proc and /noProc. Unlike a Boogie identifier it may contain any characters, which is why Dafny uses it to carry the original source-language name.

procedure {:verboseName "MyClass.Method(int) [well-formedness]"} P$$impl()

{

assert true;

}

boogie /trace attr-verbose-name.bpl

Parsing attr-verbose-name.bpl

Coalescing blocks...

Inlining...

Verifying MyClass.Method(int) [well-formedness] ...

[TRACE] Using prover: z3

[0.026 s, solver resource count: 98, 1 proof obligation]  verified

Boogie program verifier finished with 1 verified, 0 errors

(In every /trace listing in this chapter the Using prover: line has had its absolute solver path shortened to z3; timings and solver resource counts vary from run to run; and later listings show only the lines relevant to the attribute under discussion, dropping the Parsing / Coalescing blocks / Inlining preamble. Nothing has been reworded.)

boogie "/proc:MyClass*" attr-verbose-name.bpl

Boogie program verifier finished with 1 verified, 0 errors

12.4.5 {:keep} and {:include_dep}🔗

No arguments (FindBoolAttribute). Top-level declarations (:keep) and axioms (:include_dep). Only relevant under /prune.

Pruning computes, per implementation, the set of constants, functions and axioms reachable from the symbols the implementation mentions, and sends only those to the solver. :keep makes a declaration an unconditional root of that reachability computation.

function f(int): int;

function g(int): int;

axiom (forall x: int :: {f(x)} f(x) == x);

axiom {:keep} (forall x: int :: {g(x)} g(x) == x);

procedure P() { assert true; }

boogie /prune:1 /proverLog:keep.smt2 attr-keep.bpl

The head of keep.smt2, after the option preamble:

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun g (Int) Int)

(assert (forall ((x Int) ) (! (= (g x) x)

:qid |attrkeepbpl.5:23|

:skolemid |1|

:pattern ( (g x))

)))

f and its axiom were pruned; g and its axiom survived because of :keep.

:include_dep is finer grained: it makes DependencyEvaluator.AddIncoming record an incoming edge for every symbol the axiom mentions, rather than only for the symbols in the axiom’s triggers. An axiom that is not a triggered universal has no incoming edges at all without it, and so is always pruned:

function f(int): int;

function g(int): int;

axiom f(1) == 2;

axiom {:include_dep} g(1) == 2;

procedure P()

{

assert f(1) == 2;

}

procedure Q()

{

assert g(1) == 2;

}

boogie /prune:1 attr-include-dep.bpl

attr-include-dep.bpl(9,3): Error: this assertion could not be proved

Execution trace:

attr-include-dep.bpl(9,3): anon0

Boogie program verifier finished with 1 verified, 1 error

boogie /prune:0 attr-include-dep.bpl

Boogie program verifier finished with 2 verified, 0 errors

The /attrHelp text describes :include_dep as a migration aid: add it to every axiom when first turning pruning on, then remove them one at a time as you add uses clauses.

Note that axiom hiding is not attribute-driven. The hideable modifier on an axiom, the revealed modifier on a function, and the hide / reveal statements are all first-class syntax; there is no {:opaque} attribute in Boogie (see Attributes Boogie does not read).

12.5 Functions🔗

12.5.1 {:inline} and {:define}🔗

No arguments or true (FindBoolAttribute). Functions with a body.

A function written with a body and no attribute becomes an uninterpreted symbol plus a definition axiom with an auto-generated trigger. The two attributes pick different encodings instead:

function {:inline} double(x: int): int { 2 * x }

function {:define} triple(x: int): int { 3 * x }

function plain(x: int): int { 4 * x }

boogie /noVerify /print:- attr-functions.bpl

function {:inline} double(x: int) : int

{

2 * x

}

function {:define} triple(x: int) : int

{

3 * x

}

function plain(x: int) : int

uses {

axiom (forall x: int :: { plain(x): int } plain(x): int == 4 * x);

}

Restrictions, all enforced:

function {:inline} {:define} bad(x: int): int { x }

boogie attr-inline-define.bpl

attr-inline-define.bpl(1,51): error: function cannot have both :inline and :define attributes

1 parse errors detected in attr-inline-define.bpl

function {:define} id<T>(x: T): T { x }

boogie attr-define-poly.bpl

attr-define-poly.bpl(1,39): error: function with :define attribute has to be monomorphic

1 parse errors detected in attr-define-poly.bpl

Neither may be recursive, directly or mutually; FunctionDependencyChecker builds a call graph over :inline and :define functions and rejects cycles:

function {:define} f(x: int): int { if x <= 0 then 0 else f(x - 1) }

boogie attr-define-rec.bpl

attr-define-rec.bpl(1,19): Error: Call cycle detected among functions: f

The same checker reports three more errors, all reachable from ordinary source: Parameter to :inline attribute on a function must be Boolean (for {:inline 3} — the argument must be boolean, not a depth, on a function), Function with :inline attribute must have a body and Function with :define attribute must have a body. Its fourth message, A function may not have both :inline and :define attributes, is unreachable from parsed input because the parser rejects that combination first with the message shown above; it fires only for programs built directly as an AST.

:define additionally requires the monomorphic type encoding; with a polymorphic encoding ExecutionEngine refuses with Functions with :define attribute only supported with monomorphic encoding.

Because the parser, not the checker, is what turns the body into Function.Body or Function.DefinitionBody, the pretty-printer re-synthesises the attribute when it prints a function whose body field is set but whose attribute is missing — which is why AST-built programs print {:inline} you never wrote.

12.5.2 {:builtin "s"} and {:bvbuiltin "s"}🔗

One string (FindStringAttribute). Functions, and :builtin also on type constructors.

The function is not declared to the solver; instead every application is emitted with s as the head symbol. SMTLibLineariser.ExtractBuiltin looks at :bvbuiltin first and falls back to :builtin.

function {:bvbuiltin "bvadd"} bv8add(bv8, bv8): bv8;

function {:bvbuiltin "bvule"} bv8ule(bv8, bv8): bool;

function {:builtin "div"} idiv(int, int): int;

procedure P()

{

assert bv8add(3bv8, 4bv8) == 7bv8;

assert bv8ule(3bv8, 4bv8);

assert idiv(7, 2) == 3;

}

boogie attr-builtin.bpl

Boogie program verifier finished with 1 verified, 0 errors

Two details from ExtractBuiltin: a :bvbuiltin string beginning "sign_extend " or "zero_extend " is wrapped as (_ sign_extend N), a leftover accommodation for the old Simplify syntax; and if /useArrayTheory is off, a :builtin naming an array operation is ignored and the function becomes uninterpreted again.

On a type constructor, :builtin is read by MonomorphismChecker.DoesTypeCtorDeclNeedMonomorphization and by CtorType.GetBuiltin: a parameterised type constructor with :builtin is exempt from monomorphisation and needs no declaration in the SMT output. :bvbuiltin and the SMT-LIB bitvector operations and Reaching the string theory: :builtin cover the built-in names themselves.

The paper (section 11.1) writes this attribute {:bvBuiltin} with a capital B, and pairs it with a {:bvIgnore} attribute on axioms. Neither spelling exists in the tool: it is :bvbuiltin, all lower case, and :bvIgnore was never implemented.

12.5.3 {:never_pattern}🔗

Nothing, true or false (CheckBooleanAttribute). Functions.

Terms headed by this function are never chosen as automatic triggers. Boogie implements it by emitting an SMT :no-pattern annotation for every quantifier where such a term would otherwise be selected. It does not affect explicit trigger annotations.

function {:never_pattern} h(int): int;

function k(int): int;

axiom (forall x: int :: h(x) == k(x));

procedure P() { assert true; }

boogie /prune:0 /proverLog:np.smt2 attr-never-pattern.bpl

The relevant part of np.smt2:

(declare-fun h (Int) Int)

(declare-fun k (Int) Int)

(assert (forall ((x Int) ) (! (= (h x) (k x))

:qid |attrneverpatternbpl.3:15|

:skolemid |0|

:no-pattern (h x)

)))

12.5.4 {:identity}🔗

Nothing, true or false (CheckBooleanAttribute). Functions of one argument. Only relevant under /infer.

Tells the interval abstract domain to treat f(e) as e when f has one argument and its use has type X -> X. IntervalDomain trusts the attribute; it makes no attempt to check that the function really is the identity.

function {:identity} box(x: int): int;

procedure P()

{

var y: int;

y := 3;

while (*) { y := box(y); }

assert 0 <= y;

}

boogie /infer:j /instrumentInfer:e /printInstrumented /noVerify attr-identity.bpl

implementation P()

{

var y: int;

anon0:

assume {:inferred} true;

y := 3;

assume {:inferred} y == 3;

goto anon3_LoopHead;

anon3_LoopHead:  // cut point

assume {:inferred} y == 3;

assume {:inferred} y == 3;

goto anon3_LoopDone, anon3_LoopBody;

anon3_LoopBody:

assume {:inferred} y == 3;

y := box(y);

assume {:inferred} y == 3;

goto anon3_LoopHead;

anon3_LoopDone:

assume {:inferred} y == 3;

assert 0 <= y;

assume {:inferred} y == 3;

return;

}

Without the attribute the inferred invariant at the loop head degrades to true.

12.6 Procedures and implementations🔗

Everything in this section can be written on a procedure with a body, because the attribute list is cloned onto the generated implementation. Where an attribute is read from only one of the two, that is stated.

12.6.1 {:verify false}🔗

Nothing, true or false (CheckBooleanAttribute). Read from the procedure first, then the implementation, so the implementation wins.

procedure {:verify false} Skipped()

{

assert false;

}

procedure Checked()

{

assert false;

}

boogie attr-verify.bpl

attr-verify.bpl(8,3): Error: this assertion could not be proved

Execution trace:

attr-verify.bpl(8,3): anon0

Boogie program verifier finished with 0 verified, 1 error

Because the implementation is consulted second, {:verify true} on the implementation re-enables a procedure marked {:verify false}:

procedure {:verify false} P();

implementation {:verify true} P()

{

assert false;

}

boogie attr-verify-impl.bpl

attr-verify-impl.bpl(5,3): Error: this assertion could not be proved

Execution trace:

attr-verify-impl.bpl(5,3): anon0

Boogie program verifier finished with 0 verified, 1 error

Implementation.IsSkipVerification also skips an implementation when /inline:assume or /inline:assert is in force and either the implementation or its procedure carries :inline, and, under /stratifiedInline, skips everything not marked :entrypoint.

12.6.2 {:inline N}🔗

One integer (CheckIntAttribute / FindIntAttribute). Procedures, implementations, and individual call statements.

N is the inlining depth. Inliner.TryDefineCount computes the depth for a particular call as follows: the call statement’s own {:inline N} wins if it has one; otherwise it runs impl.CheckIntAttribute and then impl.Proc.CheckIntAttribute over the same variable, so when both the implementation and its procedure carry a depth the procedure’s value is the one that survives. (That is the opposite of :verify, where the implementation wins.)

procedure {:inline 0} P();

implementation {:inline 1} P()

{

assert true;

}

procedure Main()

{

call P();

assert false;

}

boogie /printInlined /noVerify attr-inline-precedence.bpl

after inlining procedure calls

procedure Main();

implementation Main()

{

anon0:

assume false;

assert false;

return;

}

Boogie program verifier finished with 0 verified, 0 errors

The procedure’s 0 beat the implementation’s 1, and because the default /inline: mode is assume the call became assume false.

Whether an inlining pass runs at all is a separate test: ExecutionEngine.Inline looks for a procedure or implementation with FindExprAttribute("inline") != null, that is, an :inline with exactly one expression argument. A bare {:inline} with no argument therefore never triggers the pass; {:inline true} does trigger it, but CheckIntAttribute then rejects the boolean, the depth stays at -1, and nothing is inlined.

procedure {:inline 1} Incr(x: int) returns (y: int)

ensures y == x + 1;

{

y := x + 1;

}

procedure Main()

{

var a: int;

call a := Incr(0);

assert a == 1;

}

boogie /printInlined /noVerify attr-inline.bpl

after inlining procedure calls

procedure Main();

implementation Main()

{

var a: int;

var inline$Incr$0$x: int;

var inline$Incr$0$y: int;

anon0:

goto inline$Incr$0$Entry;

inline$Incr$0$Entry:

inline$Incr$0$x := 0;

havoc inline$Incr$0$y;

goto inline$Incr$0$anon0;

inline$Incr$0$anon0:

inline$Incr$0$y := inline$Incr$0$x + 1;

goto inline$Incr$0$Return;

inline$Incr$0$Return:

assert inline$Incr$0$y == inline$Incr$0$x + 1;

a := inline$Incr$0$y;

goto anon0$1;

anon0$1:

assert a == 1;

return;

}

Boogie program verifier finished with 0 verified, 0 errors

What happens once the depth reaches 0 is set by /inline:: assume (the default) replaces the call with assume false, assert with assert false, spec leaves the call alone, and none disables the whole mechanism. The default matters: a procedure whose effective depth is 0 silently makes the rest of the caller unreachable rather than falling back to its specification.

{:InlineAssume} on an ensures makes the inliner emit an assume for that postcondition instead of an assert, so it is trusted at the inlined call site rather than re-checked.

12.6.3 {:priority N}🔗

One integer (CheckIntAttribute). Implementation only.

Implementations are verified in descending priority order. Values <= 0 are clamped to 1, which is also the default.

procedure A() { assert true; }

procedure {:priority 5} B() { assert true; }

procedure C() { assert true; }

boogie /trace attr-priority.bpl

Verifying B ...

[TRACE] Using prover: z3

[0.026 s, solver resource count: 98, 1 proof obligation]  verified

Verifying A ...

[0.007 s, solver resource count: 98, 1 proof obligation]  verified

Verifying C ...

[0.007 s, solver resource count: 98, 1 proof obligation]  verified

Boogie program verifier finished with 3 verified, 0 errors

Under /verifySnapshots, an implementation left at the default priority is ordered by a cache-derived priority instead, so that the ones most likely to have changed go first.

12.6.4 {:timeLimit N}, {:rlimit N}, {:random_seed N}, {:smt_option "k", "v"}🔗

:timeLimit and :rlimit take one non-negative integer (CheckUIntAttribute); :random_seed one integer (CheckIntAttribute); :smt_option exactly two arguments of which the first must be a string. All read from the implementation.

Per-implementation versions of /timeLimit, /rlimit, /randomSeed and /proverOpt. :timeLimit is in seconds and is converted to the solver’s milliseconds. Unlike the others, :smt_option accumulates: every occurrence is collected by Implementation.GetExtraSMTOptions, and the second argument is rendered with ToString(), so an integer literal works as well as a string.

procedure {:smt_option "smt.qi.eager_threshold", "10"} {:timeLimit 17} {:rlimit 1000} {:random_seed 42} P()

{

assert true;

}

boogie /proverLog:opts.smt2 attr-smt-options.bpl

grep set-option opts.smt2

Boogie program verifier finished with 1 verified, 0 errors

(set-option :print-success false)

(set-option :smt.mbqi false)

(set-option :model.compact false)

(set-option :model.v2 true)

(set-option :pp.bv_literals false)

(set-option :smt.qi.eager_threshold 10)

(set-option :timeout 17000)

(set-option :rlimit 1000)

(set-option :smt.random_seed 42)

(set-option :sat.random_seed 42)

(set-option :smt.mbqi false)

(set-option :model.compact false)

(set-option :model.v2 true)

(set-option :pp.bv_literals false)

(set-option :smt.qi.eager_threshold 10)

(The options are re-sent once per verification condition, which is why the list repeats.)

12.6.5 {:selective_checking} and {:start_checking_here}🔗

No arguments (FindBoolAttribute). :selective_checking on a procedure or implementation, :start_checking_here on an assert or assume inside it.

Under :selective_checking, every assertion is turned into an assumption except those in blocks reachable from a :start_checking_here command (and, within the block containing that command, only the assertions after it).

procedure {:selective_checking} P(x: int)

{

assert x == 1;

assume {:start_checking_here} true;

assert x == 2;

}

procedure Q(x: int)

{

assert x == 1;

assert x == 2;

}

boogie attr-selective.bpl

attr-selective.bpl(5,3): Error: this assertion could not be proved

Execution trace:

attr-selective.bpl(3,3): anon0

attr-selective.bpl(10,3): Error: this assertion could not be proved

Execution trace:

attr-selective.bpl(10,3): anon0

attr-selective.bpl(11,3): Error: this assertion could not be proved

Execution trace:

attr-selective.bpl(10,3): anon0

Boogie program verifier finished with 0 verified, 3 errors

The :selective_checking attribute is read from the implementation or its procedure, so either placement works. As the /attrHelp text puts it, assume {:start_checking_here} e; is the inverse of assume false;: the latter disables verification after it, the former disables verification before it.

12.6.6 {:kInductionDepth N}🔗

One integer (FindIntAttribute, default -1). Implementation.

Per-implementation /kInductionDepth. When the effective value is non-negative, RemoveBackEdges converts loops using k-induction rather than the standard havoc-and-assume-invariant scheme. The larger of the command-line value and the attribute value is used.

12.6.7 {:msg_if_verifies "s"}🔗

One string (FindStringAttribute). Implementation.

Printed instead of nothing when the implementation verifies.

procedure {:msg_if_verifies "P is fine"} P()

{

assert true;

}

boogie attr-msg-if-verifies.bpl

P is fine

Boogie program verifier finished with 1 verified, 0 errors

12.6.8 Other implementation attributes🔗

{:entrypoint} (no arguments) marks the roots for /stratifiedInline; under that option every implementation without it is skipped.

{:may_unverified_instrumentation} (no arguments) turns on InstrumentWithMayUnverifiedConditions, part of the result-caching machinery.

12.7 Specifications🔗

12.7.1 {:msg "s"}🔗

One string (FindStringAttribute). assert, requires, ensures.

Replaces the entire error line, position prefix included, with s. This is not a suffix or a note — Boogie prints s and nothing else, and the location information is gone.

procedure P(x: int)

{

assert {:msg "x is not two"} x == 2;

}

boogie attr-msg.bpl

x is not two

Execution trace:

attr-msg.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

It works on specification clauses as well, and follows the clause to whichever proof obligation it produces — the exit block for an ensures, the call site for a requires:

procedure P() returns (y: int)

ensures {:msg "P must return something positive"} 0 < y;

{

y := 0;

}

procedure Caller()

{

var z: int;

call z := Q(0);

}

procedure Q(x: int) returns (y: int)

requires {:msg "Q needs a positive argument"} 0 < x;

{

y := x;

}

boogie attr-msg-spec.bpl

P must return something positive

Execution trace:

attr-msg-spec.bpl(4,5): anon0

Q needs a positive argument

Execution trace:

attr-msg-spec.bpl(10,3): anon0

Boogie program verifier finished with 1 verified, 2 errors

/forceBplErrors suppresses :msg and restores the standard message.

The paper (section 11.0) proposes exactly this feature under the name {:errorMessage "..."}; the implemented name is :msg.

12.7.2 {:always_assume}🔗

No arguments (FindBoolAttribute). free requires and free ensures only; ignored on non-free specifications.

A free postcondition is normally invisible to the procedure’s own implementation, and a free precondition is normally invisible at the call site. :always_assume makes them visible: the implementation assumes the free ensures in its exit block, and the caller assumes the free requires at the call.

procedure P() returns (y: int)

free ensures {:always_assume} y == 3;

ensures y == 3;

{

havoc y;

}

procedure Q() returns (y: int)

free ensures y == 3;

ensures y == 3;

{

havoc y;

}

boogie attr-always-assume.bpl

attr-always-assume.bpl(13,1): Error: a postcondition could not be proved on this return path

attr-always-assume.bpl(10,3): Related location: this is the postcondition that could not be proved

Execution trace:

attr-always-assume.bpl(12,3): anon0

Boogie program verifier finished with 1 verified, 1 error

Free preconditions are also assumed at the call site unconditionally when /stratifiedInline is on, regardless of the attribute.

12.8 Statements🔗

12.8.1 {:subsumption n}🔗

One integer (FindIntAttribute, default -1 meaning “use the command line”). assert, and call — where it governs all of that call’s precondition checks.

After an assertion is checked, Boogie normally also assumes it, so that later assertions may rely on it. That is what makes a failing assertion mask the failures downstream of it. :subsumption overrides /subsumption for one assertion: 0 never assumes, 1 assumes except when the assertion is a quantifier, 2 always assumes. Anything else (including a non-integer argument) falls back to the command-line setting.

procedure P(x: int)

{

assert {:subsumption 0} x == 1;

assert x == 1;

}

procedure Q(x: int)

{

assert x == 1;

assert x == 1;

}

boogie attr-subsumption.bpl

attr-subsumption.bpl(3,3): Error: this assertion could not be proved

Execution trace:

attr-subsumption.bpl(3,3): anon0

attr-subsumption.bpl(4,3): Error: this assertion could not be proved

Execution trace:

attr-subsumption.bpl(3,3): anon0

attr-subsumption.bpl(9,3): Error: this assertion could not be proved

Execution trace:

attr-subsumption.bpl(9,3): anon0

Boogie program verifier finished with 0 verified, 3 errors

P reports both assertions; Q reports only the first, because it is assumed for the second.

Preconditions checked at a call site are AssertRequiresCmds, and CallCmd.ComputeDesugaring gives them a copy of the call’s attributes — not the requires clause’s. So the way to control subsumption for a call’s preconditions is to annotate the call:

procedure Q(x: int)

requires x == 1;

requires x == 1;

{ }

procedure P(y: int)

{

call {:subsumption 0} Q(y);

}

procedure R(y: int)

{

call Q(y);

}

boogie attr-subsumption-call.bpl

attr-subsumption-call.bpl(8,3): Error: a precondition for this call could not be proved

attr-subsumption-call.bpl(3,3): Related location: this is the precondition that could not be proved

Execution trace:

attr-subsumption-call.bpl(8,3): anon0

attr-subsumption-call.bpl(8,3): Error: a precondition for this call could not be proved

attr-subsumption-call.bpl(2,3): Related location: this is the precondition that could not be proved

Execution trace:

attr-subsumption-call.bpl(8,3): anon0

attr-subsumption-call.bpl(13,3): Error: a precondition for this call could not be proved

attr-subsumption-call.bpl(2,3): Related location: this is the precondition that could not be proved

Execution trace:

attr-subsumption-call.bpl(13,3): anon0

Boogie program verifier finished with 1 verified, 3 errors

:subsumption written on a requires or ensures clause itself is silently ignored: AssertEnsuresCmd has no attribute list of its own, and AssertRequiresCmd’s comes from the call.

12.8.2 {:expand}🔗

No arguments, or one integer depth (FindBoolAttribute then FindIntAttribute, default 100). assert, and the specification clauses that become assertions. The attribute is looked up on the enclosing requires, ensures or call when the assertion came from one.

Splits a conjunctive assertion into one assertion per conjunct, so that a failure names the guilty conjunct instead of the whole formula. Each generated assertion is the disjunction of the conjunct with the original expression, and carries {:subsumption 0}.

procedure P(x: int)

{

assert {:expand} x == 1 && x == 2 && x == 3;

}

boogie attr-expand.bpl

attr-expand.bpl(3,3): Error: this assertion could not be proved

Execution trace:

attr-expand.bpl(3,3): anon0

attr-expand.bpl(3,22): Error: this assertion could not be proved

Execution trace:

attr-expand.bpl(3,3): anon0

attr-expand.bpl(3,32): Error: this assertion could not be proved

Execution trace:

attr-expand.bpl(3,3): anon0

attr-expand.bpl(3,42): Error: this assertion could not be proved

Execution trace:

attr-expand.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 4 errors

The traversal descends unconditionally through &&, the conclusion of ==> and the body of a forall; there is no if-then-else case. The integer argument is not a limit on that traversal but a budget for the one thing that is bounded — unfolding the body (or definition axiom) of a called function, once per level, down to depth 0. The original assertion is kept as well, which is why three conjuncts produce four errors.

12.8.3 {:verified_under e}🔗

Exactly one boolean expression, checked at resolution and type checking (FindExprAttribute). assert.

The name reads like a restriction but the effect is a discharge: :verified_under e asserts that the obligation has already been proved in the case e, so Wlp.Cmd weakens the goal from A to e || A — equivalently !e ==> A. The assertion is required to hold only where e is false. If e is the literal true, the assertion is dropped entirely (isFullyVerified). It is written by the incremental-verification machinery, which uses it to record what a previous run already established.

Note the direction, which is easy to get backwards:

procedure A(x: int)

{

assert {:verified_under x != 1} x == 1;

}

procedure B(x: int)

{

assert {:verified_under x == 1} x == 1;

}

procedure C(x: int)

{

assert {:verified_under true} x == 99;

}

boogie attr-verified-under-polarity.bpl

attr-verified-under-polarity.bpl(8,3): Error: this assertion could not be proved

Execution trace:

attr-verified-under-polarity.bpl(8,3): anon0

Boogie program verifier finished with 2 verified, 1 error

A verifies because x != 1 || x == 1 is valid. B — the reading “only check it when x == 1”, which would make the obligation trivial — fails, because the goal is x == 1 || x == 1. C verifies because a literal true discharges the assertion outright.

Both the arity and the type are enforced:

procedure P(x: int)

{

assert {:verified_under x} x == 1;

}

boogie attr-verified-under.bpl

attr-verified-under.bpl(3,9): Error: attribute :verified_under accepts only one argument of type bool

1 type checking errors detected in attr-verified-under.bpl

The expression is substituted with the current incarnations when the block is made passive, so it may mention program variables and old.

12.8.4 {:minimize e} and {:maximize e}🔗

Exactly one expression of type int, real or a bitvector, checked at resolution and type checking (FindExprAttribute). assume only.

Emits an SMT optimisation objective, so that a counterexample minimises or maximises e. Requires a solver with optimisation support.

procedure P()

{

var x: int;

havoc x;

assume 42 < x;

assume {:minimize x} true;

assert x < 43;

}

boogie /printModel:1 attr-minimize.bpl

attr-minimize.bpl(7,3): Error: this assertion could not be proved

Execution trace:

attr-minimize.bpl(4,3): anon0

*** MODEL

x ->

x@0 -> 43

ControlFlow -> {

0 0 -> 3

0 2 -> (- 1)

0 3 -> 2

else -> (- 1)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

x ->

*** END_STATE

*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error

The counterexample is the smallest one, x = 43.

The arity check runs during resolution and the type check during type checking:

procedure P(x: int);

requires {:minimize x, x} true;

boogie attr-minimize-arity.bpl

attr-minimize-arity.bpl(2,11): Error: attributes :minimize and :maximize accept only one argument

1 name resolution errors detected in attr-minimize-arity.bpl

procedure P(b: bool)

{

assume {:minimize b} true;

}

boogie attr-minimize-type.bpl

attr-minimize-type.bpl(3,9): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv

1 type checking errors detected in attr-minimize-type.bpl

12.8.5 {:soft} and {:try}🔗

:soft takes no arguments or one integer weight; :try takes no arguments. assume only, and both require an :id on the same command.

:soft turns the assumption into an SMT assert-soft with the given weight (default 1), so the solver satisfies it if it can and drops it otherwise. :try classifies the assumption’s coverage variable as a “try” rather than an ordinary assumption, which matters to /trackVerificationCoverage.

procedure P(x: int)

{

assume {:id "s"} {:soft} x == 1;

assert false;

}

boogie /trackVerificationCoverage /proverLog:soft.smt2 attr-soft.bpl

grep assert-soft soft.smt2

attr-soft.bpl(4,3): Error: this assertion could not be proved

Execution trace:

attr-soft.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

(assert-soft soft$$s :weight 1)

The guard in Wlp.Cmd is (FindBoolAttribute("soft") || 0 < softWeight), so a bare {:soft} gives weight 1 and {:soft 5} gives weight 5, but a non-positive weight — {:soft 0} or {:soft -5} — matches neither disjunct and no assert-soft is emitted at all.

Without an :id neither attribute does anything at all, silently.

12.8.6 {:print e0, e1, ...}🔗

Any number of arguments, strings or expressions (QKeyValue walked directly). Any command carrying attributes — assert, assume, assignment, call. Requires /enhancedErrorMessages:1.

Records the listed values, evaluated in the incarnation state at that point in the program, and prints them under Augmented execution trace when a counterexample runs through that command. Identifier arguments are replaced by their current incarnation; everything else is printed as written. Every :print occurrence on the command contributes, in order, each followed by a newline.

procedure P(i: int) returns (o: int)

requires i == 42;

ensures o < 43;

{

assume {:print "entering P"} {:print "i = ", i} true;

o := i;

if (*) {

o := {:print "incrementing"} o + 1;

}

assert {:print "o = ", o} true;

}

boogie /enhancedErrorMessages:1 attr-print.bpl

attr-print.bpl(11,1): Error: a postcondition could not be proved on this return path

attr-print.bpl(3,3): Related location: this is the postcondition that could not be proved

Execution trace:

attr-print.bpl(5,3): anon0

attr-print.bpl(8,7): anon3_Then

attr-print.bpl(10,3): anon2

Augmented execution trace:

entering P

i = 42

incrementing

o = 43

Boogie program verifier finished with 0 verified, 1 error

Note the assignment: the attribute goes after :=, not before the left-hand side.

12.8.7 {:captureState "s"}🔗

One string (FindStringAttribute). assume only. Requires a model to be produced — /mv:, /printModel:1 or /enhancedErrorMessages:1.

Names a program point. When Boogie prints a counterexample model, it emits an extra *** STATE s block showing the variables whose incarnation changed since the previous captured state.

procedure P(x: int) returns (y: int)

{

assume {:captureState "on entry"} true;

y := x + 1;

assume {:captureState "after increment"} true;

assert y == x;

}

boogie /mv:- attr-capture-state.bpl

attr-capture-state.bpl(6,3): Error: this assertion could not be proved

Execution trace:

attr-capture-state.bpl(3,3): anon0

*** MODEL

x -> 0

y ->

y@0 -> 1

ControlFlow -> {

0 0 -> 3

0 2 -> (- 1)

0 3 -> 2

else -> (- 1)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

x -> 0

y ->

*** END_STATE

*** STATE on entry

*** END_STATE

*** STATE after increment

y -> 1

*** END_STATE

*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error

When a procedure containing :captureState is inlined or unrolled, the duplicated states would collide, so Implementation.MakeCaptureStateUnique rewrites the string to s$renamed$Name$n. Boogie always sends (set-option :model.compact false) to Z3, and the comment in Source/Provers/SMTLib/Z3.cs explains why: :captureState does not work with compressed models.

12.8.8 {:PossiblyUnreachable}🔗

No arguments (FindBoolAttribute). assert. Only relevant under /smoke.

The smoke tester injects assert false at each program point to find unreachable code. An assert carrying :PossiblyUnreachable suppresses the smoke test for its whole command sequence, declaring the unreachability intentional.

procedure P(x: int)

{

assume x > 0;

assume x < 0;

assert true;

}

procedure Q(x: int)

{

assume x > 0;

assume x < 0;

assert {:PossiblyUnreachable} true;

}

boogie /smoke attr-smoke.bpl

found unreachable code:

implementation P(x: int)

{

0:

goto anon0;

anon0:

assume x > 0;

assume x < 0;

assert true;

assert false;

return;

}

Boogie program verifier finished with 2 verified, 0 errors

12.8.9 {:id "s"} on statements🔗

One string (FindStringAttribute). assert, assume, call, requires, ensures, axioms, assignments, implementations.

Two unrelated uses share this name.

On an implementation it is the key for verification result caching (Verification result caching); the default is Name + hashcode + ":0", which is not stable across runs, so caching only works if you supply one.

On a statement, contract clause or axiom it names a proof element for /trackVerificationCoverage. Boogie then reports which named assumptions and axioms the proof of each goal actually needed — the basis of vacuity detection.

function f(int): int;

axiom {:id "f_ax"} (forall x: int :: {f(x)} f(x) == x);

procedure P(x: int)

{

assume {:id "useful"} x == 1;

assume {:id "useless"} x != 7;

assert {:id "goal"} f(x) == 1;

}

boogie /trackVerificationCoverage /trace attr-coverage.bpl

Verifying P ...

[TRACE] Using prover: z3

Proof dependencies:

f_ax

goal

useful

[0.041 s, solver resource count: 778, 1 proof obligation]  verified

Proof dependencies of whole program:

f_ax

goal

useful

Statement ids must be unique within a program; ResolutionContext.AddStatementId enforces it:

procedure P()

{

assert {:id "a1"} true;

assert {:id "a1"} true;

}

boogie attr-dup-id.bpl

attr-dup-id.bpl(4,2): Error: more than one statement with same id: a1

1 name resolution errors detected in attr-dup-id.bpl

/trackVerificationCoverage on its own reports only the ids you wrote — a program with none produces an empty dependency list. Filling them in is the job of /warnVacuousProofs, which implies /trackVerificationCoverage and additionally runs CoverageAnnotator to invent id_lline_ccol_kind_n for every assertion, assumption, contract clause and call that lacks one (kind is requires, ensures, assert, assume, call or other). It also renames any :id that collides with one already seen.

procedure P(x: int)

{

assume x == 1;

assume x != 7;

assert x > 0;

}

boogie /warnVacuousProofs /trace attr-vacuity.bpl

Verifying P ...

[TRACE] Using prover: z3

Proof dependencies:

id_l3_c3_assume_0

id_l5_c3_assert_2

[0.026 s, solver resource count: 530, 1 proof obligation]  verified

Proof dependencies of whole program:

id_l3_c3_assume_0

id_l5_c3_assert_2

With /trackVerificationCoverage instead, the same program prints an empty Proof dependencies list.

12.8.10 {:assumption} on local variables🔗

No arguments (FindBoolAttribute). Meaningful on local variables only; the two well-formedness checks below are applied to every variable declaration.

Declares a variable that accumulates assumptions, used by the caching machinery. It must have type bool and may not carry a where clause — Variable.Typecheck and Variable.ResolveWhere enforce both on globals and formals as well, even though only locals are ever instrumented. Boogie seeds it with assume {:assumption_variable_initialization} a; at the start of the implementation, treats a := a && e specially when computing dependencies, and excludes such variables from live-variable elimination.

procedure P()

{

var {:assumption} a0: int;

assert true;

}

boogie attr-assumption.bpl

attr-assumption.bpl(3,20): Error: assumption variable must be of type 'bool'

1 type checking errors detected in attr-assumption.bpl

12.9 Splitting the verification condition🔗

Boogie can break one implementation into several verification conditions. Four attributes control that, and all four are read on statements or on the control-flow commands the structured statements desugar into. This section gives their argument shapes and attachment points; the mechanism itself — how a part is built, why splitting is sound, what the part names mean and what /printSplit shows — is in Splitting the verification condition, and the command-line options that do the same jobs globally are in Splitting and parallelism.

12.9.1 {:split_here}🔗

No arguments (FindBoolAttribute). assert or assume.

Everything up to the marker becomes one verification condition and everything after it another, with the assertions of the other half turned into assumptions.

procedure P(x: int)

{

assert x == x;

assume {:split_here} true;

assert x + 0 == x;

}

boogie /trace attr-split-here.bpl

Verifying P ...

[TRACE] Using prover: z3

checking split 1/2 (line 1), 0.00%, (cost:4/1 last) ...

--> split #1 done,  [0.0266691 s] Valid

checking split 2/2 (line 4), 50.00%, (cost:4/1 last) ...

--> split #2 done,  [0.008337 s] Valid

[0.035 s, solver resource count: 194, 2 proof obligations]  verified

Boogie program verifier finished with 1 verified, 0 errors

(Timings vary between runs.) The /attrHelp text warns that this may occasionally double-report an error.

12.9.2 {:isolate} and {:isolate "paths"}🔗

Presence only (FindAttribute); the optional string argument "paths" is looked for among the parameters. assert, goto and return.

The marked assertion gets a verification condition to itself, with every other assertion demoted to an assumption; in the remainder, the marked assertion becomes an assumption.

procedure P(x: int)

{

assert {:isolate} x == 1;

assert x == 2;

}

boogie /trace attr-isolate.bpl

Verifying P ...

[TRACE] Using prover: z3

checking split 1/2 (line 3), 0.00%, (cost:4/1 last) ...

--> split #1 done,  [0.0281957 s] Invalid

checking split 2/2 (line 1), 49.50%, (cost:4/1 last) ...

--> split #2 done,  [0.0080851 s] Invalid

[0.036 s, solver resource count: 528, 2 proof obligations]  errors

attr-isolate.bpl(3,3): Error: this assertion could not be proved

Execution trace:

attr-isolate.bpl(3,3): anon0

attr-isolate.bpl(4,3): Error: this assertion could not be proved

Execution trace:

attr-isolate.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 2 errors

Because the test is FindAttribute(p => p.Key == "isolate") != null, any occurrence of the name isolates, whatever its arguments. assert {:isolate false} ... isolates. This is not a typo in this reference: it is what the code does.

With the string argument "paths", a separate verification condition is produced for each control-flow path reaching the assertion — but only branches whose goto carries :allow_path_isolation multiply the paths.

12.9.3 {:allow_path_isolation}🔗

No arguments (FindBoolAttribute). A goto, which in practice means writing it on the if that generates the goto.

procedure P(x: int, y: int)

{

var z: int;

z := 0;

if {:allow_path_isolation} (x > 0) { z := z + 1; } else { z := z + 2; }

if {:allow_path_isolation} (y > 0) { z := z + 3; } else { z := z + 4; }

assert {:isolate "paths"} z > 2;

}

boogie /trace attr-isolate-paths.bpl

Verifying P ...

[TRACE] Using prover: z3

checking split 1/4 (line 7), 0.00%, (cost:4/1 last) ...

--> split #1 done,  [0.0264689 s] Valid

checking split 2/4 (line 7), 25.00%, (cost:4/1 last) ...

--> split #2 done,  [0.0074078 s] Valid

checking split 3/4 (line 7), 50.00%, (cost:4/1 last) ...

--> split #3 done,  [0.0017972 s] Valid

checking split 4/4 (line 7), 75.00%, (cost:4/1 last) ...

--> split #4 done,  [0.0015774 s] Valid

[0.037 s, solver resource count: 1704, 4 proof obligations]  verified

Boogie program verifier finished with 1 verified, 0 errors

Two two-way branches give four paths.

12.9.4 {:focus}🔗

No arguments (FindBoolAttribute). assert or assume.

Each focus command produces two verification conditions: one containing only the paths through the focus block (with its ancestors’ assertions demoted to assumptions), and one containing everything except the blocks dominated by the focus block. N focus commands therefore produce up to 2N parts.

procedure P(x: int)

{

var y: int;

y := 0;

if (x > 0) {

assume {:focus} true;

y := 1;

} else {

y := 2;

}

assert y > 0;

}

boogie /trace attr-focus.bpl

Verifying P ...

[TRACE] Using prover: z3

checking split 1/2 (line 1), 0.00%, (cost:4/1 last) ...

--> split #1 done,  [0.0269016 s] Valid

checking split 2/2 (line 1), 49.51%, (cost:4/1 last) ...

--> split #2 done,  [0.0072755 s] Valid

[0.034 s, solver resource count: 316, 2 proof obligations]  verified

Boogie program verifier finished with 1 verified, 0 errors

/relaxFocus reverses the order in which foci are processed.

12.9.5 {:vcs_*}🔗

:vcs_max_cost, :vcs_max_splits and :vcs_max_keep_going_splits take one integer, read by CheckIntAttributeOnImpl; :vcs_split_on_every_assert takes nothing, true or false (CheckBooleanAttribute). Implementation.

Per-implementation forms of /vcsMaxCost, /vcsMaxSplits, /vcsMaxKeepGoingSplits and /vcsSplitOnEveryAssert. The first three control cost-driven automatic splitting; the last makes every assertion behave as though it carried :isolate.

12.10 Quantifiers, triggers and lambdas🔗

Everything in this section except :pool is written after the ::.

12.10.1 Triggers🔗

A brace group in the quantifier body that does not start with : is a trigger: a list of terms that must all be present in the proof context for the solver to instantiate the quantifier at the matching values. Several trigger groups may be given, and the quantifier fires when any one of them matches. Triggers are described in section 11.2 of the paper, which remains accurate.

axiom (forall x: int :: {f(x)} f(x) == x + 1);

12.10.2 {:nopats e}🔗

Exactly one expression. Quantifier body.

:nopats is not stored as an attribute at all: the parser turns it into a Trigger node with Pos = false, which the SMT back end emits as :no-pattern. It suppresses a term that would otherwise be selected as an automatic trigger.

function f(int): int;

function g(int): int;

axiom (forall x: int :: {:nopats g(x)} f(x) == g(x));

procedure P() { assert f(0) == g(0); }

boogie /proverLog:nopats.smt2 attr-nopats.bpl

The relevant part of nopats.smt2:

(declare-fun g (Int) Int)

(declare-fun f (Int) Int)

(assert (forall ((x Int) ) (! (= (f x) (g x))

:qid |attrnopatsbpl.3:15|

:skolemid |0|

:no-pattern (g x)

)))

The name is nopats. There is no :nopattern.

12.10.3 {:qid "s"} and {:weight N}🔗

:qid takes one string (FindStringAttribute); :weight one integer (FindIntAttribute, default 1). Quantifier body.

:qid sets the SMT :qid used in solver statistics and quantifier instantiation profiling. Without it Boogie generates filename.line:col from the first bound variable, prefixing an underscore if the result would start with a digit. :weight sets the SMT :weight, which biases the solver’s instantiation heuristics; 1 is the default and is not emitted.

/emitDebugInformation:0 suppresses :qid (and the :skolemid that appears next to it, which Boogie generates and no attribute controls); :weight survives it. :weight is also dropped wholesale if the solver configuration says it does not use weights.

See Where attributes may be written above for the (very easy) mistake of putting these before the bound variables.

12.10.4 {:pool "name"} and {:add_to_pool "name", e, ...}🔗

:pool takes one or more strings and goes on a bound variable of a quantifier or lambda. :add_to_pool takes a string followed by at least one expression, and goes on a quantifier body or on an assert / assume command. Occurrences with fewer than two arguments are ignored.

These drive Boogie’s own pool-based quantifier instantiation engine, which is independent of the solver’s trigger matching and is described in Pool-based quantifier instantiation. :pool L"" on a bound variable says “instantiate this variable with the expressions in pool L”; :add_to_pool L", e" contributes e to pool L. On a command, the expression is substituted with the incarnations live at that point; on a quantifier, the bound variables are replaced by the Skolem constants introduced when the quantifier is skolemised.

function F(int): bool;

procedure P()

{

assume (forall {:pool "L"} x: int :: F(x - 1));

assert {:add_to_pool "L", 1} F(0);

}

procedure Q()

{

assume (forall {:pool "L"} x: int :: F(x - 1));

assert F(0);

}

procedure R()

{

assume (forall x: int :: {:pool "L"} F(x - 1));

assert {:add_to_pool "L", 1} F(0);

}

boogie attr-pool.bpl

attr-pool.bpl(12,3): Error: this assertion could not be proved

Execution trace:

attr-pool.bpl(11,3): anon0

attr-pool.bpl(18,3): Error: this assertion could not be proved

Execution trace:

attr-pool.bpl(17,3): anon0

Boogie program verifier finished with 1 verified, 2 errors

P verifies. Q fails because nothing was added to pool L. R fails because :pool was written after the ::, where it becomes a quantifier attribute that nothing reads.

The /attrHelp text adds an important limitation: these attributes have no effect on quantifiers inside axioms.

12.11 Verification result caching🔗

/verifySnapshots lets Boogie reuse results across successive versions of a program. The mechanism is driven by two attributes, and it will happily reuse a stale result if you get them wrong.

{:id "s"} on the implementation is the cache key. {:checksum "s"} is the front end’s statement of “this declaration’s content”; Boogie combines it with the checksums of everything the declaration depends on to decide whether a cached result still applies. Boogie never computes a checksum from the Boogie text itself: if the front end does not supply one, it is null.

Consider two snapshots that differ in their bodies but not in their declared checksum:

// attr-snapshot.v0.bpl

procedure {:id "P:0"} {:checksum "1"} P()

{

assert 1 == 1;

}

// attr-snapshot.v1.bpl

procedure {:id "P:0"} {:checksum "1"} P()

{

assert false;

}

boogie /verifySnapshots:1 attr-snapshot.bpl

Boogie program verifier finished with 1 verified, 0 errors

Boogie program verifier finished with 1 verified, 0 errors

The assert false is never checked. Bump the checksum and it is (attr-snapshot2.v0.bpl is a copy of attr-snapshot.v0.bpl):

// attr-snapshot2.v0.bpl

procedure {:id "P:0"} {:checksum "1"} P()

{

assert 1 == 1;

}

// attr-snapshot2.v1.bpl

procedure {:id "P:0"} {:checksum "2"} P()

{

assert false;

}