diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 73b20779e7857afb330f45c926d16e683d456a92..0d644c1604bca7cbcd6c9884a42c841783aaff8d 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -81,8 +81,8 @@ let access_ptr_elts ~loc tlv =
let base = Logic_const.term ~loc (TLval tlv) basetype in
let base, basetype =
if Logic_utils.isLogicVoidPointerType basetype then begin
- let typ = Ctype Cil.charPtrType in
- Logic_const.term ~loc (TCast(false, Ctype Cil.charPtrType,base)) typ, typ
+ let typ = Ctype Cil_const.charPtrType in
+ Logic_const.term ~loc (TCast(false, Ctype Cil_const.charPtrType,base)) typ, typ
end else base, basetype
in
let offset = Logic_const.term ~loc (TBinOp (PlusPI, base, range)) basetype in
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index a45a7cc00657e86cadf0ee28cd6300fcfb495dd4..8258d59539142532eb1ef57860b55587a8aca240 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -59,6 +59,7 @@ let valid_sid = false
for the valid_sid label of Cil.mkStmt*. *)
open Cil_types
open Cil_datatype
+open Cil_const
(* Maps the start and end positions of a function declaration or definition
(including its possible contract) to its name. *)
@@ -2847,7 +2848,7 @@ let vla_alloc_fun () =
in
let res_iterm =
Logic_const.new_identified_term
- (Logic_const.tresult Cil.voidPtrType)
+ (Logic_const.tresult voidPtrType)
in
let behavior =
Cil.mk_behavior ~assigns:(Writes [(res_iterm, From [])])
@@ -4037,8 +4038,8 @@ let initStdIntegerSizes () =
in
List.iter add bases
in
- add_special_types "ptr" (Cil.bitsSizeOf Cil.voidPtrType);
- add_special_types "max" (Cil.bitsSizeOf Cil.longLongType)
+ add_special_types "ptr" (Cil.bitsSizeOf voidPtrType);
+ add_special_types "max" (Cil.bitsSizeOf longLongType)
(* [checkTypedefSize name typ] checks if [name] is acceptable as a typedef
name for type [typ]. If [name] is one of the standard integer type names
@@ -6527,8 +6528,8 @@ and doExp local_env
let ok1 =
(* accept literal strings even when expecting non-const char*;
equivalent to GCC's default behavior (-Wno-write-strings) *)
- (Typ.equal (Cil.unrollType texpected) Cil.charPtrType &&
- Typ.equal (Cil.unrollType att) Cil.charConstPtrType) ||
+ (Typ.equal (Cil.unrollType texpected) charPtrType &&
+ Typ.equal (Cil.unrollType att) charConstPtrType) ||
(* all pointers are convertible to void* *)
(Cil.isVoidPtrType texpected && Cil.isPointerType att) ||
(* allow implicit void* -> char* conversion *)
@@ -6555,7 +6556,7 @@ and doExp local_env
Kernel.warning ~wkey:Kernel.wkey_implicit_conv_void_ptr
~current:true ~once:true
"implicit conversion from %a to %a"
- Cil_datatype.Typ.pretty Cil.voidPtrType
+ Cil_datatype.Typ.pretty voidPtrType
Cil_datatype.Typ.pretty texpected;
true
end else
@@ -6958,13 +6959,13 @@ and doExp local_env
piscall := false;
let cst = CReal (infinity, FFloat, Some "INFINITY") in
pres := Cil.new_exp ~loc (Const cst);
- prestype := Cil.floatType;
+ prestype := floatType;
end
| "__fc_nan" -> begin
piscall := false;
let cst = CReal (nan, FFloat, Some "NAN") in
pres := Cil.new_exp ~loc (Const cst);
- prestype := Cil.floatType;
+ prestype := floatType;
end
(* TODO: Only keep the side effects of the 1st or 2nd argument
@@ -7604,8 +7605,8 @@ and doBinOp loc (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) =
arguments with incompatible types to a common type *)
let e1', e2' =
if not (areCompatibleTypes t1p t2p) then
- mkCastT ~oldt:t1 ~newt:Cil.voidPtrType e1,
- mkCastT ~oldt:t2 ~newt:Cil.voidPtrType e2
+ mkCastT ~oldt:t1 ~newt:voidPtrType e1,
+ mkCastT ~oldt:t2 ~newt:voidPtrType e2
else e1, e2
in
intType,
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 25843313a2d3d068e0a35213ba544232fe618400..6de7b381b38de52dfc38484f449301ead113812e 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -603,9 +603,9 @@ let xform_switch_block ?(keepSwitch=false) b =
Const (CInt64 (z,_,_))
when Integer.equal z Integer.zero
->
- new_exp ~loc:ce.eloc (UnOp(LNot,e,intType))
+ new_exp ~loc:ce.eloc (UnOp(LNot,e,Cil_const.intType))
| _ ->
- new_exp ~loc:ce.eloc (BinOp(Eq,e,ce,intType))
+ new_exp ~loc:ce.eloc (BinOp(Eq,e,ce,Cil_const.intType))
in
(* end replacement *)
let then_block =
diff --git a/src/kernel_internals/typing/infer_assigns.ml b/src/kernel_internals/typing/infer_assigns.ml
index d08ee3dc9ba141cae71fd4091e7c7a0244c74978..9f9fbbcdaa374885bb673a507e7c8559df907d44 100644
--- a/src/kernel_internals/typing/infer_assigns.ml
+++ b/src/kernel_internals/typing/infer_assigns.ml
@@ -51,7 +51,7 @@ let from_prototype kf =
let typ = vi.vtype in
if Cil.isVoidPtrType typ then
let const = typeHasAttribute "const" (Cil.typeOf_pointed typ) in
- let typ' = if const then Cil.charConstPtrType else Cil.charPtrType in
+ let typ' = if const then Cil_const.charConstPtrType else Cil_const.charPtrType in
(vi.vghost, Logic_utils.mk_cast ~loc typ' t, typ')
else (vi.vghost, t, typ)
) pointer_args
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index d1cf6d7c2701114593d52822b6c1a2399ab81387..ce13c157a6a7ec1992504a38804cff02c5768284 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -27,11 +27,11 @@ open Cil_types
let add = Logic_env.add_builtin_logic_function_gen
Logic_utils.is_same_builtin_profile
-let float_type = Ctype Cil.floatType
-let double_type = Ctype Cil.doubleType
-let long_double_type = Ctype Cil.longDoubleType
-let object_ptr = Ctype Cil.voidPtrType
-let fun_ptr = Ctype (TPtr(TFun(Cil.voidType,None,false,[]),[]))
+let float_type = Ctype Cil_const.floatType
+let double_type = Ctype Cil_const.doubleType
+let long_double_type = Ctype Cil_const.longDoubleType
+let object_ptr = Ctype Cil_const.voidPtrType
+let fun_ptr = Ctype (TPtr(TFun(Cil_const.voidType,None,false,[]),[]))
let polymorphic_type name = name, Lvar name
diff --git a/src/kernel_internals/typing/unfold_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
index 60d3ede0535983b5f740fc36331e4e246e1e16f6..73a2552df722bd16fe3680a250fca7c8b4d65b31 100644
--- a/src/kernel_internals/typing/unfold_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -692,7 +692,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
in
let h sloop new_stmts = (* To indicate that the unrolling has been done *)
let kind = Ext_terms [
- (Logic_const.term (TConst (LStr "done")) (Ctype Cil.charPtrType)) ;
+ (Logic_const.term (TConst (LStr "done")) (Ctype Cil_const.charPtrType)) ;
Logic_const.tinteger number
] in
let ext = Logic_const.new_acsl_extension "unfold" loc false kind in
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 3d078b7596b099606cde16a60dfd1d0f3aaa557f..9e78618b6bdb06be3c1319a268634522be9125e3 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -147,7 +147,7 @@ let compare v1 v2 = Datatype.Int.compare (id v1) (id v2)
let typeof v =
match v with
- | String (_,_) -> Some charConstPtrType
+ | String (_,_) -> Some Cil_const.charConstPtrType
| CLogic_Var (_, ty, _) -> Some ty
| Null -> None
| Var (v,_) | Allocated(v,_,_) -> Some (unrollType v.vtype)
@@ -156,7 +156,7 @@ let cstring_bitlength s =
let u, l =
match s with
| CSString s ->
- bitsSizeOf charType, (String.length s)
+ bitsSizeOf Cil_const.charType, (String.length s)
| CSWstring s ->
bitsSizeOf theMachine.wcharType, (List.length s)
in
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index d2191817962c8076ca6781ef95236e5953301ba1..affb4f40dcf0ccff9abc19e8111a220971f31725 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -28,7 +28,7 @@ open Cil_types
open Cil
(** [sizeof(char)] in bits *)
-let sizeofchar () = Integer.of_int (bitsSizeOf charType)
+let sizeofchar () = Integer.of_int (bitsSizeOf Cil_const.charType)
(** [sizeof(char* )] in bits *)
let sizeofpointer () = bitsSizeOf theMachine.upointType
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index 70fb5ffe33dc6c75bf847509bb5f23fc632e6936..d26c3b4642d8aacea67573cb54cc0891c2de3ccd 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -416,10 +416,10 @@ module Forwards(T : ForwardsTransfer) = struct
(* This helps when switch is used on boolean expressions. *)
| Const (CInt64 (z,_,_))
when Integer.equal z Integer.zero ->
- new_exp ~loc:exp_sw.eloc (UnOp(LNot,exp_sw,intType))
+ new_exp ~loc:exp_sw.eloc (UnOp(LNot,exp_sw,Cil_const.intType))
| _ ->
Cil.new_exp ~loc:exp_case.eloc
- (BinOp (Eq, exp_sw, exp_case, Cil.intType))
+ (BinOp (Eq, exp_sw, exp_case, Cil_const.intType))
in
let branch_case, branch_not_case = T.doGuard s exp before in
(match branch_case with
diff --git a/src/kernel_services/analysis/dataflows.ml b/src/kernel_services/analysis/dataflows.ml
index ffd8a27cd30f1a8e8080ad5d1af27c18b5b8b4d9..f62a4a9ef587f25cf996366658141eaf3eeb4a48 100644
--- a/src/kernel_services/analysis/dataflows.ml
+++ b/src/kernel_services/analysis/dataflows.ml
@@ -625,9 +625,9 @@ let transfer_switch_from_guard transfer_guard stmt state =
(* This helps when switch is used on boolean expressions. *)
| Const (CInt64 (z,_,_))
when Integer.equal z Integer.zero ->
- Cil.new_exp ~loc:cond.eloc (UnOp(LNot,cond,Cil.intType))
+ Cil.new_exp ~loc:cond.eloc (UnOp(LNot,cond,Cil_const.intType))
| _ -> Cil.new_exp ~loc:exp_case.eloc
- (BinOp (Eq, cond, exp_case, Cil.intType))
+ (BinOp (Eq, cond, exp_case, Cil_const.intType))
in
let (true_state, false_state) =
transfer_guard stmt if_equivalent_cond input_state
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 6e547143aabd00a7dcdcbb399fd44933c218fd89..cd2584047b07cd1617eacc05e95f07a5c4387079 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -365,7 +365,7 @@ let generate_exn_union e exns =
false union_name ~norig:union_name create_union_fields []
in
let create_struct_fields _ =
- let uncaught = (exn_uncaught_name, Cil.intType, None, [], loc) in
+ let uncaught = (exn_uncaught_name, Cil_const.intType, None, [], loc) in
let kind = (exn_kind_name, TEnum (e,[]), None, [], loc) in
let obj =
(exn_obj_name,
@@ -495,7 +495,7 @@ class erase_exn =
method private test_uncaught_flag loc b =
let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+ Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil_const.intType))
method private pred_uncaught_flag loc b =
let e1 =
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index a9534ac43959ab1a161c491ad93a90310a8ed4f9..7187c0295ed8864069b47111d06614c2fa395ed8 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -484,7 +484,7 @@ let build_automaton ~annotations kf =
| Switch (exp1, block, cases, _) ->
(* Guards for edges of the switch *)
let build_guard exp2 kind =
- let enode = BinOp (Eq,exp1,exp2,Cil.intType) in
+ let enode = BinOp (Eq,exp1,exp2,Cil_const.intType) in
Guard (Cil.new_exp ~loc:exp2.eloc enode, kind, stmt)
in
(* First build the automaton for the block *)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 90da2d64d11eef95d0db9b51cdb6963782a62e09..5ad2bc112494c9947014a0e3ba3ccd69f989284c 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -443,9 +443,9 @@ let create_special_float_predicate ~loc e fkind predicate =
let loc = best_loc ~loc e.eloc in
let t = Logic_utils.expr_to_term e in
let typ = match fkind with
- | FFloat -> Cil.floatType
- | FDouble -> Cil.doubleType
- | FLongDouble -> Cil.longDoubleType
+ | FFloat -> Cil_const.floatType
+ | FDouble -> Cil_const.doubleType
+ | FLongDouble -> Cil_const.longDoubleType
in
let t = Logic_utils.mk_cast ~loc typ t in
(* Different signatures, depending on the type of the argument *)
@@ -515,8 +515,8 @@ let create_predicate ?(loc=Location.unknown) alarm =
let t1 = match e1 with
| None -> begin
let typ = match Cil.unrollTypeDeep (Cil.typeOf e2) with
- | TPtr (TFun _, _) -> TPtr (TFun(Cil.voidType, None, false, []), [])
- | _ -> Cil.voidPtrType
+ | TPtr (TFun _, _) -> TPtr (TFun(Cil_const.voidType, None, false, []), [])
+ | _ -> Cil_const.voidPtrType
in
let zero = Cil.lzero () in
Logic_const.term (TCast (false, Ctype typ, zero)) (Ctype typ)
@@ -531,7 +531,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
let loc = best_loc ~loc e1.eloc in
let t1 = Logic_utils.expr_to_term e1 in
let here = Logic_const.here_label in
- let typ = Ctype Cil.charPtrType in
+ let typ = Ctype Cil_const.charPtrType in
let t1 =
Logic_const.term ~loc:(best_loc ~loc e1.eloc) (Tbase_addr(here, t1)) typ
in
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index aa3daab36e81dd122dbacefe4d25bf289e79b2a0..5beace6ba488d30b9c027c7fef661e6d78c03c2a 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -297,21 +297,21 @@ and global =
functions do not take into account the [packed] attributes and pragmas. *)
and typ =
- | TVoid of attributes (** Void type. Also predefined as {!Cil.voidType} *)
+ | TVoid of attributes (** Void type. Also predefined as {!Cil_const.voidType} *)
| TInt of ikind * attributes
(** An integer type. The kind specifies the sign and width. Several useful
- variants are predefined as {!Cil.intType}, {!Cil.uintType},
- {!Cil.longType}, {!Cil.charType}. *)
+ variants are predefined as {!Cil_const.intType}, {!Cil_const.uintType},
+ {!Cil_const.longType}, {!Cil_const.charType}. *)
| TFloat of fkind * attributes
(** A floating-point type. The kind specifies the precision. You can also use
- the predefined constant {!Cil.doubleType}. *)
+ the predefined constant {!Cil_const.doubleType}. *)
| TPtr of typ * attributes
(** Pointer type. Several useful variants are predefined as
- {!Cil.charPtrType}, {!Cil.charConstPtrType} (pointer to a constant
- character), {!Cil.voidPtrType}, {!Cil.intPtrType} *)
+ {!Cil_const.charPtrType}, {!Cil_const.charConstPtrType} (pointer to a constant
+ character), {!Cil_const.voidPtrType}, {!Cil_const.intPtrType} *)
| TArray of typ * exp option * attributes
(** Array type. It indicates the base type and the array length. *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 2e8db5af77cf3f7d3677fe374236abdffe8793ec..1bd22b76984617a2e48455be50c9c3440938e295 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -395,13 +395,13 @@ module Precedence = struct
| AUnOp (uo, _) ->
getParenthLevel
(Cil.dummy_exp
- (UnOp(uo, Cil.zero ~loc:Cil_datatype.Location.unknown, Cil.intType)))
+ (UnOp(uo, Cil.zero ~loc:Cil_datatype.Location.unknown, Cil_const.intType)))
| ABinOp (bo, _, _) ->
getParenthLevel
(Cil.dummy_exp(BinOp(bo,
Cil.zero ~loc:Cil_datatype.Location.unknown,
Cil.zero ~loc:Cil_datatype.Location.unknown,
- Cil.intType)))
+ Cil_const.intType)))
| AAddrOf _ -> addrOfLevel
| ADot _ | AIndex _ | AStar _ -> memOffset_level
| AQuestion _ -> questionLevel
@@ -1550,7 +1550,7 @@ class cil_printer () = object (self)
fprintf fmt "@[<hv>%a@[<v 2>%a (%a) %a@]@]"
(fun fmt -> self#line_directive ~forcefile:false fmt) l
self#pp_keyword "if"
- self#exp (Cil.dummy_exp(UnOp(LNot,be,Cil.intType)))
+ self#exp (Cil.dummy_exp(UnOp(LNot,be,Cil_const.intType)))
(self#unboxed_block Other) e
| If(be,{bstmts=[{skind=Goto(gref,_);labels=[]}]; battrs=[]},e,l)
@@ -1558,7 +1558,7 @@ class cil_printer () = object (self)
fprintf fmt "@[<hv>%a@[<v 2>%a (%a) %a@]@]"
(fun fmt -> self#line_directive ~forcefile:false fmt) l
self#pp_keyword "if"
- self#exp (Cil.dummy_exp(UnOp(LNot,be,Cil.intType)))
+ self#exp (Cil.dummy_exp(UnOp(LNot,be,Cil_const.intType)))
(self#unboxed_block Other) e;
| If(be,t,e,l) ->
@@ -1629,11 +1629,11 @@ class cil_printer () = object (self)
&& Cil_datatype.Stmt.equal !sref next ->
to_skip, e, rest
| [ { skind = Break _ } as s ], [] when self#may_be_skipped s ->
- to_skip, Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
+ to_skip, Cil.dummy_exp (UnOp(LNot, e, Cil_const.intType)), rest
| [ { skind = Goto(sref, _) } as s ], []
when self#may_be_skipped s
&& Cil_datatype.Stmt.equal !sref next ->
- to_skip, Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
+ to_skip, Cil.dummy_exp (UnOp(LNot, e, Cil_const.intType)), rest
| _ -> raise Not_found)
| _ -> raise Not_found
in
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 21ab7361014b2f111f5c0932bc0f28d9ede50b2d..c9bbec26a5ed4b8928e81fd5983d43aec41f70d3 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -300,7 +300,7 @@ let constant_term loc i =
{
term_node = TConst(Integer(i,None));
term_loc = loc;
- term_type = Ctype intType;
+ term_type = Ctype Cil_const.intType;
term_name = [];
}
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d1beb72f82ba5e0cfeea9164ad67f83130363ca6..87ce03d7b6970ee1886c0552d444a3b2541ff0e4 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -55,6 +55,7 @@
open Logic_const
open Cil_datatype
open Cil_types
+open Cil_const
(* ************************************************************************* *)
(* Reporting messages *)
@@ -74,34 +75,6 @@ let abort_context msg =
in
Kernel.abort ~current:true ~append msg
-let voidType = Cil_const.voidType
-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 ucharType = TInt(IUChar, [])
-let scharType = TInt(ISChar, [])
-
-let charPtrType = TPtr(charType,[])
-let ucharPtrType = TPtr(ucharType,[])
-let scharPtrType = TPtr(scharType,[])
-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, [])
-
type theMachine =
{ mutable useLogicalOperators: bool;
mutable theMachine: mach;
@@ -7614,6 +7587,38 @@ let typeDeepDropAllAttributes t =
let vis = new dropAttributes () in
visitCilType vis t
+(******************************************************************************)
+(** Forward Cil_const types *)
+(******************************************************************************)
+
+let voidType = voidType
+let intType = intType
+let uintType = uintType
+let shortType = shortType
+let ushortType = ushortType
+let longType = longType
+let longLongType = longLongType
+let ulongType = ulongType
+let ulongLongType = ulongLongType
+let charType = charType
+let ucharType = ucharType
+let scharType = scharType
+
+let charPtrType = charPtrType
+let ucharPtrType = ucharPtrType
+let scharPtrType = scharPtrType
+let charConstPtrType = charConstPtrType
+
+let voidPtrType = voidPtrType
+let voidConstPtrType = voidConstPtrType
+
+let intPtrType = intPtrType
+let uintPtrType = uintPtrType
+
+let doubleType = doubleType
+let floatType = floatType
+let longDoubleType = longDoubleType
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2391e9e598eac4e89490320a2456f688d6c363e8..0dd5e5931da9ad56dd62b294d0c5e40ef11defca 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -291,39 +291,12 @@ val foldLeftCompound:
(** {2 Values for manipulating types} *)
(* ************************************************************************* *)
-(** void *)
-val voidType: typ
-
(** is the given type "void"? *)
val isVoidType: typ -> bool
(** is the given type "void *"? *)
val isVoidPtrType: typ -> bool
-(** int *)
-val intType: typ
-
-(** unsigned int *)
-val uintType: typ
-
-(** short *)
-val shortType : typ
-
-(** unsigned short *)
-val ushortType : typ
-
-(** long *)
-val longType: typ
-
-(** long long *)
-val longLongType: typ
-
-(** unsigned long *)
-val ulongType: typ
-
-(** unsigned long long *)
-val ulongLongType: typ
-
(** Any signed integer type of size 16 bits.
It is equivalent to the ISO C int16_t type but without using the
corresponding header.
@@ -372,40 +345,6 @@ val uint32_t: unit -> typ
*)
val uint64_t: unit -> typ
-(** char *)
-val charType: typ
-val scharType: typ
-val ucharType: typ
-
-(** char * *)
-val charPtrType: typ
-val scharPtrType: typ
-val ucharPtrType: typ
-
-(** char const * *)
-val charConstPtrType: typ
-
-(** void * *)
-val voidPtrType: typ
-
-(** void const * *)
-val voidConstPtrType: typ
-
-(** int * *)
-val intPtrType: typ
-
-(** unsigned int * *)
-val uintPtrType: typ
-
-(** float *)
-val floatType: typ
-
-(** double *)
-val doubleType: typ
-
-(** long double *)
-val longDoubleType: typ
-
(** @return true if and only if the given type is a signed integer type. *)
val isSignedInteger: typ -> bool
@@ -2580,6 +2519,121 @@ val set_extension_handler:
val init_builtins_ref: (unit -> unit) ref
+(** void
+ @deprecated Frama-C+dev *)
+val voidType: typ
+[@@alert deprecated "Use Cil_const.voidType types instead."]
+
+(** int
+ @deprecated Frama-C+dev *)
+val intType: typ
+[@@alert deprecated "Use Cil_const.intType types instead."]
+
+(** unsigned int
+ @deprecated Frama-C+dev *)
+val uintType: typ
+[@@alert deprecated "Use Cil_const.uintType types instead."]
+
+(** short
+ @deprecated Frama-C+dev *)
+val shortType : typ
+[@@alert deprecated "Use Cil_const.shortType types instead."]
+
+(** unsigned short
+ @deprecated Frama-C+dev *)
+val ushortType : typ
+[@@alert deprecated "Use Cil_const.ushortType types instead."]
+
+(** long
+ @deprecated Frama-C+dev *)
+val longType: typ
+[@@alert deprecated "Use Cil_const.longType types instead."]
+
+(** long long
+ @deprecated Frama-C+dev *)
+val longLongType: typ
+[@@alert deprecated "Use Cil_const.longLongType types instead."]
+
+(** unsigned long
+ @deprecated Frama-C+dev *)
+val ulongType: typ
+[@@alert deprecated "Use Cil_const.ulongType types instead."]
+
+(** unsigned long long
+ @deprecated Frama-C+dev *)
+val ulongLongType: typ
+[@@alert deprecated "Use Cil_const.ulongLongType types instead."]
+
+(** char
+ @deprecated Frama-C+dev *)
+val charType: typ
+[@@alert deprecated "Use Cil_const.charType types instead."]
+
+(** signed char
+ @deprecated Frama-C+dev *)
+val scharType: typ
+[@@alert deprecated "Use Cil_const.scharType types instead."]
+
+(** unsigned char
+ @deprecated Frama-C+dev *)
+val ucharType: typ
+[@@alert deprecated "Use Cil_const.ucharType types instead."]
+
+(** char *
+ @deprecated Frama-C+dev *)
+val charPtrType: typ
+[@@alert deprecated "Use Cil_const.charPtrType types instead."]
+
+(** signed char *
+ @deprecated Frama-C+dev *)
+val scharPtrType: typ
+[@@alert deprecated "Use Cil_const.scharPtrType types instead."]
+
+(** unsigned char *
+ @deprecated Frama-C+dev *)
+val ucharPtrType: typ
+[@@alert deprecated "Use Cil_const.ucharPtrType types instead."]
+
+(** char const *
+ @deprecated Frama-C+dev *)
+val charConstPtrType: typ
+[@@alert deprecated "Use Cil_const.charConstPtrType types instead."]
+
+(** void *
+ @deprecated Frama-C+dev *)
+val voidPtrType: typ
+[@@alert deprecated "Use Cil_const.voidPtrType types instead."]
+
+(** void const *
+ @deprecated Frama-C+dev *)
+val voidConstPtrType: typ
+[@@alert deprecated "Use Cil_const.voidConstPtrType types instead."]
+
+(** int *
+ @deprecated Frama-C+dev *)
+val intPtrType: typ
+[@@alert deprecated "Use Cil_const.intPtrType types instead."]
+
+(** unsigned int *
+ @deprecated Frama-C+dev *)
+val uintPtrType: typ
+[@@alert deprecated "Use Cil_const.uintPtrType types instead."]
+
+(** float
+ @deprecated Frama-C+dev *)
+val floatType: typ
+[@@alert deprecated "Use Cil_const.floatType types instead."]
+
+(** double
+ @deprecated Frama-C+dev *)
+val doubleType: typ
+[@@alert deprecated "Use Cil_const.doubleType types instead."]
+
+(** long double
+ @deprecated Frama-C+dev *)
+val longDoubleType: typ
+[@@alert deprecated "Use Cil_const.longDoubleType types instead."]
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index fe00e5c8871f02bceb86ab7fcfbdf65ca32c0526..76e4ec86b744821c06c724548a61668fe2f7daeb 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -248,11 +248,11 @@ end
matching.
*)
let build_type_table () : (string, typ option) Hashtbl.t =
- let int8_t = Some Cil.scharType in
+ let int8_t = Some Cil_const.scharType in
let int16_t = try Some (Cil.int16_t ()) with Not_found -> None in
let int32_t = try Some (Cil.int32_t ()) with Not_found -> None in
let int64_t = try Some (Cil.int64_t ()) with Not_found -> None in
- let uint8_t = Some Cil.ucharType in
+ let uint8_t = Some Cil_const.ucharType in
let uint16_t = try Some (Cil.uint16_t ()) with Not_found -> None in
let uint32_t = try Some (Cil.uint32_t ()) with Not_found -> None in
let uint64_t = try Some (Cil.uint64_t ()) with Not_found -> None in
@@ -263,37 +263,37 @@ let build_type_table () : (string, typ option) Hashtbl.t =
("__builtin_va_list",
Some (if Cil.theMachine.theMachine.has__builtin_va_list
then TBuiltin_va_list []
- else Cil.voidPtrType));
- ("char *", Some Cil.charPtrType);
- ("char const *", Some Cil.charConstPtrType);
- ("double", Some Cil.doubleType);
- ("double *", Some (TPtr(Cil.doubleType,[])));
- ("float", Some Cil.floatType);
- ("float *", Some (TPtr(Cil.floatType,[])));
- ("int", Some Cil.intType);
- ("int *", Some Cil.intPtrType);
- ("int volatile *", Some (TPtr(typeAddVolatile Cil.intType,[])));
- ("long", Some Cil.longType);
- ("long double", Some Cil.longDoubleType);
- ("long double *", Some (TPtr(Cil.longDoubleType,[])));
- ("long long", Some Cil.longLongType);
- ("long long volatile *", Some (TPtr(typeAddVolatile Cil.longLongType,[])));
- ("short", Some Cil.shortType);
- ("short volatile *", Some (TPtr(typeAddVolatile Cil.shortType,[])));
- ("signed char", Some Cil.scharType);
- ("signed char volatile *", Some (TPtr(typeAddVolatile Cil.scharType,[])));
- ("unsigned char", Some Cil.ucharType);
- ("unsigned char volatile *", Some (TPtr(typeAddVolatile Cil.ucharType,[])));
- ("unsigned int", Some Cil.uintType);
- ("unsigned int volatile *", Some (TPtr(typeAddVolatile Cil.uintType,[])));
- ("unsigned long", Some Cil.ulongType);
- ("unsigned long long", Some Cil.ulongLongType);
- ("unsigned long long volatile *", Some (TPtr(typeAddVolatile Cil.ulongLongType,[])));
- ("unsigned short", Some Cil.ushortType);
- ("unsigned short volatile *", Some (TPtr(typeAddVolatile Cil.ushortType,[])));
- ("void", Some Cil.voidType);
- ("void *", Some Cil.voidPtrType);
- ("void const *", Some Cil.voidConstPtrType);
+ else Cil_const.voidPtrType));
+ ("char *", Some Cil_const.charPtrType);
+ ("char const *", Some Cil_const.charConstPtrType);
+ ("double", Some Cil_const.doubleType);
+ ("double *", Some (TPtr(Cil_const.doubleType,[])));
+ ("float", Some Cil_const.floatType);
+ ("float *", Some (TPtr(Cil_const.floatType,[])));
+ ("int", Some Cil_const.intType);
+ ("int *", Some Cil_const.intPtrType);
+ ("int volatile *", Some (TPtr(typeAddVolatile Cil_const.intType,[])));
+ ("long", Some Cil_const.longType);
+ ("long double", Some Cil_const.longDoubleType);
+ ("long double *", Some (TPtr(Cil_const.longDoubleType,[])));
+ ("long long", Some Cil_const.longLongType);
+ ("long long volatile *", Some (TPtr(typeAddVolatile Cil_const.longLongType,[])));
+ ("short", Some Cil_const.shortType);
+ ("short volatile *", Some (TPtr(typeAddVolatile Cil_const.shortType,[])));
+ ("signed char", Some Cil_const.scharType);
+ ("signed char volatile *", Some (TPtr(typeAddVolatile Cil_const.scharType,[])));
+ ("unsigned char", Some Cil_const.ucharType);
+ ("unsigned char volatile *", Some (TPtr(typeAddVolatile Cil_const.ucharType,[])));
+ ("unsigned int", Some Cil_const.uintType);
+ ("unsigned int volatile *", Some (TPtr(typeAddVolatile Cil_const.uintType,[])));
+ ("unsigned long", Some Cil_const.ulongType);
+ ("unsigned long long", Some Cil_const.ulongLongType);
+ ("unsigned long long volatile *", Some (TPtr(typeAddVolatile Cil_const.ulongLongType,[])));
+ ("unsigned short", Some Cil_const.ushortType);
+ ("unsigned short volatile *", Some (TPtr(typeAddVolatile Cil_const.ushortType,[])));
+ ("void", Some Cil_const.voidType);
+ ("void *", Some Cil_const.voidPtrType);
+ ("void const *", Some Cil_const.voidConstPtrType);
("size_t", Some Cil.theMachine.typeOfSizeOf);
("int8_t", int8_t);
("int16_t", int16_t);
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index bd4d41d64ce8c58ccc6f9b5170858c3aee2e8f27..bed7d0dd72d5aa760337ed34d094d45c3a8864bd 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 5edd0ba2b30af51dbd07a165e677c06ccdcb0745..b43e9f2456f8cb68c489b83d27c9e2bc96d0c962 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
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 6f8cc32aa3047d8977cc1ca2c9c55354e7dd8260..a537c6ab681949f36b0ae11f1cef72af5892d371 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -299,7 +299,7 @@ let treal_zero ?(loc=Cil_datatype.Location.unknown) ?(ltyp=Lreal) () =
term ~loc (TConst (LReal zero)) ltyp
let tstring ?(loc=Cil_datatype.Location.unknown) s =
- (* Cannot refer to Cil.charConstPtrType in this module... *)
+ (* Cannot refer to Cil_const.charConstPtrType in this module... *)
let typ = TPtr(TInt(IChar, [Attr("const", [])]),[]) in
term ~loc (TConst (LStr s)) (Ctype typ)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d21c6718d4c8ab09f8ac8d6880760d92094dce94..bb10728f604db1e0ae4887571518a7400d81b121 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1255,9 +1255,9 @@ struct
let loc = t.term_loc in
let sizeof = term ~loc (TSizeOf (logicCType ptd_type)) Linteger in
let range = trange ~loc (Some (lzero ~loc ()), Some sizeof) in
- let converted_type = set_conversion (Ctype Cil.charPtrType) t.term_type
+ let converted_type = set_conversion (Ctype Cil_const.charPtrType) t.term_type
in
- let cast = term ~loc (TCast(false, Ctype Cil.charPtrType, t)) converted_type in
+ let cast = term ~loc (TCast(false, Ctype Cil_const.charPtrType, t)) converted_type in
term ~loc (TBinOp(PlusPI,cast,range)) (make_set_type converted_type)
in
lift_set convert_one_location t
@@ -1311,7 +1311,7 @@ struct
logic_coerce (make_set_type e.term_type) e
| Linteger, Linteger | Lreal, Lreal -> e
| Linteger, Ctype t when isLogicPointerType newt && isLogicNull e ->
- c_mk_cast ~force e intType t
+ c_mk_cast ~force e Cil_const.intType t
| Linteger, (Ctype newt) | Lreal, (Ctype newt) when explicit ->
Logic_utils.mk_cast ~loc newt e
| Linteger, Ctype t when isIntegralType t ->
@@ -1899,7 +1899,7 @@ struct
else if is_arithmetic_type ot && is_arithmetic_type nt then
let typ = arithmetic_conversion ot nt in ArithConv, typ
else if is_pointer_type ot && is_pointer_type nt then
- let typ = Ctype Cil.charPtrType in
+ let typ = Ctype Cil_const.charPtrType in
PointerConv, (if is_set_type ot then make_set_type typ else typ)
else
let _,_,t = partial_unif ~overloaded:false loc t ot nt env in
@@ -2573,7 +2573,7 @@ struct
let t = Logic_utils.parse_float ~loc s in
t.term_node , t.term_type
| PLconstant (StringConstant s) ->
- TConst (LStr (unescape s)), Ctype Cil.charPtrType
+ TConst (LStr (unescape s)), Ctype Cil_const.charPtrType
| PLconstant (WStringConstant s) ->
TConst (LWStr (wcharlist_of_string s)),
Ctype (TPtr(Cil.theMachine.wcharType,[]))
@@ -2915,7 +2915,7 @@ struct
let t =
lift_set
(fun t -> Logic_const.term (Tbase_addr (l,t))
- (Ctype Cil.charPtrType)) t
+ (Ctype Cil_const.charPtrType)) t
in t.term_node, t.term_type
| PLoffset (l, t) ->
(* offset need a current label to have some semantics *)
@@ -3519,7 +3519,7 @@ struct
in
let var = Cil_const.make_logic_info_local x in
var.l_profile <- args;
- let rt = Option.value typ ~default:(Ctype Cil.voidType) in
+ let rt = Option.value typ ~default:(Ctype Cil_const.voidType) in
var.l_var_info.lv_type <- make_arrow_type args rt;
var.l_type <- typ;
var.l_body <- tdef;
@@ -4042,7 +4042,7 @@ struct
- Polymorphism is not reflected on the lvar level.
- However, such lvar should rarely if at all be seen under a Tvar.
*)
- let rt = Option.value t ~default:(Ctype Cil.voidType) in
+ let rt = Option.value t ~default:(Ctype Cil_const.voidType) in
info.l_var_info.lv_type <- make_arrow_type p rt;
info.l_tparams <- poly;
info.l_profile <- p;
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 072c245325c87aa19ce8e08e782c8407da1fc4d3..7867e987c3d7d102ff7f996afd7225820674e48d 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -91,7 +91,7 @@ let logicCType t =
| Ctype t -> t
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
logicCType (unroll_ltdef ty)
- | Lvar _ -> Cil.intType
+ | Lvar _ -> Cil_const.intType
| _ -> failwith "not a C type"
in plain_or_set logicCType t
@@ -645,11 +645,11 @@ let array_with_range arr size =
let arr = Cil.stripCasts arr in
let typ_arr = typeOf arr in
let no_cast = isAnyCharPtrType typ_arr || isAnyCharArrayType typ_arr in
- let char_ptr = Ctype Cil.charPtrType in
+ let char_ptr = Ctype Cil_const.charPtrType in
let arr = expr_to_term arr in
let arr =
if no_cast then arr
- else mk_cast ~loc Cil.charPtrType arr
+ else mk_cast ~loc Cil_const.charPtrType arr
and range_end =
Logic_const.term ~loc:size.term_loc
(TBinOp (MinusA, size, Cil.lconstant Integer.one))
@@ -2358,9 +2358,9 @@ let complete_types f = Cil.visitCilFile (new complete_types) f
let pointer_comparable ?loc ?(label=Logic_const.here_label) t1 t2 =
let preds = Logic_env.find_all_logic_functions "\\pointer_comparable" in
- let cfct_ptr = TPtr (TFun(Cil.voidType,None,false,[]),[]) in
+ let cfct_ptr = TPtr (TFun(Cil_const.voidType,None,false,[]),[]) in
let fct_ptr = Ctype cfct_ptr in
- let obj_ptr = Ctype Cil.voidPtrType in
+ let obj_ptr = Ctype Cil_const.voidPtrType in
let discriminate t =
let loc = t.term_loc in
match Logic_const.unroll_ltdef t.term_type with
@@ -2373,7 +2373,7 @@ let pointer_comparable ?loc ?(label=Logic_const.here_label) t1 t2 =
(* Value may emit pointer_comparable alarms on anything that
may be compared. We cast scalar to void* to account for
this *)
- mk_cast ~loc Cil.voidPtrType t, obj_ptr
+ mk_cast ~loc Cil_const.voidPtrType t, obj_ptr
| TVoid _ | TFun _ | TNamed _ | TComp _ | TBuiltin_va_list _
| TArray _ (* in logic array do not decay implicitly
into pointers. *)
@@ -2565,7 +2565,7 @@ and bitsLogicOffset ltyp off : Integer.t * Integer.t =
in
match unroll_type ltyp with
| Ctype typ -> loopOff typ Integer.zero Integer.zero off
- | _ -> raise (SizeOfError ("bitsLogicOffset on logic type", Cil.voidPtrType))
+ | _ -> raise (SizeOfError ("bitsLogicOffset on logic type", Cil_const.voidPtrType))
(* Handle \min(\union(args)) or \max(\union(args)), depending on [f] *)
and constFoldMinMax ~machdep f args =
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index ca1caf592ccbd382831c3db020987721ab423d75..089fbeb3457726c97f0120db57107b5e889104ce 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -229,7 +229,7 @@ end = struct
with Not_found ->
let ff_var = Cil.copyVarinfo fct_var name in
if not (Info.result_visible kf finfo) then
- Cil.setReturnTypeVI ff_var Cil.voidType;
+ Cil.setReturnTypeVI ff_var Cil_const.voidType;
(* Notice that we don't have to filter the parameter types here :
* they will be update by [Cil.setFormals] later on. *)
debug "[ff_var] Mem fct var %s:%d@."
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 9a9df3c2ca5e854cadb7226ae09a6620a8ee796b..33ce4bec21defb312688d3f5337a629d9cfcf30e 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -81,7 +81,7 @@ let builtin_show_aorai_state state args =
let () =
Cil_builtins.add_custom_builtin
- (fun () -> (show_aorai_state,Cil.voidType,[],true))
+ (fun () -> (show_aorai_state,Cil_const.voidType,[],true))
let () =
Eva.Builtins.register_builtin show_aorai_state Cacheable builtin_show_aorai_state;
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 9cb3ffa83183486aa64bcfe06c946dc9af72387a..a1043c20630a4d13948528738e6c49948125db6c 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -329,7 +329,7 @@ let crosscond_to_pred cross curr_f curr_status =
function
(* Lazy evaluation of logic operators if the result can be statically
computed *)
- | TOr (c1, c2) -> (*BinOp(LOr,convert c1,convert c2,Cil.intType)*)
+ | TOr (c1, c2) -> (*BinOp(LOr,convert c1,convert c2,Cil_const.intType)*)
begin
let (c1_val,c1_pred) = convert c1 in
match c1_val with
@@ -343,7 +343,7 @@ let crosscond_to_pred cross curr_f curr_status =
| Undefined -> (Undefined,Logic_const.por(c1_pred, c2_pred))
end
- | TAnd (c1, c2) -> (*BinOp(LAnd,convert c1,convert c2,Cil.intType)*)
+ | TAnd (c1, c2) -> (*BinOp(LAnd,convert c1,convert c2,Cil_const.intType)*)
begin
let (c1_val,c1_pred) = convert c1 in
match c1_val with
@@ -357,7 +357,7 @@ let crosscond_to_pred cross curr_f curr_status =
| Undefined -> (Undefined,Logic_const.pand(c1_pred, c2_pred))
end
- | TNot (c1) -> (*UnOp(LNot,convert c1,Cil.intType)*)
+ | TNot (c1) -> (*UnOp(LNot,convert c1,Cil_const.intType)*)
begin
let (c1_val,c1_pred) = convert c1 in
match c1_val with
@@ -415,10 +415,10 @@ let rec term_to_exp t res =
| TAlignOf ty -> new_exp ~loc (AlignOf ty)
| TAlignOfE t -> new_exp ~loc (AlignOfE (term_to_exp t res))
| TUnOp (unop, t) ->
- new_exp ~loc (UnOp (unop, term_to_exp t res, Cil.intType))
+ new_exp ~loc (UnOp (unop, term_to_exp t res, Cil_const.intType))
| TBinOp (binop, t1, t2)->
new_exp ~loc
- (BinOp(binop, term_to_exp t1 res, term_to_exp t2 res, Cil.intType))
+ (BinOp(binop, term_to_exp t1 res, term_to_exp t2 res, Cil_const.intType))
| TCast (false, Ctype ty, {term_node = TConst(LReal lreal)}) when Cil.isFloatingType ty ->
(match Cil.unrollType ty with
| TFloat(fk,_) ->
@@ -482,7 +482,7 @@ let get_bhv_aux_fct kf bhv =
vi.vdefined <- false;
vi.vghost <- true;
let (_,args,varargs,_) = Cil.splitFunctionTypeVI ovi in
- let typ = TFun(Cil.intType, args, varargs,[]) in
+ let typ = TFun(Cil_const.intType, args, varargs,[]) in
Cil.update_var_type vi typ;
Cil.setFormalsDecl vi typ;
vi.vattr <- [];
@@ -505,7 +505,7 @@ let get_bhv_aux_fct kf bhv =
let assumes = Visitor.visitFramacPredicates vis bhv.b_assumes in
let assumes = List.map Logic_const.refresh_predicate assumes in
let assigns = Writes [] in
- let ret_typ = Cil.typeAddGhost Cil.intType in
+ let ret_typ = Cil.typeAddGhost Cil_const.intType in
let post_cond =
[Normal,
Logic_const.(
@@ -549,7 +549,7 @@ let mk_behavior_call generated_kf kf bhv =
Cil.makeLocalVar
(Kernel_function.get_definition generated_kf)
~ghost:true ~referenced:true ~insert:false
- (get_fresh "bhv_aux") Cil.intType
+ (get_fresh "bhv_aux") Cil_const.intType
in
let stmt =
Cil.mkStmtOneInstr
@@ -607,7 +607,7 @@ let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
let stmts1, vars1, defs1, e1 = expnode_convert c1 in
(match Cil.isInteger e1 with
| None ->
- stmts1, vars1, defs1, Cil.new_exp ~loc (UnOp(LNot, e1,Cil.intType))
+ stmts1, vars1, defs1, Cil.new_exp ~loc (UnOp(LNot, e1,Cil_const.intType))
| Some i when Integer.is_zero i ->
[], [], Cil_datatype.Varinfo.Set.empty, Cil.one ~loc
| Some _ -> [], [], Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc)
@@ -768,13 +768,13 @@ let mk_int_term value = Cil.lconstant (Integer.of_int value)
let mk_term_from_vi vi =
Logic_const.term
(TLval((Logic_utils.lval_to_term_lval (Cil.var vi))))
- (Ctype Cil.intType)
+ (Ctype Cil_const.intType)
(** Given an lval term 'host' and an integer value 'off', it returns a lval term host[off]. *)
let mk_offseted_array host off =
Logic_const.term
(TLval(Logic_const.addTermOffsetLval (TIndex(mk_int_term (off),TNoOffset)) host))
- (Ctype Cil.intType)
+ (Ctype Cil_const.intType)
let int2enumstate nums =
let enum = find_enum nums in
@@ -792,7 +792,7 @@ let mk_offseted_array_states_as_enum host off =
(TConst(LEnum enum)) (Ctype (TEnum (enum.eihost,[]))),
TNoOffset))
host))
- (Ctype Cil.intType)
+ (Ctype Cil_const.intType)
(** Returns a lval term associated to the curState generated variable. *)
let host_state_term() = lval_to_term_lval (state_lval())
@@ -935,7 +935,7 @@ class visit_decl_loops_init () =
let name = Data_for_aorai.loopInit ^ "_" ^ (string_of_int stmt.sid) in
let typ =
Cil.typeAddAttributes
- [Attr (Cil.frama_c_ghost_formal,[])] Cil.intType
+ [Attr (Cil.frama_c_ghost_formal,[])] Cil_const.intType
in
let var = Cil.makeLocalVar ~ghost:true f ~scope name typ in
Data_for_aorai.set_varinfo name var
@@ -1988,7 +1988,7 @@ let auto_func_behaviors loc f st state =
(Logic_const.term
(TConst (constant_to_lconstant
(Data_for_aorai.op_status_to_cenum st)))
- (Ctype Cil.intType))))
+ (Ctype Cil_const.intType))))
in
let called_pre_2 =
Logic_const.new_predicate
@@ -2000,7 +2000,7 @@ let auto_func_behaviors loc f st state =
(TConst((constant_to_lconstant
(Data_for_aorai.func_to_cenum
(Kernel_function.get_name f)))))
- (Ctype Cil.intType))))
+ (Ctype Cil_const.intType))))
in
(* let old_pred = Aorai_utils.mk_old_state_pred loc in *)
[(Normal, called_pre); (Normal, called_pre_2)]
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index e1bc4cad120b9dd503d256e9623060f7138e0367..76b9240153b8180b907c3fb8c8d1e8f42dab5a21 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -163,7 +163,7 @@ class visit_adding_code_for_synchronisation =
- what about varargs?
*)
let (rettype,args,varargs,_) = Cil.splitFunctionTypeVI vi_pre in
- Cil.update_var_type vi_pre (TFun(Cil.voidType, args, varargs,[]));
+ Cil.update_var_type vi_pre (TFun(Cil_const.voidType, args, varargs,[]));
vi_pre.vattr <- [];
(* in particular get rid of __no_return if set in vi*)
@@ -176,7 +176,7 @@ class visit_adding_code_for_synchronisation =
let vi_post =
Cil.makeGlobalVar ~ghost:true
(Data_for_aorai.get_fresh (vi.vname ^ "_post_func"))
- (TFun(voidType,Some arg,false,[]))
+ (TFun(Cil_const.voidType,Some arg,false,[]))
in
Kernel_function.Hashtbl.add aux_post_table kf vi_post;
Aux_funcs.(add vi_post (Post kf));
@@ -186,9 +186,9 @@ class visit_adding_code_for_synchronisation =
we have to update the function's formals. Search
for LBLsformals. *)
Cil.setFunctionTypeMakeFormals
- fun_dec_pre (TFun(Cil.voidType, args, varargs,[]));
+ fun_dec_pre (TFun(Cil_const.voidType, args, varargs,[]));
Cil.setFunctionTypeMakeFormals
- fun_dec_post (TFun(voidType,Some arg,false,[]));
+ fun_dec_post (TFun(Cil_const.voidType, Some arg, false,[]));
(* We will now fill the function with the result
of the automaton's analysis. *)
Globals.Functions.replace_by_definition
@@ -845,7 +845,7 @@ class visit_adding_pre_post_from_buch treatloops =
(TConst
(Logic_utils.constant_to_lconstant
(Data_for_aorai.op_status_to_cenum Automaton_ast.Return)))
- (Ctype Cil.intType)))
+ (Ctype Cil_const.intType)))
in
let called_post_2 =
Logic_const.new_predicate
@@ -858,7 +858,7 @@ class visit_adding_pre_post_from_buch treatloops =
(Logic_utils.constant_to_lconstant
(Data_for_aorai.func_to_cenum
(Kernel_function.get_name kf))))
- (Ctype Cil.intType)))
+ (Ctype Cil_const.intType)))
in
let name = "Buchi_property_behavior_function_states" in
let post_cond = [Normal, called_post; Normal, called_post_2] in
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index de04fa6174b3c254124d94a18106b0d740784c5d..faccb2fa50e841c7849a6d455e19dee60aa7d351 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -96,7 +96,7 @@ module State_var =
end)
let get_state_var =
- let add_var state = Cil.makeGlobalVar ~ghost:true state.name Cil.intType in
+ let add_var state = Cil.makeGlobalVar ~ghost:true state.name Cil_const.intType in
State_var.memo add_var
let get_state_logic_var state = Cil.cvar_to_lvar (get_state_var state)
@@ -327,11 +327,11 @@ let memo_multi_state st =
match st.multi_state with
| None ->
let aux =
- Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_aux") Cil.intType
+ Cil.makeGlobalVar ~ghost:true (get_fresh "aorai_aux") Cil_const.intType
in
let laux = Cil.cvar_to_lvar aux in
let set = Cil_const.make_logic_info (get_fresh (st.name ^ "_pebble")) in
- let typ = Logic_const.make_set_type (Ctype Cil.intType) in
+ let typ = Logic_const.make_set_type (Ctype Cil_const.intType) in
set.l_var_info.lv_type <- typ;
set.l_labels <- [FormalLabel "L"];
set.l_type <- Some typ;
@@ -737,7 +737,7 @@ let type_expr metaenv env ?tr ?current e =
| PCst (Logic_ptree.StringConstant s) ->
let t =
Logic_const.term
- (TConst(LStr (Logic_typing.unescape s))) (Ctype Cil.charPtrType)
+ (TConst(LStr (Logic_typing.unescape s))) (Ctype Cil_const.charPtrType)
in
env,t,cond
| PCst (Logic_ptree.WStringConstant s) ->
@@ -1063,7 +1063,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
(* We're using an int: adds an (somewhat artificial) requirements
that the counter itself does not overflow...
*)
- let i = Cil.max_signed_number (Cil.bitsSizeOf Cil.intType) in
+ let i = Cil.max_signed_number (Cil.bitsSizeOf Cil_const.intType) in
let e = Logic_const.tint ~loc i in
TRel(Cil_types.Rlt, counter, e)
| Some e ->
@@ -1146,8 +1146,8 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
(* TODO: makes it an integer *)
let counter =
let ty = if needs_pebble then
- Cil_types.TArray (Cil.intType,None,[])
- else Cil.intType
+ Cil_types.TArray (Cil_const.intType,None,[])
+ else Cil_const.intType
in (* We won't always need a counter *)
lazy (
let
@@ -1167,7 +1167,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
else base
in
let make_counter_term st =
- Logic_const.term (TLval (make_counter st)) (Ctype Cil.intType)
+ Logic_const.term (TLval (make_counter st)) (Ctype Cil_const.intType)
in
Aorai_option.debug ~dkey "Inner start is %s; Inner end is %s"
inner_start.name inner_end.name;
@@ -1359,7 +1359,7 @@ let type_trans auto metaenv env tr =
let count = (* TODO: make it an integer. *)
Cil.makeGlobalVar
~ghost:true
- (get_fresh ("aorai_cnt_" ^ start.name)) Cil.intType
+ (get_fresh ("aorai_cnt_" ^ start.name)) Cil_const.intType
in
add_aux_variable count;
let transitions =
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index e975ededcd8d2f9a8b2ddfbbe969bc58e0d7e442..e7af75554be25389d472cadcd49357cde4bd364b 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -202,7 +202,7 @@ class propagate project fnames ~cast_intro = object(self)
(self#add_cast
~ignore_const_cast:false
~oldt:(Cil.typeOf expr')
- ~newt:Cil.charPtrType
+ ~newt:Cil_const.charPtrType
expr')
rem
in
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index e7118a6f17f93983eb90dbf84e494555d2345717..8ad48d0909a36ec4a3712a8fd27b60e1a5b029e4 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -333,7 +333,7 @@ let check_default_requires kf env contract =
the given contract in the environment *)
let check_other_requires kf env contract =
let get_or_create_assumes_var =
- mk_get_or_create_var kf Cil.intType "assumes_value"
+ mk_get_or_create_var kf Cil_const.intType "assumes_value"
in
let kinstr = Env.get_kinstr env in
let do_behavior env b =
@@ -595,7 +595,7 @@ let check_complete_and_disjoint kf env contract =
(* Create a common variable to hold the number of active behavior for the
current check *)
let get_or_create_var =
- mk_get_or_create_var kf Cil.intType "active_bhvrs"
+ mk_get_or_create_var kf Cil_const.intType "active_bhvrs"
in
(* Check the complete and disjoint clauses *)
let check_bhvrs env ppt_to_translate bhvrs =
@@ -623,7 +623,7 @@ let check_complete_and_disjoint kf env contract =
(** Insert ensures check for the given contract in the environement *)
let check_post_conds kf env contract =
let get_or_create_assumes_var =
- mk_get_or_create_var kf Cil.intType "assumes_value"
+ mk_get_or_create_var kf Cil_const.intType "assumes_value"
in
let kinstr = Env.get_kinstr env in
let do_behavior env b =
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index bd8614fe577ef9f1e3690131fb9003ba91b9e959..15fec0f05c3fc1784094848699d21790dfca44d8 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -328,7 +328,7 @@ module Logic_binding = struct
| None -> match logic_v.lv_type with
| Ctype ty -> ty
| Linteger -> Gmp_types.Z.t ()
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
+ | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil_const.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
Format.asprintf
diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml
index 847b8d042df95fad32a2081d06889eb6a0f7f1d7..c09b19780261538011de6df8a341edbea7bf9e0c 100644
--- a/src/plugins/e-acsl/src/code_generator/global_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/global_observer.ml
@@ -68,7 +68,7 @@ let mk_function name =
let vi =
Cil.makeGlobalVar ~source:true
name
- (TFun(Cil.voidType, Some [], false, []))
+ (TFun(Cil_const.voidType, Some [], false, []))
in
vi.vdefined <- true;
(* There is no contract associated with the function *)
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 4e0bd136867031ba9676dbc2d12c19a8cfa30357..324c524514be8d7c321bd78e21042f47028979b2 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -179,8 +179,8 @@ module Z = struct
let add_cast ~loc ?name env kf ty e =
let fname, new_ty =
- if Cil.isSignedInteger ty then "__gmpz_get_si", Cil.longType
- else "__gmpz_get_ui", Cil.ulongType
+ if Cil.isSignedInteger ty then "__gmpz_get_si", Cil_const.longType
+ else "__gmpz_get_ui", Cil_const.ulongType
in
let _, e, env =
Env.new_var
@@ -216,7 +216,7 @@ module Z = struct
kf
t_opt
~name
- Cil.intType
+ Cil_const.intType
(fun v _ ->
[ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
@@ -224,7 +224,7 @@ module Z = struct
"__gmpz_cmp"
[ e1; e2 ] ])
in
- Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+ Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil_const.intType)), env
end
@@ -355,7 +355,7 @@ module Q = struct
env
kf
None
- Cil.doubleType
+ Cil_const.doubleType
(fun v _ ->
[ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
@@ -379,7 +379,7 @@ module Q = struct
let e, env = get_double e env in
Options.warning
~once:true "R to float: double rounding might cause unsoundness";
- Cil.mkCastT ~force:false ~oldt:Cil.doubleType ~newt:ty e, env
+ Cil.mkCastT ~force:false ~oldt:Cil_const.doubleType ~newt:ty e, env
| TInt(IULongLong, _) ->
(* The biggest C integer type we can extract from GMP is ulong *)
Error.not_yet "R to unsigned long long"
@@ -425,7 +425,7 @@ module Q = struct
kf
t_opt
~name
- Cil.intType
+ Cil_const.intType
(fun v _ ->
[ Smart_stmt.rtl_call ~loc
~result:(Cil.var v)
@@ -433,7 +433,7 @@ module Q = struct
fname
[ e1; e2 ] ])
in
- Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+ Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil_const.intType)), env
end
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index a1b7e0269775fb75157e7df20f7fd852eeccd453..f895c38760dfdaf00642a331454bad5f0232703f 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -815,7 +815,7 @@ let inject_mtracking_handler main =
(* some non-standard arguments. *)
nulls
in
- let ptr_size = Cil.sizeOf ~loc Cil.voidPtrType in
+ let ptr_size = Cil.sizeOf ~loc Cil_const.voidPtrType in
let args = args @ [ ptr_size ] in
let init = Smart_stmt.rtl_call ~loc "memory_init" args in
let clean = Smart_stmt.rtl_call ~loc "memory_clean" [] in
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 9e34bde8fd6d18428c9553044deb93616368fb4a..766c93a81c36301c2e0086117a5ace68f1061eab 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -440,7 +440,7 @@ let update_memory_model ~loc ?result env kf caller args =
| "strncat", _ -> wrong_number_of_arguments name
| "sprintf", buffer_e :: _ :: _ ->
- let result, env = get_result_var ~loc ~name kf Cil.intType env result in
+ let result, env = get_result_var ~loc ~name kf Cil_const.intType env result in
let result_e = Smart_exp.lval ~loc result in
let env = Env.push env in
let result_t = lval_to_term ~loc result in
@@ -465,7 +465,7 @@ let update_memory_model ~loc ?result env kf caller args =
| "sprintf", _ -> wrong_number_of_arguments name
| "snprintf", buffer_e :: size_e :: _ :: _ ->
- let result, env = get_result_var ~loc ~name kf Cil.intType env result in
+ let result, env = get_result_var ~loc ~name kf Cil_const.intType env result in
let result_e = Smart_exp.lval ~loc result in
let env = Env.push env in
let n_vi, n_e, env =
diff --git a/src/plugins/e-acsl/src/code_generator/literal_observer.ml b/src/plugins/e-acsl/src/code_generator/literal_observer.ml
index 37ee1d9fb9ef1be0e474dc3956c605d67973b779..7451af15bb1ca3cb6f28522952a510997957a6c4 100644
--- a/src/plugins/e-acsl/src/code_generator/literal_observer.ml
+++ b/src/plugins/e-acsl/src/code_generator/literal_observer.ml
@@ -37,7 +37,7 @@ let literal loc env kf s =
env
kf
None
- Cil.charPtrType
+ Cil_const.charPtrType
(fun _ _ -> [] (* done in the initializer, see {!vglob_aux} *))
in
Literal_strings.add s vi;
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index 6d9ba8fad8fecd7ef66c43b2807d63045977df59..2b8566382d0c12de0f3f849ef7da6141a6ca2bdd 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -148,7 +148,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
kf
None
~name
- Cil.intType
+ Cil_const.intType
(fun v _ -> [ Smart_stmt.assigns ~loc ~result:(Cil.var v) (res_value ()) ])
in
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 421a71f5527d2043970873c6217dea212325ab9e..b69e57fa494c3b2b54841c421a2c2146b732be65 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -165,7 +165,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
let ret_ty_ptr = TPtr(ret_ty, []) (* call by reference *) in
let vname = vname ^ "_arg" in
let vi = Cil.makeVarinfo false true vname ret_ty_ptr in
- vi, Cil.voidType, vi :: params, (vname, ret_ty_ptr, []) :: params_ty_vi
+ vi, Cil_const.voidType, vi :: params, (vname, ret_ty_ptr, []) :: params_ty_vi
else
Cil.makeVarinfo false false vname ret_ty, ret_ty, params, params_ty_vi
in
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 84de94e2d1ed6012f3ee3a046460cf6822eda94f..24b46848b48a1b4d4b290611a65c74c0a0fdd272 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -206,7 +206,7 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
in
let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
(* ptr *)
- let typ_charptr = Cil.charPtrType in
+ let typ_charptr = Cil_const.charPtrType in
let ptr = Logic_const.term
~loc
(TBinOp(
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index 2c8346eb5d177a93045162d08c977098c157147e..147684a997f0fcf481abcf0099dc03678b4c4fc5 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -122,7 +122,7 @@ let convert kf env loc ~is_forall quantif =
env
kf
None
- intType
+ Cil_const.intType
(fun v _ ->
let lv = var v in
[ Smart_stmt.assigns ~loc ~result:lv init_val ])
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
index dc5a6cc5fa0c30ed1c196784a570ddef3e8babf9..81bde31f6afd33e173178dbb1a8a85837e00d27f 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
@@ -58,7 +58,7 @@ let lnot ~loc e =
with the [LNot] operator. *)
match e.enode with
| UnOp (LNot, e, _) -> e
- | _ -> Cil.new_exp ~loc (UnOp (LNot, e, Cil.intType))
+ | _ -> Cil.new_exp ~loc (UnOp (LNot, e, Cil_const.intType))
end
| Some i when Integer.equal i Integer.zero ->
(* The expression is an integer equal to zero, directly return one. *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index 8575b160506b9bec979a228e83e47ae38e1fa626..670f7316b9e3d9aa1d86a3617fc0efa4341d1e5e 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -319,7 +319,7 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
(* Creating the pointer *)
let ty = match pot with
| PoT_pred _ ->
- Cil.intType
+ Cil_const.intType
| PoT_term t ->
begin match Typing.get_number_ty ~logic_env t with
| C_integer _ | C_float _ | Nan ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index 220e628d43df44456fae548e655c04cd243791dc..584028365c4948abc71e5acf193394a1a487ec34 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -231,7 +231,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
| _ -> assert false
in
let e, adata, env =
- Memory_translate.call_valid ~adata ~loc kf name Cil.intType env t p
+ Memory_translate.call_valid ~adata ~loc kf name Cil_const.intType env t p
in
let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
@@ -268,7 +268,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
~loc
kf
"separated"
- Cil.intType
+ Cil_const.intType
env
tlist
p
@@ -295,7 +295,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
~loc
kf
"initialized"
- Cil.intType
+ Cil_const.intType
env
[ t ]
p
@@ -311,7 +311,7 @@ let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
| Some spec -> of_bool spec.freeable, adata, env
| None ->
let e, adata, env =
- Memory_translate.call ~adata ~loc kf "freeable" Cil.intType env t
+ Memory_translate.call ~adata ~loc kf "freeable" Cil_const.intType env t
in
let adata = Assert.register_pred ~loc env p e adata in
e, adata, env
@@ -356,7 +356,7 @@ let generalized_untyped_to_exp ~adata ?name kf ?rte env p =
predicate, and the typing environment must be kept. *)
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
let e, adata, env = to_exp ~adata ?name kf ~rte env p in
- assert (Typ.equal (Cil.typeOf e) Cil.intType);
+ assert (Typ.equal (Cil.typeOf e) Cil_const.intType);
let env = Env.Logic_scope.reset env in
e, adata, env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 579ccf286834d0a5c029d2bcd5edf30ef266efcb..e0693bd7f5e9036398966778435a77744f0bf4e1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -183,7 +183,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
in
(* cond = 0; *)
let cond_as_varinfo, cond_as_exp, env =
- create_and_init_var ~loc kf Cil.intType "cond" (Cil.zero ~loc) env
+ create_and_init_var ~loc kf Cil_const.intType "cond" (Cil.zero ~loc) env
in
(* lbda = 0; *)
let lbd_as_varinfo, lbd_as_exp, env =
@@ -493,7 +493,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
env
kf
None
- Cil.intType
+ Cil_const.intType
(fun vi _e ->
let result = Cil.var vi in
let fname = "__gmpz_fits_ulong_p" in
@@ -812,7 +812,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
~loc
kf
name
- Cil.voidPtrType
+ Cil_const.voidPtrType
env
t'
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index ee84ecdca58fbdb454c8d9864e413f1fb37aa039..0a97fa252a8d8709c4d23fbd9a784d9d7954810f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -226,7 +226,7 @@ let conditional_to_exp ?(name="if") ~loc kf t_opt e1 (e2, env2) (e3, env3) =
e2, Env.transfer ~from:env2 env
| _ ->
let ty = match t_opt with
- | None (* predicate *) -> Cil.intType
+ | None (* predicate *) -> Cil_const.intType
| Some t -> Typing.get_typ ~logic_env:(Env.Logic_env.get env) t
in
let _, e, env =
diff --git a/src/plugins/e-acsl/src/code_generator/typed_number.ml b/src/plugins/e-acsl/src/code_generator/typed_number.ml
index ab7f78841fdb41c4f30ac5178c5c966b918a957b..bee3fcfabeb5329c3167941e1afa878464036646 100644
--- a/src/plugins/e-acsl/src/code_generator/typed_number.ml
+++ b/src/plugins/e-acsl/src/code_generator/typed_number.ml
@@ -50,7 +50,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
only non integral value that can be seen as an integer, while the
type system infers that it is C-representable (see
tests/runtime/null.i) *)
- Cil.mkCast ~newt:Cil.longType e (* \null *)
+ Cil.mkCast ~newt:Cil_const.longType e (* \null *)
else
e
in
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 9e21ae9804e7c3f3099d1e21a2f81cc230b76b7d..0438cf68c36fa8f29fcf06353cf2dbb5ef26a993 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -566,7 +566,7 @@ let prepare_fundec kf =
let sound_verdict_vi =
lazy
(let name = Functions.RTL.mk_api_name "sound_verdict" in
- let vi = Cil.makeGlobalVar name Cil.intType in
+ let vi = Cil.makeGlobalVar name Cil_const.intType in
vi.vstorage <- Extern;
vi.vreferenced <- true;
vi.vattr <- Cil.addAttribute (Attr ("FC_BUILTIN", [])) vi.vattr;
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 401d42f473131eed05eb435afe9900debdafb8e5..07440aa5df998418c374ab4fd13264237c756b5f 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -523,7 +523,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let expr' = Eva_ast.translate_exp expr in
eval_steps expr'.typ (eval_expr expr') eval_point callstack
| Ppred pred ->
- eval_steps Cil.intType (eval_pred eval_point pred) eval_point callstack
+ eval_steps Cil_const.intType (eval_pred eval_point pred) eval_point callstack
end
let proxy =
diff --git a/src/plugins/eva/ast/eva_ast_builder.ml b/src/plugins/eva/ast/eva_ast_builder.ml
index 6653c1fcee256f03a61917c77a6e2c84d8184de4..b0e7b16dd059be1c1c3bc3fb5c0d4df822f07074 100644
--- a/src/plugins/eva/ast/eva_ast_builder.ml
+++ b/src/plugins/eva/ast/eva_ast_builder.ml
@@ -197,7 +197,7 @@ struct
else
invalid_arg "unsupported construction"
in
- mk_exp (BinOp (op, cast t e1, cast t e2, Cil.intType))
+ mk_exp (BinOp (op, cast t e1, cast t e2, Cil_const.intType))
| _ -> invalid_arg "unsupported construction"
@@ -259,7 +259,7 @@ let rec normalize_condition exp positive =
| _ ->
let op = if positive then Ne else Eq in
let typ = Cil.unrollType exp.typ in
- mk_exp (BinOp (op, zero_typed typ, exp, Cil.intType))
+ mk_exp (BinOp (op, zero_typed typ, exp, Cil_const.intType))
(* --- Hide mk optional paremeters --- *)
diff --git a/src/plugins/eva/ast/eva_ast_typing.ml b/src/plugins/eva/ast/eva_ast_typing.ml
index 365636554cf73e45f9ad1b9ca0f9cd4351865c7f..5ea656ded20229f94b1fee48d9fffbe7b1fd08bb 100644
--- a/src/plugins/eva/ast/eva_ast_typing.ml
+++ b/src/plugins/eva/ast/eva_ast_typing.ml
@@ -25,7 +25,7 @@ open Eva_ast_types
let type_of_const : constant -> typ = function
| CTopInt ik -> Cil_types.TInt (ik, [])
| CInt64 (_, ik, _) -> Cil_types.TInt (ik, [])
- | CChr _ -> Cil.intType
+ | CChr _ -> Cil_const.intType
| CString (String (_, Base.CSString _)) -> Cil.theMachine.stringLiteralType
| CString (String (_, Base.CSWstring _)) -> TPtr (Cil.theMachine.wcharType, [])
| CString (_) -> assert false (* it must be a String base*)
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index ca5f650f358ec224b171f009865347899d6d42d7..270e6a1afa0183936ea65dbe6c003578828a50bf 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -217,7 +217,7 @@ let guess_intended_malloc_type stack sizev constant_size =
| Kstmt {skind = Instr(Local_init(vi, _, _))} -> mk_typed_size vi.vtype
| _ -> raise Exit
with Exit | Cil.SizeOfError _ -> (* Default, use char *)
- { min_bytes = size_min; max_bytes = size_max; elem_typ = Cil.charType;
+ { min_bytes = size_min; max_bytes = size_max; elem_typ = Cil_const.charType;
nb_elems = nb_elems Int.one }
(* Helper function to create the best type for a new base. Builds an
@@ -376,7 +376,7 @@ let string_of_region = function
let create_weakest_base region =
let stack = { (Eva_utils.current_call_stack ()) with stack = [] } in
let type_base =
- TArray (Cil.charType, None, [])
+ TArray (Cil_const.charType, None, [])
in
let var = create_new_var stack "alloc" type_base Weak in
Self.warning ~wkey:wkey_imprecise_alloc ~current:true ~once:true
@@ -492,7 +492,7 @@ let register_malloc ?replace name ?returns_null prefix region =
Builtins.Full { c_values; c_clobbered; c_assigns = None; }
in
let name = "Frama_C_" ^ name in
- let typ () = Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
+ let typ () = Cil_const.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
Builtins.register_builtin ?replace name NoCacheCallers builtin ~typ
let () =
@@ -548,7 +548,7 @@ let () =
let replace = "calloc" in
let typ () =
let sizeof_typ = Cil.theMachine.Cil.typeOfSizeOf in
- Cil.voidPtrType, [ sizeof_typ; sizeof_typ ]
+ Cil_const.voidPtrType, [ sizeof_typ; sizeof_typ ]
in
Builtins.register_builtin ~replace name NoCacheCallers calloc_builtin ~typ
@@ -655,7 +655,7 @@ let frama_c_free state actuals =
let () =
Builtins.register_builtin ~replace:"free" "Frama_C_free" Cacheable
- frama_c_free ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
+ frama_c_free ~typ:(fun () -> (Cil_const.voidType, [Cil_const.voidPtrType]))
(* built-in for [__fc_vla_free] function. By construction, VLA should always
be mapped to a single base. *)
@@ -672,7 +672,7 @@ let frama_c_vla_free state actuals =
let () =
Builtins.register_builtin
~replace:"__fc_vla_free" "Frama_C_vla_free" Cacheable frama_c_vla_free
- ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
+ ~typ:(fun () -> (Cil_const.voidType, [Cil_const.voidPtrType]))
let free_automatic_bases stack state =
(* free automatic bases that were allocated in the current function *)
@@ -839,7 +839,7 @@ let realloc_builtin state args =
let () =
let name = "Frama_C_realloc" in
let replace = "realloc" in
- let typ () = Cil.(voidPtrType, [voidPtrType; theMachine.typeOfSizeOf]) in
+ let typ () = Cil_const.(voidPtrType, [voidPtrType; Cil.theMachine.typeOfSizeOf]) in
Builtins.register_builtin ~replace name NoCacheCallers realloc_builtin ~typ
let reallocarray_builtin state args =
@@ -873,8 +873,8 @@ let () =
let name = "Frama_C_reallocarray" in
let replace = "reallocarray" in
let typ () =
- Cil.(voidPtrType,
- [voidPtrType; theMachine.typeOfSizeOf; theMachine.typeOfSizeOf])
+ Cil_const.voidPtrType,
+ [Cil_const.voidPtrType; Cil.theMachine.typeOfSizeOf; Cil.theMachine.typeOfSizeOf]
in
Builtins.register_builtin
~replace name NoCacheCallers reallocarray_builtin ~typ
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index 798c8bdf5f85f3a334a4122befa57d06e4c1bb9e..8d4cc1bdc56ca48bbdcdf1d95bde7b30ead79932 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -339,7 +339,7 @@ let initialize_var_using_type varinfo state =
Cabs2cil.fresh_global ("WELL_"^name)
in
let hidden_var =
- Eva_utils.create_new_var hidden_var_name Cil.charType
+ Eva_utils.create_new_var hidden_var_name Cil_const.charType
in
hidden_var.vdescr <- Some (name_desc^"_WELL");
let validity = Base.Known (Integer.zero, Bit_utils.max_bit_address ()) in
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index c0c20803688576a3502210fbcd9cae6e26af8d0c..4a047f6d3d24432d777b5acdafee34091b53994c 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -234,7 +234,7 @@ struct
let loc' = Precise_locs.imprecise_location loc in
let add_base base map =
(* Null base doesn't have a type ; use void instead *)
- let typ = Option.value ~default:Cil.voidType (Base.typeof base) in
+ let typ = Option.value ~default:Cil_const.voidType (Base.typeof base) in
Map.add base (`Value (Offset.NoOffset typ)) map
in
Locations.Location_Bits.(fold_bases add_base loc'.loc empty)
diff --git a/src/plugins/eva/domains/multidim/typed_memory.ml b/src/plugins/eva/domains/multidim/typed_memory.ml
index 15e30f18787417fc23779d735b11d983aea6e75b..a819a4b1486f8820abfdbb3bb404785c516aa289 100644
--- a/src/plugins/eva/domains/multidim/typed_memory.ml
+++ b/src/plugins/eva/domains/multidim/typed_memory.ml
@@ -484,7 +484,7 @@ struct
in
match m' with
| `Top -> (* No suitable bound for the partition *)
- let+ v = f ~weak:true Cil.voidType m in v
+ let+ v = f ~weak:true Cil_const.voidType m in v
| `Bottom | `Value _ as m -> m
in aux
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index 72a5125eee1ae75a4ca07ba958248355ed351192..b6113457eabfe8554ded26bce66e34745dc25548 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -958,7 +958,7 @@ let rec stmts_of_cfg cfg current var_map locals return_exp acc =
| None -> Self.not_yet_implemented "Traces_domain: Loop without condition"
| Some(exp,nloop,bloop,n2) ->
let exp = subst_in_exp var_map exp in
- let exp = if bloop then exp else Cil.new_exp ~loc:dummy_loc (UnOp(LNot,exp,Cil.intType)) in
+ let exp = if bloop then exp else Cil.new_exp ~loc:dummy_loc (UnOp(LNot,exp,Cil_const.intType)) in
let body = stmts_of_cfg g nloop var_map locals None [] in
let acc = (List.rev (Cil.mkLoop ~guard:exp ~body ())) @ acc in
stmts_of_cfg cfg n2 var_map locals return_exp acc
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index b8b8e8f1dbf3dbc1754fb58b2fe825196bdb2eed..8c8361ee2f55a6982fdffceb878c2034b4d970d8 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -458,12 +458,12 @@ let inject_no_deps typ cvalue =
(* Integer result with no memory dependencies: constants, sizeof & alignof,
and values of logic variables.*)
-let einteger = inject_no_deps Cil.intType
+let einteger = inject_no_deps Cil_const.intType
(* Note: some reals cannot be exactly represented as floats; in which
case we do not know their under-approximation. *)
-let ereal fval = inject_no_deps Cil.doubleType (Cvalue.V.inject_float fval)
-let efloat fval = inject_no_deps Cil.floatType (Cvalue.V.inject_float fval)
+let ereal fval = inject_no_deps Cil_const.doubleType (Cvalue.V.inject_float fval)
+let efloat fval = inject_no_deps Cil_const.floatType (Cvalue.V.inject_float fval)
(* -------------------------------------------------------------------------- *)
(* --- Utilitary functions on the Cil AST --- *)
@@ -513,12 +513,12 @@ let rec isLogicNonCompositeType t =
let rec infer_type = function
| Ctype t ->
(match t with
- | TInt _ -> Cil.intType
- | TFloat _ -> Cil.doubleType
+ | TInt _ -> Cil_const.intType
+ | TFloat _ -> Cil_const.doubleType
| _ -> t)
- | Lvar _ -> Cil.voidPtrType (* For polymorphic empty sets *)
- | Linteger -> Cil.intType
- | Lreal -> Cil.doubleType
+ | Lvar _ -> Cil_const.voidPtrType (* For polymorphic empty sets *)
+ | Linteger -> Cil_const.intType
+ | Lreal -> Cil_const.doubleType
| Ltype _ | Larrow _ as t ->
if Logic_const.is_plain_type t then
unsupported (Pretty_utils.to_string Cil_datatype.Logic_type.pretty t)
@@ -548,12 +548,12 @@ let infer_binop_res_type op targ =
| PlusA | MinusA | Mult | Div -> targ
| PlusPI | MinusPI ->
assert (Cil.isPointerType targ); targ
- | MinusPP -> Cil.intType
+ | MinusPP -> Cil_const.intType
| Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr ->
(* can only be applied on integral arguments *)
- assert (Cil.isIntegralType targ); Cil.intType
+ assert (Cil.isIntegralType targ); Cil_const.intType
| Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
- Cil.intType (* those operators always return a boolean *)
+ Cil_const.intType (* those operators always return a boolean *)
(* Computes [*tsets], assuming that [tsets] has a pointer type. *)
let deref_tsets tsets = Cil.mkTermMem ~addr:tsets ~off:TNoOffset
@@ -814,7 +814,7 @@ let eval_logic_charlen wrapper env v ldeps =
let eunder = under_from_over eover in
(* the C strlen function has type size_t, but the logic strlen function has
type ℤ (signed) *)
- let etype = Cil.intType in
+ let etype = Cil_const.intType in
{ etype; ldeps; eover; empty = false; eunder }
(* Evaluates the logical predicates strchr/wcschr. *)
@@ -1057,7 +1057,7 @@ let rec eval_term ~alarm_mode env t =
let cvalue = LogicVarEnv.find logic_var env.logic_vars in
if logic_var.lv_type = Linteger
then einteger cvalue
- else inject_no_deps Cil.doubleType cvalue
+ else inject_no_deps Cil_const.doubleType cvalue
| TLval tlval ->
let lval = eval_tlval ~alarm_mode env tlval in
@@ -1095,7 +1095,7 @@ let rec eval_term ~alarm_mode env t =
let typ' = match op with
| Neg -> r.etype
| BNot -> r.etype (* can only be used on an integer type *)
- | LNot -> Cil.intType
+ | LNot -> Cil_const.intType
in
let op = Eva_ast.translate_unop op in
let v = Cvalue_forward.forward_unop r.etype op r.eover in
@@ -1149,7 +1149,7 @@ let rec eval_term ~alarm_mode env t =
in
let empty = Cvalue.V.is_bottom eunder in
{ ldeps = !deps;
- etype = Cil.intType;
+ etype = Cil_const.intType;
eunder; eover; empty; }
| TCast (false, Ctype typ, t) ->
@@ -1180,7 +1180,7 @@ let rec eval_term ~alarm_mode env t =
then V.cast_int_to_float Fval.Real r.eover
else V.cast_float_to_float Fval.Real r.eover
in
- { etype = Cil.longDoubleType; (* hack until logic type *)
+ { etype = Cil_const.longDoubleType; (* hack until logic type *)
ldeps = r.ldeps;
eover; eunder = under_from_over eover;
empty = r.empty }
@@ -1227,7 +1227,7 @@ let rec eval_term ~alarm_mode env t =
empty = true; }
| Tnull ->
- { etype = Cil.voidPtrType;
+ { etype = Cil_const.voidPtrType;
ldeps = empty_logic_deps;
eunder = Cvalue.V.singleton_zero;
eover = Cvalue.V.singleton_zero;
@@ -1243,7 +1243,7 @@ let rec eval_term ~alarm_mode env t =
with Abstract_interp.Error_Top -> Ival.top
in
let eover = Cvalue.V.inject_ival offs in
- { etype = Cil.intType;
+ { etype = Cil_const.intType;
ldeps = r.ldeps;
eover;
eunder = under_from_over eover;
@@ -1256,7 +1256,7 @@ let rec eval_term ~alarm_mode env t =
try Location_Bytes.fold_bases add_base r.eover V.bottom
with Abstract_interp.Error_Top -> r.eover
in
- { etype = Cil.charPtrType;
+ { etype = Cil_const.charPtrType;
ldeps = r.ldeps;
eover;
eunder = under_from_over eover;
@@ -1293,7 +1293,7 @@ let rec eval_term ~alarm_mode env t =
with Abstract_interp.Error_Top -> Ival.top
in
let eover = V.inject_ival bl in
- { etype = Cil.charPtrType;
+ { etype = Cil_const.charPtrType;
ldeps = r.ldeps;
eover;
eunder = under_from_over eover;
@@ -1839,7 +1839,7 @@ and eval_term_as_exact_locs ~alarm_mode env t =
let aux loc () =
let state = env_current_state env in
let v = find_or_alarm ~alarm_mode state loc in
- let v = Cvalue_forward.reinterpret Cil.longDoubleType v in
+ let v = Cvalue_forward.reinterpret Cil_const.longDoubleType v in
let is_finite =
match V.project_float v with
| exception Cvalue.V.Not_based_on_null -> Unknown
diff --git a/src/plugins/eva/utils/unit_tests.ml b/src/plugins/eva/utils/unit_tests.ml
index aa6f0b876a26605114642df08e1499fbe9507472..51f42f0629b84e0e03c5d1485e3d9cc186fe3c30 100644
--- a/src/plugins/eva/utils/unit_tests.ml
+++ b/src/plugins/eva/utils/unit_tests.ml
@@ -40,7 +40,7 @@ module Sign = struct
include Sign_value
let zero = zero
let pos = one
- let neg = inject_int Cil.uintType Integer.minus_one
+ let neg = inject_int Cil_const.uintType Integer.minus_one
let pos_or_zero = join zero pos
let neg_or_zero = join zero neg
let pos_neg = join pos neg
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index 1f60ce6bf972665d5d15c99fb4753d58d81328f9..3ed1ee561683d286ca0e5cfad26656d72977671e 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -50,7 +50,7 @@ let valid_size ?loc typ size =
let heap_status () =
let name = "__fc_heap_status" in
let make () =
- let vi = Cil.makeVarinfo ~ghost:true true false name Cil.intType in
+ let vi = Cil.makeVarinfo ~ghost:true true false name Cil_const.intType in
vi.vstorage <- Extern ;
vi
in
@@ -60,7 +60,7 @@ let heap_status () =
let make_is_allocable () =
let name = "is_allocable" in
{
- l_var_info = Cil_const.make_logic_var_global name (Ctype Cil.voidType) ;
+ l_var_info = Cil_const.make_logic_var_global name (Ctype Cil_const.voidType) ;
l_type = None ;
l_tparams = [];
l_labels = [FormalLabel("L")];
diff --git a/src/plugins/instantiate/stdlib/free.ml b/src/plugins/instantiate/stdlib/free.ml
index 8abebd80974c2ec16ecaef8d2271f80b391d4850..51514a2a75c63749d7ee6b5389fd7f183d5cb93b 100644
--- a/src/plugins/instantiate/stdlib/free.ml
+++ b/src/plugins/instantiate/stdlib/free.ml
@@ -81,7 +81,7 @@ let generate_prototype alloc_t =
let params = [
("ptr", (ptr_of alloc_t), [])
] in
- name, (TFun(Cil.voidType, Some params, false, []))
+ name, (TFun(Cil_const.voidType, Some params, false, []))
let well_typed_call _ret _fct args =
match args with
diff --git a/src/plugins/instantiate/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index 2511b81ebe748bc3243f9dd3031e5e61a3618287..1f0e77f45893a6c77746589af39442c4edb43890 100644
--- a/src/plugins/instantiate/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -38,7 +38,7 @@ let requires loc _ s1 s2 len =
let presult_memcmp ?loc p1 p2 len =
let eq = punfold_all_elems_eq ?loc p1 p2 len in
- let res = prel ?loc (Req, (tresult ?loc Cil.intType), (tinteger ?loc 0)) in
+ let res = prel ?loc (Req, (tresult ?loc Cil_const.intType), (tinteger ?loc 0)) in
piff ?loc (res, eq)
let assigns loc _ s1 s2 len =
@@ -48,7 +48,7 @@ let assigns loc _ s1 s2 len =
in
let s1_range = indirect_range loc s1 len in
let s2_range = indirect_range loc s2 len in
- let result = new_identified_term (tresult Cil.intType) in
+ let result = new_identified_term (tresult Cil_const.intType) in
let res = result, From [s1_range ; s2_range] in
Writes [ res ]
@@ -67,7 +67,7 @@ struct
open Mem_utils
let name = function_name
let prototype () =
- Data Cil.intType,
+ Data Cil_const.intType,
[
("s1" , CPtr,Strip) ;
("s2" , CPtr,Strip) ;
diff --git a/src/plugins/instantiate/tests/api/external_instantiator_registration.ml b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
index aa3c9b5c6a425206aeae937f7d69d88e2f9db39c..4d7caf142942d76167694562ea07fc1039df1946 100644
--- a/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
+++ b/src/plugins/instantiate/tests/api/external_instantiator_registration.ml
@@ -20,7 +20,7 @@ let generate_function_type t =
let params = [
("x", Cil_types.TPtr(t, []), [])
] in
- Cil_types.TFun(Cil.voidType, Some params, false, [])
+ Cil_types.TFun(Cil_const.voidType, Some params, false, [])
let generate_prototype t =
let fun_type = generate_function_type t in
diff --git a/src/plugins/instantiate/tests/plugin/needs_global.ml b/src/plugins/instantiate/tests/plugin/needs_global.ml
index 955b3cbaaac61499c5fad2b497319a6bf8363056..616517ccb7d1bff3ea90a55ac1b32352ab034fcc 100644
--- a/src/plugins/instantiate/tests/plugin/needs_global.ml
+++ b/src/plugins/instantiate/tests/plugin/needs_global.ml
@@ -14,7 +14,7 @@ let retype_args _ = function
let generate_function_type t =
let params = [("x", Cil_types.TPtr(t, []), [])] in
- Cil_types.TFun(Cil.voidType, Some params, false, [])
+ Cil_types.TFun(Cil_const.voidType, Some params, false, [])
let generate_prototype function_name t =
let fun_type = generate_function_type t in
@@ -29,7 +29,7 @@ let generate_spec needed _ _ _ =
let open Logic_const in
let open Instantiate.Global_context in
let make () =
- let vi = Cil.makeVarinfo ~ghost:true true false needed Cil.floatType in
+ let vi = Cil.makeVarinfo ~ghost:true true false needed Cil_const.floatType in
vi.vstorage <- Extern ;
vi
in
diff --git a/src/plugins/region/access.ml b/src/plugins/region/access.ml
index 5baa3096b5d7d24b5bcb9d4dd089fef236646816..50fd5154844a48c30cebfbbdb65f3efbdc6e2246 100644
--- a/src/plugins/region/access.ml
+++ b/src/plugins/region/access.ml
@@ -78,6 +78,6 @@ let typeof = function
| Term(_,lt) ->
match Cil.typeOfTermLval lt with
| Ctype ty -> ty
- | _ -> Cil.voidType
+ | _ -> Cil_const.voidType
module Set = Set.Make(struct type t = acs let compare = compare end)
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 48729ec3b6745770588ece376239f05b9ce9d628..d1dd5198156ed560a08d6e5000dfeee44d623134 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -181,7 +181,7 @@ let new_chunk (m: map) ?(size=0) ?ptr () =
let clayout =
match ptr with
| None -> if size = 0 then Blob else Cell(size,None)
- | Some _ -> Cell(Ranges.gcd size Cil.(bitsSizeOf voidPtrType), ptr)
+ | Some _ -> Cell(Ranges.gcd size (Cil.bitsSizeOf Cil_const.voidPtrType), ptr)
in Ufind.make m.store { empty with clayout }
let new_range (m: map) ?(fields=Fields.empty) ~size ~offset ~length data : node =
diff --git a/src/plugins/variadic/format_parser.ml b/src/plugins/variadic/format_parser.ml
index cfcd2d4e4c2f86d3b6180c4f81bcb3f2a34fae09..900f7c0e9a9c1dc6eb590a06c711c1840975c9cd 100644
--- a/src/plugins/variadic/format_parser.ml
+++ b/src/plugins/variadic/format_parser.ml
@@ -78,7 +78,7 @@ let rec make_flags_unique = function
(* When checking, we don't really care which type are returned but only if
it can be returned *)
let find_typedef : Format_typer.typdef_finder =
- fun _namespace _name -> Cil.voidType
+ fun _namespace _name -> Cil_const.voidType
let check_f_specification spec =
(* Check the correctness of precision and field width fields *)
diff --git a/src/plugins/variadic/format_typer.ml b/src/plugins/variadic/format_typer.ml
index 57ca6fae86a6d2096ad0843cc5bd504e77f5ce13..a0ff2df1610a0d147ce7d840e3a9212ba649bc40 100644
--- a/src/plugins/variadic/format_typer.ml
+++ b/src/plugins/variadic/format_typer.ml
@@ -45,35 +45,35 @@ let ptr typ = TPtr (typ, [])
let type_f_specifier ?find_typedef spec =
match spec.f_conversion_specifier, spec.f_length_modifier with
- | #signed_specifier, None -> Cil.intType
- | #signed_specifier, Some `hh -> Cil.scharType
- | #signed_specifier, Some `h -> Cil.shortType
- | #signed_specifier, Some `l -> Cil.longType
- | #signed_specifier, Some `ll -> Cil.longLongType
+ | #signed_specifier, None -> Cil_const.intType
+ | #signed_specifier, Some `hh -> Cil_const.scharType
+ | #signed_specifier, Some `h -> Cil_const.shortType
+ | #signed_specifier, Some `l -> Cil_const.longType
+ | #signed_specifier, Some `ll -> Cil_const.longLongType
| #signed_specifier, Some `j -> get_typedef ?find_typedef "intmax_t"
| #signed_specifier, Some `z -> get_typedef ?find_typedef "size_t"
| #signed_specifier, Some `t -> get_typedef ?find_typedef "ptrdiff_t"
- | #unsigned_specifier, None -> Cil.uintType
- | #unsigned_specifier, Some `hh -> Cil.ucharType
- | #unsigned_specifier, Some `h -> Cil.ushortType
- | #unsigned_specifier, Some `l -> Cil.ulongType
- | #unsigned_specifier, Some `ll -> Cil.ulongLongType
+ | #unsigned_specifier, None -> Cil_const.uintType
+ | #unsigned_specifier, Some `hh -> Cil_const.ucharType
+ | #unsigned_specifier, Some `h -> Cil_const.ushortType
+ | #unsigned_specifier, Some `l -> Cil_const.ulongType
+ | #unsigned_specifier, Some `ll -> Cil_const.ulongLongType
| #unsigned_specifier, Some `j -> get_typedef ?find_typedef "uintmax_t"
| #unsigned_specifier, Some `z -> get_typedef ?find_typedef "size_t"
| #unsigned_specifier, Some `t -> get_typedef ?find_typedef "ptrdiff_t"
- | #float_specifier, None -> Cil.doubleType
- | #float_specifier, Some `l -> Cil.doubleType
- | #float_specifier, Some `L -> Cil.longDoubleType
- | `c, None -> Cil.intType
+ | #float_specifier, None -> Cil_const.doubleType
+ | #float_specifier, Some `l -> Cil_const.doubleType
+ | #float_specifier, Some `L -> Cil_const.longDoubleType
+ | `c, None -> Cil_const.intType
| `c, Some `l -> get_typedef ?find_typedef "wint_t"
- | `s, None -> Cil.charPtrType
+ | `s, None -> Cil_const.charPtrType
| `s, Some `l -> ptr (get_typedef ?find_typedef "wchar_t")
- | `p, None -> Cil.voidPtrType
- | `n, None -> ptr Cil.intType
- | `n, Some `hh -> ptr Cil.scharType
- | `n, Some `h -> ptr Cil.shortType
- | `n, Some `l -> ptr Cil.longType
- | `n, Some `ll -> ptr Cil.longLongType
+ | `p, None -> Cil_const.voidPtrType
+ | `n, None -> ptr Cil_const.intType
+ | `n, Some `hh -> ptr Cil_const.scharType
+ | `n, Some `h -> ptr Cil_const.shortType
+ | `n, Some `l -> ptr Cil_const.longType
+ | `n, Some `ll -> ptr Cil_const.longLongType
| `n, Some `j -> ptr (get_typedef ?find_typedef "intmax_t")
| `n, Some `z -> ptr (get_typedef ?find_typedef "size_t")
| `n, Some `t -> ptr (get_typedef ?find_typedef "ptrdiff_t")
@@ -81,33 +81,33 @@ let type_f_specifier ?find_typedef spec =
let type_s_specifier ?find_typedef spec =
match spec.s_conversion_specifier, spec.s_length_modifier with
- | #signed_specifier, None -> ptr Cil.intType
- | #signed_specifier, Some `hh -> ptr Cil.scharType
- | #signed_specifier, Some `h -> ptr Cil.shortType
- | #signed_specifier, Some `l -> ptr Cil.longType
- | #signed_specifier, Some `ll -> ptr Cil.longLongType
+ | #signed_specifier, None -> ptr Cil_const.intType
+ | #signed_specifier, Some `hh -> ptr Cil_const.scharType
+ | #signed_specifier, Some `h -> ptr Cil_const.shortType
+ | #signed_specifier, Some `l -> ptr Cil_const.longType
+ | #signed_specifier, Some `ll -> ptr Cil_const.longLongType
| #signed_specifier, Some `j -> ptr (get_typedef ?find_typedef "intmax_t")
| #signed_specifier, Some `z -> ptr (get_typedef ?find_typedef "size_t")
| #signed_specifier, Some `t -> ptr (get_typedef ?find_typedef "ptrdiff_t")
- | #unsigned_specifier, None -> ptr Cil.uintType
- | #unsigned_specifier, Some `hh -> ptr Cil.ucharType
- | #unsigned_specifier, Some `h -> ptr Cil.ushortType
- | #unsigned_specifier, Some `l -> ptr Cil.ulongType
- | #unsigned_specifier, Some `ll -> ptr Cil.ulongLongType
+ | #unsigned_specifier, None -> ptr Cil_const.uintType
+ | #unsigned_specifier, Some `hh -> ptr Cil_const.ucharType
+ | #unsigned_specifier, Some `h -> ptr Cil_const.ushortType
+ | #unsigned_specifier, Some `l -> ptr Cil_const.ulongType
+ | #unsigned_specifier, Some `ll -> ptr Cil_const.ulongLongType
| #unsigned_specifier, Some `j -> ptr (get_typedef ?find_typedef "uintmax_t")
| #unsigned_specifier, Some `z -> ptr (get_typedef ?find_typedef "size_t")
| #unsigned_specifier, Some `t -> ptr (get_typedef ?find_typedef "ptrdiff_t")
- | #float_specifier, None -> ptr (Cil.floatType)
- | #float_specifier, Some `l -> ptr (Cil.doubleType)
- | #float_specifier, Some `L -> ptr (Cil.longDoubleType)
- | (`c | `s | `Brackets _), None -> Cil.charPtrType
+ | #float_specifier, None -> ptr (Cil_const.floatType)
+ | #float_specifier, Some `l -> ptr (Cil_const.doubleType)
+ | #float_specifier, Some `L -> ptr (Cil_const.longDoubleType)
+ | (`c | `s | `Brackets _), None -> Cil_const.charPtrType
| (`c | `s | `Brackets _), Some `l -> ptr (get_typedef ?find_typedef "wchar_t")
- | `p, None -> ptr (Cil.voidPtrType)
- | `n, None -> ptr Cil.intType
- | `n, Some `hh -> ptr Cil.scharType
- | `n, Some `h -> ptr Cil.shortType
- | `n, Some `l -> ptr Cil.longType
- | `n, Some `ll -> ptr Cil.longLongType
+ | `p, None -> ptr (Cil_const.voidPtrType)
+ | `n, None -> ptr Cil_const.intType
+ | `n, Some `hh -> ptr Cil_const.scharType
+ | `n, Some `h -> ptr Cil_const.shortType
+ | `n, Some `l -> ptr Cil_const.longType
+ | `n, Some `ll -> ptr Cil_const.longLongType
| `n, Some `j -> ptr (get_typedef ?find_typedef "intmax_t")
| `n, Some `z -> ptr (get_typedef ?find_typedef "size_t")
| `n, Some `t -> ptr (get_typedef ?find_typedef "ptrdiff_t")
@@ -121,9 +121,9 @@ let type_f_format ?find_typedef format =
| Char _ -> ()
| Specification s ->
if s.f_field_width = Some `FWStar then
- r := (Cil.intType, `ArgIn) :: !r;
+ r := (Cil_const.intType, `ArgIn) :: !r;
if s.f_precision = Some PStar then
- r := (Cil.intType, `ArgIn) :: !r;
+ r := (Cil_const.intType, `ArgIn) :: !r;
let dir = match s.f_conversion_specifier with
| `s -> `ArgInArray s.f_precision
| `n -> `ArgOut
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index 1042673127e20e1d5b0a1b23decfeb49bad7498d..7d085bed140972cd30c12cd1ade9d7996251e625 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -160,7 +160,7 @@ let translate_call ~builder callee pars =
(* Build an array to store addresses *)
let init = match vis with (* C standard forbids arrays of size 0 *)
- | [] -> [Build.(of_init (Cil.makeZeroInit ~loc Cil.voidPtrType))]
+ | [] -> [Build.(of_init (Cil.makeZeroInit ~loc Cil_const.voidPtrType))]
| l -> List.map Build.addr l
in
let ty = Build.(array (ptr void) ~size:(List.length init)) in
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 7f264061d967929e24742ee0bce6e75e10974da8..4a3c76171f47c4673c4a21496848a3c04aa18ac6 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -314,7 +314,7 @@ struct
match f.status with
| Some x -> x
| None ->
- let x = fresh_cvar ~basename:"status" Cil.intType in
+ let x = fresh_cvar ~basename:"status" Cil_const.intType in
f.status <- Some x ; x
let trigger tg =
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 7004c6c5ce66f479476dc23cedc2a85b2687e5c6..27e8c434e5cb7e535bd2abc11ecceb4b4b5cc515 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -191,7 +191,7 @@ struct
let obj = function
| I i -> C_int i
| F f -> C_float f
- | P -> C_pointer Cil.voidPtrType
+ | P -> C_pointer Cil_const.voidPtrType
| C c -> C_comp c
let tau = function
| I _ -> Lang.t_int
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 509027bee08370a83313bd1f8fd248a2adcda53d..bb8cc495995fecae948008cc20475addb2e2257e 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -161,7 +161,7 @@ let zone_to_term ?(to_char=false) loc zone =
let len = Logic_utils.expr_to_term (Cil.sizeOf ~loc pointed) in
let last = term (TBinOp(MinusA, len, tinteger ~loc 1)) len.term_type in
let range = trange ~loc (Some (tinteger ~loc 0), Some last) in
- let ptr = Logic_utils.mk_cast ~loc Cil.charPtrType ptr in
+ let ptr = Logic_utils.mk_cast ~loc Cil_const.charPtrType ptr in
term ~loc (TBinOp(PlusPI, ptr, range)) ptr.term_type
in
match zone with
@@ -175,20 +175,20 @@ let zone_to_term ?(to_char=false) loc zone =
in
let ptr =
if not to_char then ptr
- else Logic_utils.mk_cast ~loc Cil.charPtrType ptr
+ else Logic_utils.mk_cast ~loc Cil_const.charPtrType ptr
in
let range = trange ~loc (None, None) in
term ~loc (TBinOp(PlusPI, ptr, range)) ptr.term_type
let region_to_term loc = function
- | [] -> term ~loc Tempty_set (Ctype Cil.charPtrType)
+ | [] -> term ~loc Tempty_set (Ctype Cil_const.charPtrType)
| [z] -> zone_to_term loc z
| x :: tl as l ->
let fst = type_of_zone x in
let tl = List.map type_of_zone tl in
let to_char = not (List.for_all (Cil_datatype.Typ.equal fst) tl) in
let set_typ =
- make_set_type (Ctype (if to_char then Cil.charPtrType else fst))
+ make_set_type (Ctype (if to_char then Cil_const.charPtrType else fst))
in
term ~loc (Tunion (List.map (zone_to_term ~to_char loc) l)) set_typ
@@ -247,7 +247,7 @@ let welltyped zones =
in
let compare_zone a b =
Cil_datatype.Typ.compare (type_of_zone a) (type_of_zone b) in
- partition_by_type Cil.voidType [] (List.sort compare_zone zones)
+ partition_by_type Cil_const.voidType [] (List.sort compare_zone zones)
let global_zones partition =
List.map (fun z -> [z]) partition.globals
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
index d268d14ff6ed86c8c252cab81a59d2809a2e783a..68f734e9e57610f5ef3a2d72bd045af15a22cf3b 100644
--- a/src/plugins/wp/RegionAccess.ml
+++ b/src/plugins/wp/RegionAccess.ml
@@ -57,7 +57,7 @@ let pp_value fmt = function
let cc_string map exp =
let cst = Pretty_utils.to_string Cil_datatype.Exp.pretty exp in
let addrof = Region.of_cstring map ~eid:exp.eid ~cst in
- { addrof ; typeOfPointed = Cil.charType ; shift=false }
+ { addrof ; typeOfPointed = Cil_const.charType ; shift=false }
(* -------------------------------------------------------------------------- *)
(* --- Reading Values --- *)
@@ -261,7 +261,7 @@ and cc_term_value (map:map) (term:term) =
| Tnull ->
Addr_of {
addrof = Region.of_null map ;
- typeOfPointed = Cil.charType ;
+ typeOfPointed = Cil_const.charType ;
shift = false ;
}
@@ -286,7 +286,7 @@ and cc_term_value (map:map) (term:term) =
cc_term_offset_read map ofs ;
Pure
- | Tbase_addr(_at,t) -> cast Cil.voidPtrType @@ cc_term_value map t
+ | Tbase_addr(_at,t) -> cast Cil_const.voidPtrType @@ cc_term_value map t
| Tblock_length(_at,t) | Toffset(_at,t) -> cc_term map t ; Pure
| Tif(c,a,b) ->
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index e4d429a90a41a7f5b422c3c90ea8471bdf455bb4..302d9ffa31c89ecdee07d769882e1fa0f37991b6 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -285,8 +285,8 @@ let rec object_of typ =
match typ with
| TInt(i,_) -> C_int (c_int i)
| TFloat(f,_) -> C_float (c_float f)
- | TPtr(typ,_) -> C_pointer (if Cil.isVoidType typ then Cil.charType else typ)
- | TFun _ -> C_pointer Cil.voidType
+ | TPtr(typ,_) -> C_pointer (if Cil.isVoidType typ then Cil_const.charType else typ)
+ | TFun _ -> C_pointer Cil_const.voidType
| TEnum ({ekind=i},_) -> C_int (c_int i)
| TComp (comp,_) -> C_comp comp
| TArray (typ_elt,e_opt,_) ->
diff --git a/tests/cil/Change_formals.ml b/tests/cil/Change_formals.ml
index fe51268692588c39cf096254d141c2672d8710fa..4fd188fb4532146efb1cc83e0b0dbdaffbbcba33 100644
--- a/tests/cil/Change_formals.ml
+++ b/tests/cil/Change_formals.ml
@@ -18,7 +18,7 @@ class transform prj = object(_self)
(fun () ->
Options.feedback "current prj = %a"
Project.pretty (Project.current ());
- ignore(Cil.makeFormalVar fundec "ok" Cil.intType))
+ ignore(Cil.makeFormalVar fundec "ok" Cil_const.intType))
();
let g = GFun({ fundec with svar = fundec.svar }, loc) in
[g]
@@ -37,7 +37,7 @@ class transform prj = object(_self)
| TFun(typ, args, varity, attr) ->
let vtype = Cil.argsToList args in
let new_fun_typ = TFun(
- typ, Some (vtype @ [ "ok", Cil.intType, [] ]),
+ typ, Some (vtype @ [ "ok", Cil_const.intType, [] ]),
varity, attr)
in
Cil.update_var_type vi new_fun_typ;
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
index 311f8c041013ab8b03207ae341bcaf946a947fac..bdfe516697d9fe5eff21d00d8223bd7eada7db21 100644
--- a/tests/cil/insert_formal.ml
+++ b/tests/cil/insert_formal.ml
@@ -1,12 +1,12 @@
open Cil_types
let update_func f =
- let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil.intType in
- let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil.intType in
- let insert_circ_g f = Cil.makeFormalVar f ~ghost:true ~where:"^" "x" Cil.intType in
- let insert_dollar_g f = Cil.makeFormalVar f ~ghost:true ~where:"$" "x" Cil.intType in
- let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil.intType in
- let insert_a_g f = Cil.makeFormalVar f ~ghost:true ~where:"a" "x" Cil.intType in
+ let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil_const.intType in
+ let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil_const.intType in
+ let insert_circ_g f = Cil.makeFormalVar f ~ghost:true ~where:"^" "x" Cil_const.intType in
+ let insert_dollar_g f = Cil.makeFormalVar f ~ghost:true ~where:"$" "x" Cil_const.intType in
+ let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil_const.intType in
+ let insert_a_g f = Cil.makeFormalVar f ~ghost:true ~where:"a" "x" Cil_const.intType in
let circ_list = [
"void_circumflex" ;
"a_circumflex" ;
diff --git a/tests/cil/mkBinOp.ml b/tests/cil/mkBinOp.ml
index e07f3b60ab1e197091d8b5bce1575e49dc8d8bd7..99c86db95e009090ae8bc4aefca8fa8d66bd7b2f 100644
--- a/tests/cil/mkBinOp.ml
+++ b/tests/cil/mkBinOp.ml
@@ -5,19 +5,19 @@ let loc = Location.unknown
let null () =
let e = zero ~loc in
- mkCast ~force:true ~newt:voidPtrType e
+ mkCast ~force:true ~newt:Cil_const.voidPtrType e
let inull () =
let e = zero ~loc in
- mkCast ~force:true ~newt:intPtrType e
+ mkCast ~force:true ~newt:Cil_const.intPtrType e
let cone () =
let e = one ~loc in
- mkCast ~force:true ~newt:charPtrType e
+ mkCast ~force:true ~newt:Cil_const.charPtrType e
let ione () =
let e = one ~loc in
- mkCast ~force:true ~newt:intPtrType e
+ mkCast ~force:true ~newt:Cil_const.intPtrType e
let test =
let n = ref 0 in
diff --git a/tests/crowbar/test_ghost_cfg.ml b/tests/crowbar/test_ghost_cfg.ml
index 7cc14d11f1955493274dfab77be7c66717271fcc..6bd5615d31e587aed7082892479abf57e648a3c9 100644
--- a/tests/crowbar/test_ghost_cfg.ml
+++ b/tests/crowbar/test_ghost_cfg.ml
@@ -47,11 +47,11 @@ let add_stack stmt env = { env with stmt_stack = stmt :: env.stmt_stack }
let () = Project.set_current (Project.create "simple project")
-let x = Cil.makeGlobalVar "x" Cil.intType
+let x = Cil.makeGlobalVar "x" Cil_const.intType
-let y = Cil.makeGlobalVar ~ghost:true "y" Cil.intType
+let y = Cil.makeGlobalVar ~ghost:true "y" Cil_const.intType
-let f = Cil.makeGlobalVar "f" (Cil_types.TFun (Cil.voidType,Some [],false,[]))
+let f = Cil.makeGlobalVar "f" (Cil_types.TFun (Cil_const.voidType,Some [],false,[]))
let return = Cil.mkStmt (Return (None, Loc.unknown))
@@ -102,7 +102,7 @@ let gen_inst ghost env =
(Set
(Cil.var v,
Cil.new_exp ~loc
- (BinOp (PlusA,Cil.evar v,Cil.one ~loc,Cil.intType)),loc))
+ (BinOp (PlusA,Cil.evar v,Cil.one ~loc,Cil_const.intType)),loc))
in
let env = add_stack stmt env in
env, stmt
@@ -119,7 +119,7 @@ let gen_return ghost env =
let ghost = ghost_status env ghost in
let stmt = Cil.mkStmt ~ghost (Return (None, Loc.unknown)) in
let e =
- Cil.new_exp ~loc (BinOp(Lt,Cil.evar x,Cil.integer ~loc 53,Cil.intType))
+ Cil.new_exp ~loc (BinOp(Lt,Cil.evar x,Cil.integer ~loc 53,Cil_const.intType))
in
let stmt = Cil.mkStmt ~ghost (If (e,Cil.mkBlock [stmt],Cil.mkBlock[],loc)) in
let env = if ghost then { env with should_fail = true } else env in
@@ -224,7 +224,7 @@ let gen_if ghost ghost_else stmt_then stmt_else env =
let loc = Loc.unknown in
let stmt = Cil.mkEmptyStmt ~ghost ~loc () in
let e =
- Cil.new_exp ~loc (BinOp (Ne,Cil.evar ~loc x,Cil.zero ~loc,Cil.intType))
+ Cil.new_exp ~loc (BinOp (Ne,Cil.evar ~loc x,Cil.zero ~loc,Cil_const.intType))
in
let if_env = add_stack stmt env in
let if_env = { if_env with in_ghost = ghost } in
@@ -419,7 +419,7 @@ let gen_loop ghost stmts env =
in
let (new_env, stmts) = stmts new_env in
let e =
- Cil.new_exp ~loc (BinOp (Ge,Cil.evar x,Cil.integer ~loc 42,Cil.intType))
+ Cil.new_exp ~loc (BinOp (Ge,Cil.evar x,Cil.integer ~loc 42,Cil_const.intType))
in
let cond_stmt =
Cil.mkStmt ~ghost
diff --git a/tests/misc/add_assigns.ml b/tests/misc/add_assigns.ml
index fdcf2b0c5d8a47c3135d2f6f528f6acb034706b5..2498999413346f60d62d34c271bf50081227096a 100644
--- a/tests/misc/add_assigns.ml
+++ b/tests/misc/add_assigns.ml
@@ -16,7 +16,7 @@ let main () =
Logic_const.(
new_identified_term
(term (TLval (TMem (tvar (Cil.cvar_to_lvar y)), TNoOffset))
- (Ctype Cil.intType)))
+ (Ctype Cil_const.intType)))
in
let assigns = Writes [mem, FromAny] in
let bhv = Cil.mk_behavior ~assigns () in
diff --git a/tests/misc/exception.ml b/tests/misc/exception.ml
index b99e9b1122b729d9ef074b263684e8aff7cd06b0..4c9ed2c6c31713e0cfac3ab0090e13c5c5815f94 100644
--- a/tests/misc/exception.ml
+++ b/tests/misc/exception.ml
@@ -49,20 +49,20 @@ let add_int_exn f =
let c = Cil.evar (List.hd f.sformals) in
let loc = Cil_datatype.Location.unknown in
let test =
- Cil.new_exp ~loc (BinOp (Lt,c,Cil.kinteger ~loc IInt 50,Cil.intType))
+ Cil.new_exp ~loc (BinOp (Lt,c,Cil.kinteger ~loc IInt 50,Cil_const.intType))
in
- add_throw_test f Cil.intType test (SingleInit (Cil.zero ~loc))
+ add_throw_test f Cil_const.intType test (SingleInit (Cil.zero ~loc))
let add_int_ptr_exn glob f =
let c = Cil.evar (List.hd f.sformals) in
let loc = Cil_datatype.Location.unknown in
let test =
- Cil.new_exp ~loc (BinOp (Gt,c,Cil.kinteger ~loc IInt 150, Cil.intType))
+ Cil.new_exp ~loc (BinOp (Gt,c,Cil.kinteger ~loc IInt 150, Cil_const.intType))
in
let init =
SingleInit (Cil.new_exp ~loc (AddrOf(Var glob,NoOffset)))
in
- add_throw_test f Cil.intPtrType test init
+ add_throw_test f Cil_const.intPtrType test init
let add_catch my_exn my_exn2 f =
let exn_type = TComp(my_exn, []) in
@@ -73,10 +73,10 @@ let add_catch my_exn my_exn2 f =
let loc = Cil_datatype.Location.unknown in
let real_locals = f.sbody.blocals in
let v1 = Cil.makeLocalVar f "exn" exn_type in
- let v2 = Cil.makeLocalVar f "y" Cil.intType in
+ let v2 = Cil.makeLocalVar f "y" Cil_const.intType in
let v3 = Cil.makeLocalVar f "exn_aux" exn_type in
let v4 = Cil.makeLocalVar f "exn2" exn_type2 in
- let v5 = Cil.makeLocalVar f "not_thrown" Cil.doubleType in
+ let v5 = Cil.makeLocalVar f "not_thrown" Cil_const.doubleType in
f.sbody.blocals <- real_locals;
let id_block =
Cil.mkBlock [Cil.mkStmtOneInstr (Set (Cil.var v1, Cil.evar ~loc v3, loc))]
diff --git a/tests/misc/visitor_creates_func_bts_1349.ml b/tests/misc/visitor_creates_func_bts_1349.ml
index ad70dd8cd73f3a148b9de2fadff5578d38f1a1de..5feddc7e54b240b5ed5dc32ea53dfc72216c1752 100644
--- a/tests/misc/visitor_creates_func_bts_1349.ml
+++ b/tests/misc/visitor_creates_func_bts_1349.ml
@@ -5,8 +5,8 @@ class test prj = object(self)
method private create_f () =
let f = Cil.emptyFunction "f" in
f.svar.vdefined <- true;
- let x = Cil.makeFormalVar f "x" Cil.intType in
- Cil.setReturnType f Cil.intType;
+ let x = Cil.makeFormalVar f "x" Cil_const.intType in
+ Cil.setReturnType f Cil_const.intType;
Queue.add (fun () -> Cil.setFormals f [x])
self#get_filling_actions;
f.sbody <-
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index c009bfc5e6ac4bf85dff53210803700de65c5375..1d4b490aa5c804c430b772773f96bda8a523de7c 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -58,12 +58,12 @@ let main () =
def.sallstmts
in
let s3 = Kernel_function.find_return kf in
- let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
- let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
- let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
- let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
- let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
- let r = Cil.makeLocalVar def ~insert:true "r" Cil.intPtrType in
+ let j = Cil.makeLocalVar def ~insert:true "j" Cil_const.intType in
+ let k = Cil.makeLocalVar def ~insert:true "k" Cil_const.intType in
+ let l = Cil.makeLocalVar def ~insert:true "l" Cil_const.intType in
+ let p = Cil.makeLocalVar def ~insert:true "p" Cil_const.intPtrType in
+ let q = Cil.makeLocalVar def ~insert:true "q" Cil_const.intPtrType in
+ let r = Cil.makeLocalVar def ~insert:true "r" Cil_const.intPtrType in
add_assigns e1 kf s j;
add_assigns e2 kf s k;
add_assigns e1 kf s l;