diff options
Diffstat (limited to 'Test')
47 files changed, 1057 insertions, 99 deletions
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index fddce05a..8d40b81d 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -332,3 +332,18 @@ procedure W0(N: real) assert N - i <= bf0 - 1.0; } } + +// mod + +procedure Mod0(n: int) + requires 10 < n; +{ + var i: int; + + i := 0; + while (i < 10) + { + i := (i mod n) + 1; + } + assert i == 10; +} diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect index a0769ec5..980593a9 100644 --- a/Test/aitest0/Intervals.bpl.expect +++ b/Test/aitest0/Intervals.bpl.expect @@ -54,4 +54,4 @@ Execution trace: Intervals.bpl(303,3): anon3_LoopHead Intervals.bpl(303,3): anon3_LoopDone -Boogie program verifier finished with 16 verified, 11 errors +Boogie program verifier finished with 17 verified, 11 errors diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl new file mode 100644 index 00000000..6ffcd113 --- /dev/null +++ b/Test/aitest0/Issue25.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -infer:j "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +const N: int; +axiom 0 <= N; + +procedure vacuous_post() +ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25). +{ +var x: int; +x := -N; +while (x != x) { +} +} diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect new file mode 100644 index 00000000..f56502e2 --- /dev/null +++ b/Test/aitest0/Issue25.bpl.expect @@ -0,0 +1,8 @@ +Issue25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. +Issue25.bpl(8,1): Related location: This is the postcondition that might not hold. +Execution trace: + Issue25.bpl(11,3): anon0 + Issue25.bpl(12,1): anon2_LoopHead + Issue25.bpl(12,1): anon2_LoopDone + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index 68c2a5f3..11ba8afa 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -1,67 +1,138 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type Tid; -var {:layer 0,1} a:[Tid]int; +var {:layer 0,2} a:[int]int; +var {:layer 0,1} count: int; +var {:layer 1,1} {:linear "tid"} allocated:[int]bool; -procedure {:yields} {:layer 1} main() { - var {:linear "tid"} tid:Tid; +procedure {:yields} {:layer 2} main() +requires {:layer 1} allocated == MapConstBool(false); +{ + var {:layer 1} {:linear "tid"} tid:int; + var i: int; yield; - while (true) { - call tid := Allocate(); - async call P(tid); + assert {:layer 1} AllocInv(count, allocated); + while (true) + invariant {:layer 1} AllocInv(count, allocated); + { + call tid, i := Allocate(); + async call P(tid, i); yield; + assert {:layer 1} AllocInv(count, allocated); } yield; } -procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) -ensures {:layer 1} a[tid] == old(a)[tid] + 1; +procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); +ensures {:layer 2} a[tid] == old(a)[tid] + 1; { var t:int; yield; - assert {:layer 1} a[tid] == old(a)[tid]; - call t := Read(tid); + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == old(a)[tid]; + call t := Read(tid, i); yield; - assert {:layer 1} a[tid] == t; - call Write(tid, t + 1); + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == t; + call Write(tid, i, t + 1); yield; - assert {:layer 1} a[tid] == t + 1; + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == t + 1; } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) +procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int) +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} tid == i; +ensures {:atomic} +|{A: + return true; +}|; { yield; - call tid := AllocateLow(); + assert {:layer 1} AllocInv(count, allocated); + call i := AllocateLow(); + call tid := MakeLinear(i); yield; + assert {:layer 1} AllocInv(count, allocated); } -procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int); +procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:atomic} |{A: val := a[tid]; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, allocated); + call val := ReadLow(i); + yield; + assert {:layer 1} AllocInv(count, allocated); +} -procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int); +procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:atomic} |{A: a[tid] := val; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, allocated); + call WriteLow(i, val); + yield; + assert {:layer 1} AllocInv(count, allocated); +} -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); -ensures {:atomic} |{ A: return true; }|; +function {:inline} AllocInv(count: int, allocated:[int]bool): (bool) +{ + (forall x: int :: allocated[x] ==> x < count) +} + +procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int); +ensures {:atomic} +|{A: + val := a[i]; return true; +}|; + +procedure {:yields} {:layer 0,1} WriteLow(i: int, val: int); +ensures {:atomic} +|{A: + a[i] := val; return true; +}|; +procedure {:yields} {:layer 0,1} AllocateLow() returns (i: int); +ensures {:atomic} +|{A: + i := count; + count := i + 1; + return true; +}|; +// We can prove that this primitive procedure preserves the permission invariant locally. +// We only need to using its specification and the definitions of TidCollector and TidSetCollector. +procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int); +requires !allocated[i]; +modifies allocated; +ensures tid == i && allocated == old(allocated)[i := true]; -function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; -function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; +function {:builtin "MapConst"} MapConstBool(bool): [int]bool; +function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool { MapConstBool(false)[x := true] } -function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +function {:inline} {:linear "tid"} TidSetCollector(x: [int]bool) : [int]bool { x } diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect index 9823d44a..f08c6e00 100644 --- a/Test/civl/Program4.bpl.expect +++ b/Test/civl/Program4.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 12 verified, 0 errors diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl index 33535b00..68b7e6c6 100644 --- a/Test/civl/alloc.bpl +++ b/Test/civl/alloc.bpl @@ -11,21 +11,26 @@ axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && m function EmptyLmap(): (lmap); axiom (dom(EmptyLmap()) == MapConstBool(false)); -function Add(x: lmap, i: int, v: int): (lmap); -axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); +function Add(x: lmap, i: int): (lmap); +axiom (forall x: lmap, i: int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x)); function Remove(x: lmap, i: int): (lmap); axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); +function {:inline} PoolInv(unallocated:[int]bool, pool: lmap) : (bool) +{ + (forall x: int :: unallocated[x] ==> dom(pool)[x]) +} + procedure {:yields} {:layer 2} Main() -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); { var {:layer 1} {:linear "mem"} l: lmap; var i: int; par Yield() | Dummy(); while (*) - invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); + invariant {:layer 1} PoolInv(unallocated, pool); { call l, i := Alloc(); async call Thread(l, i); @@ -35,8 +40,8 @@ ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); } procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int) -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i]; requires {:layer 2} dom(local_in)[i]; { @@ -50,13 +55,13 @@ requires {:layer 2} dom(local_in)[i]; call o := Read(local, i); assert {:layer 2} o == 42; while (*) - invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); + invariant {:layer 1} PoolInv(unallocated, pool); { call l, y := Alloc(); call l := Write(l, y, 42); call o := Read(l, y); assert {:layer 2} o == 42; - call Free(l); + call Free(l, y); par Yield() | Dummy(); } par Yield() | Dummy(); @@ -68,8 +73,8 @@ procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear } procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int) -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; ensures {:right} |{ A: assume dom(l)[i]; return true; }|; { @@ -79,17 +84,21 @@ ensures {:right} |{ A: assume dom(l)[i]; return true; }|; call YieldMem(l, i); } -procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap) -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap, i: int) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +requires {:layer 1} dom(l)[i]; ensures {:both} |{ A: return true; }|; { call Yield(); + call FreeLinear(l, i); + call ReturnAddr(i); + call Yield(); } procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int) -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|; { @@ -99,8 +108,8 @@ ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|; } procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap) -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i]; ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|; @@ -116,26 +125,31 @@ modifies pool; requires dom(pool)[i]; ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i]; +procedure {:layer 1} FreeLinear({:linear_in "mem"} l: lmap, i: int); +modifies pool; +requires dom(l)[i]; +ensures pool == Add(old(pool), i); + procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap); requires dom(l)[i]; ensures l' == cons(dom(l), map(l)[i := o]); procedure {:yields} {:layer 1} Yield() -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); { yield; - assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); + assert {:layer 1} PoolInv(unallocated, pool); } procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int) -requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); -ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; { yield; - assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]); + assert {:layer 1} PoolInv(unallocated, pool); assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; } @@ -144,7 +158,7 @@ procedure {:yields} {:layer 2} Dummy() yield; } -var {:layer 1, 1} pool: lmap; +var {:layer 1, 1} {:linear "mem"} pool: lmap; var {:layer 0, 1} mem:[int]int; var {:layer 0, 1} unallocated:[int]bool; @@ -155,4 +169,7 @@ procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int); ensures {:atomic} |{ A: mem[i] := o; return true; }|; procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int); -ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|;
\ No newline at end of file +ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|; + +procedure {:yields} {:layer 0, 1} ReturnAddr(i: int); +ensures {:atomic} |{ A: unallocated[i] := true; return true; }|;
\ No newline at end of file diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl new file mode 100644 index 00000000..070cfec4 --- /dev/null +++ b/Test/civl/chris8.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1,1} x:int; + +procedure{:layer 1}{:extern} P1(i:int); +procedure{:pure}{:extern} P2(j:int); + +procedure{:yields}{:layer 1,2} A1({:layer 1}i:int) + ensures {:atomic} |{ A: return true; }|; +{ + yield; + call P1(i); + call P2(i); + yield; +} diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/civl/chris8.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl new file mode 100644 index 00000000..ad5bf271 --- /dev/null +++ b/Test/civl/funky.bpl @@ -0,0 +1,133 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +const nil: X; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +var {:layer 0, 3} A: X; +var {:layer 0, 3} B: X; +var {:layer 0, 3} counter: int; + +procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|; + +procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|; + +procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|; + +procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|; + +procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|; + +procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|; + +procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|; + +procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|; + +procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|; + +procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|; + +procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X); +ensures tid != nil; + +procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X) +ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|; +{ + yield; + call DecrB(tid); + yield; +} + +procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X) +ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|; +{ + yield; + call AssertA(tid); + yield; +} + +procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X) +ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|; +{ + yield; + call AssertB(tid); + yield; +} + +procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X) +requires {:layer 1} tid != nil; +{ + yield; + call LockA(tid); + call IncrA(tid); + call DecrA(tid); + call UnlockA(tid); + yield; +} + +procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X) +ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|; +{ + yield; + call LockB(tid); + call AbsDecrB(tid); + call IncrB(tid); + call UnlockB(tid); + yield; +} + +procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X) +requires {:layer 3} tid != nil && counter == 0; +{ + yield; + assert {:layer 3} counter == 0; + call TB(tid); + yield; +} + +procedure {:yields} {:layer 3} main({:linear "tid"} tid: X) +requires {:layer 3} tid != nil && counter == 0; +{ + var {:linear "tid"} cid: X; + + yield; + assert {:layer 3} counter == 0; + while (*) + invariant {:layer 3} counter == 0; + { + if (*) { + call cid := AllocTid(); + async call TA(cid); + } + if (*) { + call cid := AllocTid(); + async call AbsTB(cid); + } + yield; + assert {:layer 3} counter == 0; + call LockA(tid); + call AbsAssertA(tid); + call LockB(tid); + call AbsAssertB(tid); + call UnlockB(tid); + call UnlockA(tid); + yield; + assert {:layer 3} counter == 0; + } + yield; +}
\ No newline at end of file diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect new file mode 100644 index 00000000..0a114594 --- /dev/null +++ b/Test/civl/funky.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 75 verified, 0 errors diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl index 9fc55646..df19aae4 100644 --- a/Test/civl/ticket.bpl +++ b/Test/civl/ticket.bpl @@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); type X; -function {:builtin "MapConst"} mapconstbool(bool): [X]bool; const nil: X; var {:layer 0,2} t: int; var {:layer 0,2} s: int; @@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil; } procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) -requires {:layer 2} xls' == mapconstbool(true); +requires {:layer 2} xls' == MapConstBool(true); { var {:linear "tid"} tid: X; var {:linear "tid"} xls: [X]bool; @@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t); } procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool); -ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; +ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int); ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|; diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index 751ce861..a184886d 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -1,62 +1,71 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type Node = int; -const unique null: Node; + +const null: int; type lmap; -function {:linear "Node"} dom(lmap): [Node]bool; -function map(lmap): [Node]Node; -function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool; +function {:linear "Node"} dom(lmap): [int]bool; +function map(lmap): [int]int; +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; function EmptyLmap(): (lmap); axiom (dom(EmptyLmap()) == MapConstBool(false)); -function Add(x: lmap, i: Node, v: Node): (lmap); -axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); +function Add(x: lmap, i: int, v: int): (lmap); +axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); -function Remove(x: lmap, i: Node): (lmap); -axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); +function Remove(x: lmap, i: int): (lmap); +axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); -procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node); -ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|; +procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int); +ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|; -procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node); -ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C; +procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int); +ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C; B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; C: assume !dom(Stack)[i]; return true; }|; -procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap); +procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:int, v:int) returns ({:linear "Node"} l_out:lmap); ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|; -procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap); +procedure {:yields} {:layer 0,1} TransferToStack(oldVal: int, newVal: int, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap); ensures {:atomic} |{ A: assert dom(l_in)[newVal]; goto B,C; B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true; C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|; -procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool); +procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: int, newVal: int) returns (r: bool); ensures {:atomic} |{ A: goto B,C; - B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true; + B: assume oldVal == TopOfStack; TopOfStack := newVal; Used[oldVal] := true; Stack := Remove(Stack, oldVal); r := true; return true; C: assume oldVal != TopOfStack; r := false; return true; }|; -var {:layer 0} TopOfStack: Node; +var {:layer 0} TopOfStack: int; var {:linear "Node"} {:layer 0} Stack: lmap; -function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool) +function {:inline} Inv(TopOfStack: int, Stack: lmap) : (bool) { BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] && Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack))) } -var {:linear "Node"} {:layer 0} Used: lmap; +var {:linear "Node"} {:layer 0} Used: [int]bool; + +function {:inline} {:linear "Node"} NodeCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "Node"} NodeSetCollector(x: [int]bool) : [int]bool +{ + x +} -procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap) +procedure {:yields} {:layer 1} push(x: int, {:linear_in "Node"} x_lmap: lmap) requires {:layer 1} dom(x_lmap)[x]; requires {:layer 1} Inv(TopOfStack, Stack); ensures {:layer 1} Inv(TopOfStack, Stack); ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|; { - var t: Node; + var t: int; var g: bool; var {:linear "Node"} t_lmap: lmap; @@ -71,7 +80,6 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret call t_lmap := Store(t_lmap, x, t); call g, t_lmap := TransferToStack(t, x, t_lmap); if (g) { - assert {:layer 1} map(Stack)[x] == t; break; } yield; @@ -82,13 +90,13 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret assert {:expand} {:layer 1} Inv(TopOfStack, Stack); } -procedure {:yields} {:layer 1} pop() returns (t: Node) +procedure {:yields} {:layer 1} pop() returns (t: int) requires {:layer 1} Inv(TopOfStack, Stack); ensures {:layer 1} Inv(TopOfStack, Stack); -ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; +ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used[t] := true; TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; { var g: bool; - var x: Node; + var x: int; yield; assert {:layer 1} Inv(TopOfStack, Stack); @@ -115,7 +123,6 @@ function Subset([int]bool, [int]bool) returns (bool); function Empty() returns ([int]bool); function Singleton(int) returns ([int]bool); -function Reachable([int,int]bool, int) returns ([int]bool); function Union([int]bool, [int]bool) returns ([int]bool); axiom(forall x:int :: !Empty()[x]); diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl index 39dad919..0a2227b6 100644 --- a/Test/civl/wsq.bpl +++ b/Test/civl/wsq.bpl @@ -89,9 +89,9 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|; { var t: int; - var {:ghost} {:layer 3} oldH:int; - var {:ghost} {:layer 3} oldT:int; - var {:ghost} {:layer 3} oldStatusT:bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + var {:layer 3} oldStatusT:bool; call oldH, oldT := GhostRead(); yield; @@ -142,8 +142,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu { var h, t: int; var chk: bool; - var {:ghost} {:layer 3} oldH:int; - var {:ghost} {:layer 3} oldT:int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; call oldH, oldT := GhostRead(); yield; @@ -304,8 +304,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu { var h, t: int; var chk: bool; - var {:ghost} {:layer 3} oldH:int; - var {:ghost} {:layer 3} oldT:int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; call oldH, oldT := GhostRead(); yield; diff --git a/Test/commandline/multiple_procs_unusual_identifiers.bpl b/Test/commandline/multiple_procs_unusual_identifiers.bpl new file mode 100644 index 00000000..a3a4a4c1 --- /dev/null +++ b/Test/commandline/multiple_procs_unusual_identifiers.bpl @@ -0,0 +1,75 @@ +// RUN: %boogie "-proc:*Bar*" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 10 verified, 0 errors + +procedure foo() +{ + assert false; +} + +procedure bar() +{ + assert false; +} + +/* Start should be matched */ + +procedure _Bar() +{ + assert true; +} + +procedure .Bar() +{ + assert true; +} + +procedure ..Bar..() +{ + assert true; +} + +procedure $Bar() +{ + assert true; +} + +procedure #Bar() +{ + assert true; +} + +procedure 'Bar''() +{ + assert true; +} + +procedure ``Bar``() +{ + assert true; +} + +procedure ~Bar() +{ + assert true; +} + +procedure Bar^^() +{ + assert true; +} + +/* This is Boogie2 claims backslash is a valid identifier + but the parser rejects this. +procedure Bar\\() +{ + assert true; +} +*/ + +procedure ??Bar() +{ + assert true; +} + +/* End should be matched */ diff --git a/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl new file mode 100644 index 00000000..e0f8eef3 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie "-proc:*Bar" "-proc:*Foo" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 4 verified, 0 errors + +procedure foo() +{ + assert false; +} + +procedure helpfulFoo() +{ + assert true; +} + +procedure Foo() +{ + assert true; +} + +procedure translucentBar() +{ + assert true; +} + +procedure opaqueBar() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl new file mode 100644 index 00000000..0f6571ba --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "-proc:*Bar" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +procedure translucentBar() +{ + assert true; +} + +procedure opaqueBar() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl new file mode 100644 index 00000000..5cb102e2 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "-proc:bar*" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +procedure bar() +{ + assert true; +} + +procedure barzzz() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl new file mode 100644 index 00000000..7e19fe79 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie "-proc:trivial*ZZZ" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +// should not be matched +procedure trivialFooZZX() +{ + assert false; +} + +procedure trivialFooZZZ() +{ + assert true; +} + +procedure trivialBarZZZ() +{ + assert true; +} diff --git a/Test/extractloops/detLoopExtract2.bpl b/Test/extractloops/detLoopExtract2.bpl new file mode 100644 index 00000000..f2befc53 --- /dev/null +++ b/Test/extractloops/detLoopExtract2.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -nologo -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:6 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/4 +procedure {:entrypoint} Main() returns(r:int) +{ + var i, j : int; + var Flag : bool; + var b : bool; + i := 0; + j := 0; + Flag := false; + while(i<3) + { + havoc b; + if (b || Flag) { + i := i + 1; + j := j + 1; + } + else { + Flag := true; + j := j + 1; + } + } + assume !(i == j || i == j - 1); + return; +} diff --git a/Test/extractloops/detLoopExtract2.bpl.expect b/Test/extractloops/detLoopExtract2.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/extractloops/detLoopExtract2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/extractloops/detLoopExtractNested.bpl b/Test/extractloops/detLoopExtractNested.bpl new file mode 100644 index 00000000..65de20c1 --- /dev/null +++ b/Test/extractloops/detLoopExtractNested.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:100 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/1 + +var t: int; +procedure {:entrypoint} NestedLoops() +modifies t; +//ensures t == 6; +{ + var i:int, j:int; + i, j, t := 0, 0, 0; + while(i < 2) { + j := 0; + while (j < 3) { + t := t + 1; + j := j + 1; + } + i := i + 1; + } + assume true; //would be provable (!true) wihtout the fix +} + diff --git a/Test/extractloops/detLoopExtractNested.bpl.expect b/Test/extractloops/detLoopExtractNested.bpl.expect new file mode 100644 index 00000000..f4932ede --- /dev/null +++ b/Test/extractloops/detLoopExtractNested.bpl.expect @@ -0,0 +1,19 @@ +(0,0): Error BP5001: This assertion might not hold. +Execution trace: + detLoopExtractNested.bpl(12,12): anon0 + detLoopExtractNested.bpl(14,8): anon5_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(14,8): anon5_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(16,10): anon6_LoopBody + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(15,6): anon6_LoopDone + detLoopExtractNested.bpl(13,4): anon5_LoopDone + detLoopExtractNested.bpl(13,4): anon5_LoopDone + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index b4f784d3..c3c294c9 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -89,11 +89,14 @@ modifies g; procedure {:yields} {:layer 0} I({:linear_in ""} x:int) returns({:linear ""} x':int) { + yield; x' := x; + yield; } procedure {:yields} {:layer 0} J() { + yield; } procedure {:yields} {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int) diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect index 9f960f26..3c0d0b20 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect @@ -127,7 +127,8 @@ Execution trace: daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2 daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2 daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2 - daytona_bug2_ioctl_example_2.bpl(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Then#2 + daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2 + daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2 daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2 daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2 daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2 diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl new file mode 100644 index 00000000..24424e53 --- /dev/null +++ b/Test/optimization/Optimization0.bpl @@ -0,0 +1,84 @@ +// RUN: %boogie /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function may_fail(f: int) : bool; + +procedure test0() +{ + var x: int; + + havoc x; + assume 42 < x; + assume {:minimize x} true; + assert may_fail(x); +} + +procedure test1() +{ + var x: int; + + x := 24; + if (*) { + x := 42; + } + assume {:minimize x} true; + assert may_fail(x); +} + +procedure test2() +{ + var x: int; + + x := 1; + while (*) { + x := x + 1; + } + assume {:minimize x} true; + assert x < 10; +} + +procedure test3() +{ + var x: int; + + havoc x; + assume x < 42; + assume {:maximize x} true; + assert may_fail(x); +} + +procedure test4() +{ + var x: int; + + x := 24; + if (*) { + x := 42; + } + assume {:maximize x} true; + assert may_fail(x); +} + +procedure test5() +{ + var x: int; + + x := 1; + while (*) { + x := x - 1; + } + assume {:maximize x} true; + assert x < 1; +} + +procedure test6() +{ + var x: int; + + x := 1; + if (*) { + x := 2; + } + assume {:maximize x} true; + assert may_fail(x); +} diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect new file mode 100644 index 00000000..f5a51848 --- /dev/null +++ b/Test/optimization/Optimization0.bpl.expect @@ -0,0 +1,135 @@ +*** MODEL +%lbl%@280 -> false +%lbl%+260 -> true +%lbl%+39 -> true +x@0 -> 43 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 43 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(10,5): anon0 +*** MODEL +%lbl%@321 -> false +%lbl%+299 -> true +%lbl%+66 -> true +%lbl%+68 -> true +x@0@@0 -> 24 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 24 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(25,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(20,7): anon0 + Optimization0.bpl(21,5): anon3_Else + Optimization0.bpl(24,5): anon2 +*** MODEL +%lbl%@353 -> false +%lbl%+335 -> true +%lbl%+95 -> true +%lbl%+99 -> true +x@0@@1 -> 10 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization0.bpl(37,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(32,7): anon0 + Optimization0.bpl(33,5): anon3_LoopHead + Optimization0.bpl(33,5): anon3_LoopDone +*** MODEL +%lbl%@386 -> false +%lbl%+122 -> true +%lbl%+375 -> true +x@0@@2 -> 41 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 41 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(44,5): anon0 +*** MODEL +%lbl%@414 -> false +%lbl%+147 -> true +%lbl%+151 -> true +%lbl%+392 -> true +x@0@@3 -> 42 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 42 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(59,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(54,7): anon0 + Optimization0.bpl(56,11): anon3_Then + Optimization0.bpl(58,5): anon2 +*** MODEL +%lbl%@446 -> false +%lbl%+178 -> true +%lbl%+182 -> true +%lbl%+428 -> true +x@0@@4 -> 1 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization0.bpl(71,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(66,7): anon0 + Optimization0.bpl(67,5): anon3_LoopHead + Optimization0.bpl(67,5): anon3_LoopDone +*** MODEL +%lbl%@490 -> false +%lbl%+209 -> true +%lbl%+213 -> true +%lbl%+468 -> true +x@0@@5 -> 2 +tickleBool -> { + true -> true + false -> true + else -> true +} +may_fail -> { + 2 -> false + else -> false +} +*** END_MODEL +Optimization0.bpl(83,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization0.bpl(78,7): anon0 + Optimization0.bpl(80,11): anon3_Then + Optimization0.bpl(82,5): anon2 + +Boogie program verifier finished with 0 verified, 7 errors diff --git a/Test/optimization/Optimization1.bpl b/Test/optimization/Optimization1.bpl new file mode 100644 index 00000000..60df1edd --- /dev/null +++ b/Test/optimization/Optimization1.bpl @@ -0,0 +1,32 @@ +// RUN: %boogie /noVerify /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:minimize} true; +} + +procedure test1(n: int) +{ + assume {:maximize} true; +} + +procedure test2(n: int) +{ + assume {:minimize n, n} true; +} + +procedure test3(n: int) +{ + assume {:maximize n, n} true; +} + +procedure test4(n: int) +{ + assume {:minimize true} true; +} + +procedure test5(n: int) +{ + assume {:maximize true} true; +} diff --git a/Test/optimization/Optimization1.bpl.expect b/Test/optimization/Optimization1.bpl.expect new file mode 100644 index 00000000..d8508807 --- /dev/null +++ b/Test/optimization/Optimization1.bpl.expect @@ -0,0 +1,5 @@ +Optimization1.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(16,11): Error: attributes :minimize and :maximize accept only one argument +Optimization1.bpl(21,11): Error: attributes :minimize and :maximize accept only one argument +4 name resolution errors detected in Optimization1.bpl diff --git a/Test/optimization/Optimization2.bpl b/Test/optimization/Optimization2.bpl new file mode 100644 index 00000000..7d80d735 --- /dev/null +++ b/Test/optimization/Optimization2.bpl @@ -0,0 +1,12 @@ +// RUN: %boogie /noVerify /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:minimize true} true; +} + +procedure test1(n: int) +{ + assume {:maximize true} true; +} diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect new file mode 100644 index 00000000..cab2fd3d --- /dev/null +++ b/Test/optimization/Optimization2.bpl.expect @@ -0,0 +1,3 @@ +Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv +2 type checking errors detected in Optimization2.bpl diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl new file mode 100644 index 00000000..02499c31 --- /dev/null +++ b/Test/optimization/Optimization3.bpl @@ -0,0 +1,20 @@ +// RUN: %boogie /printModel:4 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0() +{ + var x: int; + + assume x < 42; + assume {:maximize x} true; + assert (exists y: int :: y < x); +} + +procedure test1() +{ + var x: int; + + assume x < 42; + assume {:maximize x} true; + assert (forall y: int :: y < x); +} diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect new file mode 100644 index 00000000..6a0066fc --- /dev/null +++ b/Test/optimization/Optimization3.bpl.expect @@ -0,0 +1,31 @@ +*** MODEL +%lbl%@80 -> false +%lbl%+33 -> true +%lbl%+61 -> true +x -> 41 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization3.bpl(10,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization3.bpl(8,5): anon0 +*** MODEL +%lbl%@115 -> false +%lbl%+105 -> true +%lbl%+56 -> true +x@@0 -> 41 +y@@0!1!1 -> 719 +tickleBool -> { + true -> true + false -> true + else -> true +} +*** END_MODEL +Optimization3.bpl(19,5): Error BP5001: This assertion might not hold. +Execution trace: + Optimization3.bpl(17,5): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg new file mode 100644 index 00000000..35c7e558 --- /dev/null +++ b/Test/optimization/lit.local.cfg @@ -0,0 +1,3 @@ +# Do not run tests in this directory and below +config.unsupported = True +# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827. diff --git a/Test/test0/AssertVerifiedUnder0.bpl b/Test/test0/AssertVerifiedUnder0.bpl new file mode 100644 index 00000000..1b054f68 --- /dev/null +++ b/Test/test0/AssertVerifiedUnder0.bpl @@ -0,0 +1,8 @@ +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0() +{ + assert {:verified_under} true; + assert {:verified_under true, false} true; +} diff --git a/Test/test0/AssertVerifiedUnder0.bpl.expect b/Test/test0/AssertVerifiedUnder0.bpl.expect new file mode 100644 index 00000000..b3d8177d --- /dev/null +++ b/Test/test0/AssertVerifiedUnder0.bpl.expect @@ -0,0 +1,3 @@ +AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument +AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument +2 name resolution errors detected in AssertVerifiedUnder0.bpl diff --git a/Test/test1/AssertVerifiedUnder0.bpl b/Test/test1/AssertVerifiedUnder0.bpl new file mode 100644 index 00000000..e419a5ef --- /dev/null +++ b/Test/test1/AssertVerifiedUnder0.bpl @@ -0,0 +1,8 @@ +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0() +{ + assert {:verified_under 4} true; + assert {:verified_under 3.0} true; +} diff --git a/Test/test1/AssertVerifiedUnder0.bpl.expect b/Test/test1/AssertVerifiedUnder0.bpl.expect new file mode 100644 index 00000000..6d3c04cd --- /dev/null +++ b/Test/test1/AssertVerifiedUnder0.bpl.expect @@ -0,0 +1,3 @@ +AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument of type bool +AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument of type bool +2 type checking errors detected in AssertVerifiedUnder0.bpl diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl new file mode 100644 index 00000000..abf26159 --- /dev/null +++ b/Test/test1/StatementIds0.bpl @@ -0,0 +1,24 @@ +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} true; + assert {:id "s0"} true; +} + +procedure test1() +{ + call {:id "s0"} P(); +} + +procedure test2(n: int) +{ + while (*) + invariant {:id "s0"} true; + invariant {:id "s0"} true; + { + } +} + +procedure P(); diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect new file mode 100644 index 00000000..4783d912 --- /dev/null +++ b/Test/test1/StatementIds0.bpl.expect @@ -0,0 +1,5 @@ +StatementIds0.bpl(7,4): Error: more than one statement with same id: s0 +StatementIds0.bpl(12,4): Error: more than one statement with same id: s0 +StatementIds0.bpl(18,6): Error: more than one statement with same id: s0 +StatementIds0.bpl(19,6): Error: more than one statement with same id: s0 +4 name resolution errors detected in StatementIds0.bpl diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 5d9d41c5..6939fee4 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -14,17 +14,17 @@ $mv_state_const -> 3 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m -m@0 -> (- 276) -m@1 -> (- 275) -m@3 -> (- 275) +m@0 -> (- 2) +m@1 -> (- 1) +m@3 -> (- 1) r -> **r -r@0 -> (- 550) +r@0 -> (- 2) this -> T@Ref!val!0 x -> 719 y -> **y Select_[Ref,FieldName]$int -> { - |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276) - else -> (- 276) + |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2) + else -> (- 2) } $mv_state -> { 3 0 -> true @@ -49,13 +49,13 @@ tickleBool -> { *** STATE top *** END_STATE *** STATE then - m -> (- 276) + m -> (- 2) *** END_STATE *** STATE postUpdate0 - m -> (- 275) + m -> (- 1) *** END_STATE *** STATE end - r -> (- 550) + r -> (- 2) m -> 7 *** END_STATE *** END_MODEL diff --git a/Test/test2/BadLineNumber.bpl b/Test/test2/BadLineNumber.bpl new file mode 100644 index 00000000..b8776a4e --- /dev/null +++ b/Test/test2/BadLineNumber.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure p(); + ensures false; + +implementation p() +{ + if (*) + { + } + else + { + } +}
\ No newline at end of file diff --git a/Test/test2/BadLineNumber.bpl.expect b/Test/test2/BadLineNumber.bpl.expect new file mode 100644 index 00000000..bc5d1984 --- /dev/null +++ b/Test/test2/BadLineNumber.bpl.expect @@ -0,0 +1,7 @@ +BadLineNumber.bpl(15,1): Error BP5003: A postcondition might not hold on this return path. +BadLineNumber.bpl(5,3): Related location: This is the postcondition that might not hold. +Execution trace: + BadLineNumber.bpl(9,5): anon0 + BadLineNumber.bpl(14,5): anon3_Else + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl new file mode 100644 index 00000000..a955495a --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assume {:id "s0"} 0 < n; +} + +procedure test1(n: int) +{ + assume {:id "s0"} 0 < n; +} diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect new file mode 100644 index 00000000..9e420fa7 --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect @@ -0,0 +1,3 @@ +unnecessaryassumes0.bpl(7,4): Error: more than one statement with same id: s0 +unnecessaryassumes0.bpl(12,4): Error: more than one statement with same id: s0 +2 name resolution errors detected in unnecessaryassumes0.bpl diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl new file mode 100644 index 00000000..04226dfd --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie /printNecessaryAssumes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assert 0 <= n; // verified under s0 +} + +procedure test1(n: int) +{ + assume 0 < n; + assume {:id "s1"} n == 3; + assert 0 <= n; // verified under true +} + +procedure test2(n: int) +{ + assume 0 < n; + assume {:id "s2"} n <= 42; + assume {:id "s3"} 42 <= n; + assert n == 42; // verified under s2 and s3 +} diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect new file mode 100644 index 00000000..dd04bb46 --- /dev/null +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect @@ -0,0 +1,3 @@ +Necessary assume command(s): s0, s3, s2 + +Boogie program verifier finished with 3 verified, 0 errors |