diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-07-20 18:43:27 +0200 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-07-20 18:45:57 +0200 |
commit | 740f004792b49e59f3980150cb8d543737adbc4b (patch) | |
tree | 4d25c0dba0532db533768c460748098114d2d11b /Test/snapshots/Snapshots40.v1.bpl | |
parent | 535d0b56285a436251bd955f3da9fb550c1a2e79 (diff) |
Added another test.
Diffstat (limited to 'Test/snapshots/Snapshots40.v1.bpl')
-rw-r--r-- | Test/snapshots/Snapshots40.v1.bpl | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Test/snapshots/Snapshots40.v1.bpl b/Test/snapshots/Snapshots40.v1.bpl new file mode 100644 index 00000000..e1c505f8 --- /dev/null +++ b/Test/snapshots/Snapshots40.v1.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "-1"} Foo(b: bool); + +implementation {:id "Foo"} {:checksum "2"} Foo(b: bool) +{ + var r: int; + + assert b; + call r := Sum(42); + assert r != 0; + assert r == (42 * 43) div 2; +} + +procedure {:checksum "1"} Sum(n: int) returns (r: int); + requires 0 <= n; + ensures n <= r; |