diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-05 15:42:12 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-05 15:42:12 -0800 |
| commit | 47ac92a139c1cc11ff7f68b726960fcd902e41d2 (patch) | |
| tree | 2cf5bbb30998c8f3987020196c82d94573f1a870 /Test/datatypes | |
| parent | f82dab21f1240fb3f8d67a880f4f93017d85c345 (diff) | |
fixed datatype bug reported by Chris
fixed function body referring to globals bug
Diffstat (limited to 'Test/datatypes')
| -rw-r--r-- | Test/datatypes/Answer | 4 | ||||
| -rw-r--r-- | Test/datatypes/ex.bpl | 11 | ||||
| -rw-r--r-- | Test/datatypes/runtest.bat | 2 |
3 files changed, 16 insertions, 1 deletions
diff --git a/Test/datatypes/Answer b/Test/datatypes/Answer index 7b7b411a..bac8f345 100644 --- a/Test/datatypes/Answer +++ b/Test/datatypes/Answer @@ -12,3 +12,7 @@ Execution trace: t2.bpl(16,3): anon0
Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- ex.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/datatypes/ex.bpl b/Test/datatypes/ex.bpl new file mode 100644 index 00000000..32b302f3 --- /dev/null +++ b/Test/datatypes/ex.bpl @@ -0,0 +1,11 @@ +type{:datatype} finite_map;
+function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;
+
+type{:datatype} partition;
+function{:constructor} partition(owners:[int]int, vars:[int]finite_map):partition;
+
+procedure P(arr:finite_map)
+ requires dom#finite_map(arr)[0];
+ ensures dom#finite_map(arr)[0];
+{
+}
diff --git a/Test/datatypes/runtest.bat b/Test/datatypes/runtest.bat index fe2aa09d..2ff4bad8 100644 --- a/Test/datatypes/runtest.bat +++ b/Test/datatypes/runtest.bat @@ -4,7 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries
set BPLEXE=%BOOGIEDIR%\Boogie.exe
-for %%f in (t1.bpl t2.bpl) do (
+for %%f in (t1.bpl t2.bpl ex.bpl) do (
echo.
echo -------------------- %%f --------------------
%BPLEXE% %* /typeEncoding:m %%f
|