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/test0/Prog0.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/test0/Prog0.bpl')
-rw-r--r-- | Test/test0/Prog0.bpl | 106 |
1 files changed, 53 insertions, 53 deletions
diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index d9e467ec..51383660 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,53 +1,53 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// BoogiePL Examples
-
-type elements;
-
-var x:int; var y:real; var z:ref; // Variables
-var x.3:bool; var $ar:ref; // Names can have glyphs
-
-const a, b, c:int; // Consts
-
-function f (int, int) returns (int); // Function with arity 2
-function g ( int , int) returns (int); // Function with arity 2
-function h(int,int) returns (int); // Function with arity 2
-
-function m (int) returns (int); // Function with arity 1
-function k(int) returns (int); // Function with arity 1
-
-
-axiom
- (forall x : int :: f(g(h(a,b),c),x) > 100) ;
-
-procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int);
-
-
-procedure q(x:int, y:ref) returns (z:int) // Procedure with output params
- requires x > 0; // as many req/ens/mod you want
- ensures z > 3;
- ensures old(x) == 1; // old only in ensures..
- modifies z,y,$ar;
-{
- var t, s: int;
- var r: [int,ref]ref;
-
- start: // one label per block
- t := x;
- s := t;
- z := x + t;
- call s, r,z := p(t,r[3,null]); // procedure call with mutiple returns
- goto continue, end ; // as many labels as you like
-
- continue:
- return; // ends control flow
-
- end:
- goto start;
-}
-
-procedure s(e: elements) { L: return; }
-procedure r (x:int, y:ref) returns (z:int);
-
-type ref;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +// BoogiePL Examples + +type elements; + +var x:int; var y:real; var z:ref; // Variables +var x.3:bool; var $ar:ref; // Names can have glyphs + +const a, b, c:int; // Consts + +function f (int, int) returns (int); // Function with arity 2 +function g ( int , int) returns (int); // Function with arity 2 +function h(int,int) returns (int); // Function with arity 2 + +function m (int) returns (int); // Function with arity 1 +function k(int) returns (int); // Function with arity 1 + + +axiom + (forall x : int :: f(g(h(a,b),c),x) > 100) ; + +procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int); + + +procedure q(x:int, y:ref) returns (z:int) // Procedure with output params + requires x > 0; // as many req/ens/mod you want + ensures z > 3; + ensures old(x) == 1; // old only in ensures.. + modifies z,y,$ar; +{ + var t, s: int; + var r: [int,ref]ref; + + start: // one label per block + t := x; + s := t; + z := x + t; + call s, r,z := p(t,r[3,null]); // procedure call with mutiple returns + goto continue, end ; // as many labels as you like + + continue: + return; // ends control flow + + end: + goto start; +} + +procedure s(e: elements) { L: return; } +procedure r (x:int, y:ref) returns (z:int); + +type ref; +const null : ref; |