From 6204a4510168dbcd95a0e9e0ec255fb58bb44d87 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 13 Feb 2013 13:19:38 -0800 Subject: fixed bugs in typechecking of linear sets added regressions to linear sets removed the need to supply the builtin map operations manually --- Test/linear/Answer | 20 +++++++++++++++ Test/linear/Maps.bpl | 24 ----------------- Test/linear/list.bpl | 4 +++ Test/linear/runtest.bat | 4 +-- Test/linear/typecheck.bpl | 65 +++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 91 insertions(+), 26 deletions(-) create mode 100644 Test/linear/Answer delete mode 100644 Test/linear/Maps.bpl create mode 100644 Test/linear/typecheck.bpl (limited to 'Test/linear') diff --git a/Test/linear/Answer b/Test/linear/Answer new file mode 100644 index 00000000..86e42862 --- /dev/null +++ b/Test/linear/Answer @@ -0,0 +1,20 @@ + +-------------------- typecheck.bpl -------------------- +typecheck.bpl(6,22): Error: a linear domain must be consistently attached to variables of a particular type +typecheck.bpl(18,22): Error: a linear domain can be attached to either a set or a scalar type +typecheck.bpl(31,9): Error: Only simple assignment allowed on linear sets +typecheck.bpl(33,6): Error: Only variable can be assigned to a linear variable +typecheck.bpl(35,6): Error: Only linear variable can be assigned to another linear variable +typecheck.bpl(39,6): Error: Variable of one domain being assigned to a variable of another domain +typecheck.bpl(45,9): Error: A linear set can occur only once in the rhs +typecheck.bpl(49,4): Error: A linear set can occur only once as an in parameter +typecheck.bpl(51,4): Error: Only variable can be assigned to a linear variable +typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same +typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same +typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter +typecheck.bpl(64,6): Error: Only linear variable can be assigned to another linear variable +0 type checking errors detected in typecheck.bpl + +-------------------- list.bpl -------------------- + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/linear/Maps.bpl b/Test/linear/Maps.bpl deleted file mode 100644 index 5f302034..00000000 --- a/Test/linear/Maps.bpl +++ /dev/null @@ -1,24 +0,0 @@ -type X; - -function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int; -function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int; -function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int; -function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int; -function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int; -function {:builtin "MapConst"} MapConstInt(int) : [X]int; -function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; -function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool; -function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; -function {:builtin "MapNot"} MapNot([X]bool) : [X]bool; -function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int; -function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool; -function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool; -function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool; -function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool; -function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool; -function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool; -function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool; -function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool; - - - diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl index 9a333351..f4badca9 100644 --- a/Test/linear/list.bpl +++ b/Test/linear/list.bpl @@ -1,3 +1,7 @@ +type X; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + var head: X; var tail: X; var {:linear "Mem"} D: [X]bool; diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat index 28c91996..df176994 100644 --- a/Test/linear/runtest.bat +++ b/Test/linear/runtest.bat @@ -3,9 +3,9 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe -for %%f in (list.bpl) do ( +for %%f in (typecheck.bpl list.bpl) do ( echo. echo -------------------- %%f -------------------- - %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f Maps.bpl + %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f ) diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl new file mode 100644 index 00000000..f79f8fb5 --- /dev/null +++ b/Test/linear/typecheck.bpl @@ -0,0 +1,65 @@ +type X; + +procedure A() +{ + var {:linear "A"} a: X; + var {:linear "A"} b: int; +} + +procedure B() +{ + var {:linear "B"} a: X; + var {:linear "B"} b: [X]bool; +} + +procedure C() +{ + var {:linear "C"} a: X; + var {:linear "C"} c: [X]int; +} + +function f(X): X; + +procedure D() +{ + var {:linear "D"} a: X; + var {:linear "D"} x: X; + var {:linear "D"} b: [X]bool; + var c: X; + var {:linear "D2"} d: X; + + b[a] := true; + + a := f(a); + + a := c; + + c := a; + + a := d; + + a := a; + + a, x := x, a; + + a, x := x, x; + + call a, x := E(a, x); + + call a, x := E(a, a); + + call a, x := E(a, f(a)); + + call a, x := E(a, d); + + call d, x := E(a, x); + + call a, x := E(c, x); + + call c, x := E(a, x); +} + +procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X) +{ + c := a; +} \ No newline at end of file -- cgit v1.2.3