From a30715d14eb0ca05daaac5b26bf410dca76c3979 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Wed, 16 Aug 2023 20:15:39 +0100 Subject: [PATCH] Add helper function for Alloc resource_type --- backend/cn/global.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/backend/cn/global.ml b/backend/cn/global.ml index b40c465c8..52dc71bff 100644 --- a/backend/cn/global.ml +++ b/backend/cn/global.ml @@ -18,8 +18,13 @@ type t = lemmata : (Locations.t * AT.lemmat) SymMap.t; } +let mk_alloc : IndexTerms.t -> ResourceTypes.predicate_type = + let name : ResourceTypes.predicate_name = PName (Sym.fresh_named "__CN_Alloc") in + fun pointer -> { name; pointer; iargs = []; } + let empty = - let alloc = Sym.fresh_named "__cn_alloc" in + let [@ocaml.warning "-8"] { name=PName alloc ; _ } : ResourceTypes.predicate_type = + mk_alloc IndexTerms.null_ in let def : ResourcePredicates.definition = { loc = Locations.other (__FILE__ ^ ":" ^ string_of_int __LINE__); pointer = Sym.fresh_named "__cn_alloc_ptr";