diff options
Diffstat (limited to 'Test/test21/InterestingExamples2.bpl')
-rw-r--r-- | Test/test21/InterestingExamples2.bpl | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/Test/test21/InterestingExamples2.bpl b/Test/test21/InterestingExamples2.bpl index 6fc8d259..4c07ee68 100644 --- a/Test/test21/InterestingExamples2.bpl +++ b/Test/test21/InterestingExamples2.bpl @@ -1,20 +1,20 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
-// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
-// RUN: %diff "%s.p.expect" "%t"
-// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
-// RUN: %diff "%s.a.expect" "%t"
-
-
-procedure P() returns () {
-var m : <a>[a]ref;
-var n : <b>[b]b;
-var o : ref;
-
-m[5] := null;
-assert m[true := o][5] == null;
-assert m[n[true] := o][5] == null;
-}
-
-type ref;
-const null : ref;
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" + + +procedure P() returns () { +var m : <a>[a]ref; +var n : <b>[b]b; +var o : ref; + +m[5] := null; +assert m[true := o][5] == null; +assert m[n[true] := o][5] == null; +} + +type ref; +const null : ref; |