Change Synonym type printing to what it was, use a workaround in TypeToString() instead. Add test for /typeEncoding:m.

3 files changed, 60 insertions, 0 deletions

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