From 4e51bca1ef891bb9cc22b359cff83cc193e7543d Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 15 Nov 2024 18:23:55 +0100
Subject: [PATCH] [kernel compatiblity] Use records for Cil_types.typ
---
meta_bindings.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/meta_bindings.ml b/meta_bindings.ml
index 1d23d72..01674af 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -119,8 +119,8 @@ let add_ghost_code flags =
let base_type = Logic_utils.logicCType typ in
(* The _set is either a fixed array or a pointer *)
let ctype = match flags.static_bindings with
- | Some n -> TArray (base_type, Some (Cil.integer ~loc:unkloc n), [])
- | None -> TPtr (base_type, [])
+ | Some n -> Cil_const.mk_tarray base_type (Some (Cil.integer ~loc:unkloc n))
+ | None -> Cil_const.mk_tptr base_type
in
let var = Cil.makeGlobalVar (setname name) ctype in
let svar = Cil.makeGlobalVar (sizename name) Cil_const.uintType in
--
GitLab