diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Test/test1/WhereTyping.bpl | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Test/test1/WhereTyping.bpl')
-rw-r--r-- | Test/test1/WhereTyping.bpl | 94 |
1 files changed, 47 insertions, 47 deletions
diff --git a/Test/test1/WhereTyping.bpl b/Test/test1/WhereTyping.bpl index 0884e8ef..b3675f45 100644 --- a/Test/test1/WhereTyping.bpl +++ b/Test/test1/WhereTyping.bpl @@ -1,47 +1,47 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int where g == 12;
-
-procedure P(x: int where x > 0) returns (y: int where y < 0);
- requires x < 100;
- modifies g;
- ensures -100 < y;
-
-implementation P(xx: int) returns (yy: int)
-{
- var a: int;
- var b: int;
-
- start:
- a := xx;
- call b := P(a);
- yy := b;
- return;
-}
-
-type double;
-function F(double) returns (double);
-function G(double) returns (bool);
-
-procedure Q(omega: double where omega == F(omega),
- psi: double where psi + 1 == 0, // error: psi doesn't have right type for +
- pi: double where F(pi), // error: F has wrong return type
- sigma: double where G(sigma));
-
-
-const SomeConstant: name;
-function fgh(int) returns (int);
-
-procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int)
-{
- var k: int where k != SomeConstant; // fine, since SomeConstants refers to the out parameter
- var m: name where m != SomeConstant; // error: types don't match up
- var r: ref where (forall abc: int :: abc == SomeConstant);
- var b: bool;
- start:
- b := (forall x: int :: fgh(x) < SomeConstant);
- b := (forall l: name :: l == SomeConstant); // error: SomeConstant here refers to the out parameter
- return;
-}
-
-type ref, name;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var g: int where g == 12; + +procedure P(x: int where x > 0) returns (y: int where y < 0); + requires x < 100; + modifies g; + ensures -100 < y; + +implementation P(xx: int) returns (yy: int) +{ + var a: int; + var b: int; + + start: + a := xx; + call b := P(a); + yy := b; + return; +} + +type double; +function F(double) returns (double); +function G(double) returns (bool); + +procedure Q(omega: double where omega == F(omega), + psi: double where psi + 1 == 0, // error: psi doesn't have right type for + + pi: double where F(pi), // error: F has wrong return type + sigma: double where G(sigma)); + + +const SomeConstant: name; +function fgh(int) returns (int); + +procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int) +{ + var k: int where k != SomeConstant; // fine, since SomeConstants refers to the out parameter + var m: name where m != SomeConstant; // error: types don't match up + var r: ref where (forall abc: int :: abc == SomeConstant); + var b: bool; + start: + b := (forall x: int :: fgh(x) < SomeConstant); + b := (forall l: name :: l == SomeConstant); // error: SomeConstant here refers to the out parameter + return; +} + +type ref, name; |