diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae /Test/codeexpr/CodeExpr0.bpl | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
Diffstat (limited to 'Test/codeexpr/CodeExpr0.bpl')
| -rw-r--r-- | Test/codeexpr/CodeExpr0.bpl | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl new file mode 100644 index 00000000..62a4225f --- /dev/null +++ b/Test/codeexpr/CodeExpr0.bpl @@ -0,0 +1,53 @@ +procedure P()
+{
+ assert |{ A: return true; }|;
+}
+
+// ------------
+
+procedure Q()
+{
+ assert |{ var x: bool; A: x := true; return x; }|;
+}
+
+procedure R()
+{
+ assert |{ var x: bool; A: x := false; return x; }|; // error
+}
+
+procedure S()
+{
+ assert |{ var x: bool; A: return x; }|; // error
+}
+
+// ------------
+
+procedure T(x: int, y: int)
+ requires |{ var z: bool;
+ Start: goto A;
+ A: z := false; goto B, C;
+ B: assume 0 <= x; goto D;
+ C: assume x < 0; goto R;
+ D: goto E, F;
+ E: assume 0 <= y; z := true; goto R;
+ F: assume y < 0; goto R;
+ R: return z;
+ }|;
+{
+ assert 0 <= x + y;
+}
+
+procedure U(x: int, y: int)
+ requires |{ var z: bool;
+ Start: goto A;
+ A: z := false; goto B, C;
+ B: assume 0 <= x; goto D;
+ C: assume x < 0; goto R;
+ D: goto E, F;
+ E: assume 0 <= y; z := true; goto R;
+ F: assume y < 0; goto R;
+ R: return z;
+ }|;
+{
+ assert x <= y; // error
+}
|