Add alloc resource predicate definition

rems-project · Aug 15, 2023 · 1dc6cf8 · 1dc6cf8
1 parent 0679240
commit 1dc6cf8
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 3 deletions.
diff --git a/backend/cn/context.ml b/backend/cn/context.ml
@@ -52,7 +52,7 @@ let empty =
   let alloc_id = Sym.fresh_named "__cn_alloc_history" in
   let loc_str = __FILE__ ^ ":" ^ string_of_int __LINE__ in
   let l_info = (Locations.other loc_str, lazy (Pp.string loc_str)) in
-  let bt = (BT.Map(Alloc_id, Record [(Id.id "base", Loc); (Id.id "len", Integer)])) in
+  let bt = (BT.Map(Alloc_id, Record [(Id.id "base", Integer); (Id.id "len", Integer)])) in
   let logical = SymMap.(empty |> add alloc_id (BaseType bt, l_info)) in
   {
     computational = SymMap.empty;

diff --git a/backend/cn/global.ml b/backend/cn/global.ml
@@ -19,11 +19,20 @@ type t =
   } 
 
 let empty = 
+  let alloc = Sym.fresh_named "__cn_alloc" in
+  let def : ResourcePredicates.definition =
+  { loc = Locations.other (__FILE__ ^ ":" ^ string_of_int __LINE__);
+    pointer = Sym.fresh_named "__cn_alloc_ptr";
+    iargs = [];
+    oarg_bt = Unit;
+    clauses = None;
+  } in
+  let resource_predicates = SymMap.(empty |> add alloc def) in
   { struct_decls = SymMap.empty;
     datatypes = SymMap.empty;
     datatype_constrs = SymMap.empty;
     fun_decls = SymMap.empty;
-    resource_predicates = SymMap.empty;
+    resource_predicates;
     logical_functions = SymMap.empty;
     lemmata = SymMap.empty;
   }

diff --git a/backend/cn/resourcePredicates.ml b/backend/cn/resourcePredicates.ml
@@ -113,4 +113,4 @@ let identify_right_clause provable def pointer iargs =
             | `True -> try_clauses clauses
             | `False -> None          
       in
-      try_clauses clauses
+      try_clauses clauses
diff --git a/tests/run-cn.sh b/tests/run-cn.sh