diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 42759eb6818675841b52e6064d661aa118df76ad..b7fde909eecf878fdf5a70830f6c9b2d81c46bbd 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -520,8 +520,7 @@ let make_annot ~one_line default lexbuf s =
*)
| Logic_ptree.Acode_annot (loc,a) -> CODE_ANNOT (a, loc)
| Logic_ptree.Aloop_annot (loc,a) -> LOOP_ANNOT (a,loc)
- | Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc)
- | Logic_ptree.Acustom(loc,id, a) -> CUSTOM_ANNOT(a, id, loc))
+ | Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc))
| None -> (* error occured and annotation is discarded. Find a normal token. *)
default lexbuf
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index fd98d6e4a86d7443a68f668ad7b5a71766080dc5..527a0d838609bec7d70a16033672b19907eef7a9 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -316,7 +316,6 @@ let in_ghost_block ?(battrs=[]) l =
%token <Logic_ptree.code_annot * Cabs.cabsloc> CODE_ANNOT
%token <Logic_ptree.code_annot list * Cabs.cabsloc> LOOP_ANNOT
%token <string * Cabs.cabsloc> ATTRIBUTE_ANNOT
-%token <Logic_ptree.custom_tree * string * Cabs.cabsloc> CUSTOM_ANNOT
%token <string> IDENT
%token <int64 list * Cabs.cabsloc> CST_CHAR
@@ -469,7 +468,6 @@ ghost_globals:
/*** Global Definition ***/
global:
| DECL { GLOBANNOT $1 }
-| CUSTOM_ANNOT { let (x,y,z) = $1 in CUSTOM(x,y,z) }
| declaration { $1 }
| function_def { $1 }
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 4029bbd19f1f7059500d1d8b00739c26b8e86032..044cf5f450289b8bdbb8b30ca552da416397558c 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -132,8 +132,6 @@
"continues", (fun _ -> CONTINUES), false;
"contract", (fun _ -> CONTRACT), false;
(* ACSL extension for external spec file *)
- "custom", (fun _ -> CUSTOM), false;
- (* ACSL extension for custom annotations *)
"decreases", (fun _ -> DECREASES), false;
"disjoint", (fun _ -> DISJOINT), false;
"double", (fun _ -> DOUBLE), true;
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 6f0ad747309650ac647c2d41ccb6c6a4f3eecbaa..f9b208480cd931080b16966f3dd58ddfd18495db 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -297,7 +297,6 @@
%token TYPEOF BSTYPE
%token WITH CONST
%token INITIALIZED DANGLING
-%token CUSTOM
%token LSQUAREPIPE RSQUAREPIPE
%token IN
%token PI
@@ -1328,19 +1327,6 @@ annot:
| annotation EOF { $1 }
| is_acsl_spec any EOF { Aspec }
| decl_list EOF { Adecl ($1) }
-| CUSTOM any_identifier COLON custom_tree EOF { Acustom(loc (),$2, $4) }
-;
-
-custom_tree:
-| TYPE type_spec { CustomType $2 }
-| LOGIC lexpr { CustomLexpr $2 }
-| any_identifier_non_logic { CustomOther($1,[]) }
-| any_identifier_non_logic LPAR custom_tree_list RPAR { CustomOther($1,$3) }
-;
-
-custom_tree_list:
-| custom_tree { [$1] }
-| custom_tree COMMA custom_tree_list { $1::$3 }
;
annotation:
@@ -1881,10 +1867,6 @@ any_identifier:
| keyword { $1 }
;
-any_identifier_non_logic:
-| identifier_or_typename { $1 }
-| non_logic_keyword { $1 }
-
identifier_or_typename: /* allowed as C field names */
| TYPENAME { $1 } /* followed by the same list than 'identifier' */
| IDENTIFIER { $1 }
@@ -2025,7 +2007,6 @@ non_logic_keyword:
| is_acsl_spec { $1 }
| is_acsl_decl_or_code_annot { $1 }
| is_acsl_other { $1 }
-| CUSTOM { "custom" (* token that cannot be used in C fields *) }
;
bs_keyword:
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index a37810a3b3f5299ae30d6ad60ae49e071f30f5d6..55c5b0fb1f41fe6fed44bfce1bd690bf9cc2f982 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -103,7 +103,7 @@ let access_elts ~loc ?size tlv =
let extract_mem_term ~loc acc tlv =
match Logic_utils.unroll_type (Cil.typeOfTermLval tlv) with
| Ctype (TPtr _ ) -> access_ptr_elts ~loc tlv :: acc
- | Ctype (TArray(_,e,_,_)) ->
+ | Ctype (TArray(_,e,_)) ->
let size = Option.bind e (Cil.constFoldToInt ~machdep:true) in
access_elts ~loc ?size tlv :: acc
| _ -> acc
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 71b94389cf2b0354d5c17e656c770e146b56d750..655659d92b813eec05a9f09a624742febffaf6be 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -624,7 +624,7 @@ let process_pragmas_pack_align_field_attributes fi fattrs cattr =
else begin
let sizeof_type =
match Cil.unrollType fi.ftype with
- | TArray (_, None, _, _) ->
+ | TArray (_, None, _) ->
(* flexible array member: use size of pointer *)
Cil.bitsSizeOf theMachine.upointType
| _ ->
@@ -678,7 +678,7 @@ let gotoTargetNextAddr: int ref = ref 0
* is *)
let isTransparentUnion (t: typ) : fieldinfo option =
match unrollType t with
- | TComp (comp, _, _) when not comp.cstruct ->
+ | TComp (comp, _) when not comp.cstruct ->
(* Turn transparent unions into the type of their first field *)
if typeHasAttribute "transparent_union" t then begin
match comp.cfields with
@@ -1175,10 +1175,10 @@ let constFoldTypeVisitor = object
inherit nopCilVisitor
method! vtype t: typ visitAction =
match t with
- | TArray(bt, Some len, _, a) ->
+ | TArray(bt, Some len, a) ->
let len' = constFold true len in
ChangeDoChildrenPost (
- TArray(bt, Some len', empty_size_cache (), a),
+ TArray(bt, Some len', a),
(fun x -> x)
)
| _ -> DoChildren
@@ -1313,7 +1313,7 @@ let findCompType ghost kind name attr =
let self, isnew = createCompInfo iss name ~norig:name in
if isnew then
cabsPushGlobal (GCompTagDecl (self, CurrentLoc.get ()));
- TComp (self, empty_size_cache (), attr)
+ TComp (self, attr)
in
try
let old, _ = lookupTypeNoError ghost kind name in (* already defined *)
@@ -2591,17 +2591,17 @@ let rec cabsTypeCombineAttributes what a0 t =
| TEnum (enum, a) -> TEnum (enum, add a)
| TPtr (t, a) -> TPtr (t, add a)
| TFun (t, args, isva, a) -> TFun(t, args, isva, add a)
- | TComp (comp, s, a) -> TComp (comp, s, add a)
+ | TComp (comp, a) -> TComp (comp, add a)
| TNamed (t, a) -> TNamed (t, add a)
| TBuiltin_va_list a -> TBuiltin_va_list (add a)
- | TArray (t, l, s, a) ->
+ | TArray (t, l, a) ->
let att_elt, att_typ = Cil.splitArrayAttributes a0 in
- TArray (cabsArrayPushAttributes what att_elt t, l, s,
+ TArray (cabsArrayPushAttributes what att_elt t, l,
combineAttributes what att_typ a)
end
and cabsArrayPushAttributes what al = function
- | TArray (bt, l, s, a) ->
- TArray (cabsArrayPushAttributes what al bt, l, s, a)
+ | TArray (bt, l, a) ->
+ TArray (cabsArrayPushAttributes what al bt, l, a)
| t -> cabsTypeCombineAttributes what al t
let cabsTypeAddAttributes =
@@ -2661,17 +2661,17 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
| TInt(IInt, olda), TEnum (ei, a) -> TEnum(ei, combineAttributes what olda a)
- | TComp (oldci, _, olda) , TComp (ci, _, a) ->
+ | TComp (oldci, olda) , TComp (ci, a) ->
if oldci.cstruct <> ci.cstruct then
raise (Cannot_combine "different struct/union types");
let comb_a = combineAttributes what olda a in
if oldci.cname = ci.cname then
- TComp (oldci, empty_size_cache (), comb_a)
+ TComp (oldci, comb_a)
else
raise (Cannot_combine (Format.sprintf "%ss with different tags"
(if oldci.cstruct then "struct" else "union")))
- | TArray (oldbt, oldsz, _, olda), TArray (bt, sz, _, a) ->
+ | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
let newbt = combineTypes CombineOther oldbt bt in
let newsz =
match oldsz, sz with
@@ -2701,7 +2701,7 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
raise (Cannot_combine "different array lengths")
in
- TArray (newbt, newsz, empty_size_cache (), combineAttributes what olda a)
+ TArray (newbt, newsz, combineAttributes what olda a)
| TPtr (oldbt, olda), TPtr (bt, a) ->
TPtr (combineTypes CombineOther oldbt bt, combineAttributes what olda a)
@@ -2847,7 +2847,7 @@ let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
included_qualifiers ~context a1 a2)
args1 args2
| TPtr (t1', a1), TPtr (t2', a2)
- | TArray (t1', _, _, a1), TArray (t2', _, _, a2) ->
+ | TArray (t1', _, a1), TArray (t2', _, a2) ->
(included_qualifiers ~context a1 a2) &&
let context = qualifier_context_ptr context in
have_compatible_qualifiers_deep ~context t1' t2'
@@ -2991,10 +2991,10 @@ let rec castTo ?context ?(fromsource=false)
| TArray _, TPtr _ -> result
- | TArray(t1,_,_,_), TArray(t2,None,_,_)
+ | TArray(t1,_,_), TArray(t2,None,_)
when Cil_datatype.Typ.equal t1 t2 -> (nt', e)
- | TPtr _, TArray(_,_,_,_) ->
+ | TPtr _, TArray(_,_,_) ->
error "Cast over a non-scalar type %a" Cil_printer.pp_typ nt';
| TEnum _, TInt _ -> result
@@ -3032,7 +3032,7 @@ let rec castTo ?context ?(fromsource=false)
(* Even casts between structs are allowed when we are only
* modifying some attributes *)
- | TComp (comp1, _, _), TComp (comp2, _, _) when comp1.ckey = comp2.ckey ->
+ | TComp (comp1, _), TComp (comp2, _) when comp1.ckey = comp2.ckey ->
result
(** If we try to pass a transparent union value to a function
@@ -3040,7 +3040,7 @@ let rec castTo ?context ?(fromsource=false)
* have been changed to the type of the first argument, and we'll
* see a cast from a union to the type of the first argument. Turn
* that into a field access *)
- | TComp(_, _, _), _ -> begin
+ | TComp(_, _), _ -> begin
match isTransparentUnion ot with
| None ->
Kernel.fatal ~current:true "castTo %a -> %a"
@@ -3299,7 +3299,7 @@ let conditionalConversion (t2: typ) (t3: typ) : typ =
match unrollType t2, unrollType t3 with
| (TInt _ | TEnum _ | TFloat _), (TInt _ | TEnum _ | TFloat _) ->
arithmeticConversion t2 t3
- | TComp (comp2,_,_), TComp (comp3,_,_)
+ | TComp (comp2,_), TComp (comp3,_)
when comp2.ckey = comp3.ckey -> t2
| TPtr(_, _), TPtr(TVoid _, _) -> t2
| TPtr(TVoid _, _), TPtr(_, _) -> t3
@@ -3433,7 +3433,7 @@ let rec collectInitializer
Kernel.debug ~dkey "Initializing object of type %a to %a"
Cil_printer.pp_typ thistype Cil_printer.pp_exp e;
SingleInit e, thistype, Cil_datatype.Lval.Set.union r reads
- | TArray (bt, leno, _, at), CompoundPre (pMaxIdx, pArray) ->
+ | TArray (bt, leno, at), CompoundPre (pMaxIdx, pArray) ->
Kernel.debug ~dkey
"Initialization of an array object of type %a with index max %d"
Cil_printer.pp_typ thistype !pMaxIdx;
@@ -3503,7 +3503,7 @@ let rec collectInitializer
let newtype =
(* detect flexible array member initialization *)
match thistype, Cil.unrollType parenttype with
- | TArray (_, None, _, _), TComp (comp, _, _)
+ | TArray (_, None, _), TComp (comp, _)
when comp.cstruct && len > 0 ->
(* incomplete array type inside a struct => FAM, with
a non-empty initializer (len > 0)
@@ -3514,13 +3514,13 @@ let rec collectInitializer
Kernel.error ~once:true ~current:true
"static initialization of flexible array members is an \
unsupported GNU extension";
- TArray (typ, None, empty_size_cache (), at)
+ TArray (typ, None, at)
| _ -> (* not a flexible array member *)
if len = 0 && not (Cil.gccMode() || Cil.msvcMode ()) then
Kernel.error ~once:true ~current:true
"arrays of size zero not supported in C99@ \
(only allowed as compiler extensions)";
- TArray (typ, Some (integer ~loc len), empty_size_cache (), at)
+ TArray (typ, Some (integer ~loc len), at)
in
CompoundInit (newtype, (* collect [] endAt*)init),
(* If the sizes of the initializers have not been used anywhere,
@@ -3529,7 +3529,7 @@ let rec collectInitializer
(if len_used then newtype else thistype),
reads
- | TComp (comp, _, _) as t,
+ | TComp (comp, _) as t,
CompoundPre (pMaxIdx, pArray) when comp.cstruct ->
Kernel.debug ~dkey
"Initialization of an object of type %a with at least %d components"
@@ -3558,7 +3558,7 @@ let rec collectInitializer
collect 0 reads (Option.value ~default:[] comp.cfields) in
CompoundInit (thistype, init), thistype, reads
- | TComp (comp, _, _), CompoundPre (pMaxIdx, pArray) when not comp.cstruct ->
+ | TComp (comp, _), CompoundPre (pMaxIdx, pArray) when not comp.cstruct ->
Kernel.debug ~dkey
"Initialization of an object of type %a with at least %d components"
Cil_printer.pp_typ thistype !pMaxIdx;
@@ -3677,7 +3677,7 @@ and normalSubobj (so: subobj) : unit =
advanceSubobj so
end else begin
let fst = List.hd nextflds
- and baseTyp = TComp (compinfo,empty_size_cache (), []) in
+ and baseTyp = TComp (compinfo, []) in
so.soTyp <- Cil.typeOffset baseTyp fst;
so.soOff <- addOffset fst parOff
end
@@ -3742,7 +3742,7 @@ let fieldsToInit
else if prefix anonCompFieldName f.fname && not found
&& f.forig_name <> f.fname then
match unrollType f.ftype with
- | TComp (comp, _, _) ->
+ | TComp (comp, _) ->
add_comp offset comp acc (* go deeper inside *)
| _ ->
abort_context "unnamed field type is not a struct/union"
@@ -3779,7 +3779,7 @@ let find_field_offset cond (fidlist: fieldinfo list) : offset =
Field(fid, NoOffset)
| fid :: rest when prefix anonCompFieldName fid.fname -> begin
match unrollType fid.ftype with
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
(try
let off = search (Option.value ~default:[] ci.cfields) in
Field(fid,off)
@@ -4326,9 +4326,9 @@ let default_argument_promotion idx exp =
| TInt(k,_) -> TInt(k,[])
| TFloat(FFloat,_) -> doubleType
| TFloat(k,_) -> TFloat(k,[])
- | TPtr(t,_) | TArray(t,_,_,_) -> TPtr(t,[])
+ | TPtr(t,_) | TArray(t,_,_) -> TPtr(t,[])
| (TFun _) as t -> TPtr(t,[])
- | TComp(ci,_,_) -> TComp(ci,{ scache = Not_Computed },[])
+ | TComp(ci,_) -> TComp(ci,[])
| TEnum(ei,_) -> TEnum(ei,[])
| TBuiltin_va_list _ ->
abort_context "implicit prototype cannot have variadic arguments"
@@ -4462,7 +4462,7 @@ let checkTypedefSize name typ =
let rec checkRestrictQualifierDeep t =
if typeHasQualifier "restrict" t then
match unrollType t with
- | TArray (bt, _, _, _) | TPtr (bt, _) ->
+ | TArray (bt, _, _) | TPtr (bt, _) ->
if isFunctionType bt then
Kernel.error ~once:true ~current:true
"function pointer type does not allow 'restrict' qualifier"
@@ -4472,7 +4472,7 @@ let rec checkRestrictQualifierDeep t =
"invalid usage of 'restrict' qualifier"
else
match unrollType t with
- | TArray (bt, _, _, _) | TPtr (bt, _) ->
+ | TArray (bt, _, _) | TPtr (bt, _) ->
checkRestrictQualifierDeep bt
| TFun (rt, args, _, _) ->
checkRestrictQualifierDeep rt;
@@ -4826,7 +4826,6 @@ let rec doSpecList ghost (suggestedAnonName: string)
| TPtr(bt, _) -> (* This is the type of array elements *)
TArray(bt,
Some (new_exp ~loc:e'.eloc (SizeOfStr s)),
- empty_size_cache (),
[])
| _ -> abort_context "The typeOf a string is not a pointer type"
end
@@ -5214,7 +5213,7 @@ and doType (ghost:bool) isFuncArg
Kernel.error ~once:true ~current:true
"static specifier inside array argument is allowed only in \
function argument";
- doDeclType (TArray(bt, lo, empty_size_cache (), al')) acc d
+ doDeclType (TArray(bt, lo, al')) acc d
| Cabs.PROTO (d, args, ghost_args, isva) ->
(* Start a scope for the parameter names *)
@@ -5325,13 +5324,13 @@ and doType (ghost:bool) isFuncArg
| [] -> ()
| a :: args' ->
(match unrollType a.vtype with
- | TArray(bt,lo,_,attr) ->
+ | TArray(bt,lo,attr) ->
(* Note that for multi-dimensional arrays we strip off only
the first TArray and leave bt alone. *)
let real_type = turnArrayIntoPointer bt lo attr in
Cil.update_var_type a real_type
| TFun _ -> Cil.update_var_type a (TPtr(a.vtype, []))
- | TComp (_, _,_) -> begin
+ | TComp (_,_) -> begin
match isTransparentUnion a.vtype with
| None -> ()
| Some fstfield ->
@@ -5359,7 +5358,7 @@ and doType (ghost:bool) isFuncArg
in
let tres =
match unrollType bt with
- | TArray(t,lo,_,attr) -> turnArrayIntoPointer t lo attr
+ | TArray(t,lo,attr) -> turnArrayIntoPointer t lo attr
| _ -> bt
in
(* Drop qualifiers on the return type. They are meaningless (qualifiers
@@ -5477,7 +5476,7 @@ and makeCompType ghost (isstruct: bool)
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
then begin
match Cil.unrollType ftype with
- | TArray(_,None,_,_) when last_group && last_field ->
+ | TArray(_,None,_) when last_group && last_field ->
begin
(* possible flexible array member; check if struct contains at least
one other field *)
@@ -5558,8 +5557,8 @@ and makeCompType ghost (isstruct: bool)
in
let rec is_circular t =
match Cil.unrollType t with
- | TArray(bt,_,_,_) -> is_circular bt
- | TComp (comp',_,_) ->
+ | TArray(bt,_,_) -> is_circular bt
+ | TComp (comp',_) ->
if Cil_datatype.Compinfo.equal comp comp' then begin
(* abort and not error, as this circularity could lead
to infinite recursion... *)
@@ -5585,7 +5584,6 @@ and makeCompType ghost (isstruct: bool)
faddrof = false;
fsize_in_bits = None;
foffset_in_bits = None;
- fpadding_in_bits = None;
} :: flds
in
fold addFieldInfo flds nl
@@ -5622,7 +5620,7 @@ and makeCompType ghost (isstruct: bool)
Kernel.error ~source
"field %s occurs multiple times in aggregate %a. \
Previous occurrence is at line %d."
- f.fname Cil_printer.pp_typ (TComp(comp,{scache = Not_Computed},[]))
+ f.fname Cil_printer.pp_typ (TComp(comp,[]))
(fst oldf.floc).Filepath.pos_lnum
with Not_found ->
(* Do not add unnamed bitfields: they can share the empty name. *)
@@ -5664,7 +5662,7 @@ and makeCompType ghost (isstruct: bool)
(* ignore (E.log "makeComp: %s: %a\n" comp.cname d_attrlist a); *)
let a = Cil.addAttributes comp.cattr a in
comp.cattr <- process_pragmas_pack_align_comp_attributes comp a;
- let res = TComp (comp,empty_size_cache (), []) in
+ let res = TComp (comp, []) in
(* Create a typedef for this one *)
cabsPushGlobal (GCompTag (comp, CurrentLoc.get ()));
@@ -5685,7 +5683,7 @@ and preprocessCast ghost (specs: Cabs.specifier)
* will resolve this later, when we'll convert casts to unions. *)
let ie' =
match unrollType typ, ie with
- | TComp (c, _, _), Cabs.SINGLE_INIT _ when not c.cstruct ->
+ | TComp (c, _), Cabs.SINGLE_INIT _ when not c.cstruct ->
Cabs.COMPOUND_INIT [(Cabs.INFIELD_INIT ("___matching_field",
Cabs.NEXT_INIT),
ie)]
@@ -5695,7 +5693,7 @@ and preprocessCast ghost (specs: Cabs.specifier)
* when we do again the specs we get the right name *)
let specs1 =
match typ with
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
List.map
(function
Cabs.SpecType (Cabs.Tstruct ("", _, [])) ->
@@ -5763,7 +5761,7 @@ and doExp local_env
let processArrayFun e t =
let loc = e.eloc in
match e.enode, unrollType t with
- | (Lval(lv) | CastE(_, {enode = Lval lv})), TArray(tbase, _, _, a) ->
+ | (Lval(lv) | CastE(_, {enode = Lval lv})), TArray(tbase, _, a) ->
mkStartOfAndMark loc lv, TPtr(tbase, a)
| Lval(Mem _, _), TFun _ -> e, t (* Do not turn pointer function types *)
| (Lval(lv) | CastE(_, {enode = Lval lv})), TFun _ ->
@@ -5972,7 +5970,7 @@ and doExp local_env
in
let field_offset =
match unrollType t' with
- | TComp (comp, _, _) -> findField str comp
+ | TComp (comp, _) -> findField str comp
| _ ->
Kernel.fatal ~current:true "expecting a struct with field %s" str
in
@@ -5994,11 +5992,11 @@ and doExp local_env
in
let pointedt = match unrollType t' with
| TPtr(t1, _) -> t1
- | TArray(t1,_,_,_) -> t1
+ | TArray(t1,_,_) -> t1
| _ -> Kernel.fatal ~current:true "expecting a pointer to a struct"
in
let field_offset = match unrollType pointedt with
- | TComp (comp, _, _) -> findField str comp
+ | TComp (comp, _) -> findField str comp
| x ->
Kernel.fatal ~current:true
"expecting a struct with field %s. Found %a. t1 is %a"
@@ -8159,7 +8157,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* If we are at an array of characters and the initializer is a
* string literal (optionally enclosed in braces) then explode the
* string into characters *)
- | TArray(bt, leno, _, _ ),
+ | TArray(bt, leno, _ ),
(Cabs.NEXT_INIT,
(Cabs.SINGLE_INIT({ expr_node = Cabs.CONSTANT (Cabs.CONST_STRING s)} as e)|
Cabs.COMPOUND_INIT
@@ -8221,7 +8219,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* [weimer] Wed Jan 30 15:38:05 PST 2002
* Despite what the compiler says, this match case is used and it is
* important. *)
- | TArray(bt, leno, _, _),
+ | TArray(bt, leno, _),
(Cabs.NEXT_INIT,
(Cabs.SINGLE_INIT({expr_node = Cabs.CONSTANT (Cabs.CONST_WSTRING s)} as e)|
Cabs.COMPOUND_INIT
@@ -8294,7 +8292,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
doInit local_env asconst add_implicit_ensures preinit' so acc' restil
(* If we are at an array and we see a single initializer then it must
* be one for the first element *)
- | TArray(bt, leno, _, _), (Cabs.NEXT_INIT, Cabs.SINGLE_INIT _oneinit) :: _restil ->
+ | TArray(bt, leno, _), (Cabs.NEXT_INIT, Cabs.SINGLE_INIT _oneinit) :: _restil ->
(* Grab the length if there is one *)
let leno = integerArrayLength leno in
so.stack <- InArray(so.soOff, bt, leno, ref 0) :: so.stack;
@@ -8302,20 +8300,20 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Start over with the fields *)
doInit local_env asconst add_implicit_ensures preinit so acc allinitl
(* An incomplete structure with any initializer is an error. *)
- | TComp (comp, _, _), _ :: restil when comp.cfields = None ->
+ | TComp (comp, _), _ :: restil when comp.cfields = None ->
Kernel.error ~current:true ~once:true
"variable `%s' has initializer but incomplete type" so.host.vname;
doInit local_env asconst add_implicit_ensures preinit so acc restil
(* If we are at a composite and we see a single initializer of the same
* type as the composite then grab it all. If the type is not the same
* then we must go on and try to initialize the fields *)
- | TComp (comp, _, _), (Cabs.NEXT_INIT, Cabs.SINGLE_INIT oneinit) :: restil ->
+ | TComp (comp, _), (Cabs.NEXT_INIT, Cabs.SINGLE_INIT oneinit) :: restil ->
let r,se, oneinit', t' =
doExp (no_paren_local_env local_env) asconst oneinit (AExp None)
in
let r = Cil_datatype.Lval.Set.of_list r in
if (match unrollType t' with
- | TComp (comp', _, _) when comp'.ckey = comp.ckey -> true
+ | TComp (comp', _) when comp'.ckey = comp.ckey -> true
| _ -> false)
then begin
(* Initialize the whole struct *)
@@ -8351,7 +8349,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
doInit local_env asconst add_implicit_ensures preinit' so se restil
(* An array with a compound initializer. The initializer is for the
* array elements *)
- | TArray (bt, leno, _, _), (Cabs.NEXT_INIT, Cabs.COMPOUND_INIT initl) :: restil ->
+ | TArray (bt, leno, _), (Cabs.NEXT_INIT, Cabs.COMPOUND_INIT initl) :: restil ->
(* Create a separate object for the array *)
let so' = makeSubobj so.host so.soTyp so.soOff in
(* Go inside the array *)
@@ -8382,7 +8380,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
doInit local_env asconst add_implicit_ensures preinit' so acc' restil
(* We have a designator that tells us to select the matching union field.
* This is to support a GCC extension *)
- | TComp(ci, _, _) as targ,
+ | TComp(ci, _) as targ,
[(Cabs.NEXT_INIT,
Cabs.COMPOUND_INIT
[(Cabs.INFIELD_INIT ("___matching_field", Cabs.NEXT_INIT),
@@ -8415,7 +8413,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
[Cabs.INFIELD_INIT (fi.fname, Cabs.NEXT_INIT), Cabs.SINGLE_INIT oneinit]
(* A structure with a composite initializer. We initialize the fields*)
- | TComp (comp, _, _), (Cabs.NEXT_INIT, Cabs.COMPOUND_INIT initl) :: restil ->
+ | TComp (comp, _), (Cabs.NEXT_INIT, Cabs.COMPOUND_INIT initl) :: restil ->
(* Create a separate subobject iterator *)
let so' = makeSubobj so.host so.soTyp so.soOff in
(* Go inside the comp *)
@@ -8479,7 +8477,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
| Cabs.NEXT_INIT -> acc
| Cabs.INFIELD_INIT (fn, whatnext) -> begin
match unrollType so.soTyp with
- | TComp (comp, _, _) ->
+ | TComp (comp, _) ->
let toinit = fieldsToInit comp (Some fn) in
so.stack <- InComp(so.soOff, comp, toinit) :: so.stack;
normalSubobj so;
@@ -8491,7 +8489,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
| Cabs.ATINDEX_INIT(idx, whatnext) -> begin
match unrollType so.soTyp with
- | TArray (bt, leno, _, _) ->
+ | TArray (bt, leno, _) ->
let ilen = integerArrayLength leno in
let nextidx', doidx =
let (r,doidx, idxe', _) =
@@ -9057,15 +9055,15 @@ and createLocal ghost ((_, sto, _, _) as specs)
(* Fix the length *)
(match vi.vtype, ie', et with
(* We have a length now *)
- | TArray(_,None, _, _), _, TArray(_, Some _, _, _) ->
+ | TArray(_,None, _), _, TArray(_, Some _, _) ->
Cil.update_var_type vi et
(* Initializing a local array *)
- | TArray(TInt((IChar|IUChar|ISChar), _) as bt, None, l, a),
+ | TArray(TInt((IChar|IUChar|ISChar), _) as bt, None, a),
SingleInit({enode = Const(CStr s);eloc=loc}), _ ->
Cil.update_var_type vi
(TArray(bt,
Some (integer ~loc (String.length s + 1)),
- l, a))
+ a))
| _, _, _ -> ());
(* Now create assignments instead of the initialization *)
@@ -9635,21 +9633,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
end;
empty
- | Cabs.CUSTOM (custom, name, location) when isglobal ->
- begin
- let loc = convLoc location in
- CurrentLoc.set loc;
- try
- let tcustom = Ltyping.custom custom in
- let attr = fc_stdlib_attribute [] in
- cabsPushGlobal (GAnnot(Dcustom_annot(tcustom, name, attr,loc),loc))
- with LogicTypeError ((source,_),msg) ->
- Kernel.warning
- ~wkey:Kernel.wkey_annot_error ~source
- "%s. Ignoring custom annotation" msg
- end;
- empty
- | Cabs.CUSTOM _ | Cabs.GLOBANNOT _ | Cabs.PRAGMA _ | Cabs.GLOBASM _ | Cabs.FUNDEF _ ->
+ | Cabs.GLOBANNOT _ | Cabs.PRAGMA _ | Cabs.GLOBASM _ | Cabs.FUNDEF _ ->
Kernel.fatal ~current:true "this form of declaration must be global"
and doTypedef ghost ((specs, nl): Cabs.name_group) =
@@ -9710,13 +9694,13 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
begin
match newTyp' with (* do NOT unroll type here,
redefinitions of typedefs are ok *)
- | TComp (newci, _, _) ->
+ | TComp (newci, _) ->
(* Composite types with different tags may be compatible, but here
we use the tags to try and detect if the type is being redefined,
which is NOT allowed. *)
begin
match unrollType typeinfo.ttype with
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
if ci.cname <> newci.cname then
(* different tags => we consider that the type is being redefined *)
error_conflicting_types ()
@@ -9781,7 +9765,7 @@ and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
| _ -> false) specs
in
match restyp with
- | TComp(ci, _, al) ->
+ | TComp(ci, al) ->
if isadef then begin
ci.cattr <- cabsAddAttributes ci.cattr al;
(* The GCompTag was already added *)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 0cbb74f56b4634077f09227e0f550a8684c85537..f53bf4685640ed645803b0b785f35dfc1fde7293 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -94,7 +94,7 @@ class visitor = object(self)
method private ghost_incompatible nt ot =
match (unrollType nt), (unrollType ot) with
| TPtr (nt', _), TPtr(ot', _)
- | TPtr (nt', _), TArray(ot', _, _, _) ->
+ | TPtr (nt', _), TArray(ot', _, _) ->
Cil.isGhostType nt' <> Cil.isGhostType ot' ||
self#ghost_incompatible nt' ot'
| _ ->
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index 2fe91919b97468a14703d68482a841936cc37672..5dd9e930a3d55c9750fcdbe938c49bd383a0b37b 100644
--- a/src/kernel_internals/typing/infer_annotations.ml
+++ b/src/kernel_internals/typing/infer_annotations.ml
@@ -77,7 +77,7 @@ let assigns_from_prototype kf =
type *)
let rec mk_offset set typ =
match Cil.unrollType typ with
- | TArray (typ_elem, size, _, _) ->
+ | TArray (typ_elem, size, _) ->
let range = match size with
| None -> make_range None
| Some size ->
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 0d20565d540de63b748142d6194a57dd69d4920e..112319715aa4d6806ad5c797a47db2603f6d8779 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -535,12 +535,12 @@ let hash_type t =
| TFloat (fkind,_) -> 5 * acc + Hashtbl.hash fkind
| TPtr(t,_) when depth < 5 -> aux (7*acc) (depth+1) t
| TPtr _ -> 7 * acc
- | TArray (t,_,_,_) when depth < 5 -> aux (9*acc) (depth+1) t
+ | TArray (t,_,_) when depth < 5 -> aux (9*acc) (depth+1) t
| TArray _ -> 9 * acc
| TFun (r,_,_,_) when depth < 5 -> aux (11*acc) (depth+1) r
| TFun _ -> 11 * acc
| TNamed (t,_) -> 13 * acc + Hashtbl.hash t.tname
- | TComp(c,_,_) ->
+ | TComp(c,_) ->
let mul = if c.cstruct then 17 else 19 in
mul * acc + Hashtbl.hash c.cname
| TEnum (e,_) -> 23 * acc + Hashtbl.hash e.ename
@@ -650,7 +650,6 @@ let lcEq = PlainMerging.create_eq_table 111 (* Logic constructors *)
let laEq = PlainMerging.create_eq_table 111 (* Axiomatics *)
let llEq = PlainMerging.create_eq_table 111 (* Lemmas *)
-let lcusEq = PlainMerging.create_eq_table 111 (* Custom *)
let lvEq = VolatileMerging.create_eq_table 111
let mfEq = ModelMerging.create_eq_table 111
@@ -668,7 +667,6 @@ let ltSyn = PlainMerging.create_syn_table 111
let lcSyn = PlainMerging.create_syn_table 111
let laSyn = PlainMerging.create_syn_table 111
let llSyn = PlainMerging.create_syn_table 111
-let lcusSyn = PlainMerging.create_syn_table 111
let lvSyn = VolatileMerging.create_syn_table 111
let mfSyn = ModelMerging.create_syn_table 111
let extSyn = ExtMerging.create_syn_table 111
@@ -862,8 +860,6 @@ let rec global_annot_without_irrelevant_attributes ga =
match ga with
| Dvolatile(vi,rd,wr,attr,loc) ->
Dvolatile(vi,rd,wr,drop_attributes_for_merge attr,loc)
- | Dcustom_annot (c,n,attr,loc) ->
- Dcustom_annot (c,n,drop_attributes_for_merge attr,loc)
| Daxiomatic(n,l,attr,loc) ->
Daxiomatic(n,List.map global_annot_without_irrelevant_attributes l,
drop_attributes_for_merge attr,loc)
@@ -925,12 +921,6 @@ let rec global_annot_pass1 g = match g with
ignore (ModelMerging.getNode
mfEq mfSyn !currentFidx (mfi.mi_name,mfi.mi_base_type) mfi
(Some (l, !currentDeclIdx)))
- | Dcustom_annot (c, n, _, l) ->
- Format.eprintf "Mergecil : custom@.";
- CurrentLoc.set l;
- ignore (PlainMerging.getNode
- lcusEq lcusSyn !currentFidx n (n,(c,l))
- (Some (l, !currentDeclIdx)))
| Dinvariant (pi,l) ->
CurrentLoc.set l;
ignore (LogicMerging.getNode
@@ -1043,12 +1033,12 @@ let rec combineTypes (what: combineWhat)
* leaking types from new to old *)
| TInt(IInt, olda), TEnum (ei, a) -> TEnum(ei, addAttributes olda a)
- | TComp (oldci, _, olda) , TComp (ci, _, a) ->
+ | TComp (oldci, olda) , TComp (ci, a) ->
matchCompInfo oldfidx oldci fidx ci;
(* If we get here we were successful *)
- TComp (oldci, empty_size_cache (), addAttributes olda a)
+ TComp (oldci, addAttributes olda a)
- | TArray (oldbt, oldsz, _, olda), TArray (bt, sz, _, a) ->
+ | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
let combbt = combineTypes CombineOther oldfidx oldbt fidx bt in
let combinesz =
match oldsz, sz with
@@ -1059,7 +1049,7 @@ let rec combineTypes (what: combineWhat)
if same_int64 oldsz' sz' then oldsz else
raise (Failure "different array sizes")
in
- TArray (combbt, combinesz, empty_size_cache (), addAttributes olda a)
+ TArray (combbt, combinesz, addAttributes olda a)
| TPtr (oldbt, olda), TPtr (bt, a) ->
TPtr (combineTypes CombineOther oldfidx oldbt fidx bt,
@@ -1463,8 +1453,8 @@ let rec update_type_repr t =
PlainMerging.add_eq_table tEq (oldnode.nfidx, n) renamed_node;
end;
TNamed(node.ndata,attrs)
- | TComp (ci,_,attrs) ->
- TComp (update_compinfo ci, {scache = Not_Computed}, attrs)
+ | TComp (ci,attrs) ->
+ TComp (update_compinfo ci, attrs)
| _ -> t
let static_var_visitor = object
@@ -1825,7 +1815,7 @@ let oneFilePass1 (f:file) : unit =
else begin (* Go inside and clean the referenced flag for the
* declared tags *)
match t.ttype with
- TComp (ci, _, _ ) ->
+ TComp (ci, _ ) ->
ci.creferenced <- false;
(* Create a node for it *)
ignore
@@ -2083,7 +2073,7 @@ class renameVisitorClass =
* is not a root. *)
method! vtype (t: typ) =
match t with
- TComp (ci, _, a) when not ci.creferenced -> begin
+ TComp (ci, a) when not ci.creferenced -> begin
match PlainMerging.findReplacement true sEq !currentFidx ci.cname with
None ->
Kernel.debug ~dkey:Kernel.dkey_linker "No renaming needed %s(%d)"
@@ -2093,11 +2083,9 @@ class renameVisitorClass =
Kernel.debug ~dkey:Kernel.dkey_linker
"Renaming use of %s(%d) to %s(%d)"
ci.cname !currentFidx ci'.cname oldfidx;
- ChangeTo (TComp (ci',
- empty_size_cache (),
- visitCilAttributes (self :> cilVisitor) a))
+ ChangeTo (TComp (ci', visitCilAttributes (self :> cilVisitor) a))
end
- | TComp(ci,_,_) ->
+ | TComp(ci,_) ->
Kernel.debug ~dkey:Kernel.dkey_linker
"%s(%d) referenced. No change" ci.cname !currentFidx;
DoChildren
@@ -2362,19 +2350,6 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
mfEq (!currentFidx,(mf'.mi_name,mf'.mi_base_type))).ndata;
| Some _ -> ()
end
- | Dcustom_annot (_c, n, _, l) ->
- begin
- CurrentLoc.set l;
- match
- PlainMerging.findReplacement
- true lcusEq !currentFidx n
- with
- | None ->
- let g = visitCilGlobal renameVisitor g in
- if not in_axiomatic then
- mergePushGlobals g
- | Some _ -> ()
- end
| Dlemma (n,_,_,_,_,l) ->
begin
CurrentLoc.set l;
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index eb6d64f77d50809496712ae0e5fe13d58d5a1408..8103797ff666d3534f82087cc37e2ea9e60bb995 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -450,7 +450,7 @@ class markReachableVisitor
self#visitAttrs attrs;
self#mark_enum e
- | TComp(c, _, attrs) ->
+ | TComp(c, attrs) ->
let old = is_reachable reachable_tbl (Comp c) in
if not old then
begin
@@ -481,7 +481,7 @@ class markReachableVisitor
| TVoid a | TInt (_,a) | TFloat (_,a) | TBuiltin_va_list a ->
self#visitAttrs a
| TPtr(ty,a) -> ignore (self#vtype ty); self#visitAttrs a
- | TArray(ty,sz, _, a) ->
+ | TArray(ty,sz, a) ->
ignore (self#vtype ty); self#visitAttrs a;
Option.iter (ignore $ (visitCilExpr (self:>cilVisitor))) sz
| TFun (ty, args,_,a) ->
@@ -625,7 +625,7 @@ class markReferencedVisitor = object
ti.treferenced <- true;
end;
DoChildren
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
if not (Stack.is_empty inside_typ) then begin
Kernel.debug ~current:true ~dkey "referenced: comp %s" ci.cname;
ci.creferenced <- true;
diff --git a/src/kernel_internals/typing/substitute_const_globals.ml b/src/kernel_internals/typing/substitute_const_globals.ml
index 3544d1f61df0916503baec586a127ee9954853fe..6a6690d893bef687d8d64cf6a75b53fa4964d140 100644
--- a/src/kernel_internals/typing/substitute_const_globals.ml
+++ b/src/kernel_internals/typing/substitute_const_globals.ml
@@ -36,7 +36,7 @@ class constGlobSubstVisitorClass : cilVisitor = object
'const' and respective initializers. *)
method! vglob g =
let rec is_arithmetic_type = function
- | TArray (typ, _, _, _) -> is_arithmetic_type typ
+ | TArray (typ, _, _) -> is_arithmetic_type typ
| TInt _ | TFloat _ | TEnum _ -> true
| _ -> false
in
diff --git a/src/kernel_services/abstract_interp/abstract_offset.ml b/src/kernel_services/abstract_interp/abstract_offset.ml
index 3c5978e24889ed2143709e20cad26943140e6188..79cb38a36308ccc1116970f93a10a7d9f0091f73 100644
--- a/src/kernel_services/abstract_interp/abstract_offset.ml
+++ b/src/kernel_services/abstract_interp/abstract_offset.ml
@@ -86,7 +86,7 @@ struct
| Field (fi, sub) -> Field (fi, of_cil_offset oracle fi.ftype sub)
| Index (exp, sub) ->
match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _, _) ->
+ | TArray (elem_typ, array_size, _) ->
let idx = oracle exp in
assert_valid_index idx array_size;
Index (idx, elem_typ, of_cil_offset oracle elem_typ sub)
@@ -97,7 +97,7 @@ struct
NoOffset typ
else
match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _, _) ->
+ | TArray (elem_typ, array_size, _) ->
let range, rem =
try
let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
@@ -121,7 +121,7 @@ struct
let sub = of_int_val ~base_typ:elem_typ ~typ rem in
Index (range, elem_typ, sub)
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
if not ci.cstruct then
(* Ignore unions for now *)
raise Abstract_interp.Error_Top
@@ -168,7 +168,7 @@ struct
Field (fi, of_term_offset fi.ftype sub)
| TIndex (index, sub) ->
begin match Cil.unrollType base_typ with
- | TArray (elem_typ, array_size, _, _) ->
+ | TArray (elem_typ, array_size, _) ->
let idx = index_of_term array_size index in
assert_valid_index idx array_size;
Index (idx, elem_typ, of_term_offset elem_typ sub)
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index e51034b01ee27349bb1805957d10dd95b2d4525a..6472cf24e0d3f8f56565aa5db0c31a08f7df47ce 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -253,8 +253,8 @@ let is_weak = function
(* Does a C type end by an empty struct? *)
let rec final_empty_struct = function
- | TArray (typ, _, _, _) -> final_empty_struct typ
- | TComp (compinfo, _, _) ->
+ | TArray (typ, _, _) -> final_empty_struct typ
+ | TComp (compinfo, _) ->
begin
match compinfo.cfields with
| Some [] | None -> true
diff --git a/src/kernel_services/abstract_interp/multidim.ml b/src/kernel_services/abstract_interp/multidim.ml
index 9918b74bd1866321f0af2279b97bfc7dbc176c93..552d76e7f1adc700b9f94d56ea4fc81e855f3147 100644
--- a/src/kernel_services/abstract_interp/multidim.ml
+++ b/src/kernel_services/abstract_interp/multidim.ml
@@ -221,7 +221,7 @@ let of_offset oracle base_typ offset =
aux fi.ftype (Integer.of_int field_size) (add_int x field_offset) sub
| Index (exp, sub) ->
match base_typ with
- | TArray (elem_typ, _array_size, _, _) ->
+ | TArray (elem_typ, _array_size, _) ->
let idx = of_exp oracle exp in
let elem_size = Integer.of_int (Cil.bitsSizeOf elem_typ) in
let x' = add x (mul_integer idx elem_size) in
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index d57b792f32faa0b48413ad3f59833bc31b5c3694..0d32820b1e62d4e850b3b7603cbc4df4ef3c33bb 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -2652,7 +2652,7 @@ module Int_Intervals = struct
match typ with
| Some t -> t
| None ->
- Cil_types.(TArray (TInt(IUChar,[]), None, Cil.empty_size_cache (), []))
+ Cil_types.(TArray (TInt(IUChar,[]), None, []))
in
match i with
| Top -> Format.pp_print_string fmt "[..]"
diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml
index 05113200c9874e6c1788f18d98e131a062b16627..779bf41c4668613aca904c989869c9f84de04235 100644
--- a/src/kernel_services/analysis/bit_utils.ml
+++ b/src/kernel_services/analysis/bit_utils.ml
@@ -119,7 +119,7 @@ let sizeof_lval lv =
let sizeof_pointed typ =
match unrollType typ with
| TPtr (typ,_) -> sizeof typ
- | TArray(typ,_,_,_) -> sizeof typ
+ | TArray(typ,_,_) -> sizeof typ
| _ ->
Kernel.fatal "TYPE IS: %a (unrolled as %a)"
Printer.pp_typ typ
@@ -130,7 +130,7 @@ let sizeof_pointed typ =
let osizeof_pointed typ =
match unrollType typ with
| TPtr (typ,_) -> osizeof typ
- | TArray(typ,_,_,_) -> osizeof typ
+ | TArray(typ,_,_) -> osizeof typ
| _ ->
assert false (*
Format.printf "TYPE IS: %a\n" Printer.pp_typ typ;
@@ -239,7 +239,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
raw_bits 'b' start stop)
)
- | TComp (compinfo, _, _) as typ ->
+ | TComp (compinfo, _) as typ ->
let size = Integer.of_int (try bitsSizeOf typ
with SizeOfError _ -> 0)
in
@@ -342,7 +342,7 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop =
raw_bits '?' start stop
end
- | TArray (typ, _, _, _) ->
+ | TArray (typ, _, _) ->
let size =
try Integer.of_int (bitsSizeOf typ)
with Cil.SizeOfError _ -> Integer.zero
@@ -468,7 +468,7 @@ let rec type_compatible t1 t2 =
| TInt (i1, _), TInt (i2, _) -> i1 = i2
| TFloat (f1, _), TFloat (f2, _) -> f1 = f2
| TPtr (t1, _), TPtr (t2, _) -> type_compatible t1 t2
- | TArray (t1', s1, _, _), TArray (t2', s2, _, _) ->
+ | TArray (t1', s1, _), TArray (t2', s2, _) ->
type_compatible t1' t2' &&
(s1 == s2 || try Integer.equal (Cil.lenOfArray64 s1) (Cil.lenOfArray64 s2)
with Cil.LenOfArray -> false)
@@ -482,7 +482,7 @@ let rec type_compatible t1 t2 =
(fun (_, t1, _) (_, t2, _) -> type_compatible t1 t2) l1 l2
with Invalid_argument _ -> false)
| TNamed _, TNamed _ -> assert false
- | TComp (c1, _, _), TComp (c2, _, _) -> c1.ckey = c2.ckey
+ | TComp (c1, _), TComp (c2, _) -> c1.ckey = c2.ckey
| TEnum (e1, _), TEnum (e2, _) -> e1.ename = e2.ename
| TBuiltin_va_list _, TBuiltin_va_list _ -> true
| (TVoid _ | TInt _ | TFloat _ | TPtr _ | TArray _ | TFun _ | TNamed _ |
@@ -517,7 +517,7 @@ let rec find_offset typ ~offset om =
NoOffset, typ
else
match Cil.unrollType typ with
- | TArray (typ_elt, _, _, _) ->
+ | TArray (typ_elt, _, _) ->
let size_elt = Integer.of_int (Cil.bitsSizeOf typ_elt) in
if Integer.(equal size_elt zero) then
begin
@@ -528,7 +528,7 @@ let rec find_offset typ ~offset om =
Since the sizeof each element is zero, any offset is valid anyway.
*)
let typ =
- TArray (typ_elt, Some minus_one_expr, Cil.empty_size_cache (),[])
+ TArray (typ_elt, Some minus_one_expr, [])
in
Index (minus_one_expr, NoOffset), typ
end
@@ -551,14 +551,14 @@ let rec find_offset typ ~offset om =
let nb = Integer.e_div size size_elt in
let exp_nb = Cil.kinteger64 ~loc nb in
let typ =
- TArray (typ_elt, Some exp_nb, Cil.empty_size_cache (),[])
+ TArray (typ_elt, Some exp_nb, [])
in
Index (exp_start, NoOffset), typ
else (* We match different parts of multiple cells: too imprecise. *)
raise NoMatchingOffset
end
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
let rec find_field = function
| [] -> raise NoMatchingOffset
| fi :: q ->
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 2a063fe0b9752b8756e2074cf694495167a9ab5f..f6dd804a26cad36fb2dad70cca71704f0d137671 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -290,7 +290,7 @@ let get_type_tag t =
| TFloat(FDouble,_) -> "d"
| TFloat (FLongDouble,_) -> "ld"
| TPtr(t,_) -> "p" ^ aux t
- | TArray(t,_,_,_) -> "a" ^ aux t
+ | TArray(t,_,_) -> "a" ^ aux t
| TFun(rt,l,_,_) ->
let base = "fun" ^ aux rt in
(match l with
@@ -298,7 +298,7 @@ let get_type_tag t =
| Some l ->
List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
| TNamed _ -> Kernel.fatal "named type not correctly unrolled"
- | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
+ | TComp (s,_) -> (if s.cstruct then "S" else "U") ^ s.cname
| TEnum (e,_) -> "E" ^ e.ename
| TBuiltin_va_list _ -> "va"
in "__fc_" ^ aux t
@@ -358,7 +358,7 @@ let generate_exn_union e exns =
let kind = (exn_kind_name, TEnum (e,[]), None, [], loc) in
let obj =
(exn_obj_name,
- TComp(exn_kind_union, { scache = Not_Computed } , []), None, [], loc)
+ TComp(exn_kind_union, []), None, [], loc)
in
Some [uncaught; kind; obj]
in
@@ -552,7 +552,7 @@ class erase_exn =
let e = generate_exn_enum exns in
let u,s = generate_exn_union e exns in
let exn =
- Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
+ Cil.makeGlobalVar "__fc_exn" (TComp (s,[]))
in
self#update_enum_bindings e exns;
self#update_union_bindings u exns;
@@ -563,7 +563,7 @@ class erase_exn =
GCompTag (u,loc) ::
GEnumTag (e,loc) :: new_types;
exn_var <- Some exn;
- let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
+ let exn_init = Cil.makeZeroInit ~loc (TComp(s,[]))
in
let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
ChangeDoChildrenPost(
diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index a01c5184db4fab9e995d6ddcd2624f9695a54962..b2767a1a9e131934f3e15fb13b508496e8715180 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -72,7 +72,7 @@ struct
let to_exp = Cil.integer ~loc:unknown_loc in
let size = Option.map to_exp size in
Listed typ,
- Ctype (TArray (t, size, Cil.empty_size_cache (), []))
+ Ctype (TArray (t, size, []))
| _, _ -> raise NotACType
@@ -89,10 +89,10 @@ struct
| TInt (kind, l) -> TInt (kind, add_to l)
| TFloat (kind, l) -> TFloat (kind, add_to l)
| TPtr (typ, l) -> TPtr (typ, add_to l)
- | TArray (typ, size, cache, l) -> TArray (typ, size, cache, add_to l)
+ | TArray (typ, size, l) -> TArray (typ, size, add_to l)
| TFun (typ, args, variadic, l) -> TFun (typ, args, variadic, add_to l)
| TNamed (typeinfo, l) -> TNamed (typeinfo, add_to l)
- | TComp (compinfo, cache, l) -> TComp (compinfo, cache, add_to l)
+ | TComp (compinfo, l) -> TComp (compinfo, add_to l)
| TEnum (enuminfo, l) -> TEnum (enuminfo, add_to l)
| TBuiltin_va_list l -> TBuiltin_va_list (add_to l)
in
@@ -445,8 +445,8 @@ struct
| (Field (lv,_) | FieldNamed (lv,_)) as e ->
let (host, offset) as lv' = build_lval ~loc lv in
let host', offset', ci = match Cil.(unrollTypeDeep (typeOfLval lv')) with
- | TComp (ci,_,_) -> host, offset, ci
- | TPtr (TComp (ci,_,_),_) ->
+ | TComp (ci,_) -> host, offset, ci
+ | TPtr (TComp (ci,_),_) ->
Mem (Cil.new_exp ~loc (Lval lv')), Cil_types.NoOffset, ci
| _ -> typing_error "trying to get a field of an lvalue which is not \
of composite type or pointer to a composite type"
@@ -522,8 +522,8 @@ struct
| lty -> lty
in
let host', offset', ci = match lty with
- | Ctype (TComp (ci,_,_)) -> host, offset, ci
- | Ctype (TPtr (TComp (ci,_,_),_)) ->
+ | Ctype (TComp (ci,_)) -> host, offset, ci
+ | Ctype (TPtr (TComp (ci,_),_)) ->
TMem (Logic_const.term ~loc (Cil_types.TLval tlv') lty), TNoOffset, ci
| _ -> typing_error "trying to get a field of an lvalue which is not \
of composite type or pointer to a composite type"
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 1346e1315fa366e2a2f69c0ee95c16669f530f95..8869fe97088901d6ae11313b3bb9cb474203aec4 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1372,7 +1372,7 @@ let dependencies_of_global annot =
let rec remove_declared_global_annot logic_vars = function
| Dfun_or_pred(li,_) | Dinvariant(li,_) | Dtype_annot(li,_) ->
Cil_datatype.Logic_info.Set.remove li logic_vars
- | Dvolatile _ | Dtype _ | Dlemma _ | Dmodel_annot _ | Dcustom_annot _
+ | Dvolatile _ | Dtype _ | Dlemma _ | Dmodel_annot _
| Dextended _ ->
logic_vars
| Daxiomatic (_,l,_, _) ->
@@ -1698,7 +1698,7 @@ let logic_info_of_global s =
| Dfun_or_pred(li,_) | Dinvariant(li,_) | Dtype_annot(li,_) ->
check_logic_info li acc
| Daxiomatic (_,l, _, _) -> List.fold_left check_one acc l
- | Dtype _ | Dvolatile _ | Dlemma _ | Dmodel_annot _ | Dcustom_annot _
+ | Dtype _ | Dvolatile _ | Dlemma _ | Dmodel_annot _
| Dextended _
-> acc
in
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 11e5418d283c0fc78ba3b315f546b606985e0415..1f798027f2b6803d8a9987ee8394323a902c3d14 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -200,7 +200,7 @@ and typ =
{!Cil.charPtrType}, {!Cil.charConstPtrType} (pointer to a constant
character), {!Cil.voidPtrType}, {!Cil.intPtrType} *)
- | TArray of typ * exp option * bitsSizeofTypCache * attributes
+ | TArray of typ * exp option * attributes
(** Array type. It indicates the base type and the array length. *)
| TFun of typ * (string * typ * attributes) list option * bool * attributes
@@ -224,7 +224,7 @@ and typ =
attributes are in addition to those given when the type name was
defined. *)
- | TComp of compinfo * bitsSizeofTypCache * attributes
+ | TComp of compinfo * attributes
(** A reference to a struct or a union type. All references to the
same struct or union must share the same compinfo among them and
with a [GCompTag] global that precedes all uses (except maybe
@@ -265,14 +265,6 @@ and fkind =
| FDouble (** [double] *)
| FLongDouble (** [long double] *)
-(** This is used to cache the computation of the size of types in bits. *)
-and bitsSizeofTyp =
- | Not_Computed
- | Computed of int
- | Not_Computable of (string * typ) (** Explanation of the error *)
-
-and bitsSizeofTypCache = { mutable scache : bitsSizeofTyp}
-
(* ************************************************************************* *)
(** {2 Attributes} *)
(* ************************************************************************* *)
@@ -444,10 +436,6 @@ and fieldinfo = {
(** Offset at which the field starts in the structure.
Do not read this field directly. Use {!Cil.fieldBitsOffset} or
{!Cil.bitsOffset} instead. *)
-
- mutable fpadding_in_bits: int option;
- (** (Deprecated.) Store the size of the padding that follows the field, if any.
- @deprecated only Jessie uses this *)
}
(* ************************************************************************* *)
@@ -1834,15 +1822,6 @@ and global_annotation =
argument of type t *)
| Dextended of acsl_extension * attributes * location
(** Extended global clause. *)
- | Dcustom_annot of custom_tree * string * attributes * location
- (*Custom declaration*)
-
-and custom_tree = CustomDummy
-(*
- | CustomType of logic_type
- | CustomLexpr of lexpr
- | CustomOther of string * (custom_tree list)
-*)
type kinstr =
| Kstmt of stmt
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index d4c0e7a40739f78a3d16d0e9c599531f567de6d5..9509c39017ad1f8a15e040830783111061472961 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -756,13 +756,13 @@ module Types = struct
| GCompTag (ci, _loc) ->
let kind = Logic_typing.(if ci.cstruct then Struct else Union) in
let name_tag = (ci.cname, kind) in
- Types.add name_tag (TComp (ci, Cil.empty_size_cache (), []));
+ Types.add name_tag (TComp (ci, []));
TypeNameToGlobal.replace name_tag g
| GCompTagDecl (ci, _) ->
let kind = Logic_typing.(if ci.cstruct then Struct else Union) in
let name_tag = (ci.cname, kind) in
- Types.add name_tag (TComp (ci, Cil.empty_size_cache (), []))
+ Types.add name_tag (TComp (ci, []))
| _ -> ()
in
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 6d6d06b8b3a2c7a741a6e75492d64b5a936afa1b..1c13e3837def8e03a1443671d311a1170d3f689f 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1682,7 +1682,6 @@ let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
(* Must ensure that the first property is the best one in order to represent
the annotation (see ip_of_global_annotation_single) *)
let ip_of_global_annotation a =
- let once = true in
let rec aux acc = function
| Daxiomatic(iax_name, l, iax_attrs, _) ->
let iax_props = List.fold_left aux [] l in
@@ -1710,10 +1709,6 @@ let ip_of_global_annotation a =
in
IPTypeInvariant {iti_name=l.l_var_info.lv_name;
iti_type; iti_pred; iti_loc} :: acc
- | Dcustom_annot(_c, _n, _, _) ->
- (* TODO *)
- Kernel.warning ~once "ignoring status of custom annotation";
- acc
| Dmodel_annot _ | Dfun_or_pred _ | Dvolatile _ | Dtype _ ->
(* no associated status for these annotations *)
acc
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index 3c4fc5fa62e932fb0a647a6559faf055e45e411e..c2227e1696c0bd9b2fc707d366b3748dd0b8dc64 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -191,7 +191,6 @@ and pp_def fmt = function
List.iter (fun def -> fprintf fmt ",@ def(%a)" pp_def def) defs;
fprintf fmt ")@]"
| GLOBANNOT _ -> fprintf fmt "GLOBANNOT"
- | CUSTOM _ -> fprintf fmt "CUSTOM"
and pp_file fmt (s,l) =
fprintf fmt "@[FILE %a, {" Filepath.Normalized.pp_abs s;
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 2afe7bfc31ffbf04f057b23e73ad4d9f9cccd5cd..041ad81546544c1a946bc4dae5fba040bdd471fd 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -712,10 +712,10 @@ class cil_printer () = object (self)
self#varname fmt v.vname
method private no_ghost_at_first_level = function
- | TArray(t, e, b, a) ->
+ | TArray(t, e, a) ->
let t = Cil.typeRemoveAttributes [ "ghost" ] t in
let a = Cil.dropAttribute "ghost" a in
- TArray (t, e, b, a)
+ TArray (t, e, a)
| t -> Cil.typeRemoveAttributes [ "ghost" ] t
(* variable declaration *)
@@ -727,7 +727,7 @@ class cil_printer () = object (self)
if v.vformal && not state.print_cil_as_is then begin
match v.vtype with
| TPtr(t,a) when Cil.hasAttribute "arraylen" a ->
- { v with vtype = TArray(t, None, { scache = Not_Computed }, a)}
+ { v with vtype = TArray(t, None, a)}
| _ -> v
end
else v
@@ -1963,7 +1963,7 @@ class cil_printer () = object (self)
| TFloat(fkind, a) ->
fprintf fmt "%a%a%a" self#fkind fkind self#attributes a pname true
- | TComp (comp, _, a) -> (* A reference to a struct *)
+ | TComp (comp, a) -> (* A reference to a struct *)
fprintf fmt
"%a %a%a%a"
self#pp_keyword (if comp.cstruct then "struct" else "union")
@@ -2009,7 +2009,7 @@ class cil_printer () = object (self)
in
self#typ (Some name'') fmt bt'
- | TArray (elemt, lo, _, a) ->
+ | TArray (elemt, lo, a) ->
let atts_elem, a = Cil.splitArrayAttributes a in
let size_info,a =
List.partition
@@ -3273,10 +3273,6 @@ class cil_printer () = object (self)
current_label <- old_label
| Dmodel_annot (mfi,_) ->
self#model_info fmt mfi
- | Dcustom_annot(_c, n ,_attr, _) ->
- (* attributes are meant to be purely internal for now. *)
- fprintf fmt "@[%a %s: <...>@]@\n"
- self#pp_acsl_keyword "custom" n
| Dinvariant (pred,_) ->
let old_label = current_label in
(match pred.l_labels with [l] -> current_label <- l | _ -> ());
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 46ad10d89ee51a494b73c6082025c7f13d276576..f9c1724b21ea587c2532165f5f982ac4ec7f99a3 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -126,16 +126,16 @@ and pp_typ fmt = function
| TInt(ikind,attributes) -> Format.fprintf fmt "TInt(%a,%a)" pp_ikind ikind pp_attributes attributes
| TFloat(fkind,attributes) -> Format.fprintf fmt "TFloat(%a,%a)" pp_fkind fkind pp_attributes attributes
| TPtr(typ,attributes) -> Format.fprintf fmt "TPtr(%a,%a)" pp_typ typ pp_attributes attributes
- | TArray(typ,exp_option,bitsSizeofTypCache,attributes) ->
- Format.fprintf fmt "TArray(%a,%a,%a,%a)" pp_typ typ (pp_option pp_exp) exp_option
- pp_bitsSizeofTypCache bitsSizeofTypCache pp_attributes attributes
+ | TArray(typ,exp_option,attributes) ->
+ Format.fprintf fmt "TArray(%a,%a,%a)" pp_typ typ (pp_option pp_exp) exp_option
+ pp_attributes attributes
| TFun(typ,string_typ_attributes_tuple_list_option,bool,attributes) ->
Format.fprintf fmt "TFun(%a,%a,%a,%a)" pp_typ typ
(pp_option (pp_list (pp_tuple3 pp_string pp_typ pp_attributes))) string_typ_attributes_tuple_list_option
pp_bool bool pp_attributes attributes
| TNamed(typeinfo,attributes) ->
Format.fprintf fmt "TNamed(%a,%a)" pp_typeinfo typeinfo pp_attributes attributes
- | TComp(compinfo,bitsSizeofTypCache,attributes) -> Format.fprintf fmt "TComp(%a,%a,%a)" pp_compinfo compinfo pp_bitsSizeofTypCache bitsSizeofTypCache pp_attributes attributes
+ | TComp(compinfo,attributes) -> Format.fprintf fmt "TComp(%a,%a)" pp_compinfo compinfo pp_attributes attributes
| TEnum(enuminfo,attributes) -> Format.fprintf fmt "TEnum(%a,%a)" pp_enuminfo enuminfo pp_attributes attributes
| TBuiltin_va_list(attributes) -> Format.fprintf fmt "TBuiltin_va_list(%a)" pp_attributes attributes
@@ -158,14 +158,6 @@ and pp_fkind fmt = function
| FDouble -> Format.fprintf fmt "FDouble"
| FLongDouble -> Format.fprintf fmt "FLongDouble"
-and pp_bitsSizeofTyp fmt = function
- | Not_Computed -> Format.fprintf fmt "Not_Computed"
- | Computed(int) -> Format.fprintf fmt "Computed(%a)" pp_int int
- | Not_Computable(string,typ) -> Format.fprintf fmt "Not_Computable(%a,%a)" pp_string string pp_typ typ
-
-and pp_bitsSizeofTypCache fmt bitsSizeofTypCache = Format.fprintf fmt "{scache=%a}"
- pp_bitsSizeofTyp bitsSizeofTypCache.scache
-
and pp_attribute fmt = function
| Attr(string,attrparam_list) ->
Format.fprintf fmt "Attr(%a,%a)" pp_string string (pp_list pp_attrparam) attrparam_list
@@ -239,7 +231,6 @@ and pp_fieldinfo fmt fieldinfo =
faddrof=%a;\
fsize_in_bits=%a;\
foffset_in_bits=%a;\
- fpadding_in_bits=%a;\
}"
pp_compinfo fieldinfo.fcomp
pp_string fieldinfo.forig_name
@@ -251,7 +242,6 @@ and pp_fieldinfo fmt fieldinfo =
pp_bool fieldinfo.faddrof
(pp_option pp_int) fieldinfo.fsize_in_bits
(pp_option pp_int) fieldinfo.foffset_in_bits
- (pp_option pp_int) fieldinfo.fpadding_in_bits
else
Format.fprintf fmt
"{\
@@ -1028,15 +1018,10 @@ and pp_global_annotation fmt = function
Format.fprintf fmt "Dtype_annot(%a,%a)" pp_logic_info logic_info pp_location location
| Dmodel_annot(model_info,location) ->
Format.fprintf fmt "Dmodel_annot(%a,%a)" pp_model_info model_info pp_location location
- | Dcustom_annot(custom_tree,string,attributes,location) ->
- Format.fprintf fmt "Dcustom_annot(%a,%a,%a,%a)" pp_custom_tree custom_tree pp_string string
- pp_attributes attributes pp_location location
| Dextended (e,attr,loc) ->
Format.fprintf fmt "Dextended(%a,%a,%a)"
pp_acsl_extension e pp_attributes attr pp_location loc
-and pp_custom_tree fmt _custom_tree = Format.fprintf fmt "CustomDummy"
-
and pp_variant fmt = pp_pair pp_term (pp_option pp_logic_info) fmt
let pp_kinstr fmt = function
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index 70cafd3ad0cff0567590dda23d31da57d4501b26..1f9f96be7d91156fa8bd30165c5547cc98a4f271 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -74,9 +74,6 @@ val pp_global : Format.formatter -> Cil_types.global -> unit
val pp_typ : Cil_types.typ Pretty_utils.formatter
val pp_ikind : Format.formatter -> Cil_types.ikind -> unit
val pp_fkind : Format.formatter -> Cil_types.fkind -> unit
-val pp_bitsSizeofTyp : Format.formatter -> Cil_types.bitsSizeofTyp -> unit
-val pp_bitsSizeofTypCache :
- Format.formatter -> Cil_types.bitsSizeofTypCache -> unit
val pp_attribute : Cil_types.attribute Pretty_utils.formatter
val pp_attributes : Format.formatter -> Cil_types.attributes -> unit
val pp_attrparam : Cil_types.attrparam Pretty_utils.formatter
@@ -158,7 +155,6 @@ val pp_funspec : Format.formatter -> Cil_types.funspec -> unit
val pp_code_annotation : Cil_types.code_annotation Pretty_utils.formatter
val pp_funbehavior : Format.formatter -> Cil_types.funbehavior -> unit
val pp_global_annotation : Cil_types.global_annotation Pretty_utils.formatter
-val pp_custom_tree : Format.formatter -> Cil_types.custom_tree -> unit
val pp_kinstr : Format.formatter -> Cil_types.kinstr -> unit
val pp_cil_function : Format.formatter -> Cil_types.cil_function -> unit
val pp_kernel_function : Format.formatter -> Cil_types.kernel_function -> unit
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 908d9db116e7d766ce5023155baee302e36e0374..affd3f51673f89106c1421ab6932f87249397e83 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -622,8 +622,6 @@ and print_def fmt def =
fprintf fmt "@[/*@@@ @[%a@]@ */@]@\n"
(pp_list ~sep:"@\n" Logic_print.print_decl) annot
- | CUSTOM _ -> fprintf fmt "<custom annot>"
-
| PRAGMA (a,_) ->
fprintf fmt "@[#pragma %a@]@\n" print_expression a
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5a6d061550307bde4b0e4c779f754c4cbda856d1..bb5c62f1ed2417e8c9ffd44677f5b30fc9e476b9 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -401,34 +401,34 @@ let block_of_local (fdec:fundec) vi =
(** {2 Types} *)
(* ************************************************************************** *)
-let array_type ?length ?(attr=[]) ty = TArray(ty,length,empty_size_cache (),attr)
+let array_type ?length ?(attr=[]) ty = TArray(ty,length,attr)
let direct_array_size ty =
match unrollType ty with
- | TArray(_ty,Some size,_,_) -> value_of_integral_expr size
- | TArray(_ty,None,_,_) -> Integer.zero
+ | TArray(_ty,Some size,_) -> value_of_integral_expr size
+ | TArray(_ty,None,_) -> Integer.zero
| _ -> assert false
let rec array_size ty =
match unrollType ty with
- | TArray(elemty,Some _,_,_) ->
+ | TArray(elemty,Some _,_) ->
if isArrayType elemty then
Integer.mul (direct_array_size ty) (array_size elemty)
else direct_array_size ty
- | TArray(_,None,_,_) -> Integer.zero
+ | TArray(_,None,_) -> Integer.zero
| _ -> assert false
let direct_element_type ty = match unrollType ty with
- | TArray(eltyp,_,_,_) -> eltyp
+ | TArray(eltyp,_,_) -> eltyp
| _ -> assert false
let element_type ty =
let rec elem_type ty = match unrollType ty with
- | TArray(eltyp,_,_,_) -> elem_type eltyp
+ | TArray(eltyp,_,_) -> elem_type eltyp
| _ -> ty
in
match unrollType ty with
- | TArray(eltyp,_,_,_) -> elem_type eltyp
+ | TArray(eltyp,_,_) -> elem_type eltyp
| _ -> assert false
let direct_pointed_type ty =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 62ff92225ba4da0d65c488779e020111e199a5cc..705f2c39c7a471b53903976e05469a354f88a085 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -103,8 +103,6 @@ let doubleType = TFloat(FDouble, [])
let floatType = TFloat(FFloat, [])
let longDoubleType = TFloat (FLongDouble, [])
-let empty_size_cache () = {scache=Not_Computed}
-
type theMachine =
{ mutable useLogicalOperators: bool;
mutable theMachine: mach;
@@ -366,8 +364,8 @@ let rec typeAttrs = function
| TFloat (_, a) -> a
| TNamed (t, a) -> addAttributes a (typeAttrs t.ttype)
| TPtr (_, a) -> a
- | TArray (_, _, _,a) -> a
- | TComp (comp, _, a) -> addAttributes comp.cattr a
+ | TArray (_, _,a) -> a
+ | TComp (comp, a) -> addAttributes comp.cattr a
| TEnum (enum, a) -> addAttributes enum.eattr a
| TFun (_, _, _, a) -> a
| TBuiltin_va_list a -> a
@@ -378,8 +376,8 @@ let typeAttr = function
| TFloat (_, a)
| TNamed (_, a)
| TPtr (_, a)
- | TArray (_, _, _, a)
- | TComp (_, _, a)
+ | TArray (_, _, a)
+ | TComp (_, a)
| TEnum (_, a)
| TFun (_, _, _, a)
| TBuiltin_va_list a -> a
@@ -391,8 +389,8 @@ let setTypeAttrs t a =
| TFloat (f, _) -> TFloat (f, a)
| TNamed (t, _) -> TNamed(t, a)
| TPtr (t', _) -> TPtr(t', a)
- | TArray (t', l, s, _) -> TArray(t', l, s, a)
- | TComp (comp, s, _) -> TComp (comp, s, a)
+ | TArray (t', l, _) -> TArray(t', l, a)
+ | TComp (comp, _) -> TComp (comp, a)
| TEnum (enum, _) -> TEnum (enum, a)
| TFun (r, args, v, _) -> TFun(r,args,v,a)
| TBuiltin_va_list _ -> TBuiltin_va_list a
@@ -422,20 +420,20 @@ let rec typeAddAttributes a0 t =
| TFloat (fk, a) -> TFloat (fk, add a)
| TEnum (enum, a) -> TEnum (enum, add a)
| TPtr (t, a) -> TPtr (t, add a)
- | TArray (t, l, s, a) ->
+ | TArray (t, l, a) ->
let att_elt, att_typ = splitArrayAttributes a0 in
- TArray (arrayPushAttributes att_elt t, l, s,
+ TArray (arrayPushAttributes att_elt t, l,
addAttributes att_typ a)
| TFun (t, args, isva, a) -> TFun(t, args, isva, add a)
- | TComp (comp, s, a) -> TComp (comp, s, add a)
+ | TComp (comp, a) -> TComp (comp, add a)
| TNamed (t, a) -> TNamed (t, add a)
| TBuiltin_va_list a -> TBuiltin_va_list (add a)
end
(* Push attributes that belong to the type of the elements of the array as
far as possible *)
and arrayPushAttributes al = function
- | TArray (bt, l, s, a) ->
- TArray (arrayPushAttributes al bt, l, s, a)
+ | TArray (bt, l, a) ->
+ TArray (arrayPushAttributes al bt, l, a)
| t -> typeAddAttributes al t
(**** Look for the presence of an attribute in a type ****)
@@ -446,7 +444,7 @@ let rec typeHasQualifier attr typ =
match typ with
| TNamed (t, a) ->
hasAttribute attr a || typeHasQualifier attr t.ttype
- | TArray (t, _, _, a) ->
+ | TArray (t, _, a) ->
typeHasQualifier attr t || (* ill-formed type *) hasAttribute attr a
| _ -> hasAttribute attr (typeAttrs typ)
@@ -455,8 +453,8 @@ let typeHasAttributeMemoryBlock a (ty:typ): bool =
let rec visit (t: typ) : unit =
match t with
| TNamed (r, a') -> f a' ; visit r.ttype
- | TArray(t, _, _, a') -> f a'; visit t
- | TComp (comp, _, a') -> f a';
+ | TArray(t, _, a') -> f a'; visit t
+ | TComp (comp, a') -> f a';
List.iter
(fun fi -> f fi.fattr; visit fi.ftype)
(Option.value ~default:[] comp.cfields)
@@ -492,9 +490,9 @@ let rec typeRemoveAttributes ?anl t =
| TFloat (fk, a) -> reshare a (fun a -> TFloat (fk, a))
| TEnum (enum, a) -> reshare a (fun a -> TEnum (enum, a))
| TPtr (t, a) -> reshare a (fun a -> TPtr (t, a))
- | TArray (t, l, s, a) -> reshare a (fun a -> TArray (t, l, s, a))
+ | TArray (t, l, a) -> reshare a (fun a -> TArray (t, l, a))
| TFun (t, args, isva, a) -> reshare a (fun a -> TFun(t, args, isva, a))
- | TComp (comp, s, a) -> reshare a (fun a -> TComp (comp, s, a))
+ | TComp (comp, a) -> reshare a (fun a -> TComp (comp, a))
| TBuiltin_va_list a -> reshare a (fun a -> TBuiltin_va_list a)
| TNamed (tn, a) ->
let tn' = typeRemoveAttributes ?anl tn.ttype in
@@ -521,12 +519,12 @@ let rec typeRemoveAttributesDeep (anl: string list) t =
let t' = typeRemoveAttributesDeep anl t in
if t != t' then TPtr(t', dropAttributes anl a)
else reshare a (fun a -> TPtr(t,a))
- | TArray (t, l, s, a) ->
+ | TArray (t, l, a) ->
let t' = typeRemoveAttributesDeep anl t in
- if t!=t' then TArray(t', l, s, dropAttributes anl a)
- else reshare a (fun a -> TArray (t, l, s, a))
+ if t!=t' then TArray(t', l, dropAttributes anl a)
+ else reshare a (fun a -> TArray (t, l, a))
| TFun (t, args, isva, a) -> reshare a (fun a -> TFun(t, args, isva, a))
- | TComp (comp, s, a) -> reshare a (fun a -> TComp (comp, s, a))
+ | TComp (comp, a) -> reshare a (fun a -> TComp (comp, a))
| TBuiltin_va_list a -> reshare a (fun a -> TBuiltin_va_list a)
| TNamed (tn, a) ->
let tn' = typeRemoveAttributesDeep anl tn.ttype in
@@ -2143,9 +2141,6 @@ and childrenAnnotation vis a =
Queue.add (fun () -> Logic_env.add_model_field mfi')
vis#get_filling_actions;
if mfi' != mfi then Dmodel_annot (mfi',loc) else a
- | Dcustom_annot(c,n,attr,loc) ->
- let attr' = visitCilAttributes vis attr in
- if attr != attr' then Dcustom_annot(c,n,attr',loc) else a
| Dvolatile(tset,rvi,wvi,attr,loc) ->
let tset' = mapNoCopy (visitCilIdTerm vis) tset in
let rvi' = optMapNoCopy (visitCilVarUse vis) rvi in
@@ -2623,22 +2618,22 @@ and childrenType (vis : cilVisitor) (t : typ) : typ =
let t1' = fTyp t1 in
let a' = fAttr a in
if t1' != t1 || a' != a then TPtr(t1', a') else t
- | TArray(t1, None, _, a) ->
+ | TArray(t1, None, a) ->
let t1' = fTyp t1 in
let a' = fAttr a in
- if t1' != t1 || a' != a then TArray(t1', None, empty_size_cache (), a') else t
- | TArray(t1, Some e, _, a) ->
+ if t1' != t1 || a' != a then TArray(t1', None, a') else t
+ | TArray(t1, Some e, a) ->
let t1' = fTyp t1 in
let e' = visitCilExpr vis e in
let a' = fAttr a in
- if t1' != t1 || e' != e || a' != a then TArray(t1', Some e',empty_size_cache (), a') else t
+ if t1' != t1 || e' != e || a' != a then TArray(t1', Some e',a') else t
(* DON'T recurse into the compinfo, this is done in visitCilGlobal.
User can iterate over cinfo.cfields manually, if desired.*)
- | TComp(cinfo, _, a) ->
+ | TComp(cinfo, a) ->
let cinfo' = Visitor_behavior.Get.compinfo vis#behavior cinfo in
let a' = fAttr a in
- if a != a' || cinfo' != cinfo then TComp(cinfo',empty_size_cache (), a') else t
+ if a != a' || cinfo' != cinfo then TComp(cinfo',a') else t
| TFun(rettype, args, isva, a) ->
let rettype' = fTyp rettype in
@@ -3379,9 +3374,9 @@ let rec unrollTypeDeep (t: typ) : typ =
match t with
TNamed (r, a') -> withAttrs (addAttributes al a') r.ttype
| TPtr(t, a') -> TPtr(unrollTypeDeep t, addAttributes al a')
- | TArray(t, l, s, a') ->
+ | TArray(t, l, a') ->
let att_elt, att_typ = splitArrayAttributes al in
- TArray(arrayPushAttributes att_elt (unrollTypeDeep t), l, s,
+ TArray(arrayPushAttributes att_elt (unrollTypeDeep t), l,
addAttributes att_typ a')
| TFun(rt, args, isva, a') ->
TFun (unrollTypeDeep rt,
@@ -3705,7 +3700,7 @@ let typeOf_pointed typ =
*)
let typeOf_array_elem t =
match unrollType t with
- | TArray (ty_elem, _, _, _) -> ty_elem
+ | TArray (ty_elem, _, _) -> ty_elem
| _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
let no_op_coerce typ t =
@@ -3750,7 +3745,7 @@ let rec typeOf (e: exp) : typ =
| AddrOf (lv) -> TPtr(typeOfLval lv, [])
| StartOf (lv) ->
match unrollType (typeOfLval lv) with
- | TArray (t,_,_,attrs) -> TPtr(t, attrs)
+ | TArray (t,_,attrs) -> TPtr(t, attrs)
| _ -> Kernel.fatal ~current:true "typeOf: StartOf on a non-array"
and typeOfInit (i: init) : typ =
@@ -3775,13 +3770,13 @@ and typeOffset basetyp = function
NoOffset -> basetyp
| Index (_, o) -> begin
match unrollType basetyp with
- TArray (t, _, _, _baseAttrs) ->
+ TArray (t, _, _baseAttrs) ->
typeOffset t o
| _ -> Kernel.fatal ~current:true "typeOffset: Index on a non-array"
end
| Field (fi, o) ->
match unrollType basetyp with
- | TComp (_, _,baseAttrs) ->
+ | TComp (_, baseAttrs) ->
let attrs = filter_qualifier_attributes baseAttrs in
(* if the field is mutable, it can written to even if it is
part of a const object (but a const subpart of the field
@@ -3864,7 +3859,7 @@ and typeTermOffset basetyp =
match basetyp with
| Ctype typ ->
begin match unrollType typ with
- TArray (t, _, _, baseAttrs) ->
+ TArray (t, _, baseAttrs) ->
let elementType = typeTermOffset (Ctype t) o in
blendAttributes baseAttrs elementType
| _ ->
@@ -3887,7 +3882,7 @@ and typeTermOffset basetyp =
let rec elt_type = function
| Ctype typ ->
begin match unrollType typ with
- TComp (_, _, baseAttrs) ->
+ TComp (_, baseAttrs) ->
let fieldType = typeTermOffset (Ctype fi.ftype) o in
blendAttributes baseAttrs fieldType
| _ -> Kernel.fatal ~current:true "typeTermOffset: Field on a non-compound"
@@ -3933,12 +3928,12 @@ let rec isWFGhostType t =
and isWFGhostType' t =
if not (isGhostType t) then isWFNonGhostType t
else match t with
- | TPtr(t, _) | TArray(t, _, _, _) -> isWFGhostType' t
+ | TPtr(t, _) | TArray(t, _, _) -> isWFGhostType' t
| _ -> true
and isWFNonGhostType t =
if isGhostType t then false
else match t with
- | TPtr(t, _) | TArray(t, _, _, _) -> isWFNonGhostType t
+ | TPtr(t, _) | TArray(t, _, _) -> isWFNonGhostType t
| _ -> true
(**
@@ -3947,21 +3942,62 @@ and isWFNonGhostType t =
**
**)
exception SizeOfError of string * typ
-let find_size_in_cache s f =
- match s.scache with
- | Not_Computed ->
- let r =
- try
- f ()
- with SizeOfError (msg, typ) as e ->
- s.scache <- Not_Computable (msg, typ);
- raise e
- in
- s.scache <- Computed r;
- r
- | Not_Computable (msg, typ) -> raise (SizeOfError (msg, typ))
- | Computed r -> r
+type sizeof_or_error =
+ | Size of int
+ | Error of string * typ
+
+module SizeOfOrError = Datatype.Make(struct
+ include Datatype.Undefined
+
+ let name = "Cil.SizeOfOrError"
+ type t = sizeof_or_error
+ let reprs = [
+ Size 0 ;
+ Error ("", voidType)
+ ]
+ let compare a b =
+ match a, b with
+ | Size a, Size b -> Int.compare a b
+ | Error (sa, ta), Error(sb, tb) ->
+ let s = String.compare sa sb in
+ if s = 0 then Cil_datatype.Typ.compare ta tb
+ else s
+ | Size _, _ -> 1
+ | _, Size _ -> -1
+
+ let equal = Datatype.from_compare
+ let hash = Hashtbl.hash
+ let rehash = Datatype.identity
+ let copy = Datatype.identity
+ let mem_project = Datatype.never_any_project
+ end)
+
+module TypSize =
+ State_builder.Hashtbl
+ (TypNoAttrs.Hashtbl)
+ (SizeOfOrError)
+ (struct
+ let name = "Cil.CompInfoSize"
+ let dependencies = [] (* depends on Ast.self; see below *)
+ let size = 47
+ end)
+
+let find_sizeof t f =
+ try match TypSize.find t with
+ | Size size -> size
+ | Error (msg, t') -> raise (SizeOfError(msg, t'))
+ with Not_found ->
+ try
+ let size = f () in
+ TypSize.add t (Size size) ;
+ size
+ with SizeOfError(t',msg) as e ->
+ TypSize.add t (Error (t', msg)) ;
+ raise e
+
+let selfTypSize = TypSize.self
+let () = dependency_on_ast selfTypSize
(* Some basic type utilities *)
let rank : ikind -> int = function
@@ -4055,12 +4091,12 @@ let rec bytesAlignOf t =
| TFloat(FLongDouble, _) ->
theMachine.theMachine.alignof_longdouble
| TNamed (t, _) -> bytesAlignOf t.ttype
- | TArray (t, _, _, _) -> bytesAlignOf t
+ | TArray (t, _, _) -> bytesAlignOf t
| TPtr _ | TBuiltin_va_list _ ->
theMachine.theMachine.alignof_ptr
(* For composite types get the maximum alignment of any field inside *)
- | TComp (c, _, _) ->
+ | TComp (c, _) ->
(* On GCC the zero-width fields do not contribute to the alignment. On
* MSVC only those zero-width that _do_ appear after other
* bitfields contribute to the alignment. So we drop those that
@@ -4344,8 +4380,8 @@ and offsetOfFieldAcc_MSVC last (fi: fieldinfo)
Currently, we only use it for flexible array members *)
and bitsSizeOfEmptyArray typ =
match unrollType typ with
- | TArray (_, None, _, _) -> 0
- | TArray (_, Some e, _, _) -> begin
+ | TArray (_, None, _) -> 0
+ | TArray (_, Some e, _) -> begin
match constFoldToInt e with
| Some i when Integer.is_zero i ->
(* Used for GCC extension of non-C99 flexible array members.
@@ -4369,20 +4405,21 @@ and bitsSizeOf t =
| TPtr _ -> 8 * theMachine.theMachine.sizeof_ptr
| TBuiltin_va_list _ -> 8 * theMachine.theMachine.sizeof_ptr
| TNamed (t, _) -> bitsSizeOf t.ttype
- | TComp ({cfields=None} as comp, _, _) ->
+ | TComp ({cfields=None} as comp, _) ->
raise
(SizeOfError
(Format.sprintf "abstract type '%s'" (compFullName comp), t))
- | TComp ({cfields=Some[]}, scache,_) when acceptEmptyCompinfo() ->
- find_size_in_cache scache (fun () -> 0)
- | TComp ({cfields=Some[]} as comp,_,_) ->
- (* sizeof() empty structs/arrays is only allowed on GCC/MSVC *)
- raise
- (SizeOfError
- (Format.sprintf "empty struct '%s'" (compFullName comp), t))
- | TComp (comp, scache, _) when comp.cstruct -> (* Struct *)
- find_size_in_cache
- scache
+ | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
+ find_sizeof t (fun () -> 0)
+ | TComp ({cfields=Some[]} as comp,_) ->
+ find_sizeof t
+ (fun () ->
+ (* sizeof() empty structs/arrays is only allowed on GCC/MSVC *)
+ raise
+ (SizeOfError
+ (Format.sprintf "empty struct '%s'" (compFullName comp), t)))
+ | TComp (comp, _) when comp.cstruct -> (* Struct *)
+ find_sizeof t
(fun () ->
(* Go and get the last offset *)
let startAcc =
@@ -4404,9 +4441,8 @@ and bitsSizeOf t =
else
addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
- | TComp (comp, scache, _) -> (* Union *)
- find_size_in_cache
- scache
+ | TComp (comp, _) -> (* Union *)
+ find_sizeof t
(fun () ->
(* Get the maximum of all fields *)
let startAcc =
@@ -4426,9 +4462,8 @@ and bitsSizeOf t =
(* Add trailing by simulating adding an extra field *)
addTrailing max (8 * bytesAlignOf t))
- | TArray(bt, Some len, scache, _) ->
- find_size_in_cache
- scache
+ | TArray(bt, Some len, _) ->
+ find_sizeof t
(fun () ->
begin
match (constFold true len).enode with
@@ -4458,8 +4493,10 @@ and bitsSizeOf t =
else
raise (SizeOfError ("Undefined sizeof on a function.", t))
- | TArray (_, None, _, _) ->
- raise (SizeOfError ("Size of array without number of elements.", t))
+ | TArray (_, None, _) ->
+ find_sizeof t
+ (fun () ->
+ raise (SizeOfError ("Size of array without number of elements.", t)))
(* Iterator on the fields of a structure, with additional information about
having reached the last field (for flexible member arrays) *)
@@ -4518,7 +4555,7 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
| Field(f, off) ->
if check_invariants then
(match unrollType baset with
- | TComp (ci, _, _) -> assert (ci == f.fcomp)
+ | TComp (ci, _) -> assert (ci == f.fcomp)
| _ -> assert false);
let offsbits, size = fieldBitsOffset f in
loopOff f.ftype size (start + offsbits) off
@@ -5418,7 +5455,6 @@ let global_annotation_attributes = function
| Dtype_annot ({l_var_info = { lv_attr }}, _) -> lv_attr
| Dmodel_annot ({ mi_attr }, _) -> mi_attr
| Dextended (_,attrs,_) -> attrs
- | Dcustom_annot (_,_,attrs,_) -> attrs
let global_attributes = function
| GType ({ttype},_) -> typeAttrs ttype
@@ -5762,11 +5798,11 @@ let isArrayType t = match unrollTypeSkel t with
| _ -> false
let isAnyCharArrayType t = match unrollTypeSkel t with
- | TArray(tau,_,_,_) when isAnyCharType tau -> true
+ | TArray(tau,_,_) when isAnyCharType tau -> true
| _ -> false
let isCharArrayType t = match unrollTypeSkel t with
- | TArray(tau,_,_,_) when isCharType tau -> true
+ | TArray(tau,_,_) when isCharType tau -> true
| _ -> false
let isStructOrUnionType t = match unrollTypeSkel t with
@@ -5973,8 +6009,8 @@ let existsType (f: typ -> existsAction) (t: typ) : bool =
| ExistsMaybe ->
(match t with
TNamed (t', _) -> loop t'.ttype
- | TComp (c, _,_) -> loopComp c
- | TArray (t', _, _, _) -> loop t'
+ | TComp (c,_) -> loopComp c
+ | TArray (t', _, _) -> loop t'
| TPtr (t', _) -> loop t'
| TFun (rt, args, _, _) ->
(loop rt || List.exists (fun (_, at, _) -> loop at)
@@ -6033,7 +6069,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
SingleInit (new_exp ~loc (Const(CInt64(Integer.zero, ik, None))))
| TFloat(fk, _) -> SingleInit(new_exp ~loc (Const(CReal(0.0, fk, None))))
| TEnum _ -> SingleInit (zero ~loc)
- | TComp (comp, _, _) as t' when comp.cstruct ->
+ | TComp (comp, _) as t' when comp.cstruct ->
let inits =
List.fold_right
(fun f acc ->
@@ -6044,7 +6080,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
(Option.value ~default:[] comp.cfields) []
in
CompoundInit (t', inits)
- | TComp (comp, _, _) when not comp.cstruct ->
+ | TComp (comp, _) when not comp.cstruct ->
(match comp.cfields with
| Some [] -> CompoundInit(t, []) (* tolerate empty initialization. *)
| Some (f :: _rest) ->
@@ -6053,7 +6089,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
CompoundInit(t, [(Field(f, NoOffset), makeZeroInit ~loc f.ftype)])
| None ->
Kernel.fatal "Initialization of incomplete struct")
- | TArray(bt, Some len, _, _) as t' ->
+ | TArray(bt, Some len, _) as t' ->
let n =
match constFoldToInt len with
| Some n -> Integer.to_int_exn n
@@ -6066,7 +6102,7 @@ let rec makeZeroInit ~loc (t: typ) : init =
in
CompoundInit(t', loopElems [] (n - 1))
- | TArray (_bt, None, _, _) as t' ->
+ | TArray (_bt, None, _) as t' ->
(* Unsized array, allow it and fill it in later
* (see cabs2cil.ml, collectInitializer) *)
CompoundInit (t', [])
@@ -6092,7 +6128,7 @@ let foldLeftCompound
~(initl: (offset * init) list)
~(acc: 'a) : 'a =
match unrollType ct with
- | TArray(bt, leno, _, _) -> begin
+ | TArray(bt, leno, _) -> begin
let default () =
(* iter over the supplied initializers *)
List.fold_left (fun acc (o, i) -> doinit o i bt acc) acc initl
@@ -6140,7 +6176,7 @@ let foldLeftCompound
else default ()
end
- | TComp (_comp, _, _) ->
+ | TComp (_comp, _) ->
let getTypeOffset = function
Field(f, NoOffset) -> f.ftype
| _ -> Kernel.fatal ~current:true "foldLeftCompound: malformed initializer"
@@ -6153,12 +6189,12 @@ let foldLeftCompound
let rec has_flexible_array_member t =
let is_flexible_array t =
match unrollType t with
- | TArray (_, None, _, _) -> true
- | TArray (_, Some z, _, _) -> (msvcMode() || gccMode()) && isZero z
+ | TArray (_, None, _) -> true
+ | TArray (_, Some z, _) -> (msvcMode() || gccMode()) && isZero z
| _ -> false
in
match unrollType t with
- | TComp ({ cfields = Some ((_::_) as l) },_,_) ->
+ | TComp ({ cfields = Some ((_::_) as l) },_) ->
let last = (Extlib.last l).ftype in
is_flexible_array last ||
((gccMode() || msvcMode()) && has_flexible_array_member last)
@@ -6170,15 +6206,15 @@ let rec has_flexible_array_member t =
let rec isCompleteType ?(allowZeroSizeArrays=gccMode()) ?(last_field=false) t =
match unrollType t with
| TVoid _ -> false (* void is an incomplete type by definition (6.2.5§19) *)
- | TArray(t, None, _, _) ->
+ | TArray(t, None, _) ->
last_field && is_complete_agg_member ~allowZeroSizeArrays ~last_field t
- | TArray(t, Some z, _, _) when isZero z ->
+ | TArray(t, Some z, _) when isZero z ->
allowZeroSizeArrays &&
is_complete_agg_member ~allowZeroSizeArrays ~last_field t
- | TArray(t, Some _, _, _) ->
+ | TArray(t, Some _, _) ->
is_complete_agg_member ~allowZeroSizeArrays ~last_field t
- | TComp ( { cfields = None } , _, _) -> false
- | TComp ( { cstruct ; cfields = Some flds }, _, _) -> (* Struct or union *)
+ | TComp ( { cfields = None }, _) -> false
+ | TComp ( { cstruct ; cfields = Some flds }, _) -> (* Struct or union *)
complete_type_fields ~allowZeroSizeArrays cstruct flds
| TEnum({eitems = []},_) -> false
| TEnum _ -> true
@@ -6216,7 +6252,7 @@ let is_mutable_or_initialized (host, offset) =
aux
(can_mutate || hasAttribute frama_c_mutable fi.fattr)
fi.ftype off
- | TArray(typ, _, _, _), Index(_, off) -> aux can_mutate typ off
+ | TArray(typ, _, _), Index(_, off) -> aux can_mutate typ off
| _, Index _ -> Kernel.fatal "Index on a non-array type"
in
match host with
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 32bd684f7f20b1382a140f9adf088d42bbf4d68a..b7fb1ce9064956baea8bc0a2a4ae21ec5b6e6194 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2131,9 +2131,6 @@ val peepHole1: (instr -> instr list option) -> stmt list -> unit
of the error *)
exception SizeOfError of string * typ
-(** Create a fresh size cache with [Not_Computed] *)
-val empty_size_cache : unit -> bitsSizeofTypCache
-
(** Give the unsigned kind corresponding to any integer kind *)
val unsignedVersionOf : ikind -> ikind
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index ebd6fe21fa6b1402e5d6d68aa137c4440e217347..e5e57b1738d4a64a76e9f38265b59122ff589173 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -129,7 +129,6 @@ let mkCompInfo
faddrof = false;
fsize_in_bits = None;
foffset_in_bits = None;
- fpadding_in_bits = None;
})) (mkfspec comp) in
comp.cfields <- flds;
comp
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 7303b1159c0a49e9fac14fc7b699a50f6597489e..6c438f5dd51da9fd580b0ae03731c1c1a586a0ac 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -440,7 +440,8 @@ let compare_exp_struct_eq = Extlib.mk_fun "compare_exp_struct_eq"
type type_compare_config =
{ by_name : bool;
logic_type: bool;
- unroll: bool }
+ unroll: bool;
+ no_attrs:bool; }
let rec compare_attribute config a1 a2 = match a1, a2 with
| Attr (s1, l1), Attr (s2, l2) ->
@@ -449,10 +450,12 @@ let rec compare_attribute config a1 a2 = match a1, a2 with
| Attr _, AttrAnnot _ -> -1
| AttrAnnot _, Attr _ -> 1
and compare_attributes config l1 l2 =
- let l1, l2 = if config.logic_type
- then !drop_non_logic_attributes l1, !drop_non_logic_attributes l2
- else l1,l2
- in compare_list (compare_attribute config) l1 l2
+ if config.no_attrs then 0
+ else
+ let l1, l2 = if config.logic_type
+ then !drop_non_logic_attributes l1, !drop_non_logic_attributes l2
+ else l1,l2
+ in compare_list (compare_attribute config) l1 l2
and compare_attrparam_list config l1 l2 =
compare_list (compare_attrparam config) l1 l2
and compare_attrparam config a1 a2 = match a1, a2 with
@@ -520,7 +523,7 @@ and compare_type config t1 t2 =
compare_chain
(compare_type config) t1 t2
(compare_attributes config) l1 l2
- | TArray (t1', e1, _, l1), TArray (t2', e2, _, l2) ->
+ | TArray (t1', e1, l1), TArray (t2', e2, l2) ->
compare_chain compare_array_sizes e1 e2
(compare_chain
(compare_type config) t1' t2'
@@ -534,7 +537,7 @@ and compare_type config t1 t2 =
assert (not config.unroll);
compare_chain (=?=) t1.tname t2.tname
(compare_attributes config) a1 a2
- | TComp (c1, _, l1), TComp (c2, _, l2) ->
+ | TComp (c1, l1), TComp (c2, l2) ->
let res =
if config.by_name
then (=?=) c1.cname c2.cname
@@ -576,14 +579,14 @@ let rec hash_type config t =
| TFloat (f, l) -> Hashtbl.hash (f, 3, hash_attributes config l)
| TPtr (t, l) ->
Hashtbl.hash (hash_type config t, 4, hash_attributes config l)
- | TArray (t, _, _, l) ->
+ | TArray (t, _, l) ->
Hashtbl.hash (hash_type config t, 5, hash_attributes config l)
| TFun (r, a, v, l) ->
Hashtbl.hash
(hash_type config r, 6, hash_args config a, v, hash_attributes config l)
| TNamed (ti, l) ->
Hashtbl.hash (ti.tname, 7, hash_attributes config l)
- | TComp (c, _, l) ->
+ | TComp (c, l) ->
Hashtbl.hash
((if config.by_name then Hashtbl.hash c.cname else c.ckey), 8,
hash_attributes config l)
@@ -602,7 +605,9 @@ module Attribute=struct
include Make_with_collections
(struct
type t = attribute
- let config = { by_name = false; logic_type = false; unroll = true }
+ let config =
+ { by_name = false; logic_type = false;
+ unroll = true; no_attrs = false }
let name = "Attribute"
let reprs = [ AttrAnnot "" ]
let compare = compare_attribute config
@@ -644,7 +649,9 @@ module Typ= struct
include
MakeTyp
(struct
- let config = { by_name = false; logic_type = false; unroll = true; }
+ let config =
+ { by_name = false; logic_type = false;
+ unroll = true; no_attrs = false}
let name = "Typ"
end)
let toplevel_attr = function
@@ -653,8 +660,8 @@ module Typ= struct
| TFloat (_, a) -> a
| TNamed (_, a) -> a
| TPtr (_, a) -> a
- | TArray (_, _, _,a) -> a
- | TComp (_, _, a) -> a
+ | TArray (_, _,a) -> a
+ | TComp (_, a) -> a
| TEnum (_, a) -> a
| TFun (_, _, _, a) -> a
| TBuiltin_va_list a -> a
@@ -663,17 +670,28 @@ end
module TypByName =
MakeTyp
(struct
- let config = { by_name = true; logic_type = false; unroll = false; }
+ let config = { by_name = true; logic_type = false;
+ unroll = false; no_attrs = false }
let name = "TypByName"
end)
module TypNoUnroll =
MakeTyp
(struct
- let config = { by_name = false; logic_type = false; unroll = false; }
+ let config = { by_name = false; logic_type = false;
+ unroll = false; no_attrs = false }
let name = "TypNoUnroll"
end)
+module TypNoAttrs =
+ MakeTyp
+ (struct
+ let config =
+ { by_name = false; logic_type = false;
+ unroll = true; no_attrs = true}
+ let name = "TypNoAttrs"
+ end)
+
module Typeinfo =
Make_with_collections
(struct
@@ -843,8 +861,8 @@ module Fieldinfo = struct
floc = loc;
faddrof = false;
fsize_in_bits = None;
- foffset_in_bits = None;
- fpadding_in_bits = None }
+ foffset_in_bits = None
+ }
:: acc)
acc
Location.reprs)
@@ -1472,7 +1490,8 @@ module Logic_info_structural = struct
in
if name_cmp <> 0 then name_cmp else begin
let config =
- { by_name = true ; logic_type = true ; unroll = true }
+ { by_name = true ; logic_type = true ;
+ unroll = true ; no_attrs = false }
in
let prm_cmp p1 p2 =
compare_logic_type config p1.lv_type p2.lv_type
@@ -1514,7 +1533,8 @@ end
module Logic_type =
Make_Logic_type(
struct
- let config = { by_name = false; logic_type = true; unroll = true }
+ let config = { by_name = false; logic_type = true;
+ unroll = true; no_attrs = false }
let name = "Logic_type"
end)
@@ -1522,14 +1542,16 @@ module Logic_type_ByName =
Make_Logic_type(
struct
let name = "Logic_type_ByName"
- let config = { by_name = true; logic_type = true; unroll = false }
+ let config = { by_name = true; logic_type = true;
+ unroll = false; no_attrs = false }
end)
module Logic_type_NoUnroll =
Make_Logic_type(
struct
let name = "Logic_type_NoUnroll"
- let config = { by_name = false; logic_type = false; unroll = false }
+ let config = { by_name = false; logic_type = false;
+ unroll = false; no_attrs = false }
end)
module Model_info = struct
@@ -2252,12 +2274,6 @@ module Global_annotation = struct
| Dmodel_annot(l1,_), Dmodel_annot(l2,_) -> Model_info.compare l1 l2
| Dmodel_annot _, _ -> -1
| _, Dmodel_annot _ -> 1
- | Dcustom_annot(_, n1, attr1, _),
- Dcustom_annot(_, n2, attr2, _) ->
- let res = Datatype.String.compare n1 n2 in
- if res = 0 then Attributes.compare attr1 attr2 else res
- | Dcustom_annot _, _ -> -1
- | _, Dcustom_annot _ -> 1
| Dextended (ext1, _, _), Dextended (ext2, _, _) ->
Datatype.Int.compare ext1.ext_id ext2.ext_id
@@ -2277,7 +2293,6 @@ module Global_annotation = struct
| Dinvariant(l,_) -> 13 * Logic_info.hash l
| Dtype_annot(l,_) -> 17 * Logic_info.hash l
| Dmodel_annot(l,_) -> 19 * Model_info.hash l
- | Dcustom_annot(_,n,_,_) -> 23 * Datatype.String.hash n
| Dextended ({ext_id},_,_) -> 29 * Datatype.Int.hash ext_id
let copy = Datatype.undefined
@@ -2292,7 +2307,6 @@ module Global_annotation = struct
| Dtype_annot(_, loc) -> loc
| Dmodel_annot(_, loc) -> loc
| Dvolatile(_, _, _, _,loc) -> loc
- | Dcustom_annot(_,_,_,loc) -> loc
| Dextended(_,_,loc) -> loc
let attr = function
@@ -2304,7 +2318,6 @@ module Global_annotation = struct
| Dtype_annot({ l_var_info = { lv_attr}}, _) -> lv_attr
| Dmodel_annot({ mi_attr }, _) -> mi_attr
| Dvolatile(_, _, _, attr, _) -> attr
- | Dcustom_annot(_,_,attr,_) -> attr
| Dextended (_,attr,_) -> attr
end
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index a311f2302423743e3e081fd6fb10fdfdebbc87ad..df5138305b7a051784a19e7f9c6e893383ac0648 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -246,6 +246,8 @@ module TypByName: S_with_collections_pretty with type t = typ
*)
module TypNoUnroll: S_with_collections_pretty with type t = typ
+(** Types, with comparison over struct done by key and ignoring attributes. *)
+module TypNoAttrs: S_with_collections_pretty with type t = typ
module Typeinfo: S_with_collections with type t = typeinfo
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 02ddf0546dfd710c93257d0749f47b3dcfc0940a..f9587d4ee3a3698a21a6a1eada47cd42a2ffb220 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1256,7 +1256,7 @@ let extract_logic_infos g =
let rec aux acc = function
| Dfun_or_pred (li,_) | Dinvariant (li,_) | Dtype_annot (li,_) -> li :: acc
| Dvolatile _ | Dtype _ | Dlemma _
- | Dmodel_annot _ | Dcustom_annot _ | Dextended _ -> acc
+ | Dmodel_annot _ | Dextended _ -> acc
| Daxiomatic(_,l,_,_) -> List.fold_left aux acc l
in aux [] g
@@ -1446,7 +1446,7 @@ class reorder_ast: Visitor.frama_c_visitor =
recursive definition of type %s"
ty.tname)
typedefs
- | TComp(ci,_,_) ->
+ | TComp(ci,_) ->
if not (Compinfo.Set.mem ci known_compinfo) then begin
self#add_needed_decl (GCompTagDecl (ci,Location.unknown));
self#add_known_compinfo ci
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 18d9d1cab1c9cf85ba664712c59e7b59b99bee85..98621cdf80a70d89f4afc98b7c5f8b8b768ed332 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -1316,7 +1316,7 @@ module Base_checker = struct
method! vtype ty =
match ty with
- | TArray (_, _, _, la) ->
+ | TArray (_, _, la) ->
let elt, _ = Cil.splitArrayAttributes la in
if elt != [] then
Kernel.fatal
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 8950bee942e7e3b170c56269a8aa0383a916a3c3..b8c0cc94f21d40b61fbda1551f41c15d66d7b4cb 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -765,7 +765,7 @@ struct
ignore (Logic_env.find_model_field f ty); true
with Not_found ->
(match Cil.unrollType ty with
- | TComp(comp,_,_) ->
+ | TComp(comp,_) ->
List.exists
(fun x -> x.fname = f)
(Option.value ~default:[] comp.cfields)
@@ -773,7 +773,7 @@ struct
let plain_type_of_c_field loc f ty =
match Cil.unrollType ty with
- | TComp (comp, _, attrs) ->
+ | TComp (comp, attrs) ->
(try
let attrs = Cil.filter_qualifier_attributes attrs in
let field = C.find_comp_field comp f in
@@ -932,8 +932,7 @@ struct
with Not_found ->
ctxt.error loc "size of array must be an integral value";
in
- Ctype (TArray (ctype ty, size,
- Cil.empty_size_cache (),[]))
+ Ctype (TArray (ctype ty, size,[]))
| LTpointer ty -> Ctype (TPtr (ctype ty, []))
| LTenum e ->
(try Ctype (ctxt.find_type Enum e)
@@ -1338,8 +1337,8 @@ struct
result
| TInt _, TPtr _ -> result
| TPtr _, TInt _ -> result
- | ((TArray (told,_,_,_) | TPtr (told,_)),
- (TPtr (tnew,_) | TArray(tnew,_,_,_)))
+ | ((TArray (told,_,_) | TPtr (told,_)),
+ (TPtr (tnew,_) | TArray(tnew,_,_)))
when is_same_c_type told tnew -> result
| (TPtr _ | TArray _), (TPtr _ | TArray _)
when isLogicNull e -> result
@@ -1366,7 +1365,7 @@ struct
result
| (TInt _ | TEnum _ | TPtr _ ), TVoid _ ->
(ot, e)
- | TComp (comp1, _, _), TComp (comp2, _, _)
+ | TComp (comp1, _), TComp (comp2, _)
when comp1.ckey = comp2.ckey ->
nt, e
| _ ->
@@ -4308,8 +4307,6 @@ struct
let annot = C.on_error annot rollback_transaction
- let custom _c = CustomDummy
-
end
(*
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 9db60f4b059866436d82d192083d0e22c07fcb95..838eede9a178bc670da52354425b8a4571119714 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -233,8 +233,6 @@ sig
val annot : Logic_ptree.decl -> global_annotation
- val custom : Logic_ptree.custom_tree -> Cil_types.custom_tree
-
(** [funspec behaviors f prms typ spec] type-checks a function contract.
@param behaviors list of existing behaviors (outside of the current
spec, e.g. in the spec of the corresponding declaration when type-checking
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index d6df9c98e3aef8ddfd0de87164106a6ee54ffee9..4131258363e4c9061a648e697590d3f603aea9a3 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -96,7 +96,7 @@ let logicCType t =
let plain_array_to_ptr ty =
match unroll_type ty with
- | Ctype(TArray(ty,lo,_,attr) as tarr) ->
+ | Ctype(TArray(ty,lo,attr) as tarr) ->
let length_attr =
match lo with
| None -> []
@@ -734,7 +734,6 @@ let rec add_attribute_glob_annot a g =
| Dlemma(n,labs,t,p,al,l) ->
Dlemma(n,labs,t,p,Cil.addAttribute a al,l)
| Dmodel_annot (mi,_) -> mi.mi_attr <- Cil.addAttribute a mi.mi_attr; g
- | Dcustom_annot(c,n,al,l) -> Dcustom_annot(c,n,Cil.addAttribute a al, l)
| Dextended (e,al,l) -> Dextended(e,Cil.addAttribute a al,l)
let behavior_has_only_assigns bhvs =
@@ -1250,9 +1249,6 @@ let rec is_same_global_annotation ga1 ga2 =
| Dinvariant (li1,_), Dinvariant (li2,_) -> is_same_logic_info li1 li2
| Dtype_annot (li1,_), Dtype_annot (li2,_) -> is_same_logic_info li1 li2
| Dmodel_annot (li1,_), Dmodel_annot (li2,_) -> is_same_model_info li1 li2
- | Dcustom_annot (c1, n1, attr1, _),
- Dcustom_annot (c2, n2, attr2, _) ->
- is_same_string n1 n2 && c1 = c2 && is_same_attributes attr1 attr2
| Dvolatile(t1,r1,w1,attr1,_), Dvolatile(t2,r2,w2,attr2,_) ->
is_same_list is_same_identified_term t1 t2 &&
is_same_opt (fun x y -> x.vname = y.vname) r1 r2 &&
@@ -1260,10 +1256,10 @@ let rec is_same_global_annotation ga1 ga2 =
is_same_attributes attr1 attr2
| Dextended(id1,_,_), Dextended(id2,_,_) -> id1 = id2
| (Dfun_or_pred _ | Daxiomatic _ | Dtype _ | Dlemma _
- | Dinvariant _ | Dtype_annot _ | Dcustom_annot _ | Dmodel_annot _
+ | Dinvariant _ | Dtype_annot _ | Dmodel_annot _
| Dvolatile _ | Dextended _),
(Dfun_or_pred _ | Daxiomatic _ | Dtype _ | Dlemma _
- | Dinvariant _ | Dtype_annot _ | Dcustom_annot _ | Dmodel_annot _
+ | Dinvariant _ | Dtype_annot _ | Dmodel_annot _
| Dvolatile _ | Dextended _) -> false
let is_same_axiomatic ax1 ax2 =
@@ -2653,7 +2649,7 @@ let const_fold_trange_bounds typ b e =
| Some te -> extract (constFoldTermToInt te)
| None ->
match Cil.unrollType typ with
- | TArray (_, Some size, _, _) ->
+ | TArray (_, Some size, _) ->
Integer.pred (extract (Cil.isInteger size))
| _ -> raise CannotSimplify
in
diff --git a/src/kernel_services/parsetree/cabs.mli b/src/kernel_services/parsetree/cabs.mli
index 4605ae02e5d7596765c9173a0429fc8e9e88878a..44d168dec6fbdef792a3bd9d673216dfce5e9431 100644
--- a/src/kernel_services/parsetree/cabs.mli
+++ b/src/kernel_services/parsetree/cabs.mli
@@ -173,8 +173,6 @@ and definition =
| STATIC_ASSERT of expression * string * cabsloc
| LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
| GLOBANNOT of Logic_ptree.decl list
- (** Logical declaration (axiom, logic, etc.)*)
- | CUSTOM of Logic_ptree.custom_tree * string * cabsloc
(** the file name, and then the list of toplevel forms.
@plugin development guide *)
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index 14b0e66acbc617f9be372a6d9cc3eeef6287c106..539e06499c9577704aa9506441db1f44fad2e1e4 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -160,7 +160,6 @@ let get_definitionloc (d : definition) : cabsloc =
| LINKAGE (_, l, _) -> l
| GLOBANNOT({Logic_ptree.decl_loc = l }::_) -> l
| GLOBANNOT [] -> assert false
- | CUSTOM (_,_,l) -> l
let get_statementloc (s : statement) : cabsloc =
begin
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 7d991ee30f09194f5fbacbbcae2644cf6557852b..3a92d2bb5173bc3ef530adee820fb483c1a7ad71 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -379,13 +379,6 @@ type code_annot =
@modify 18.0-Argon
*)
-(** custom trees *)
-
-type custom_tree =
- | CustomType of logic_type
- | CustomLexpr of lexpr
- | CustomOther of string * (custom_tree list)
-
(** all kind of annotations*)
type annot =
| Adecl of decl list (** global annotation. *)
@@ -396,7 +389,6 @@ type annot =
| Acode_annot of location * code_annot (** code annotation. *)
| Aloop_annot of location * code_annot list (** loop annotation. *)
| Aattribute_annot of location * string (** attribute annotation. *)
- | Acustom of location * string * custom_tree
(** ACSL extension for external spec file **)
type ext_decl =
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index ef15f460f554a4082a9dc13498c820159f1f70f6..21f0b0fbb9dbd20c9c9a889931b240e925d8d7ff 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -264,7 +264,6 @@ and childrenDefinition vis d =
let dl' = mapNoCopyList (visitCabsDefinition vis) dl in
if dl' != dl then LINKAGE (n, l, dl') else d
| GLOBANNOT _ -> d
- | CUSTOM _ -> d
and visitCabsBlock vis (b: block) : block =
doVisit vis vis#vblock childrenBlock b
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 3d001b2524b0f7d6fd532cae5bcbdafd2f5a340f..e46dd0eceea1402a7fb1445203ca096edf5c2a54 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -569,7 +569,7 @@ let memo_aux_variable tr counter used_prms vi =
let my_type =
match counter with
| None -> vi.vtype
- | Some _ -> TArray(vi.vtype,None,{scache=Not_Computed},[])
+ | Some _ -> TArray(vi.vtype,None,[])
in
let my_var =
Cil.makeGlobalVar (get_fresh ("aorai_" ^ vi.vname)) my_type
@@ -1152,7 +1152,7 @@ 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,{scache=Not_Computed},[])
+ Cil_types.TArray (Cil.intType,None,[])
else Cil.intType
in (* We won't always need a counter *)
lazy (
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index e248da44020dd21d9765622a0d92ad7301a25ebd..42c19e2aeb1608d5a68bfc6db6dc259fd93a7ba8 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -722,21 +722,34 @@ let rec infer t =
infer t
| TBinOp (MinusPP, t, _) ->
(match Cil.unrollType (get_cty t) with
- | TArray(_, _, { scache = Computed n (* size in bits *) }, _) ->
- (* the second argument must be in the same block than [t]. Consequently
- the result of the difference belongs to [0; \block_length(t)] *)
- let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
- ival Integer.zero (Integer.of_int nb_bytes)
- | TArray _ | TPtr _ ->
+ | TArray(_, _, _) as ta ->
+ begin
+ try
+ let n = Cil.bitsSizeOf ta in
+ (* the second argument must be in the same block than [t].
+ Consequently the result of the difference belongs to
+ [0; \block_length(t)] *)
+ let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+ ival Integer.zero (Integer.of_int nb_bytes)
+ with Cil.SizeOfError _ ->
+ Lazy.force interv_of_unknown_block
+ end
+ | TPtr _ ->
Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tblock_length (_, t)
| Toffset(_, t) ->
(match Cil.unrollType (get_cty t) with
- | TArray(_, _, { scache = Computed n (* size in bits *) }, _) ->
- let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
- singleton_of_int nb_bytes
- | TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
+ | TArray(_, _, _) as ta ->
+ begin
+ try
+ let n = Cil.bitsSizeOf ta in
+ let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+ singleton_of_int nb_bytes
+ with Cil.SizeOfError _ ->
+ Lazy.force interv_of_unknown_block
+ end
+ | TPtr _ -> Lazy.force interv_of_unknown_block
| _ -> assert false)
| Tnull -> singleton_of_int 0
| TLogic_coerce (_, t) -> infer t
@@ -870,7 +883,7 @@ and infer_term_host thost =
| TMem t ->
let ty = Logic_utils.logicCType t.term_type in
match Cil.unrollType ty with
- | TPtr(ty, _) | TArray(ty, _, _, _) ->
+ | TPtr(ty, _) | TArray(ty, _, _) ->
interv_of_typ ty
| _ ->
Options.fatal "unexpected type %a for term %a"
diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 95d7a0cbdec000205aad2f0e0cf25d07716545d8..c512bfa64bca2b89a9bf5e0a1c367a5555e8fc32 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -146,8 +146,8 @@ let do_register_data ~loc kf env { data_ptr } name e =
| TPtr _ -> "ptr", [ e ]
| TArray _ -> "array", [ e ]
| TFun _ -> "fun", []
- | TComp ({ cstruct = true }, _, _) -> "struct", []
- | TComp ({ cstruct = false }, _, _) -> "union", []
+ | TComp ({ cstruct = true }, _) -> "struct", []
+ | TComp ({ cstruct = false }, _) -> "union", []
| TEnum ({ ekind }, _) -> ikind_to_string ekind, [ Cil.one ~loc; e ]
| TVoid _
| TBuiltin_va_list _ -> "other", []
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
index 670c48a1da0740bcbe759ad5e05d1d6a633c2088..51e7f01a4601d950b2968476272a85eaca8a5b6d 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.ml
+++ b/src/plugins/e-acsl/src/code_generator/assigns.ml
@@ -35,7 +35,7 @@ let rec is_ptr_free typ = match Cil.unrollType typ with
| TInt (_, _)
| TFloat (_, _) -> true
| TPtr (_, _) -> false
- | TArray (ty, _, _, _) -> is_ptr_free ty
+ | TArray (ty, _, _) -> is_ptr_free ty
| TFun (_, _, _, _) ->
(* a function cannot be an argument of a function *)
assert false
@@ -44,7 +44,7 @@ let rec is_ptr_free typ = match Cil.unrollType typ with
assert false
| TEnum (_, _)
| TBuiltin_va_list _ -> true
- | TComp (cinfo, _, _) ->
+ | TComp (cinfo, _) ->
match cinfo.cfields with
| None -> raise NoAssigns
| Some fields ->
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 61ee968e4adbfed0dc6942774ce3bbdb89257209..0a8733cbafaec3454019096110574b22c9853c74 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -41,7 +41,7 @@ let length_exp ~loc kf env ~name array =
let elem_typ, array_len =
match Logic_aggr.get_array_typ_opt (Cil.typeOf array) with
| None -> Options.fatal "Trying to retrieve the length of a non-array"
- | Some (t, len, _, _) -> t, len
+ | Some (t, len, _) -> t, len
in
try
let len = Cil.lenOfArray64 array_len 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 05daa0901645a3397d56b893666e7d31af83818c..561199aa97ed7d3679507d33a4a3ec381c4712d5 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -198,7 +198,7 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
in
(* s *)
let ty = match Cil.unrollType (Misc.cty ptr.term_type) with
- | TPtr(ty, _) | TArray(ty, _, _, _) -> ty
+ | TPtr(ty, _) | TArray(ty, _, _) -> ty
| _ -> assert false
in
let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
index a5e7c5fe5aefe466632e806910b562348c4b101b..6bcc645ed33146fae568d5f28a990776299f511a 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml
@@ -38,7 +38,7 @@ let assigns_field ~loc vi name value =
let ty = vi.vtype in
let compinfo =
match Cil.unrollType ty with
- | TComp (compinfo, _, _) -> compinfo
+ | TComp (compinfo, _) -> compinfo
| _ ->
Options.fatal
"type of %a (%a) is not a structure"
@@ -67,7 +67,7 @@ let struct_local_init ~loc vi fields =
let ty = vi.vtype in
let compinfo =
match Cil.unrollType ty with
- | TComp (compinfo, _, _) -> compinfo
+ | TComp (compinfo, _) -> compinfo
| _ ->
Options.fatal
"type of %a (%a) is not a structure"
@@ -175,7 +175,7 @@ let named_store_stmt name ?str_size vi =
let loc = vi.vdecl in
let store = rtl_call ~loc name in
match ty, str_size with
- | TArray(_, Some _,_,_), None ->
+ | TArray(_, Some _,_), None ->
store [ Cil.evar ~loc vi; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size ->
store [ Cil.evar ~loc vi ; size ]
@@ -203,7 +203,7 @@ let delete_stmt ?(is_addr=false) vi =
let loc = vi.vdecl in
let mk = rtl_call ~loc "delete_block" in
match is_addr, Cil.unrollType vi.vtype with
- | _, TArray(_, Some _, _, _) | true, _ -> mk [ Cil.evar ~loc vi ]
+ | _, TArray(_, Some _, _) | true, _ -> mk [ Cil.evar ~loc vi ]
| _ -> mk [ Cil.mkAddrOfVi vi ]
let mark_readonly vi =
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml
index 4a8b24ffe2f99d4854420242e8ae640daf53159b..76b9b82f14bfc551589125ed64b04dd84e49b1db 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.ml
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml
@@ -63,7 +63,6 @@ module Make() = struct
ttype = TArray(
TNamed(!t_struct_torig_ref, []),
Some (Cil.one ~loc:Cil_datatype.Location.unknown),
- { scache = Not_Computed },
[]);
treferenced = true;
}
diff --git a/src/plugins/e-acsl/src/libraries/logic_aggr.ml b/src/plugins/e-acsl/src/libraries/logic_aggr.ml
index ba60807ee51df1303fac0ce2a447e1a186c853d7..e08ca8acbaeffb887cd5de96ff7466103c4c5909 100644
--- a/src/plugins/e-acsl/src/libraries/logic_aggr.ml
+++ b/src/plugins/e-acsl/src/libraries/logic_aggr.ml
@@ -36,7 +36,7 @@ let rec get_array_typ_opt ty =
else
match ty with
| TNamed (r, _) -> get_array_typ_opt r.ttype
- | TArray (t, eo, bsot, a) -> Some (t, eo, bsot, a)
+ | TArray (t, eo, a) -> Some (t, eo, a)
| _ -> None
(** @return true iff the type is an array *)
diff --git a/src/plugins/e-acsl/src/libraries/logic_aggr.mli b/src/plugins/e-acsl/src/libraries/logic_aggr.mli
index dd22c340dbbe73a6b5aa86742dc12cdf9a8bcfd9..b8acfb91f8afc53613fa9b3257ced108a13209a5 100644
--- a/src/plugins/e-acsl/src/libraries/logic_aggr.mli
+++ b/src/plugins/e-acsl/src/libraries/logic_aggr.mli
@@ -25,7 +25,7 @@ open Cil_types
(** Utilities function for aggregate types. *)
val get_array_typ_opt:
- typ -> (typ * exp option * bitsSizeofTypCache * attributes) option
+ typ -> (typ * exp option * attributes) option
(** @return the content of the array type if [ty] is an array, or None
otherwise. *)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 1d24782c859ce33e1d9fcfc0cddb12ccf74705e2..67843ca710078d81b47a8ae81d7a0b9d91ca2586 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1753,7 +1753,7 @@ class main_window () : main_window_extension_points =
let opt_tag_name =
match typ with
| TNamed (ti, _) -> Some (Logic_typing.Typedef, ti.torig_name)
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
let tag = if ci.cstruct then Logic_typing.Struct
else Logic_typing.Union
in
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 4f7eaadff93fcb86334575d288d1f757d3d4efe1..175759021e2de6b12128a14b06107233d801466d 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -321,7 +321,6 @@ module MYTREE = struct
| Dinvariant (li, _) -> Some (global_name li.l_var_info.lv_name)
| Dtype_annot (li, _) -> Some (global_name li.l_var_info.lv_name)
| Dmodel_annot (mf, _) -> Some (global_name mf.mi_name)
- | Dcustom_annot _ -> Some "custom clause"
| Dextended (e,_,_) -> Some ("ACSL extension " ^ (extension_name e))
let make_list_globals hide sort_order globs =
diff --git a/src/plugins/gui/gui_printers.ml b/src/plugins/gui/gui_printers.ml
index 9b0887e126f5af673f4635258380bcf34633c3f2..2da156cdd780427dfc8d222d4ae877da8a25ad96 100644
--- a/src/plugins/gui/gui_printers.ml
+++ b/src/plugins/gui/gui_printers.ml
@@ -97,7 +97,7 @@ let lid_of_loc loc =
E.g. for [t = int***], returns [int]. *)
let rec get_type_specifier (t:typ) =
match t with
- | TPtr (bt, _) | TArray (bt, _, _, _) -> get_type_specifier bt
+ | TPtr (bt, _) | TArray (bt, _, _) -> get_type_specifier bt
| _ -> t
let pp_tcomp_unfolded fmt comp attrs =
@@ -123,14 +123,14 @@ let pp_typ_unfolded fmt (t : typ) =
begin
(* unfolds the typedef, and one step further if it is a TComp/TEnum *)
match ty.ttype with
- | TComp (comp, _, cattrs) ->
+ | TComp (comp, cattrs) ->
pp_tcomp_unfolded fmt comp (Cil.addAttributes attrs cattrs)
| TEnum (enum, eattrs) ->
pp_enum_unfolded fmt enum (Cil.addAttributes attrs eattrs)
| _ ->
Printer.pp_typ fmt (Cil.typeAddAttributes attrs ty.ttype)
end
- | TComp (comp, _, attrs) -> pp_tcomp_unfolded fmt comp attrs
+ | TComp (comp, attrs) -> pp_tcomp_unfolded fmt comp attrs
| TEnum (enum, attrs) -> pp_enum_unfolded fmt enum attrs
| _ -> Printer.pp_typ fmt t
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index d6c84731ce88000100c3e31dced5e99ecc7baea2..de8b7f434f0a16f3ee6c372fcd186bd82a3aea31 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -239,7 +239,6 @@ let translate_history_elt old_helt =
| GAnnot(Dinvariant _,_), GAnnot(Dinvariant _,_)
| GAnnot(Dtype_annot _,_), GAnnot(Dtype_annot _,_)
| GAnnot(Dmodel_annot _,_), GAnnot(Dmodel_annot _,_)
- | GAnnot(Dcustom_annot _,_), GAnnot(Dcustom_annot _,_)
-> (** they have no names *) ()
| _ -> (** different constructors *) ()
in
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index ba6e991a881428f3a5c521004920df9cafbf40ee..73d8c143d88b562fc8391e432765ce74357c4017 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -69,9 +69,9 @@ let rec string_of_typ_aux = function
| TFloat(FLongDouble, _) -> "ldouble"
| TPtr(t, _) -> "ptr_" ^ string_of_typ t
| TEnum (ei, _) -> "e_" ^ ei.ename
- | TComp (ci, _, _) when ci.cstruct -> "st_" ^ ci.cname
- | TComp (ci, _, _) -> "un_" ^ ci.cname
- | TArray (t, Some e, _, _) ->
+ | TComp (ci, _) when ci.cstruct -> "st_" ^ ci.cname
+ | TComp (ci, _) -> "un_" ^ ci.cname
+ | TArray (t, Some e, _) ->
"arr" ^ (string_of_exp e) ^ "_" ^ string_of_typ t
| t ->
Options.fatal "unsupported type %a" Cil_printer.pp_typ t
@@ -114,7 +114,7 @@ let tdivide ?loc t1 t2 =
let ttype_of_pointed t =
match Logic_utils.unroll_type t with
- | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Ctype t
+ | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _)) -> Ctype t
| _ -> Options.fatal "ttype_of_pointed on a non pointer type"
let tbuffer_range ?loc ptr len =
@@ -130,7 +130,7 @@ let rec tunref_range ?loc ptr len =
term (TLval tlval) typ
and tunref_range_unfold ?loc lval typ =
match typ with
- | Ctype(TArray(typ, Some e, _, _)) ->
+ | Ctype(TArray(typ, Some e, _)) ->
let len = Logic_utils.expr_to_term ~coerce:true e in
let last = tminus ?loc len (tinteger ?loc 1) in
let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
@@ -155,7 +155,7 @@ let taccess ?loc ptr offset =
| _ -> Options.fatal "taccess on a non pointer type"
let sizeofpointed = function
- | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _, _)) -> Cil.bytesSizeOf t
+ | Ctype(TPtr(t, _)) | Ctype(TArray(t, _, _)) -> Cil.bytesSizeOf t
| _ -> Options.fatal "size_of_pointed on a non pointer type"
let sizeof = function
@@ -217,7 +217,7 @@ and pall_elems_eq ?loc depth t1 t2 len =
pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
and peq_unfold ?loc depth t1 t2 =
match Logic_utils.unroll_type t1.term_type with
- | Ctype(TArray(_, Some len, _, _)) ->
+ | Ctype(TArray(_, Some len, _)) ->
let len = Logic_utils.expr_to_term ~coerce:true len in
pall_elems_eq ?loc depth t1 t2 len
| _ -> prel ?loc (Req, t1, t2)
@@ -233,7 +233,7 @@ and pall_elems_pred ?loc depth t1 len pred =
pforall ?loc ([ind], (pimplies ?loc (bounds, eq)))
and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
match Logic_utils.unroll_type t1.term_type with
- | Ctype(TArray(_, opt_len, _, _)) ->
+ | Ctype(TArray(_, opt_len, _)) ->
let len =
match opt_len, dyn_len with
| Some len, None -> Logic_utils.expr_to_term ~coerce:true len
@@ -242,7 +242,7 @@ and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
Options.fatal "Unfolding array: cannot find a length"
in
pall_elems_pred ?loc (depth+1) t1 len pred
- | Ctype(TComp(ci, _, _)) ->
+ | Ctype(TComp(ci, _)) ->
pall_fields_pred ?loc depth t1 ci pred
| _ -> pred ?loc t1
and pall_fields_pred ?loc ?(flex_mem_len=None) depth t1 ci pred =
@@ -262,7 +262,7 @@ and pall_fields_pred ?loc ?(flex_mem_len=None) depth t1 ci pred =
let punfold_flexible_struct_pred ?loc the_struct bytes_len pred =
let struct_len = tinteger ?loc (sizeof the_struct.term_type) in
let ci = match the_struct.term_type with
- | Ctype(TComp(ci, _, _) as t) when Cil.has_flexible_array_member t -> ci
+ | Ctype(TComp(ci, _) as t) when Cil.has_flexible_array_member t -> ci
| _ -> Options.fatal "Unfolding flexible on a non flexible structure"
in
let flex_type = Ctype (Extlib.last (Option.get ci.cfields)).ftype in
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index e488ba9e61c68732db77ba52d3cc9621eba803db..68865aa4c84bf819c9d9c750663907fc90ebefe0 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -29,9 +29,9 @@ let unexpected = Options.fatal "Stdlib.Basic_alloc: unexpected: %s"
let valid_size ?loc typ size =
let p = match typ with
- | TComp (ci, _, _) when Cil.has_flexible_array_member typ ->
+ | TComp (ci, _) when Cil.has_flexible_array_member typ ->
let elem = match (last (Option.value ~default:[] ci.cfields)).ftype with
- | TArray(t, _ , _, _) -> tinteger ?loc (Cil.bytesSizeOf t)
+ | TArray(t, _, _) -> tinteger ?loc (Cil.bytesSizeOf t)
| _ -> unexpected "non array last field on flexible structure"
in
let base = tinteger ?loc (Cil.bytesSizeOf typ) in
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index 8a527ca3cfb82f95ecda6ee864af39d3621a5732..7ff01f234adc96c9314df75b0ad27a30e1a6bc56 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -44,14 +44,14 @@ end
let rec any_char_composed_type t =
match t with
| t when Cil.isAnyCharType t -> true
- | TArray(t, _, _, _) -> any_char_composed_type t
+ | TArray(t, _, _) -> any_char_composed_type t
| _ -> false
let rec base_char_type t =
assert (any_char_composed_type t) ;
match t with
| t when Cil.isAnyCharType t -> t
- | TArray(t, _, _, _) -> base_char_type t
+ | TArray(t, _, _) -> base_char_type t
| _ -> assert false
@@ -186,11 +186,11 @@ let memset_value e =
let rec contains_union_type t =
match Cil.unrollType t with
- | TComp({ cstruct = false }, _, _) ->
+ | TComp({ cstruct = false }, _) ->
true
- | TComp({ cfields = Some fields }, _, _) ->
+ | TComp({ cfields = Some fields }, _) ->
List.exists contains_union_type (List.map (fun f -> f.ftype) fields)
- | TArray(t, _, _, _) ->
+ | TArray(t, _, _) ->
contains_union_type t
| _ -> false
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 315698ea973cbc168f0fd59e634f9b33257602a9..c5bcdaeeddad81d07dee522a05b3c46552bb4f8b 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -116,7 +116,6 @@ class metricsCabsVisitor = object(self)
| PRAGMA _
| STATIC_ASSERT _
| LINKAGE _
- | CUSTOM _
| GLOBANNOT _ -> Cil.DoChildren;
method! vexpr expr =
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index ba9c014025a4da2270e8c782cbf0b5987bec0561..6cef7e541ab3fe1d2e2f7b6e0c97343e2bd64307 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -326,7 +326,6 @@ class slocVisitor ~libc : sloc_visitor = object(self)
| Dinvariant (toto, _) -> toto.l_var_info.lv_name
| Dtype_annot (ta, _) -> ta.l_var_info.lv_name
| Dmodel_annot (mi, _) -> mi.mi_name
- | Dcustom_annot (_c, _n, _, _) -> " (Custom) "
| Dextended ({ext_name}, _, _) -> " (Extension " ^ ext_name ^ ")"
end
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
index 6b3f9d0343eedbd928d8ca292d0bf3bcca43689e..448af313ea283befccaa4f5f45e872f423153a86 100644
--- a/src/plugins/reduc/collect.ml
+++ b/src/plugins/reduc/collect.ml
@@ -80,14 +80,14 @@ end
let rec collect_off typ =
match typ with
| TInt _ | TFloat _ -> [ NoOffset ]
- | TComp ({cfields = Some flds}, _, _) ->
+ | TComp ({cfields = Some flds}, _) ->
List.fold_left collect_fields [] flds
- | TArray (arrtyp, e_opt, _, _) ->
+ | TArray (arrtyp, e_opt, _) ->
debug "Array of length %a" (Pretty_utils.pp_opt Printer.pp_exp) e_opt;
begin try collect_array arrtyp [] (Cil.lenOfArray64 e_opt)
with Cil.LenOfArray -> [] end
| TVoid _ | TFun _ | TPtr _ | TEnum _ | TNamed _ | TBuiltin_va_list _
- | TComp ({cfields = None}, _, _)-> []
+ | TComp ({cfields = None}, _)-> []
and collect_fields acc fld =
let offs = collect_off fld.ftype in
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index b1d99f4d05903c1c5a1271ab1f66c6c8792fe92f..1e027d5d5f170a4c2463d74a83296d85c2cab93d 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -84,7 +84,7 @@ let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
check_array_access default off fi.ftype true
| Index (e, off) ->
match Cil.unrollType typ with
- | TArray (bt, Some size, _, _) ->
+ | TArray (bt, Some size, _) ->
if Kernel.SafeArrays.get () || not in_struct then begin
(* Generate an assertion for this access, then go deeper in
case other accesses exist *)
@@ -95,7 +95,7 @@ let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
[-unsafe-arrays]. Honor the option and generate only
the default [\valid] assertion *)
check_array_access true off bt in_struct
- | TArray (bt, None, _, _) -> check_array_access true off bt in_struct
+ | TArray (bt, None, _) -> check_array_access true off bt in_struct
| _ -> assert false
in
match lv with
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 2beb56b02391c49ee0a3bbd6b49f5ee3b87a567b..aca7884a975a08ddca485c64df4748b3394fe69e 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -62,7 +62,7 @@ class collect_visitor = object (self)
debug "add used enum %s@." ei.ename;
Hashtbl.add used_enuminfo ei.ename (); DoChildren
end
- | TComp(ci,_,_) ->
+ | TComp(ci,_) ->
if Hashtbl.mem used_compinfo ci.cname then SkipChildren
else begin
debug "add used comp %s@." ci.cname;
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 177c7f980d55a010df054ee50392ffaa2b057dd8..dd27fe5eca32e88f8c9f79e491182deb7a6d29bb 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -234,22 +234,22 @@ let guess_intended_malloc_type stack sizev constant_size =
let type_from_nb_elems tsize =
let typ = tsize.elem_typ in
match tsize.nb_elems with
- | None -> TArray (typ, None, Cil.empty_size_cache (), [])
+ | None -> TArray (typ, None, [])
| Some nb ->
if Int.equal Int.one nb
then typ
else
let loc = Cil.CurrentLoc.get () in
let esize_arr = Cil.kinteger64 ~loc nb in (* [nb] fits in size_t *)
- TArray (typ, Some esize_arr, Cil.empty_size_cache (), [])
+ TArray (typ, Some esize_arr, [])
(* Generalize a type into an array type without size. Useful for variables
whose size is mutated. *)
let weaken_type typ =
match Cil.unrollType typ with
- | TArray (_, None, _, _) -> typ
- | TArray (typ, Some _, _, _) | typ ->
- TArray (typ, None, Cil.empty_size_cache (), [])
+ | TArray (_, None, _) -> typ
+ | TArray (typ, Some _, _) | typ ->
+ TArray (typ, None, [])
(* size for which the base is certain to be valid *)
let size_sure_valid b = match Base.validity b with
@@ -381,7 +381,7 @@ let string_of_region = function
let create_weakest_base region =
let stack = [ fst (Globals.entry_point ()), Kglobal ] in
let type_base =
- TArray (Cil.charType, None, Cil.empty_size_cache (), [])
+ TArray (Cil.charType, None, [])
in
let var = create_new_var stack "alloc" type_base Weak in
Value_parameters.warning ~wkey:wkey_imprecise_alloc ~current:true ~once:true
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index c1b59f768dfa5a9877f07e581ae1997ca39670cb..6309adb64fb18947419e58d53a12c82ffc069644 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -439,16 +439,16 @@ let memset_typ_offsm_int full_typ i =
(* Do not produce NaN or infinites here (unless they are accepted
by the engine). *)
if Fval.is_finite f = True then update size v' else update size v
- | TComp ({ cstruct = true ; cfields = l}, _, _) -> (* struct *)
+ | TComp ({ cstruct = true ; cfields = l}, _) -> (* struct *)
let aux_field offsm fi =
let offset_fi = Int.of_int (fst (Cil.fieldBitsOffset fi)) in
aux fi.ftype (Int.add offset offset_fi) offsm
in
List.fold_left aux_field offsm (Option.value ~default:[] l)
- | TComp ({ cstruct = false ; cfields = l}, _, _) -> (* union *)
+ | TComp ({ cstruct = false ; cfields = l}, _) -> (* union *)
(* Use only the first field. This is somewhat arbitrary *)
aux (List.hd (Option.get l)).ftype offset offsm
- | TArray (typelt, nb, _, _) -> begin
+ | TArray (typelt, nb, _) -> begin
let nb = Cil.lenOfArray64 nb in (* always succeeds, we computed the
size of the entire type earlier *)
if Integer.(gt nb zero) then begin
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 58725f9e485194a4728aa0724c1a5ed92bd30b7b..d6cecc8bb7e738f2d54184f7b805db51b2998ddf 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -98,7 +98,7 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
let reject_empty_struct b offset typ =
match Cil.unrollType typ with
- | TComp (ci, _, _) ->
+ | TComp (ci, _) ->
if ci.cfields = Some [] && not (Cil.acceptEmptyCompinfo ()) then
Value_parameters.abort ~current:true
"@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \
@@ -147,7 +147,6 @@ let initialize_var_using_type varinfo state =
let arr_pointed_typ =
TArray(typ,
Some (Cil.kinteger64 ~loc:varinfo.vdecl i),
- Cil.empty_size_cache (),
[])
in
let hidden_var_name =
@@ -197,7 +196,7 @@ let initialize_var_using_type varinfo state =
| true, true -> assert false (* inconsistent *)
end
- | TArray (typ, len, _, _) ->
+ | TArray (typ, len, _) ->
begin try
let size = Cil.lenOfArray len in
let size_elt = Integer.of_int (Cil.bitsSizeOf typ) in
@@ -300,7 +299,7 @@ let initialize_var_using_type varinfo state =
bind_entire_loc Cvalue.V.top_int;
end
- | TComp ({cstruct=true;} as compinfo, _, _) -> (* Struct *)
+ | TComp ({cstruct=true;} as compinfo, _) -> (* Struct *)
reject_empty_struct b offset_orig typ;
let treat_field state field =
match field.fbitfield with
@@ -321,7 +320,7 @@ let initialize_var_using_type varinfo state =
bind_entire_loc Cvalue.V.top_int;
end
- | TComp ({cstruct=false}, _, _) when Cil.is_fully_arithmetic typ ->
+ | TComp ({cstruct=false}, _) when Cil.is_fully_arithmetic typ ->
reject_empty_struct b offset_orig typ;
(* Union of arithmetic types *)
bind_entire_loc Cvalue.V.top_int
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 0e2a13fd90ec36d6cc41ae61740b9c272e18229d..9a171581a4fc9e7865ee0433a1c36c778d9c2ef7 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -1034,7 +1034,7 @@ module Make
| NoOffset -> return (Loc.no_offset, typ, false)
| Index (index_expr, remaining) ->
let typ_pointed, array_size = match Cil.unrollType typ with
- | TArray (t, size, _, _) -> t, size
+ | TArray (t, size, _) -> t, size
| t -> Value_parameters.fatal ~current:true
"Got type '%a'" Printer.pp_typ t
in
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 27a16ec4928a4fd6f33be06c4e7a69e9fcecf97c..b458e4be0ccf9759546b73bcc5cc40115d24f441 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1672,7 +1672,7 @@ and eval_toffset ~alarm_mode env typ toffset =
empty = false; }
| TIndex (idx, remaining) ->
let typ_e, size = match Cil.unrollType typ with
- | TArray (t, size, _, _) -> t, size
+ | TArray (t, size, _) -> t, size
| _ -> ast_error "index on a non-array"
in
let idx = constraint_trange idx size in
diff --git a/src/plugins/value/utils/eval_typ.ml b/src/plugins/value/utils/eval_typ.ml
index 01c976e7a6bfba8b47117219ed521a9cc85a5746..abbfccf9ed65c716e56277bce67fd825b4f43814 100644
--- a/src/plugins/value/utils/eval_typ.ml
+++ b/src/plugins/value/utils/eval_typ.ml
@@ -78,7 +78,7 @@ let is_compatible_function ~typ_pointed ~typ_fun =
Cil.isSigned ik1 = Cil.isSigned ik2 &&
Cil.bitsSizeOfInt ik1 = Cil.bitsSizeOfInt ik2
| TFloat (fk1, _), TFloat (fk2, _) -> fk1 = fk2
- | TComp (ci1, _, _), TComp (ci2, _, _) ->
+ | TComp (ci1, _), TComp (ci2, _) ->
Cil_datatype.Compinfo.equal ci1 ci2
| _ -> false
in
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 602702acd66bbaaab44efbb5d1bf7e70b024278a..c2c63c2dff907c792e9efb14e3a2de9d65ff1dea 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -289,7 +289,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
| Field (fi, off) -> aux_offset fi.ftype off
| Index (idx, off) -> begin
match Cil.unrollType typ with
- | TArray (typ_e, size, _, _) -> begin
+ | TArray (typ_e, size, _) -> begin
aux_offset typ_e off;
try
let size = Cil.lenOfArray64 size in
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 777e49b571ffdd246d66d329319d75c9a2e0fdf0..1d1d75ff0d7d9e1712064b3a7ec7ab757c3aa3a3 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -193,7 +193,7 @@ module V = struct
if o = NoOffset then
let o' = match Cil.unrollType typ_base with
| TArray _ -> Index (Cil.(zero Cil_builtins.builtinLoc), NoOffset)
- | TComp (ci, _, _) -> Field (List.hd (Option.get ci.cfields), NoOffset)
+ | TComp (ci, _) -> Field (List.hd (Option.get ci.cfields), NoOffset)
| _ -> raise Bit_utils.NoMatchingOffset
in o', ok
else o, ok
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index fbe8497770d7b38725a7b4332cc0b06e50dada25..f2fd26fac784cc6ed0341290b6319f28852bdf16 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -66,7 +66,7 @@ let mk_aggregator env fun_name a_pos pname a_type =
(* Get the aggregate type of elements *)
let _,ptyp,_ = List.nth params a_pos in
let a_param = pname, match ptyp with
- | TArray (typ,_,_,_)
+ | TArray (typ,_,_)
| TPtr (typ, _) -> typ
| _ ->
Self.warning ~current:true
diff --git a/src/plugins/variadic/environment.ml b/src/plugins/variadic/environment.ml
index 0fb7737edb8a8731e725fe06ea1dfaef5bde0536..8be3b2d3c4f664d886dc9417b66ff3ac344b6166 100644
--- a/src/plugins/variadic/environment.ml
+++ b/src/plugins/variadic/environment.ml
@@ -84,9 +84,9 @@ let find_type (env : t) (namespace : Logic_typing.type_namespace)
| Logic_typing.Typedef ->
TNamed (find_typedef env tname, [])
| Logic_typing.Struct ->
- TComp (find_struct env tname, {scache=Not_Computed}, [])
+ TComp (find_struct env tname, [])
| Logic_typing.Union ->
- TComp (find_union env tname, {scache=Not_Computed}, [])
+ TComp (find_union env tname, [])
| Logic_typing.Enum ->
TEnum (find_enum env tname, [])
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index 3e4a54ca47cbf8dae2803864a313f97290f61f20..0d3faf7370690d6520fe523710e6f9436d8563f4 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -34,11 +34,11 @@ open Lang.F
module WpLog = Wp_parameters
let constfold_ctyp = function
- | TArray (_,Some {enode = (Const CInt64 _) },_,_) as ct -> ct
- | TArray (ty,Some len,cache,attr) as ct -> begin
+ | TArray (_,Some {enode = (Const CInt64 _) },_) as ct -> ct
+ | TArray (ty,Some len,attr) as ct -> begin
match Cil.constFold true len with
| {enode = (Const CInt64 _) } as len ->
- TArray(ty,Some len,cache,attr)
+ TArray(ty,Some len,attr)
| _ -> ct
end
| ct -> ct
@@ -496,10 +496,10 @@ struct
let ct = constfold_ctyp ct in
let acc = (* updated acc with default init of structure *)
match ct with
- | TComp ( { cfields = None },_,_) ->
+ | TComp ( { cfields = None },_) ->
Wp_parameters.fatal
"Initializer for incomplete type %a" Cil_printer.pp_typ ct
- | TComp ( { cstruct ; cfields = Some fields },_,_)
+ | TComp ( { cstruct ; cfields = Some fields },_)
when cstruct && (* not for union... *)
(List.length initl) < (List.length fields) ->
(* default init for unintialized field of a struct *)
@@ -522,7 +522,7 @@ struct
| _ -> acc
in
match ct with
- | TArray (ty,len,_,_) ->
+ | TArray (ty,len,_) ->
let delayed =
match len with (* number of required elements *)
| Some {enode = (Const CInt64 (size,_,_))} ->
diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index f001bf763bb000df5c4e3e6c3ca774711c7c3fbf..004028084d65997cfbce96a8ecee066cb7415a5e 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -68,7 +68,7 @@ struct
let index ty =
match Cil.unrollType ty with
- | TArray(te,n,_,_) ->
+ | TArray(te,n,_) ->
begin
match Option.bind n Ctypes.get_int with
| None -> failwith "Wp.Layout: unkown array size"
@@ -96,7 +96,7 @@ struct
let typ_of_comp cache comp =
try H.find cache comp with Not_found ->
- let typ = TComp(comp,Cil.empty_size_cache (),[]) in
+ let typ = TComp(comp,[]) in
H.add cache comp typ ; typ
let field_offset _cache fd =
@@ -489,7 +489,7 @@ struct
let rec get_dim s rds typ =
if s = Cil.bitsSizeOf typ then Some (List.rev rds) else
match Cil.unrollType typ with
- | TArray( te , Some e , _ , _ ) ->
+ | TArray( te , Some e , _ ) ->
begin match Ctypes.get_int e with
| None -> None
| Some n -> get_dim s (if n = 1 then rds else n::rds) te
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index c499f8273512dfd0d37bdadeb87968c4c66e8366..73c014d98693b1db3d65e66adeb477c644091570 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -418,7 +418,6 @@ class visitor =
| Dvolatile _
| Dmodel_annot _
- | Dcustom_annot _
| Dextended _
-> SkipChildren
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 9d845883439b776bee5ede25aea258c3f81e3c0a..8bf846d8d084393897f903a8b04b0bbe2f2edf60 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1180,14 +1180,14 @@ struct
| TInt _ | TFloat _ | TVoid _ | TEnum _ | TNamed _ | TBuiltin_va_list _
-> F.p_true
| TPtr _ | TFun _ -> phi v
- | TComp({ cfields = None },_,_) ->
+ | TComp({ cfields = None },_) ->
F.p_true
- | TComp({ cfields = Some fields },_,_) ->
+ | TComp({ cfields = Some fields },_) ->
F.p_all
(fun fd ->
forall_pointers phi (e_getfield v (Cfield (fd, KValue))) fd.ftype)
fields
- | TArray(elt,_,_,_) ->
+ | TArray(elt,_,_) ->
let k = Lang.freshvar Qed.Logic.Int in
F.p_forall [k] (forall_pointers phi (e_get v (e_var k)) elt)
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index 08cf3b9e386295e0ee4a6e1b9e837c9f82432f68..b8b16aa0c91609a331d673f6033ddca622279ba3 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -254,7 +254,7 @@ let isIndexType t =
let getCompoundType env ~loc typ =
match Cil.unrollType typ with
- | TComp(comp,_,_) -> comp
+ | TComp(comp,_) -> comp
| _ -> error env ~loc "Expected compound type for term"
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 38513f4d9802ccb03089d5f67750b120f28eec31..cdf647d13bec57f4b12eed8dcf16e004e201d1bf 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -266,7 +266,7 @@ let get_int64 e =
let dimension t =
let rec flat k d = function
| TNamed (r,_) -> flat k d r.ttype
- | TArray(ty,Some e,_,_) ->
+ | TArray(ty,Some e,_) ->
flat (succ k) (Int64.mul d (constant e)) ty
| te -> k , d , te
in flat 1 Int64.one t
@@ -286,8 +286,8 @@ let rec object_of typ =
| TPtr(typ,_) -> C_pointer (if Cil.isVoidType typ then Cil.charType else typ)
| TFun _ -> C_pointer Cil.voidType
| TEnum ({ekind=i},_) -> C_int (c_int i)
- | TComp (comp,_,_) -> C_comp comp
- | TArray (typ_elt,e_opt,_,_) ->
+ | TComp (comp,_) -> C_comp comp
+ | TArray (typ_elt,e_opt,_) ->
begin
match array_size e_opt with
| None ->
@@ -470,7 +470,7 @@ let sizeof_defined = function
| C_array { arr_flat = None } -> false
| _ -> true
-let typ_comp cinfo = TComp(cinfo,Cil.empty_size_cache(),[])
+let typ_comp cinfo = TComp(cinfo,[])
let bits_sizeof_comp cinfo = Cil.bitsSizeOf (typ_comp cinfo)
@@ -479,7 +479,7 @@ let bits_sizeof_array ainfo =
| Some a ->
let csize = Cil.kinteger64
~loc:Cil_builtins.builtinLoc (Z.of_int64 a.arr_cell_nbr) in
- let ctype = TArray(a.arr_cell,Some csize,Cil.empty_size_cache(),[]) in
+ let ctype = TArray(a.arr_cell,Some csize,[]) in
Cil.bitsSizeOf ctype
| None ->
if WpLog.ExternArrays.get () then
diff --git a/tests/crowbar/complete_type.ml b/tests/crowbar/complete_type.ml
index 3cae6790456519071aa9351c84a579e9a6c67317..dec73a79cc1c746fef65bdf4ad218d157f2ee6f0 100644
--- a/tests/crowbar/complete_type.ml
+++ b/tests/crowbar/complete_type.ml
@@ -44,7 +44,7 @@ let mk_array_type (is_gcc, typ, types, kind) length =
let length =
Option.map (Cil.kinteger ~loc Cil.(theMachine.kindOfSizeOf)) length
in
- (is_gcc, TArray (typ, length, { scache = Not_Computed }, []), types, kind)
+ (is_gcc, TArray (typ, length, []), types, kind)
let mk_named_type (is_gcc, ttype, types, kind) =
let tname = type_name () in
@@ -89,7 +89,7 @@ let mk_comp_type
if nb_fields = 0 then GCompTagDecl (compinfo, loc)
else GCompTag (compinfo,loc)
in
- (is_gcc, TComp (compinfo, { scache = Not_Computed }, []), glob :: types, kind)
+ (is_gcc, TComp (compinfo, []), glob :: types, kind)
let mk_enum_type is_def is_gcc =
let ename = type_name () in
diff --git a/tests/crowbar/mutable.ml b/tests/crowbar/mutable.ml
index 2ce2ae6d5995f0bcdb2ccd5ed4aadacbb1164d28..0ff13ea6c49cf7c488932b2a100a5cfb5eb4ab65 100644
--- a/tests/crowbar/mutable.ml
+++ b/tests/crowbar/mutable.ml
@@ -53,13 +53,13 @@ let mk_composite_type field_kind (subtypes, subkind) =
let typ_attr = tattr_of_kind field_kind in
let subtype = List.hd subtypes in
let kind = merge_kind field_kind subkind in
- let field_type = TComp (subtype, { scache = Not_Computed }, typ_attr) in
+ let field_type = TComp (subtype, typ_attr) in
(mk_type field_type field_attr) :: subtypes, kind
let rec mk_offset { cfields } =
let field = List.hd cfields in
let offset =
- match field.ftype with TComp(comp,_,_) -> mk_offset comp | _ -> NoOffset
+ match field.ftype with TComp(comp,_) -> mk_offset comp | _ -> NoOffset
in
Field (field, offset)
@@ -84,7 +84,7 @@ let generate_failure_file is_const =
let fmt = Format.formatter_of_out_channel out in
let typ = List.hd types in
let x =
- Cil.makeGlobalVar "x" (TComp (typ, { scache = Not_Computed }, []))
+ Cil.makeGlobalVar "x" (TComp (typ, []))
in
let y =
Cil.makeGlobalVar "y" (TInt (IInt,[]))
@@ -124,7 +124,7 @@ let test (types, kind) =
let out_type = List.hd types in
let offset = mk_offset out_type in
let inner_type =
- Cil.typeOffset (TComp (out_type, { scache = Not_Computed }, [])) offset
+ Cil.typeOffset (TComp (out_type, [])) offset
in
match kind with
| NoAttr | Mutable ->
diff --git a/tests/crowbar/offset_anonymous_field.ml b/tests/crowbar/offset_anonymous_field.ml
index a5357631574cfa2344a05507563a68a669d39dc5..f62efd3a1f9724256d417a984f5143ffa9470da6 100644
--- a/tests/crowbar/offset_anonymous_field.ml
+++ b/tests/crowbar/offset_anonymous_field.ml
@@ -101,14 +101,14 @@ let mk_composite_type choice cstruct res1 anon1 res2 anon2 res3 anon3 =
let offsets =
lift_offset cstruct res1 anon1 field1 res2 anon2 field2 res3 anon3 field3
in
- let mytype = TComp (info, { scache = Not_Computed }, []) in
+ let mytype = TComp (info, []) in
let structs = info :: res1.structs @ res2.structs @ res3.structs in
{ designator; mytype; structs; offsets }
let rec mk_offset { cfields } =
let field = List.hd cfields in
let offset =
- match field.ftype with TComp(comp,_,_) -> mk_offset comp | _ -> NoOffset
+ match field.ftype with TComp(comp,_) -> mk_offset comp | _ -> NoOffset
in
Field (field, offset)
@@ -139,7 +139,7 @@ let generate_failure_file =
let fmt = Format.formatter_of_out_channel out in
let typ = List.hd types in
let x =
- Cil.makeGlobalVar "x" (TComp (typ, { scache = Not_Computed }, []))
+ Cil.makeGlobalVar "x" (TComp (typ, []))
in
let lvx = Var x, offset in
let typ = Cil.typeOfLval lvx in
diff --git a/tests/libc/check_libc_anonymous_tags.ml b/tests/libc/check_libc_anonymous_tags.ml
index 96910a7f5614aff8ce8eb1fd6ea2a5364f454540..c57db98104c49e29b04fa97b48f459248f6b4fd9 100644
--- a/tests/libc/check_libc_anonymous_tags.ml
+++ b/tests/libc/check_libc_anonymous_tags.ml
@@ -38,7 +38,7 @@ class tags_visitor = object
Kernel.warning ~current:true ~once:true
"anonymous enum in Frama-C stdlib";
()
- | TComp (ci, _, _) when ci.corig_name = "" && !in_stdlib ->
+ | TComp (ci, _) when ci.corig_name = "" && !in_stdlib ->
Kernel.warning ~current:true ~once:true
"anonymous %s in Frama-C stdlib"
(if ci.cstruct then "struct" else "union")
diff --git a/tests/misc/exception.ml b/tests/misc/exception.ml
index b057828398230dd11276504b14b858067a38e390..0f5029a48ab9aa00c90f2c2f913c613760390768 100644
--- a/tests/misc/exception.ml
+++ b/tests/misc/exception.ml
@@ -30,7 +30,7 @@ let add_throw_test f exn_type test init =
let add_my_exn my_exn f =
let c = Cil.evar (List.hd f.sformals) in
- let exn_type = TComp(my_exn,{ scache = Not_Computed},[]) in
+ let exn_type = TComp(my_exn,[]) in
let loc = Cil_datatype.Location.unknown in
let init =
CompoundInit(
@@ -59,8 +59,8 @@ let add_int_ptr_exn glob f =
add_throw_test f Cil.intPtrType test init
let add_catch my_exn my_exn2 f =
- let exn_type = TComp(my_exn, { scache = Not_Computed }, []) in
- let exn_type2 = TComp(my_exn2, {scache = Not_Computed }, []) in
+ let exn_type = TComp(my_exn, []) in
+ let exn_type2 = TComp(my_exn2, []) in
let exn_field = Field (List.hd (Option.get my_exn.cfields), NoOffset) in
let exn2_field = Field (List.hd (Option.get my_exn2.cfields), NoOffset) in
let loc = Cil_datatype.Location.unknown in
@@ -177,5 +177,3 @@ let () = Frontc.add_syntactic_transformation add_exn_cabs
let add_exn_cat = File.register_code_transformation_category "add_exn"
let () = File.add_code_transformation_before_cleanup add_exn_cat add_exn
-
-
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index 4f307bc08e320c54251ce0bdc10c3218f3b2399c..a4715ea3d0a87386c4ab6add6fb877e37c9bf7fe 100644
--- a/tests/syntax/ghost_cv_var_decl.ml
+++ b/tests/syntax/ghost_cv_var_decl.ml
@@ -24,7 +24,7 @@ and in_array_ghost_status fmt lval =
Format.fprintf fmt "%a" ghost_status lval
and comp_ghost_status fmt lval =
match Cil.typeOfLval lval with
- | TComp({ cfields }, _, _) ->
+ | TComp({ cfields }, _) ->
Format.fprintf fmt "{ " ;
List.iter (field_ghost_status fmt lval) (Option.value ~default:[] cfields) ;
Format.fprintf fmt " }"