10.3. Flow based types🔗

Flow based types allow the type of a variable to change throughout the control-flow of the program, which enables having more precise types which improves verification performance.

Source program:

var foo := new Foo;
foo#x := 1;
foo := null;
foo#x := 2;

Inferred program:

var foo := new Foo;
foo#x := 1;
var foo_2: Nullable<Foo> := from_NotNull(foo);
foo_2 := null;
as_notNull(foo_2)#x := 2;