diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/test2/B.bpl | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/test2/B.bpl')
-rw-r--r-- | Test/test2/B.bpl | 176 |
1 files changed, 88 insertions, 88 deletions
diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl index 78f91915..c90c156b 100644 --- a/Test/test2/B.bpl +++ b/Test/test2/B.bpl @@ -1,88 +1,88 @@ -// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// ----------- BEGIN PRELUDE
-
-var Heap: [ref, name]int;
-const N: name;
-
-procedure Q0()
-{
- var h: int;
-
- entry:
- goto Else;
-
- Then:
- h := 15;
- goto end;
-
- Else:
- assume h == 0;
- goto end;
-
- end:
- assert 0 <= h;
- return;
-}
-
-procedure Q1()
-{
- var h: int;
-
- entry:
- goto Else;
-
- Then:
- h := -15;
- goto end;
-
- Else:
- assume h == 0;
- goto end;
-
- end:
- h := -h;
- assert 0 <= h;
- return;
-}
-
-procedure P0(this: ref)
- modifies Heap;
-{
- entry:
- goto Else;
-
- Then:
- Heap[this, N] := 15;
- goto end;
-
- Else:
- assume Heap[this, N] == 0;
- goto end;
-
- end:
- assert 0 <= Heap[this, N];
- return;
-}
-
-procedure P1(this: ref)
- modifies Heap;
-{
- entry:
- goto Else;
-
- Then:
- Heap[this, N] := -15;
- goto end;
-
- Else:
- assume Heap[this, N] == 0;
- goto end;
-
- end:
- Heap[this, N] := -Heap[this, N];
- assert 0 <= Heap[this, N];
- return;
-}
-
-type name, ref;
+// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// ----------- BEGIN PRELUDE + +var Heap: [ref, name]int; +const N: name; + +procedure Q0() +{ + var h: int; + + entry: + goto Else; + + Then: + h := 15; + goto end; + + Else: + assume h == 0; + goto end; + + end: + assert 0 <= h; + return; +} + +procedure Q1() +{ + var h: int; + + entry: + goto Else; + + Then: + h := -15; + goto end; + + Else: + assume h == 0; + goto end; + + end: + h := -h; + assert 0 <= h; + return; +} + +procedure P0(this: ref) + modifies Heap; +{ + entry: + goto Else; + + Then: + Heap[this, N] := 15; + goto end; + + Else: + assume Heap[this, N] == 0; + goto end; + + end: + assert 0 <= Heap[this, N]; + return; +} + +procedure P1(this: ref) + modifies Heap; +{ + entry: + goto Else; + + Then: + Heap[this, N] := -15; + goto end; + + Else: + assume Heap[this, N] == 0; + goto end; + + end: + Heap[this, N] := -Heap[this, N]; + assert 0 <= Heap[this, N]; + return; +} + +type name, ref; |