summaryrefslogtreecommitdiff
path: root/Test/test1/AttributeTyping.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test1/AttributeTyping.bpl')
-rw-r--r--Test/test1/AttributeTyping.bpl74
1 files changed, 37 insertions, 37 deletions
diff --git a/Test/test1/AttributeTyping.bpl b/Test/test1/AttributeTyping.bpl
index bcd98feb..713f464c 100644
--- a/Test/test1/AttributeTyping.bpl
+++ b/Test/test1/AttributeTyping.bpl
@@ -1,38 +1,38 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-const {:Incorrect pux0 ++ F0(pux1)} pux0: int;
-
-function {:Incorrect F0(pux0 < 0) + pux1} F0(int) returns (int);
-
-axiom {:Incorrect F0(pux0 == pux1)} true;
-
-var {:Incorrect pux0 && pux1} pux1: int;
-
-procedure {:Incorrect !(pux0 - pux1)} P();
-
-implementation {:Incorrect pux0 ==> pux1} P()
-{
-}
-
-// ------ and here are various correct things
-
-
-
-const {:Correct hux0 + F1(hux1)} hux0: int;
-
-function {:Correct F1(hux0) + hux1} F1(int) returns (int);
-
-axiom {:Correct F1(hux0 + hux1)} true;
-
-var {:Correct hux0*hux1} hux1: int;
-
-procedure {:Correct hux0 - hux1} H();
-
-implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} H()
-{
-}
-
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+const {:Incorrect pux0 ++ F0(pux1)} pux0: int;
+
+function {:Incorrect F0(pux0 < 0) + pux1} F0(int) returns (int);
+
+axiom {:Incorrect F0(pux0 == pux1)} true;
+
+var {:Incorrect pux0 && pux1} pux1: int;
+
+procedure {:Incorrect !(pux0 - pux1)} P();
+
+implementation {:Incorrect pux0 ==> pux1} P()
+{
+}
+
+// ------ and here are various correct things
+
+
+
+const {:Correct hux0 + F1(hux1)} hux0: int;
+
+function {:Correct F1(hux0) + hux1} F1(int) returns (int);
+
+axiom {:Correct F1(hux0 + hux1)} true;
+
+var {:Correct hux0*hux1} hux1: int;
+
+procedure {:Correct hux0 - hux1} H();
+
+implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} H()
+{
+}
+
+
type any; \ No newline at end of file