From 73ec4170af6c28458d1940bf74f09c38a24d12a5 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 26 Jul 2024 16:15:06 +0200
Subject: [PATCH] [kernel] Add other type constructors in Cil_const

---
 src/kernel_services/ast_queries/cil_const.ml  | 28 ++++++
 src/kernel_services/ast_queries/cil_const.mli | 89 +++++++++++++++++++
 2 files changed, 117 insertions(+)

diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index bd4d41d64ce..bed7d0dd72d 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -44,7 +44,35 @@
 
 open Cil_types
 
+(* Types *)
+
 let voidType = TVoid([])
+let intType = TInt(IInt,[])
+let uintType = TInt(IUInt,[])
+let shortType = TInt(IShort, [])
+let ushortType = TInt(IUShort, [])
+let longType = TInt(ILong,[])
+let longLongType = TInt(ILongLong,[])
+let ulongType = TInt(IULong,[])
+let ulongLongType = TInt(IULongLong, [])
+let charType = TInt(IChar, [])
+let scharType = TInt(ISChar, [])
+let ucharType = TInt(IUChar, [])
+
+let charPtrType = TPtr(charType,[])
+let scharPtrType = TPtr(scharType,[])
+let ucharPtrType = TPtr(ucharType,[])
+let charConstPtrType = TPtr(TInt(IChar, [Attr("const", [])]),[])
+
+let voidPtrType = TPtr(voidType, [])
+let voidConstPtrType = TPtr(TVoid [Attr ("const", [])], [])
+
+let intPtrType = TPtr(intType, [])
+let uintPtrType = TPtr(uintType, [])
+
+let doubleType = TFloat(FDouble, [])
+let floatType = TFloat(FFloat, [])
+let longDoubleType = TFloat (FLongDouble, [])
 
 module Vid = State_builder.SharedCounter(struct let name = "vid_counter" end)
 module Sid = State_builder.SharedCounter(struct let name = "sid" end)
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 5edd0ba2b30..b43e9f2456f 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -45,8 +45,97 @@
 (** Smart constructors for some CIL data types *)
 open Cil_types
 
+(** void *)
 val voidType: typ
 
+(** int
+    @since Frama-C+dev *)
+val intType: typ
+
+(** unsigned
+    @since Frama-C+dev *)
+val uintType: typ
+
+(** short
+    @since Frama-C+dev *)
+val shortType : typ
+
+(** unsigned short
+    @since Frama-C+dev *)
+val ushortType : typ
+
+(** long
+    @since Frama-C+dev *)
+val longType: typ
+
+(** long long
+    @since Frama-C+dev *)
+val longLongType: typ
+
+(** unsigned long
+    @since Frama-C+dev *)
+val ulongType: typ
+
+(** unsigned long long
+    @since Frama-C+dev *)
+val ulongLongType: typ
+
+(** char
+    @since Frama-C+dev *)
+val charType: typ
+
+(** signed char
+    @since Frama-C+dev *)
+val scharType: typ
+
+(** unsigned char
+    @since Frama-C+dev *)
+val ucharType: typ
+
+(** char *
+    @since Frama-C+dev *)
+val charPtrType: typ
+
+(** signed char *
+    @since Frama-C+dev *)
+val scharPtrType: typ
+
+(** unisgned char *
+    @since Frama-C+dev *)
+val ucharPtrType: typ
+
+(** char const *
+    @since Frama-C+dev *)
+val charConstPtrType: typ
+
+(** void *
+    @since Frama-C+dev *)
+val voidPtrType: typ
+
+(** void const *
+    @since Frama-C+dev *)
+val voidConstPtrType: typ
+
+(** int *
+    @since Frama-C+dev *)
+val intPtrType: typ
+
+(** unsigned int *
+    @since Frama-C+dev *)
+val uintPtrType: typ
+
+(** float
+    @since Frama-C+dev *)
+val floatType: typ
+
+(** double
+    @since Frama-C+dev *)
+val doubleType: typ
+
+(** long double
+    @since Frama-C+dev *)
+val longDoubleType: typ
+
 module Vid: sig val next: unit -> int end
 module Sid: sig val next: unit -> int end
 module Eid: sig val next: unit -> int end
-- 
GitLab