From ce2156e0b37f2efdb2e17aa1998c1c6a71adf062 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Wed, 18 Aug 2010 01:09:33 +0000
Subject: Change Synonym type printing to what it was, use a workaround in
 TypeToString() instead. Add test for /typeEncoding:m.

---
 Test/test2/Answer            | 29 +++++++++++++++++++++++++++++
 Test/test2/TypeEncodingM.bpl | 25 +++++++++++++++++++++++++
 Test/test2/runtest.bat       |  6 ++++++
 3 files changed, 60 insertions(+)
 create mode 100644 Test/test2/TypeEncodingM.bpl

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index a9329010..5cea9721 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -380,6 +380,35 @@ Execution trace:
         LambdaPoly.bpl(34,5): anon5_Else
 
 Boogie program verifier finished with 1 verified, 3 errors
+
+-------------------- Arrays.bpl /typeEncoding:m --------------------
+Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(38,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+        Arrays.bpl(42,3): start
+Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+        Arrays.bpl(123,3): start
+
+Boogie program verifier finished with 8 verified, 2 errors
+
+-------------------- Lambda.bpl /typeEncoding:m --------------------
+Lambda.bpl(37,3): Error BP5001: This assertion might not hold.
+Execution trace:
+        Lambda.bpl(36,5): anon0
+Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
+Execution trace:
+        Lambda.bpl(36,5): anon0
+
+Boogie program verifier finished with 4 verified, 2 errors
+
+-------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
+TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
+Execution trace:
+        TypeEncodingM.bpl(11,9): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
 -------------------- sk_hack.bpl --------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test2/TypeEncodingM.bpl b/Test/test2/TypeEncodingM.bpl
new file mode 100644
index 00000000..01c95f7a
--- /dev/null
+++ b/Test/test2/TypeEncodingM.bpl
@@ -0,0 +1,25 @@
+type TT;
+
+procedure A()
+{
+  var M : [int]bool;
+  var N : [int,int]bool;
+  var Z : [int,bool]TT;
+  var t : TT;
+
+
+  M[10] := true;
+  M[20] := false;
+  N[10,20] := true;
+  N[10,21] := false;
+  N[11,20] := false;
+
+  assert M[10];
+  assert !M[20];
+
+  assert N[10,20];
+  assert !N[11,20];
+  assert !N[10,21];
+
+  assert Z[10,true] == t;
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index dbe5b726..f704e263 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -17,6 +17,12 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
   %BGEXE% %* /noinfer %%f
 )
 
+for %%f in (Arrays.bpl Lambda.bpl TypeEncodingM.bpl ) do (
+  echo.
+  echo -------------------- %%f /typeEncoding:m --------------------
+  %BGEXE% %* /noinfer /typeEncoding:m %%f
+)
+
 echo -------------------- sk_hack.bpl --------------------
 %BGEXE% %* /noinfer /bv:z sk_hack.bpl 
 
-- 
cgit v1.2.3