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/ex.bpl | |
| parent | f82dab21f1240fb3f8d67a880f4f93017d85c345 (diff) | |
fixed datatype bug reported by Chris
fixed function body referring to globals bug
Diffstat (limited to 'Test/datatypes/ex.bpl')
| -rw-r--r-- | Test/datatypes/ex.bpl | 11 |
1 files changed, 11 insertions, 0 deletions
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];
+{
+}
|