diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b4c42752be638a6b7cdd8ba9e550ce1b5208ad34..71cc190bbc9f1e001a4ca8e231d52803b3c01de2 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -46,9 +46,6 @@
(* Type check and elaborate ABS to CIL *)
(* The references to ISO means ANSI/ISO 9899-1999 *)
-module A = Cabs
-module C = Cabshelper
-module V = Cabsvisit
module H = Hashtbl
module IH = Datatype.Int.Hashtbl
@@ -193,14 +190,14 @@ let is_stdlib_function_macro n = List.mem n no_suppress_function_macro
let is_stdlib_macro n = List.mem n no_redefine_macro
let is_bitwise_bop = function
- | A.BAND | A.BOR | A.XOR -> true
+ | Cabs.BAND | Cabs.BOR | Cabs.XOR -> true
| _ -> false
let is_relational_bop = function
| EQ | NE | LT | GT | LE | GE -> true
| _ -> false
-let rec stripParen = function { expr_node = A.PAREN e } -> stripParen e | e -> e
+let rec stripParen = function { expr_node = Cabs.PAREN e } -> stripParen e | e -> e
let rec is_dangerous_offset = function
NoOffset -> false
@@ -728,8 +725,8 @@ let check_logical_operand e t =
"operand of bitwise operator has boolean type"
| _ ->
let rec aux = function
- | { expr_node = A.PAREN e} -> aux e
- | { expr_node = A.BINARY (bop,_,_); expr_loc = (source, _) }
+ | { expr_node = Cabs.PAREN e} -> aux e
+ | { expr_node = Cabs.BINARY (bop,_,_); expr_loc = (source, _) }
when is_relational_bop bop ->
Kernel.warning ~wkey:Kernel.wkey_cert_exp_46 ~source
"operand of bitwise operator is a logical relation"
@@ -1066,8 +1063,8 @@ let newAlphaName
(*** In order to process GNU_BODY expressions we must record that a given
*** COMPUTATION is interesting *)
-let gnu_body_result : (A.statement * ((exp * typ) option ref)) ref
- = ref ({stmt_ghost = false; stmt_node = A.NOP (cabslu "_NOP")}, ref None)
+let gnu_body_result : (Cabs.statement * ((exp * typ) option ref)) ref
+ = ref ({stmt_ghost = false; stmt_node = Cabs.NOP (cabslu "_NOP")}, ref None)
(*** When we do statements we need to know the current return type *)
let dummy_function = emptyFunction "@dummy@"
@@ -2320,8 +2317,8 @@ let lookupLabel ghost l =
| _ -> raise Not_found
with Not_found -> l
-class gatherLabelsClass : V.cabsVisitor = object (self)
- inherit V.nopCabsVisitor
+class gatherLabelsClass : Cabsvisit.cabsVisitor = object (self)
+ inherit Cabsvisit.nopCabsVisitor
(* We have to know if a label is local to know if it is an error if
* another label with the same name exists. But a local label can be
@@ -2380,12 +2377,12 @@ end
duplicate labels when unfolding short-circuiting logical operators
and when creating labels for (some) continue statements. *)
class registerLabelsVisitor = object
- inherit V.nopCabsVisitor
+ inherit Cabsvisit.nopCabsVisitor
method! vstmt s =
- let currentLoc = convLoc (C.get_statementloc s) in
+ let currentLoc = convLoc (Cabshelper.get_statementloc s) in
(match s.stmt_node with
- | A.LABEL (lbl,_,_) ->
+ | Cabs.LABEL (lbl,_,_) ->
Alpha.registerAlphaName alphaTable (kindPlusName "label" lbl) currentLoc
| _ -> ());
DoChildren
@@ -3778,31 +3775,31 @@ let findField n comp =
(* Utility ***)
let rec replaceLastInList
- (lst: A.expression list)
- (how: A.expression -> A.expression) : A.expression list=
+ (lst: Cabs.expression list)
+ (how: Cabs.expression -> Cabs.expression) : Cabs.expression list=
match lst with
| [] -> []
| [e] -> [how e]
| h :: t -> h :: replaceLastInList t how
-let convBinOp (bop: A.binary_operator) : binop =
+let convBinOp (bop: Cabs.binary_operator) : binop =
match bop with
- | A.ADD -> PlusA
- | A.SUB -> MinusA
- | A.MUL -> Mult
- | A.DIV -> Div
- | A.MOD -> Mod
- | A.BAND -> BAnd
- | A.BOR -> BOr
- | A.XOR -> BXor
- | A.SHL -> Shiftlt
- | A.SHR -> Shiftrt
- | A.EQ -> Eq
- | A.NE -> Ne
- | A.LT -> Lt
- | A.LE -> Le
- | A.GT -> Gt
- | A.GE -> Ge
+ | Cabs.ADD -> PlusA
+ | Cabs.SUB -> MinusA
+ | Cabs.MUL -> Mult
+ | Cabs.DIV -> Div
+ | Cabs.MOD -> Mod
+ | Cabs.BAND -> BAnd
+ | Cabs.BOR -> BOr
+ | Cabs.XOR -> BXor
+ | Cabs.SHL -> Shiftlt
+ | Cabs.SHR -> Shiftrt
+ | Cabs.EQ -> Eq
+ | Cabs.NE -> Ne
+ | Cabs.LT -> Lt
+ | Cabs.LE -> Le
+ | Cabs.GT -> Gt
+ | Cabs.GE -> Ge
| _ -> Kernel.fatal ~current:true "convBinOp"
(**** PEEP-HOLE optimizations ***)
@@ -3907,7 +3904,7 @@ let afterConversion ~ghost (c: chunk) : chunk =
res
(***** Try to suggest a name for the anonymous structures *)
-let suggestAnonName (nl: A.name list) =
+let suggestAnonName (nl: Cabs.name list) =
match nl with
| [] -> ""
| (n, _, _, _) :: _ -> n
@@ -4085,10 +4082,10 @@ type local_env =
{ authorized_reads: Lval.Set.t;
known_behaviors: string list;
is_ghost: bool;
- is_paren: bool; (* true for expressions whose parent is A.PAREN *)
+ is_paren: bool; (* true for expressions whose parent is Cabs.PAREN *)
inner_paren: bool
(* used during unop/binop traversal to distinguish between
- A.PAREN (A.UNOP(...)) and A.UNOP(A.PAREN(...)) *)
+ Cabs.PAREN (Cabs.UNOP(...)) and Cabs.UNOP(Cabs.PAREN(...)) *)
}
let empty_local_env =
@@ -4467,10 +4464,10 @@ let rec doSpecList ghost (suggestedAnonName: string)
(* This string will be part of
* the names for anonymous
* structures and enums *)
- (specs: A.spec_elem list)
+ (specs: Cabs.spec_elem list)
(* Returns the base type, the storage, whether it is inline and the
* (unprocessed) attributes *)
- : typ * storage * bool * A.attribute list =
+ : typ * storage * bool * Cabs.attribute list =
(* Do one element and collect the type specifiers *)
let isinline = ref false in (* If inline appears *)
(* The storage is placed here *)
@@ -4482,37 +4479,37 @@ let rec doSpecList ghost (suggestedAnonName: string)
* qualifiers never apply to structures (ISO 6.7.3), whereas GCC
* attributes always do (GCC manual 4.30). Therefore, they are
* collected and processed separately. *)
- let attrs : A.attribute list ref = ref [] in (* __attribute__, etc. *)
- let cvattrs : A.cvspec list ref = ref [] in (* const/volatile *)
+ let attrs : Cabs.attribute list ref = ref [] in (* __attribute__, etc. *)
+ let cvattrs : Cabs.cvspec list ref = ref [] in (* const/volatile *)
let suggestedAnonName =
if suggestedAnonName <> "" then suggestedAnonName
else if get_current_stdheader () = "" then ""
else "fc_stdlib"
in
- let doSpecElem (se: A.spec_elem)
- (acc: A.typeSpecifier list)
- : A.typeSpecifier list =
+ let doSpecElem (se: Cabs.spec_elem)
+ (acc: Cabs.typeSpecifier list)
+ : Cabs.typeSpecifier list =
match se with
- | A.SpecTypedef -> acc
- | A.SpecInline -> isinline := true; acc
- | A.SpecStorage st ->
+ | Cabs.SpecTypedef -> acc
+ | Cabs.SpecInline -> isinline := true; acc
+ | Cabs.SpecStorage st ->
if !storage <> NoStorage then
Kernel.error ~once:true ~current:true "Multiple storage specifiers";
let sto' =
match st with
- | A.NO_STORAGE -> NoStorage
- | A.AUTO -> NoStorage
- | A.REGISTER -> Register
- | A.STATIC -> Static
- | A.EXTERN -> Extern
+ | Cabs.NO_STORAGE -> NoStorage
+ | Cabs.AUTO -> NoStorage
+ | Cabs.REGISTER -> Register
+ | Cabs.STATIC -> Static
+ | Cabs.EXTERN -> Extern
in
storage := sto';
acc
- | A.SpecCV cv -> cvattrs := cv :: !cvattrs; acc
- | A.SpecAttr a -> attrs := a :: !attrs; acc
- | A.SpecType ts -> ts :: acc
- | A.SpecPattern _ -> abort_context "SpecPattern in cabs2cil input"
+ | Cabs.SpecCV cv -> cvattrs := cv :: !cvattrs; acc
+ | Cabs.SpecAttr a -> attrs := a :: !attrs; acc
+ | Cabs.SpecType ts -> ts :: acc
+ | Cabs.SpecPattern _ -> abort_context "SpecPattern in cabs2cil input"
in
(* Now scan the list and collect the type specifiers. Preserve the order *)
let tspecs = List.fold_right doSpecElem specs [] in
@@ -4521,10 +4518,10 @@ let rec doSpecList ghost (suggestedAnonName: string)
(* GCC allows a named type that appears first to be followed by things
* like "short", "signed", "unsigned" or "long". *)
match tspecs with
- | A.Tnamed _ :: (_ :: _ as rest) when Cil.gccMode () ->
+ | Cabs.Tnamed _ :: (_ :: _ as rest) when Cil.gccMode () ->
(* If rest contains "short" or "long" then drop the Tnamed *)
- if List.exists (function A.Tshort -> true
- | A.Tlong -> true | _ -> false) rest then
+ if List.exists (function Cabs.Tshort -> true
+ | Cabs.Tlong -> true | _ -> false) rest then
rest
else
tspecs
@@ -4533,31 +4530,31 @@ let rec doSpecList ghost (suggestedAnonName: string)
in
let tspecs'' =
match specs, List.rev tspecs' with
- | A.SpecTypedef :: _, A.Tnamed _ :: [] ->
+ | Cabs.SpecTypedef :: _, Cabs.Tnamed _ :: [] ->
tspecs'
- | A.SpecTypedef :: _, A.Tnamed _ :: rest ->
+ | Cabs.SpecTypedef :: _, Cabs.Tnamed _ :: rest ->
List.rev rest
| _ -> tspecs'
in
(* Sort the type specifiers *)
let sortedspecs =
let order = function (* Don't change this *)
- | A.Tvoid -> 0
- | A.Tsigned -> 1
- | A.Tunsigned -> 2
- | A.Tchar -> 3
- | A.Tshort -> 4
- | A.Tlong -> 5
- | A.Tint -> 6
- | A.Tint64 -> 7
- | A.Tfloat -> 8
- | A.Tdouble -> 9
+ | Cabs.Tvoid -> 0
+ | Cabs.Tsigned -> 1
+ | Cabs.Tunsigned -> 2
+ | Cabs.Tchar -> 3
+ | Cabs.Tshort -> 4
+ | Cabs.Tlong -> 5
+ | Cabs.Tint -> 6
+ | Cabs.Tint64 -> 7
+ | Cabs.Tfloat -> 8
+ | Cabs.Tdouble -> 9
| _ -> 10 (* There should be at most one of the others *)
in
List.stable_sort (fun ts1 ts2 ->
Datatype.Int.compare (order ts1) (order ts2)) tspecs''
in
- let getTypeAttrs () : A.attribute list =
+ let getTypeAttrs () : Cabs.attribute list =
(* Partitions the attributes in !attrs.
Type attributes are removed from attrs and returned, so that they
can go into the type definition. Name attributes are left in attrs,
@@ -4575,97 +4572,97 @@ let rec doSpecList ghost (suggestedAnonName: string)
(* And now try to make sense of it. See ISO 6.7.2 *)
let bt =
match sortedspecs with
- | [A.Tvoid] -> TVoid []
- | [A.Tchar] -> TInt(IChar, [])
- | [A.Tbool] -> TInt(IBool, [])
- | [A.Tsigned; A.Tchar] -> TInt(ISChar, [])
- | [A.Tunsigned; A.Tchar] -> TInt(IUChar, [])
+ | [Cabs.Tvoid] -> TVoid []
+ | [Cabs.Tchar] -> TInt(IChar, [])
+ | [Cabs.Tbool] -> TInt(IBool, [])
+ | [Cabs.Tsigned; Cabs.Tchar] -> TInt(ISChar, [])
+ | [Cabs.Tunsigned; Cabs.Tchar] -> TInt(IUChar, [])
- | [A.Tshort] -> TInt(IShort, [])
- | [A.Tsigned; A.Tshort] -> TInt(IShort, [])
- | [A.Tshort; A.Tint] -> TInt(IShort, [])
- | [A.Tsigned; A.Tshort; A.Tint] -> TInt(IShort, [])
+ | [Cabs.Tshort] -> TInt(IShort, [])
+ | [Cabs.Tsigned; Cabs.Tshort] -> TInt(IShort, [])
+ | [Cabs.Tshort; Cabs.Tint] -> TInt(IShort, [])
+ | [Cabs.Tsigned; Cabs.Tshort; Cabs.Tint] -> TInt(IShort, [])
- | [A.Tunsigned; A.Tshort] -> TInt(IUShort, [])
- | [A.Tunsigned; A.Tshort; A.Tint] -> TInt(IUShort, [])
+ | [Cabs.Tunsigned; Cabs.Tshort] -> TInt(IUShort, [])
+ | [Cabs.Tunsigned; Cabs.Tshort; Cabs.Tint] -> TInt(IUShort, [])
| [] -> TInt(IInt, [])
- | [A.Tint] -> TInt(IInt, [])
- | [A.Tsigned] -> TInt(IInt, [])
- | [A.Tsigned; A.Tint] -> TInt(IInt, [])
+ | [Cabs.Tint] -> TInt(IInt, [])
+ | [Cabs.Tsigned] -> TInt(IInt, [])
+ | [Cabs.Tsigned; Cabs.Tint] -> TInt(IInt, [])
- | [A.Tunsigned] -> TInt(IUInt, [])
- | [A.Tunsigned; A.Tint] -> TInt(IUInt, [])
+ | [Cabs.Tunsigned] -> TInt(IUInt, [])
+ | [Cabs.Tunsigned; Cabs.Tint] -> TInt(IUInt, [])
- | [A.Tlong] -> TInt(ILong, [])
- | [A.Tsigned; A.Tlong] -> TInt(ILong, [])
- | [A.Tlong; A.Tint] -> TInt(ILong, [])
- | [A.Tsigned; A.Tlong; A.Tint] -> TInt(ILong, [])
+ | [Cabs.Tlong] -> TInt(ILong, [])
+ | [Cabs.Tsigned; Cabs.Tlong] -> TInt(ILong, [])
+ | [Cabs.Tlong; Cabs.Tint] -> TInt(ILong, [])
+ | [Cabs.Tsigned; Cabs.Tlong; Cabs.Tint] -> TInt(ILong, [])
- | [A.Tunsigned; A.Tlong] -> TInt(IULong, [])
- | [A.Tunsigned; A.Tlong; A.Tint] -> TInt(IULong, [])
+ | [Cabs.Tunsigned; Cabs.Tlong] -> TInt(IULong, [])
+ | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tint] -> TInt(IULong, [])
- | [A.Tlong; A.Tlong] -> TInt(ILongLong, [])
- | [A.Tsigned; A.Tlong; A.Tlong] -> TInt(ILongLong, [])
- | [A.Tlong; A.Tlong; A.Tint] -> TInt(ILongLong, [])
- | [A.Tsigned; A.Tlong; A.Tlong; A.Tint] -> TInt(ILongLong, [])
+ | [Cabs.Tlong; Cabs.Tlong] -> TInt(ILongLong, [])
+ | [Cabs.Tsigned; Cabs.Tlong; Cabs.Tlong] -> TInt(ILongLong, [])
+ | [Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> TInt(ILongLong, [])
+ | [Cabs.Tsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> TInt(ILongLong, [])
- | [A.Tunsigned; A.Tlong; A.Tlong] -> TInt(IULongLong, [])
- | [A.Tunsigned; A.Tlong; A.Tlong; A.Tint] -> TInt(IULongLong, [])
+ | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong] -> TInt(IULongLong, [])
+ | [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> TInt(IULongLong, [])
(* int64 is to support MSVC *)
- | [A.Tint64] -> TInt(ILongLong, [])
- | [A.Tsigned; A.Tint64] -> TInt(ILongLong, [])
+ | [Cabs.Tint64] -> TInt(ILongLong, [])
+ | [Cabs.Tsigned; Cabs.Tint64] -> TInt(ILongLong, [])
- | [A.Tunsigned; A.Tint64] -> TInt(IULongLong, [])
+ | [Cabs.Tunsigned; Cabs.Tint64] -> TInt(IULongLong, [])
- | [A.Tfloat] -> TFloat(FFloat, [])
- | [A.Tdouble] -> TFloat(FDouble, [])
+ | [Cabs.Tfloat] -> TFloat(FFloat, [])
+ | [Cabs.Tdouble] -> TFloat(FDouble, [])
- | [A.Tlong; A.Tdouble] -> TFloat(FLongDouble, [])
+ | [Cabs.Tlong; Cabs.Tdouble] -> TFloat(FLongDouble, [])
(* Now the other type specifiers *)
- | [A.Tnamed "__builtin_va_list"]
+ | [Cabs.Tnamed "__builtin_va_list"]
when Cil.theMachine.theMachine.has__builtin_va_list ->
TBuiltin_va_list []
- | [A.Tnamed "__fc_builtin_size_t"] -> Cil.theMachine.typeOfSizeOf
- | [A.Tnamed n] ->
+ | [Cabs.Tnamed "__fc_builtin_size_t"] -> Cil.theMachine.typeOfSizeOf
+ | [Cabs.Tnamed n] ->
(match lookupType ghost "type" n with
| (TNamed _) as x, _ -> x
| _ ->
Kernel.fatal ~current:true "Named type %s is not mapped correctly" n)
- | [A.Tstruct (n, None, _)] -> (* A reference to a struct *)
+ | [Cabs.Tstruct (n, None, _)] -> (* A reference to a struct *)
if n = "" then
Kernel.error ~once:true ~current:true
"Missing struct tag on incomplete struct";
findCompType ghost "struct" n []
- | [A.Tstruct (n, Some nglist, extraAttrs)] -> (* A definition of a struct *)
+ | [Cabs.Tstruct (n, Some nglist, extraAttrs)] -> (* A definition of a struct *)
let n' =
if n <> "" then n else anonStructName "struct" suggestedAnonName in
(* Use the (non-cv, non-name) attributes in !attrs now *)
let a = extraAttrs @ (getTypeAttrs ()) in
makeCompType ghost true n' ~norig:n nglist (doAttributes ghost a)
- | [A.Tunion (n, None, _)] -> (* A reference to a union *)
+ | [Cabs.Tunion (n, None, _)] -> (* A reference to a union *)
if n = "" then
Kernel.error ~once:true ~current:true
"Missing union tag on incomplete union";
findCompType ghost "union" n []
- | [A.Tunion (n, Some nglist, extraAttrs)] -> (* A definition of a union *)
+ | [Cabs.Tunion (n, Some nglist, extraAttrs)] -> (* A definition of a union *)
let n' =
if n <> "" then n else anonStructName "union" suggestedAnonName in
(* Use the attributes now *)
let a = extraAttrs @ (getTypeAttrs ()) in
makeCompType ghost false n' ~norig:n nglist (doAttributes ghost a)
- | [A.Tenum (n, None, _)] -> (* Just a reference to an enum *)
+ | [Cabs.Tenum (n, None, _)] -> (* Just a reference to an enum *)
if n = "" then
Kernel.error ~once:true ~current:true
"Missing enum tag on incomplete enum";
findCompType ghost "enum" n []
- | [A.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *)
+ | [Cabs.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *)
let n' =
if n <> "" then n else anonStructName "enum" suggestedAnonName in
(* make a new name for this enumeration *)
@@ -4736,7 +4733,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
and loop i = function
[] -> []
- | (kname, { expr_node = A.NOTHING}, cloc) :: rest ->
+ | (kname, { expr_node = Cabs.NOTHING}, cloc) :: rest ->
(* use the passed-in 'i' as the value, since none specified *)
processName kname i (convLoc cloc) rest
@@ -4792,7 +4789,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
cabsPushGlobal (GEnumTag (enum, CurrentLoc.get ()));
res
- | [A.TtypeofE e] ->
+ | [Cabs.TtypeofE e] ->
let (_, s, e', t) =
doExp (ghost_local_env ghost) CNoConst e AExpLeaveArrayFun
in
@@ -4816,7 +4813,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
*)
t'
- | [A.TtypeofT (specs, dt)] ->
+ | [Cabs.TtypeofT (specs, dt)] ->
doOnlyType ghost specs dt
| l ->
@@ -4828,7 +4825,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
(* given some cv attributes, convert them into named attributes for
* uniform processing *)
-and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
+and convertCVtoAttr (src: Cabs.cvspec list) : Cabs.attribute list =
match src with
| [] -> []
| CV_CONST :: tl -> ("const",[]) :: (convertCVtoAttr tl)
@@ -4852,7 +4849,7 @@ and makeVarInfoCabs
~allowVarSizeArrays:isformal (* For locals we handle var-sized arrays
before makeVarInfoCabs; for formals
we do it afterwards *)
- bt (A.PARENTYPE(attrs, ndt, a)) in
+ bt (Cabs.PARENTYPE(attrs, ndt, a)) in
(*Format.printf "Got yp:%a->%a(%a)@." d_type bt d_type vtype d_attrlist nattr;*)
if hasAttribute "thread" nattr then begin
let wkey = Kernel.wkey_inconsistent_specifier in
@@ -4910,7 +4907,7 @@ and makeVarSizeVarInfo ghost (ldecl : location)
~isglobal:false
ldecl spec_res (n,ndt,a), empty, zero ~loc:ldecl, false
-and doAttr ghost (a: A.attribute) : attribute list =
+and doAttr ghost (a: Cabs.attribute) : attribute list =
(* Strip the leading and trailing underscore *)
match a with
| ("__attribute__", []) -> [] (* An empty list of gcc attributes *)
@@ -4921,10 +4918,10 @@ and doAttr ghost (a: A.attribute) : attribute list =
let rec attrOfExp (strip: bool)
?(foldenum=true)
- (a: A.expression) : attrparam =
+ (a: Cabs.expression) : attrparam =
let loc = a.expr_loc in
match a.expr_node with
- | A.VARIABLE n -> begin
+ | Cabs.VARIABLE n -> begin
let n' = if strip then stripUnderscore n else n in
(** See if this is an enumeration *)
try
@@ -4940,51 +4937,51 @@ and doAttr ghost (a: A.attribute) : attribute list =
| _ -> ACons (n', [])
with Not_found -> ACons(n', [])
end
- | A.CONSTANT (A.CONST_STRING s) -> AStr s
- | A.CONSTANT (A.CONST_INT str) -> begin
+ | Cabs.CONSTANT (Cabs.CONST_STRING s) -> AStr s
+ | Cabs.CONSTANT (Cabs.CONST_INT str) -> begin
match (parseIntExp ~loc str).enode with
| Const (CInt64 (v64,_,_)) ->
AInt v64
| _ ->
Kernel.fatal ~current:true "Invalid attribute constant: %s" str
end
- | A.CONSTANT (A.CONST_FLOAT str) ->
+ | Cabs.CONSTANT (Cabs.CONST_FLOAT str) ->
ACons ("__fc_float", [AStr str])
- | A.CALL({expr_node = A.VARIABLE n}, args, []) -> begin
+ | Cabs.CALL({expr_node = Cabs.VARIABLE n}, args, []) -> begin
let n' = if strip then stripUnderscore n else n in
let ae' = List.map ae args in
ACons(n', ae')
end
- | A.EXPR_SIZEOF e -> ASizeOfE (ae e)
- | A.TYPE_SIZEOF (bt, dt) -> ASizeOf (doOnlyType ghost bt dt)
- | A.EXPR_ALIGNOF e -> AAlignOfE (ae e)
- | A.TYPE_ALIGNOF (bt, dt) -> AAlignOf (doOnlyType ghost bt dt)
- | A.BINARY(A.AND, aa1, aa2) ->
+ | Cabs.EXPR_SIZEOF e -> ASizeOfE (ae e)
+ | Cabs.TYPE_SIZEOF (bt, dt) -> ASizeOf (doOnlyType ghost bt dt)
+ | Cabs.EXPR_ALIGNOF e -> AAlignOfE (ae e)
+ | Cabs.TYPE_ALIGNOF (bt, dt) -> AAlignOf (doOnlyType ghost bt dt)
+ | Cabs.BINARY(Cabs.AND, aa1, aa2) ->
ABinOp(LAnd, ae aa1, ae aa2)
- | A.BINARY(A.OR, aa1, aa2) ->
+ | Cabs.BINARY(Cabs.OR, aa1, aa2) ->
ABinOp(LOr, ae aa1, ae aa2)
- | A.BINARY(A.ASSIGN,aa1,aa2) ->
+ | Cabs.BINARY(Cabs.ASSIGN,aa1,aa2) ->
(* Bit of a hack to account for OSX specific syntax. *)
ACons ("__fc_assign", [ae aa1; ae aa2])
- | A.BINARY(abop, aa1, aa2) ->
+ | Cabs.BINARY(abop, aa1, aa2) ->
ABinOp (convBinOp abop, ae aa1, ae aa2)
- | A.UNARY(A.PLUS, aa) -> ae aa
- | A.UNARY(A.MINUS, aa) -> AUnOp (Neg, ae aa)
- | A.UNARY(A.BNOT, aa) -> AUnOp(BNot, ae aa)
- | A.UNARY(A.NOT, aa) -> AUnOp(LNot, ae aa)
- | A.MEMBEROF (e, s) -> ADot (ae e, s)
- | A.PAREN(e) -> attrOfExp strip ~foldenum:foldenum e
- | A.UNARY(A.MEMOF, aa) -> AStar (ae aa)
- | A.UNARY(A.ADDROF, aa) -> AAddrOf (ae aa)
- | A.MEMBEROFPTR (aa1, s) -> ADot(AStar(ae aa1), s)
- | A.INDEX(aa1, aa2) -> AIndex(ae aa1, ae aa2)
- | A.QUESTION(aa1, aa2, aa3) -> AQuestion(ae aa1, ae aa2, ae aa3)
+ | Cabs.UNARY(Cabs.PLUS, aa) -> ae aa
+ | Cabs.UNARY(Cabs.MINUS, aa) -> AUnOp (Neg, ae aa)
+ | Cabs.UNARY(Cabs.BNOT, aa) -> AUnOp(BNot, ae aa)
+ | Cabs.UNARY(Cabs.NOT, aa) -> AUnOp(LNot, ae aa)
+ | Cabs.MEMBEROF (e, s) -> ADot (ae e, s)
+ | Cabs.PAREN(e) -> attrOfExp strip ~foldenum:foldenum e
+ | Cabs.UNARY(Cabs.MEMOF, aa) -> AStar (ae aa)
+ | Cabs.UNARY(Cabs.ADDROF, aa) -> AAddrOf (ae aa)
+ | Cabs.MEMBEROFPTR (aa1, s) -> ADot(AStar(ae aa1), s)
+ | Cabs.INDEX(aa1, aa2) -> AIndex(ae aa1, ae aa2)
+ | Cabs.QUESTION(aa1, aa2, aa3) -> AQuestion(ae aa1, ae aa2, ae aa3)
| _ ->
Kernel.fatal ~current:true
"cabs2cil: invalid expression in attribute: %a"
Cprint.print_expression a
- and ae (e: A.expression) = attrOfExp false e in
+ and ae (e: Cabs.expression) = attrOfExp false e in
(* Sometimes we need to convert attrarg into attr *)
let arg2attr = function
@@ -5003,7 +5000,7 @@ and doAttr ghost (a: A.attribute) : attribute list =
else
[Attr(stripUnderscore s, List.map (attrOfExp ~foldenum:false false) el)]
-and doAttributes (ghost:bool) (al: A.attribute list) : attribute list =
+and doAttributes (ghost:bool) (al: Cabs.attribute list) : attribute list =
List.fold_left (fun acc a -> cabsAddAttributes (doAttr ghost a) acc) [] al
(* A version of Cil.partitionAttributes that works on CABS attributes.
@@ -5012,8 +5009,8 @@ and doAttributes (ghost:bool) (al: A.attribute list) : attribute list =
and cabsPartitionAttributes
ghost
~(default:attributeClass)
- (attrs: A.attribute list) :
- A.attribute list * A.attribute list * A.attribute list =
+ (attrs: Cabs.attribute list) :
+ Cabs.attribute list * Cabs.attribute list * Cabs.attribute list =
let rec loop (n,f,t) = function
[] -> n, f, t
| a :: rest ->
@@ -5039,7 +5036,7 @@ and doType (ghost:bool) isFuncArg
?(allowZeroSizeArrays=false)
?(allowVarSizeArrays=false)
(bt: typ) (* The base type *)
- (dt: A.decl_type)
+ (dt: Cabs.decl_type)
(* Returns the new type and the accumulated name (or type attribute
if nameoftype = AttrType) attributes *)
: typ * attribute list =
@@ -5050,8 +5047,8 @@ and doType (ghost:bool) isFuncArg
let rec doDeclType (bt: typ) (acc: attribute list) decl_type =
checkRestrictQualifierDeep bt;
match decl_type with
- | A.JUSTBASE -> bt, acc
- | A.PARENTYPE (a1, d, a2) ->
+ | Cabs.JUSTBASE -> bt, acc
+ | Cabs.PARENTYPE (a1, d, a2) ->
let a1' = doAttributes ghost a1 in
let a1n, a1f, a1t = partitionAttributes AttrType a1' in
let a2' = doAttributes ghost a2 in
@@ -5100,7 +5097,7 @@ and doType (ghost:bool) isFuncArg
(* Now add the name attributes and return *)
restyp', cabsAddAttributes a1n (cabsAddAttributes a2n nattr)
- | A.PTR (al, d) ->
+ | Cabs.PTR (al, d) ->
let al' = doAttributes ghost al in
let an, af, at = partitionAttributes AttrType al' in
(* Now recurse *)
@@ -5121,7 +5118,7 @@ and doType (ghost:bool) isFuncArg
(* Now add the name attributes and return *)
restyp', cabsAddAttributes an nattr
- | A.ARRAY (d, al, len) ->
+ | Cabs.ARRAY (d, al, len) ->
if Cil.isFunctionType bt then
Kernel.error ~once:true ~current:true
"declaration of array of function type '%a`"
@@ -5147,7 +5144,7 @@ and doType (ghost:bool) isFuncArg
Cil_printer.pp_typ bt;
let lo =
match len.expr_node with
- | A.NOTHING -> None
+ | Cabs.NOTHING -> None
| _ ->
(* Check that len is a constant expression.
We used to also cast the length to int here, but that's
@@ -5194,7 +5191,7 @@ and doType (ghost:bool) isFuncArg
function argument";
doDeclType (TArray(bt, lo, empty_size_cache (), al')) acc d
- | A.PROTO (d, args, ghost_args, isva) ->
+ | Cabs.PROTO (d, args, ghost_args, isva) ->
(* Start a scope for the parameter names *)
enterScope ();
(* Intercept the old-style use of varargs.h. On GCC this means that
@@ -5205,7 +5202,7 @@ and doType (ghost:bool) isFuncArg
if args != [] && Cil.msvcMode () = not isva then begin
let newisva = ref isva in
let rec doLast = function
- [([A.SpecType (A.Tnamed atn)], (an, A.JUSTBASE, [], _))]
+ [([Cabs.SpecType (Cabs.Tnamed atn)], (an, Cabs.JUSTBASE, [], _))]
when isOldStyleVarArgTypeName atn &&
isOldStyleVarArgName an -> begin
(* Turn it into a vararg *)
@@ -5351,11 +5348,11 @@ and doType (ghost:bool) isFuncArg
(* If this is a declarator for a variable size array then turn it into a
pointer type and a length *)
-and isVariableSizedArray ghost (dt: A.decl_type)
- : (A.decl_type * chunk * exp) option =
+and isVariableSizedArray ghost (dt: Cabs.decl_type)
+ : (Cabs.decl_type * chunk * exp) option =
let res = ref None in
let rec findArray = function
- ARRAY (JUSTBASE, al, lo) when lo.expr_node != A.NOTHING ->
+ ARRAY (JUSTBASE, al, lo) when lo.expr_node != Cabs.NOTHING ->
(* Checks whether the expression is an integer constant expression,
that is:
– it contains no side-effect
@@ -5382,12 +5379,12 @@ and isVariableSizedArray ghost (dt: A.decl_type)
| None -> None
| Some (se, e) -> Some (dt', se, e)
-and doOnlyType ghost (specs: A.spec_elem list) (dt: A.decl_type) : typ =
+and doOnlyType ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
let bt',sto,inl,attrs = doSpecList ghost "" specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true "Storage or inline specifier in type only";
let tres, nattr =
- doType ghost false AttrType bt' (A.PARENTYPE(attrs, dt, [])) in
+ doType ghost false AttrType bt' (Cabs.PARENTYPE(attrs, dt, [])) in
if nattr <> [] then
Kernel.error ~once:true ~current:true
"Name attributes in only_type: %a" Cil_printer.pp_attributes nattr;
@@ -5397,7 +5394,7 @@ and doOnlyType ghost (specs: A.spec_elem list) (dt: A.decl_type) : typ =
and makeCompType ghost (isstruct: bool)
(n: string)
~(norig: string)
- (nglist: A.field_group list)
+ (nglist: Cabs.field_group list)
(a: attribute list) =
(* Make a new name for the structure *)
let kind = if isstruct then "struct" else "union" in
@@ -5412,7 +5409,7 @@ and makeCompType ghost (isstruct: bool)
in
let addFieldGroup ~last:last_group (flds : fieldinfo list)
- ((s: A.spec_elem list), (nl: (A.name * A.expression option) list)) =
+ ((s: Cabs.spec_elem list), (nl: (Cabs.name * Cabs.expression option) list)) =
(* Do the specifiers exactly once *)
let sugg = match nl with
| [] -> ""
@@ -5421,7 +5418,7 @@ and makeCompType ghost (isstruct: bool)
let bt, sto, inl, attrs = doSpecList ghost sugg s in
(* Do the fields *)
let addFieldInfo ~last:last_field (flds : fieldinfo list)
- (((n,ndt,a,cloc) : A.name), (widtho : A.expression option))
+ (((n,ndt,a,cloc) : Cabs.name), (widtho : Cabs.expression option))
: fieldinfo list =
let source = fst cloc in
if sto <> NoStorage || inl then
@@ -5430,7 +5427,7 @@ and makeCompType ghost (isstruct: bool)
let ftype, fattr =
doType
~allowZeroSizeArrays ghost false (AttrName false) bt
- (A.PARENTYPE(attrs, ndt, a))
+ (Cabs.PARENTYPE(attrs, ndt, a))
in
(* check for fields whose type is incomplete. In particular, this rules
out circularity:
@@ -5634,10 +5631,10 @@ and makeCompType ghost (isstruct: bool)
(* Now create a typedef with just this type *)
res
-and preprocessCast ghost (specs: A.specifier)
- (dt: A.decl_type)
- (ie: A.init_expression)
- : A.specifier * A.decl_type * A.init_expression =
+and preprocessCast ghost (specs: Cabs.specifier)
+ (dt: Cabs.decl_type)
+ (ie: Cabs.init_expression)
+ : Cabs.specifier * Cabs.decl_type * Cabs.init_expression =
let typ = doOnlyType ghost specs dt in
(* If we are casting to a union type then we have to treat this as a
* constructor expression. This is to handle the gcc extension that allows
@@ -5646,10 +5643,10 @@ and preprocessCast ghost (specs: A.specifier)
* will resolve this later, when we'll convert casts to unions. *)
let ie' =
match unrollType typ, ie with
- | TComp (c, _, _), A.SINGLE_INIT _ when not c.cstruct ->
- A.COMPOUND_INIT [(A.INFIELD_INIT ("___matching_field",
- A.NEXT_INIT),
- ie)]
+ | TComp (c, _, _), Cabs.SINGLE_INIT _ when not c.cstruct ->
+ Cabs.COMPOUND_INIT [(Cabs.INFIELD_INIT ("___matching_field",
+ Cabs.NEXT_INIT),
+ ie)]
| _, _ -> ie
in
(* Maybe specs contains an unnamed composite. Replace with the name so that
@@ -5659,10 +5656,10 @@ and preprocessCast ghost (specs: A.specifier)
| TComp (ci, _, _) ->
List.map
(function
- A.SpecType (A.Tstruct ("", _, [])) ->
- A.SpecType (A.Tstruct (ci.cname, None, []))
- | A.SpecType (A.Tunion ("", _, [])) ->
- A.SpecType (A.Tunion (ci.cname, None, []))
+ Cabs.SpecType (Cabs.Tstruct ("", _, [])) ->
+ Cabs.SpecType (Cabs.Tstruct (ci.cname, None, []))
+ | Cabs.SpecType (Cabs.Tunion ("", _, [])) ->
+ Cabs.SpecType (Cabs.Tunion (ci.cname, None, []))
| s -> s) specs
| _ -> specs
in
@@ -5709,7 +5706,7 @@ and isIntegerConstant ghost (aexp) : int option =
*)
and doExp local_env
(asconst: expConst) (* This expression is used as a constant *)
- (e: A.expression)
+ (e: Cabs.expression)
(what: expAction)
=
let ghost = local_env.is_ghost in
@@ -5783,14 +5780,14 @@ and doExp local_env
in
let result =
match e.expr_node with
- | A.PAREN e -> doExp (paren_local_env local_env) asconst e what
- | A.NOTHING when what = ADrop ->
+ | Cabs.PAREN e -> doExp (paren_local_env local_env) asconst e what
+ | Cabs.NOTHING when what = ADrop ->
finishExp [] (unspecified_chunk empty) (integer ~loc 0) intType
- | A.NOTHING ->
+ | Cabs.NOTHING ->
let res = new_exp ~loc (Const(CStr "exp_nothing")) in
finishExp [] (unspecified_chunk empty) res (typeOf res)
(* Do the potential lvalues first *)
- | A.VARIABLE n -> begin
+ | Cabs.VARIABLE n -> begin
if is_stdlib_function_macro n then begin
(* These must be macros. They can be implemented with a function
of the same name, but in that case, it is not possible to
@@ -5854,7 +5851,7 @@ and doExp local_env
Kernel.abort ~current:true "Cannot resolve variable %s" n
end
end
- | A.INDEX (e1, e2) -> begin
+ | Cabs.INDEX (e1, e2) -> begin
(* Recall that doExp turns arrays into StartOf pointers *)
let (r1, se1, e1', t1) =
doExp (no_paren_local_env local_env) CNoConst e1 (AExp None) in
@@ -5892,7 +5889,7 @@ and doExp local_env
in
finishExp reads se (new_exp ~loc (Lval res)) (dropQualifiers tresult)
end
- | A.UNARY (A.MEMOF, e) ->
+ | Cabs.UNARY (Cabs.MEMOF, e) ->
if asconst = CConst then
Kernel.warning ~current:true "MEMOF in constant";
let (r,se, e', t) =
@@ -5916,7 +5913,7 @@ and doExp local_env
(* e.str = (& e + off(str)). If e = (be + beoff) then e.str = (be
* + beoff + off(str)) *)
- | A.MEMBEROF (e, str) ->
+ | Cabs.MEMBEROF (e, str) ->
(* member of is actually allowed if we only take the address *)
(* if isconst then Cil.error "MEMBEROF in constant"; *)
let (r,se, e', t') =
@@ -5951,7 +5948,7 @@ and doExp local_env
finishExp reads se (new_exp ~loc (Lval lv')) (dropQualifiers field_type)
(* e->str = * (e + off(str)) *)
- | A.MEMBEROFPTR (e, str) ->
+ | Cabs.MEMBEROFPTR (e, str) ->
if asconst = CConst then
Kernel.warning ~current:true "MEMBEROFPTR in constant";
let (r,se, e', t') =
@@ -5978,21 +5975,21 @@ and doExp local_env
in
finishExp reads se (new_exp ~loc (Lval lv')) (dropQualifiers field_type)
- | A.CONSTANT ct -> begin
+ | Cabs.CONSTANT ct -> begin
match ct with
- | A.CONST_INT str -> begin
+ | Cabs.CONST_INT str -> begin
let res = parseIntExp ~loc str in
finishExp [] (unspecified_chunk empty) res (typeOf res)
end
- | A.CONST_WSTRING (ws: int64 list) ->
+ | Cabs.CONST_WSTRING (ws: int64 list) ->
let res =
new_exp ~loc
(Const(CWStr ((* intlist_to_wstring *) ws)))
in
finishExp [] (unspecified_chunk empty) res (typeOf res)
- | A.CONST_STRING s ->
+ | Cabs.CONST_STRING s ->
(* Maybe we buried __FUNCTION__ in there *)
let s' =
try
@@ -6012,11 +6009,11 @@ and doExp local_env
let res = new_exp ~loc (Const(CStr s')) in
finishExp [] (unspecified_chunk empty) res (typeOf res)
- | A.CONST_CHAR char_list ->
+ | Cabs.CONST_CHAR char_list ->
let a, b = (interpret_character_constant char_list) in
finishExp [] (unspecified_chunk empty) (new_exp ~loc (Const a)) b
- | A.CONST_WCHAR char_list ->
+ | Cabs.CONST_WCHAR char_list ->
(* matth: I can't see a reason for a list of more than one char
* here, since the kinteger64 below will take only the lower 16
* bits of value. ('abc' makes sense, because CHAR constants have
@@ -6030,7 +6027,7 @@ and doExp local_env
in
finishExp [] (unspecified_chunk empty) result (typeOf result)
- | A.CONST_FLOAT str -> begin
+ | Cabs.CONST_FLOAT str -> begin
Floating_point.set_round_nearest_even ();
let kind, parsed_float = Floating_point.parse str in
let nearest_float = parsed_float.Floating_point.f_nearest in
@@ -6046,13 +6043,13 @@ and doExp local_env
end
end
- | A.TYPE_SIZEOF (bt, dt) ->
+ | Cabs.TYPE_SIZEOF (bt, dt) ->
let typ = doOnlyType local_env.is_ghost bt dt in
fail_if_incompatible_sizeof ~ensure_complete:true "sizeof" typ;
let res = new_exp ~loc (SizeOf typ) in
finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
- | A.EXPR_SIZEOF e ->
+ | Cabs.EXPR_SIZEOF e ->
(* Allow non-constants in sizeof *)
(* Do not convert arrays and functions into pointers. *)
let (_, se, e', lvt) =
@@ -6073,13 +6070,13 @@ and doExp local_env
in
finishExp [] scope_chunk size theMachine.typeOfSizeOf
- | A.TYPE_ALIGNOF (bt, dt) ->
+ | Cabs.TYPE_ALIGNOF (bt, dt) ->
let typ = doOnlyType local_env.is_ghost bt dt in
fail_if_incompatible_sizeof ~ensure_complete:true "alignof" typ;
let res = new_exp ~loc (AlignOf typ) in
finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
- | A.EXPR_ALIGNOF e ->
+ | Cabs.EXPR_ALIGNOF e ->
let (_, se, e', lvt) =
doExp (no_paren_local_env local_env) CNoConst e AExpLeaveArrayFun
in
@@ -6095,7 +6092,7 @@ and doExp local_env
finishExp [] scope_chunk (new_exp ~loc (AlignOfE(e'')))
theMachine.typeOfSizeOf
- | A.CAST ((specs, dt), ie) ->
+ | Cabs.CAST ((specs, dt), ie) ->
let s', dt', ie' = preprocessCast local_env.is_ghost specs dt ie in
(* We know now that we can do s' and dt' many times *)
let typ = doOnlyType local_env.is_ghost s' dt' in
@@ -6115,12 +6112,12 @@ and doExp local_env
(* Remember here if we have done the Set *)
let (r,se, e', t'), (needcast: bool) =
match ie' with
- | A.SINGLE_INIT e ->
+ | Cabs.SINGLE_INIT e ->
doExp (no_paren_local_env local_env) asconst e what', true
- | A.NO_INIT -> Kernel.fatal ~current:true "missing expression in cast"
+ | Cabs.NO_INIT -> Kernel.fatal ~current:true "missing expression in cast"
- | A.COMPOUND_INIT _ -> begin
+ | Cabs.COMPOUND_INIT _ -> begin
(* Pretend that we are declaring and initializing a brand new
* variable *)
let newvar = "__constr_expr_" ^ string_of_int (!constrExprId) in
@@ -6142,7 +6139,7 @@ and doExp local_env
in
(* Now pretend that e is just a reference to the newly created
* variable *)
- let v = { expr_node = A.VARIABLE newvar; expr_loc = loc } in
+ let v = { expr_node = Cabs.VARIABLE newvar; expr_loc = loc } in
let r, se, e', t' =
doExp (no_paren_local_env local_env) asconst v what'
in
@@ -6177,7 +6174,7 @@ and doExp local_env
in
finishExp r se e'' t''
- | A.UNARY(A.MINUS, e) ->
+ | Cabs.UNARY(Cabs.MINUS, e) ->
let (r, se, e', t) =
doExp (no_paren_local_env local_env) asconst e (AExp None)
in
@@ -6191,7 +6188,7 @@ and doExp local_env
else
Kernel.fatal ~current:true "Unary - on a non-arithmetic type"
- | A.UNARY(A.BNOT, e) ->
+ | Cabs.UNARY(Cabs.BNOT, e) ->
let (r, se, e', t) =
doExp (no_paren_local_env local_env) asconst e (AExp None)
in
@@ -6202,17 +6199,17 @@ and doExp local_env
else
Kernel.fatal ~current:true "Unary ~ on a non-integral type"
- | A.UNARY(A.PLUS, e) -> doExp (no_paren_local_env local_env) asconst e what
+ | Cabs.UNARY(Cabs.PLUS, e) -> doExp (no_paren_local_env local_env) asconst e what
- | A.UNARY(A.ADDROF, e) ->
+ | Cabs.UNARY(Cabs.ADDROF, e) ->
(* some normalization is needed here to remove potential COMMA, QUESTION
and PAREN. the normalization will take care of setting
local_env.is_paren as appropriate while removing PAREN. *)
let action local_env e what =
match e.expr_node with
- | A.COMMA _ | A.QUESTION _ | A.PAREN _ ->
+ | Cabs.COMMA _ | Cabs.QUESTION _ | Cabs.PAREN _ ->
Kernel.fatal ~current:true "normalization of unop failed"
- | A.VARIABLE s when
+ | Cabs.VARIABLE s when
isOldStyleVarArgName s
&& (match !currentFunctionFDEC.svar.vtype with
TFun(_, _, true, _) -> true | _ -> false) ->
@@ -6250,15 +6247,15 @@ and doExp local_env
doExp local_env asconst
(cabs_exp loc
- (A.CALL (cabs_exp loc (A.VARIABLE "__builtin_next_arg"),
- [cabs_exp loc (A.CONSTANT (A.CONST_INT "0"))],[])))
+ (Cabs.CALL (cabs_exp loc (Cabs.VARIABLE "__builtin_next_arg"),
+ [cabs_exp loc (Cabs.CONSTANT (Cabs.CONST_INT "0"))],[])))
what
end
- | A.VARIABLE _ | A.UNARY (A.MEMOF, _) (* Regular lvalues *)
- | A.CONSTANT (A.CONST_STRING _) | A.CONSTANT (A.CONST_WSTRING _)
- | A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _
- | A.CAST (_, A.COMPOUND_INIT _) ->
+ | Cabs.VARIABLE _ | Cabs.UNARY (Cabs.MEMOF, _) (* Regular lvalues *)
+ | Cabs.CONSTANT (Cabs.CONST_STRING _) | Cabs.CONSTANT (Cabs.CONST_WSTRING _)
+ | Cabs.INDEX _ | Cabs.MEMBEROF _ | Cabs.MEMBEROFPTR _
+ | Cabs.CAST (_, Cabs.COMPOUND_INIT _) ->
begin
let (r, se, e', t) =
doExp local_env CNoConst e (AExp None)
@@ -6295,17 +6292,17 @@ and doExp local_env
end
| _ -> Kernel.fatal ~current:true "Unexpected operand for addrof"
in
- normalize_unop A.ADDROF action CNoConst
+ normalize_unop Cabs.ADDROF action CNoConst
(no_paren_local_env local_env) e what
- | A.UNARY((A.PREINCR|A.PREDECR) as uop, e) ->
+ | Cabs.UNARY((Cabs.PREINCR|Cabs.PREDECR) as uop, e) ->
let action local_env e _what =
match e.expr_node with
- | A.COMMA _ | A.QUESTION _ | A.PAREN _ ->
+ | Cabs.COMMA _ | Cabs.QUESTION _ | Cabs.PAREN _ ->
Kernel.fatal ~current:true "normalization of unop failed"
- | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
- A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ |
- A.CAST _ (* A GCC extension *)) -> begin
- let uop' = if uop = A.PREINCR then PlusA else MinusA in
+ | (Cabs.VARIABLE _ | Cabs.UNARY (Cabs.MEMOF, _) | (* Regular lvalues *)
+ Cabs.INDEX _ | Cabs.MEMBEROF _ | Cabs.MEMBEROFPTR _ |
+ Cabs.CAST _ (* A GCC extension *)) -> begin
+ let uop' = if uop = Cabs.PREINCR then PlusA else MinusA in
if asconst = CConst then
Kernel.warning ~current:true "PREINCR or PREDECR in constant";
let (r, se, e', t) = doExp local_env CNoConst e (AExp None) in
@@ -6330,18 +6327,18 @@ and doExp local_env
in
normalize_unop uop action asconst (no_paren_local_env local_env) e what
- | A.UNARY((A.POSINCR|A.POSDECR) as uop, e) ->
+ | Cabs.UNARY((Cabs.POSINCR|Cabs.POSDECR) as uop, e) ->
let action local_env e what =
match e.expr_node with
- | A.COMMA _ | A.QUESTION _ | A.PAREN _ ->
+ | Cabs.COMMA _ | Cabs.QUESTION _ | Cabs.PAREN _ ->
Kernel.fatal ~current:true "normalization of unop failed"
- | A.VARIABLE _ | A.UNARY (A.MEMOF, _) (* Regular lvalues *)
- | A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _
- | A.CAST _ (* A GCC extension *) -> begin
+ | Cabs.VARIABLE _ | Cabs.UNARY (Cabs.MEMOF, _) (* Regular lvalues *)
+ | Cabs.INDEX _ | Cabs.MEMBEROF _ | Cabs.MEMBEROFPTR _
+ | Cabs.CAST _ (* A GCC extension *) -> begin
if asconst = CConst then
Kernel.warning ~current:true "POSTINCR or POSTDECR in constant";
(* If we do not drop the result then we must save the value *)
- let uop' = if uop = A.POSINCR then PlusA else MinusA in
+ let uop' = if uop = Cabs.POSINCR then PlusA else MinusA in
let (r,se, e', t) = doExp local_env CNoConst e (AExp None) in
let lv = get_lval_compound_assigned "++ or --" e' in
let se' = remove_reads lv se in
@@ -6357,7 +6354,7 @@ and doExp local_env
let descr =
Format.asprintf "%a%s"
Cil_descriptive_printer.pp_exp e'
- (if uop = A.POSINCR then "++" else "--") in
+ (if uop = Cabs.POSINCR then "++" else "--") in
let tmp = newTempVar ~ghost loc descr true t in
([var tmp],
local_var_chunk se' tmp +++
@@ -6386,14 +6383,14 @@ and doExp local_env
in
normalize_unop uop action asconst (no_paren_local_env local_env) e what
- | A.BINARY(A.ASSIGN, e1, e2) ->
+ | Cabs.BINARY(Cabs.ASSIGN, e1, e2) ->
let action local_env asconst e what =
match e.expr_node with
- | A.COMMA _ | A.QUESTION _ | A.CAST (_,A.SINGLE_INIT _) | A.PAREN _ ->
+ | Cabs.COMMA _ | Cabs.QUESTION _ | Cabs.CAST (_,Cabs.SINGLE_INIT _) | Cabs.PAREN _ ->
Kernel.fatal
~current:true "normalization of lval in assignment failed"
- | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
- A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ ) -> begin
+ | (Cabs.VARIABLE _ | Cabs.UNARY (Cabs.MEMOF, _) | (* Regular lvalues *)
+ Cabs.INDEX _ | Cabs.MEMBEROF _ | Cabs.MEMBEROFPTR _ ) -> begin
if asconst = CConst then
Kernel.warning ~current:true "ASSIGN in constant";
let se0 = unspecified_chunk empty in
@@ -6462,10 +6459,10 @@ and doExp local_env
| _ -> Kernel.fatal ~current:true "Invalid left operand for ASSIGN"
in
normalize_binop
- A.ASSIGN action (no_paren_local_env local_env) asconst e1 e2 what
- | A.BINARY((A.ADD|A.SUB|A.MUL|A.DIV|A.MOD|A.BAND|A.BOR|A.XOR|
- A.SHL|A.SHR|A.EQ|A.NE|A.LT|A.GT|A.GE|A.LE) as bop,
- e1, e2) ->
+ Cabs.ASSIGN action (no_paren_local_env local_env) asconst e1 e2 what
+ | Cabs.BINARY((Cabs.ADD|Cabs.SUB|Cabs.MUL|Cabs.DIV|Cabs.MOD|Cabs.BAND|Cabs.BOR|Cabs.XOR|
+ Cabs.SHL|Cabs.SHR|Cabs.EQ|Cabs.NE|Cabs.LT|Cabs.GT|Cabs.GE|Cabs.LE) as bop,
+ e1, e2) ->
let check_bitwise = is_bitwise_bop bop && not local_env.is_paren in
let se0 = unspecified_chunk empty in
let bop' = convBinOp bop in
@@ -6482,30 +6479,30 @@ and doExp local_env
finishExp (r1 @ r2) ((se0 @@ se1) @@ se2) result tresult
(* assignment operators *)
- | A.BINARY((A.ADD_ASSIGN|A.SUB_ASSIGN|A.MUL_ASSIGN|A.DIV_ASSIGN|
- A.MOD_ASSIGN|A.BAND_ASSIGN|A.BOR_ASSIGN|A.SHL_ASSIGN|
- A.SHR_ASSIGN|A.XOR_ASSIGN) as bop, e1, e2) ->
+ | Cabs.BINARY((Cabs.ADD_ASSIGN|Cabs.SUB_ASSIGN|Cabs.MUL_ASSIGN|Cabs.DIV_ASSIGN|
+ Cabs.MOD_ASSIGN|Cabs.BAND_ASSIGN|Cabs.BOR_ASSIGN|Cabs.SHL_ASSIGN|
+ Cabs.SHR_ASSIGN|Cabs.XOR_ASSIGN) as bop, e1, e2) ->
let se0 = unspecified_chunk empty in
let action local_env asconst e _what =
match e.expr_node with
- | A.COMMA _ | A.QUESTION _ | A.PAREN _ ->
+ | Cabs.COMMA _ | Cabs.QUESTION _ | Cabs.PAREN _ ->
Kernel.fatal ~current:true "normalization of lval in compound assignment failed"
- | A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
- A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ |
- A.CAST _ (* GCC extension *) -> begin
+ | Cabs.VARIABLE _ | Cabs.UNARY (Cabs.MEMOF, _) | (* Regular lvalues *)
+ Cabs.INDEX _ | Cabs.MEMBEROF _ | Cabs.MEMBEROFPTR _ |
+ Cabs.CAST _ (* GCC extension *) -> begin
if asconst = CConst then
Kernel.warning ~current:true "op_ASSIGN in constant";
let bop' = match bop with
- | A.ADD_ASSIGN -> PlusA
- | A.SUB_ASSIGN -> MinusA
- | A.MUL_ASSIGN -> Mult
- | A.DIV_ASSIGN -> Div
- | A.MOD_ASSIGN -> Mod
- | A.BAND_ASSIGN -> BAnd
- | A.BOR_ASSIGN -> BOr
- | A.XOR_ASSIGN -> BXor
- | A.SHL_ASSIGN -> Shiftlt
- | A.SHR_ASSIGN -> Shiftrt
+ | Cabs.ADD_ASSIGN -> PlusA
+ | Cabs.SUB_ASSIGN -> MinusA
+ | Cabs.MUL_ASSIGN -> Mult
+ | Cabs.DIV_ASSIGN -> Div
+ | Cabs.MOD_ASSIGN -> Mod
+ | Cabs.BAND_ASSIGN -> BAnd
+ | Cabs.BOR_ASSIGN -> BOr
+ | Cabs.XOR_ASSIGN -> BXor
+ | Cabs.SHL_ASSIGN -> Shiftlt
+ | Cabs.SHR_ASSIGN -> Shiftrt
| _ -> Kernel.fatal ~current:true "binary +="
in
let (r1,se1, e1', t1) = doExp local_env CNoConst e (AExp None) in
@@ -6540,7 +6537,7 @@ and doExp local_env
in
normalize_binop
bop action (no_paren_local_env local_env) asconst e1 e2 what
- | A.BINARY((A.AND|A.OR), _, _) | A.UNARY(A.NOT, _) -> begin
+ | Cabs.BINARY((Cabs.AND|Cabs.OR), _, _) | Cabs.UNARY(Cabs.NOT, _) -> begin
let ce = doCondExp local_env asconst e in
(* We must normalize the result to 0 or 1 *)
match ce with
@@ -6579,13 +6576,13 @@ and doExp local_env
intType
end
- | A.CALL(f, args, ghost_args) ->
+ | Cabs.CALL(f, args, ghost_args) ->
let (rf,sf, f', ft') =
match (stripParen f).expr_node with
(* Treat the VARIABLE case separate because we might be calling a
* function that does not have a prototype. In that case assume it
* takes INTs as arguments *)
- | A.VARIABLE n -> begin
+ | Cabs.VARIABLE n -> begin
try
(* First look for polymorphic builtins. The typing rule is
luckily always the same one. *)
@@ -7283,7 +7280,7 @@ and doExp local_env
(fun v -> prechunk:= local_var_chunk !prechunk v) !locals;
finishExp [] !prechunk !pres !prestype
- | A.COMMA el ->
+ | Cabs.COMMA el ->
if asconst = CConst then Kernel.warning ~current:true "COMMA in constant";
(* We must ignore AExpLeaveArrayFun (a.k.a. 'do not decay pointers')
if the expression at hand is a sequence with strictly more than
@@ -7312,7 +7309,7 @@ and doExp local_env
in
loop empty el
- | A.QUESTION (e1, e2, e3) -> begin
+ | Cabs.QUESTION (e1, e2, e3) -> begin
(* Compile the conditional expression *)
let ghost = local_env.is_ghost in
let ce1 = doCondExp (no_paren_local_env local_env) asconst e1 in
@@ -7325,7 +7322,7 @@ and doExp local_env
* the type of the result *)
let r2, se2, e2'o (* is an option. None means use e1 *), t2 =
match e2.expr_node with
- | A.NOTHING -> begin (* The same as the type of e1 *)
+ | Cabs.NOTHING -> begin (* The same as the type of e1 *)
match ce1 with
| CEExp (_, e1') ->
[], unspecified_chunk empty, None, typeOf e1'
@@ -7516,17 +7513,17 @@ and doExp local_env
end
end
end
- | A.GNU_BODY b -> begin
- (* Find the last A.COMPUTATION and remember it. This one is invoked
+ | Cabs.GNU_BODY b -> begin
+ (* Find the last Cabs.COMPUTATION and remember it. This one is invoked
* on the reversed list of statements. *)
let findLastComputation = function
s :: _ ->
let rec findLast st = match st.stmt_node with
- | A.SEQUENCE (_, s, _) -> findLast s
+ | Cabs.SEQUENCE (_, s, _) -> findLast s
| CASE (_, s, _) -> findLast s
| CASERANGE (_, _, s, _) -> findLast s
| LABEL (_, s, _) -> findLast s
- | A.COMPUTATION _ ->
+ | Cabs.COMPUTATION _ ->
begin
match local_env.is_ghost,st.stmt_ghost with
| true,true | false, false -> st
@@ -7543,12 +7540,12 @@ and doExp local_env
let lastComp, isvoidbody =
match what with
| ADrop -> (* We are dropping the result *)
- {stmt_ghost = local_env.is_ghost; stmt_node = A.NOP loc}, true
+ {stmt_ghost = local_env.is_ghost; stmt_node = Cabs.NOP loc}, true
| _ ->
- try findLastComputation (List.rev b.A.bstmts), false
+ try findLastComputation (List.rev b.Cabs.bstmts), false
with Not_found ->
Kernel.fatal ~current:true "Cannot find COMPUTATION in GNU.body"
- (* A.NOP cabslu, true *)
+ (* Cabs.NOP cabslu, true *)
in
let loc = Cabshelper.get_statementloc lastComp in
(* Prepare some data to be filled by doExp ghost *)
@@ -7579,7 +7576,7 @@ and doExp local_env
finishExp [] se e t
end
- | A.LABELADDR l -> begin (* GCC's taking the address of a label *)
+ | Cabs.LABELADDR l -> begin (* GCC's taking the address of a label *)
let l = lookupLabel ghost l in (* To support locally declared labels *)
let addrval =
try H.find gotoTargetHash l
@@ -7594,7 +7591,7 @@ and doExp local_env
(makeCast (integer ~loc addrval) voidPtrType) voidPtrType
end
- | A.EXPR_PATTERN _ -> abort_context "EXPR_PATTERN in cabs2cil input"
+ | Cabs.EXPR_PATTERN _ -> abort_context "EXPR_PATTERN in cabs2cil input"
in
(*let (_a,b,_c,_d) = result in
@@ -7607,26 +7604,26 @@ and doExp local_env
and normalize_unop unop action asconst local_env e what =
match e.expr_node with
- | A.COMMA el -> (* GCC extension *)
+ | Cabs.COMMA el -> (* GCC extension *)
doExp (no_inner_paren local_env) asconst
{ e with
expr_node =
- A.COMMA
+ Cabs.COMMA
(replaceLastInList el
- (fun e -> { e with expr_node = A.UNARY(unop, e)})) }
+ (fun e -> { e with expr_node = Cabs.UNARY(unop, e)})) }
what
- | A.QUESTION (e1, e2, e3) -> (* GCC extension *)
+ | Cabs.QUESTION (e1, e2, e3) -> (* GCC extension *)
doExp (no_inner_paren local_env) asconst
{ e with
expr_node =
- A.QUESTION
+ Cabs.QUESTION
(e1,
- { e2 with expr_node = A.UNARY(unop, e2)},
- { e3 with expr_node = A.UNARY(unop, e3)})}
+ { e2 with expr_node = Cabs.UNARY(unop, e2)},
+ { e3 with expr_node = Cabs.UNARY(unop, e3)})}
what
- | A.PAREN e1 ->
+ | Cabs.PAREN e1 ->
doExp (inner_paren local_env) asconst
- { e with expr_node = A.UNARY(unop, e1)} what
+ { e with expr_node = Cabs.UNARY(unop, e1)} what
| _ ->
action
{ local_env with
@@ -7636,39 +7633,39 @@ and normalize_unop unop action asconst local_env e what =
and normalize_binop binop action local_env asconst le re what =
match le.expr_node with
- | A.COMMA el -> (* GCC extension *)
+ | Cabs.COMMA el -> (* GCC extension *)
doExp (no_inner_paren local_env) asconst
(cabs_exp le.expr_loc
- (A.COMMA
+ (Cabs.COMMA
(replaceLastInList el
- (fun e -> cabs_exp e.expr_loc (A.BINARY(binop, e, re))))))
+ (fun e -> cabs_exp e.expr_loc (Cabs.BINARY(binop, e, re))))))
what
- | A.QUESTION (e1, e2q, e3q) -> (* GCC extension *)
+ | Cabs.QUESTION (e1, e2q, e3q) -> (* GCC extension *)
(*TODO: prevent duplication of e2: this is incorrect
if it contains labels *)
(* let r2,se2,e2,t2 = doExp authorized_reads ghost asconst e2 in*)
doExp (no_inner_paren local_env) asconst
(cabs_exp le.expr_loc
- (A.QUESTION
+ (Cabs.QUESTION
(e1,
- cabs_exp e2q.expr_loc (A.BINARY(binop, e2q, re)),
- cabs_exp e3q.expr_loc (A.BINARY(binop, e3q, re)))))
+ cabs_exp e2q.expr_loc (Cabs.BINARY(binop, e2q, re)),
+ cabs_exp e3q.expr_loc (Cabs.BINARY(binop, e3q, re)))))
what
- | A.CAST (t, A.SINGLE_INIT e) when binop = A.ASSIGN -> (* GCC extension *)
+ | Cabs.CAST (t, Cabs.SINGLE_INIT e) when binop = Cabs.ASSIGN -> (* GCC extension *)
doExp (no_inner_paren local_env) asconst
(cabs_exp le.expr_loc
- (A.CAST
+ (Cabs.CAST
(t,
- A.SINGLE_INIT
+ Cabs.SINGLE_INIT
(cabs_exp e.expr_loc
- (A.BINARY
+ (Cabs.BINARY
(binop, e,
(cabs_exp re.expr_loc
- (A.CAST (t, A.SINGLE_INIT re)))))))))
+ (Cabs.CAST (t, Cabs.SINGLE_INIT re)))))))))
what
- | A.PAREN e1 ->
+ | Cabs.PAREN e1 ->
doExp (inner_paren local_env) asconst
- (cabs_exp le.expr_loc (A.BINARY(binop,e1,re))) what
+ (cabs_exp le.expr_loc (Cabs.BINARY(binop,e1,re))) what
| _ ->
action
{ local_env with is_paren = local_env.inner_paren; inner_paren = false }
@@ -7794,7 +7791,7 @@ and doCondExp local_env asconst
?ctxt (* ctxt is used internally to determine if we should apply
the conditional side effects hook (see above)
and should not appear (i.e. be None) in toplevel calls. *)
- (e: A.expression) : condExpRes =
+ (e: Cabs.expression) : condExpRes =
let ghost = local_env.is_ghost in
let rec addChunkBeforeCE (c0: chunk) ce =
let c0 = remove_effects c0 in
@@ -7817,7 +7814,7 @@ and doCondExp local_env asconst
in
let loc = e.expr_loc in
let result = match e.expr_node with
- | A.BINARY (A.AND, e1, e2) -> begin
+ | Cabs.BINARY (Cabs.AND, e1, e2) -> begin
let ce1 = doCondExp (no_paren_local_env local_env) asconst ?ctxt e1 in
let ce2 = doCondExp (no_paren_local_env local_env) asconst ~ctxt:e e2 in
let ce1 = remove_effects_ce ce1 in
@@ -7836,7 +7833,7 @@ and doCondExp local_env asconst
| _ -> CEAnd (ce1, ce2)
end
- | A.BINARY (A.OR, e1, e2) -> begin
+ | Cabs.BINARY (Cabs.OR, e1, e2) -> begin
let ce1 = doCondExp (no_paren_local_env local_env) asconst ?ctxt e1 in
let ce2 = doCondExp (no_paren_local_env local_env) asconst ~ctxt:e e2 in
let ce1 = remove_effects_ce ce1 in
@@ -7855,7 +7852,7 @@ and doCondExp local_env asconst
| _ -> CEOr (ce1, ce2)
end
- | A.UNARY(A.NOT, e1) -> begin
+ | Cabs.UNARY(Cabs.NOT, e1) -> begin
match doCondExp (no_paren_local_env local_env) asconst ?ctxt e1 with
| CEExp (se1, e) when isEmpty se1 ->
let t = typeOf e in
@@ -7865,7 +7862,7 @@ and doCondExp local_env asconst
| ce1 -> CENot ce1
end
- | A.PAREN e ->
+ | Cabs.PAREN e ->
doCondExp (paren_local_env local_env) asconst ?ctxt e
| _ ->
@@ -7976,7 +7973,7 @@ and compileCondExp ~ghost ce st sf =
(* A special case for conditionals *)
and doCondition local_env asconst
(* If we are in constants, we do our best to eliminate the conditional *)
- (e: A.expression)
+ (e: Cabs.expression)
(st: chunk)
(sf: chunk) : chunk =
if isEmpty st && isEmpty sf(*TODO: ignore attribute FRAMA_C_KEEP_BLOCK*) then
@@ -7998,7 +7995,7 @@ and doCondition local_env asconst
chunk
end
-and doPureExp local_env (e : A.expression) : exp =
+and doPureExp local_env (e : Cabs.expression) : exp =
let (_,se, e', _) = doExp local_env CConst e (AExp None) in
if isNotEmpty se then
Kernel.error
@@ -8011,7 +8008,7 @@ and doFullExp local_env const e what =
(* there is a sequence point after a full exp *)
empty @@ (se', local_env.is_ghost),e,t
-and doInitializer local_env (vi: varinfo) (inite: A.init_expression)
+and doInitializer local_env (vi: varinfo) (inite: Cabs.init_expression)
(* Return the accumulated chunk, the initializer and the new type (might be
* different for arrays), together with the lvals read during evaluation of
* the initializer (for local intialization)
@@ -8025,7 +8022,7 @@ and doInitializer local_env (vi: varinfo) (inite: A.init_expression)
let so = makeSubobj vi vi.vtype NoOffset in
let asconst = if vi.vglob then CConst else CNoConst in
doInit local_env asconst Extlib.nop NoInitPre so
- (unspecified_chunk empty) [ (A.NEXT_INIT, inite) ]
+ (unspecified_chunk empty) [ (Cabs.NEXT_INIT, inite) ]
in
if restl <> [] then
Kernel.warning ~current:true "Ignoring some initializers";
@@ -8067,12 +8064,12 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let whoami fmt = Cil_printer.pp_lval fmt (Var so.host, so.soOff) in
let initl1 =
match initl with
- | (A.NEXT_INIT,
- A.SINGLE_INIT ({ expr_node = A.CAST ((s, dt), ie)} as e)) :: rest ->
+ | (Cabs.NEXT_INIT,
+ Cabs.SINGLE_INIT ({ expr_node = Cabs.CAST ((s, dt), ie)} as e)) :: rest ->
let s', dt', ie' = preprocessCast ghost s dt ie in
- (A.NEXT_INIT,
- A.SINGLE_INIT
- ({expr_node = A.CAST ((s', dt'), ie'); expr_loc = e.expr_loc}))
+ (Cabs.NEXT_INIT,
+ Cabs.SINGLE_INIT
+ ({expr_node = Cabs.CAST ((s', dt'), ie'); expr_loc = e.expr_loc}))
:: rest
| _ -> initl
in
@@ -8081,16 +8078,16 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let initl2 =
match initl1 with
| (what,
- A.SINGLE_INIT
- ({expr_node = A.CAST ((specs, dt), A.COMPOUND_INIT ci)})) :: rest ->
- let s', dt', _ie' = preprocessCast ghost specs dt (A.COMPOUND_INIT ci) in
+ Cabs.SINGLE_INIT
+ ({expr_node = Cabs.CAST ((specs, dt), Cabs.COMPOUND_INIT ci)})) :: rest ->
+ let s', dt', _ie' = preprocessCast ghost specs dt (Cabs.COMPOUND_INIT ci) in
let typ = doOnlyType ghost s' dt' in
if Typ.equal
(Cil.typeDeepDropAllAttributes typ)
(Cil.typeDeepDropAllAttributes so.soTyp)
then
(* Drop the cast *)
- (what, A.COMPOUND_INIT ci) :: rest
+ (what, Cabs.COMPOUND_INIT ci) :: rest
else
(* Keep the cast. A new var will be created to hold
the intermediate value. *)
@@ -8106,25 +8103,25 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
match allinitl with
| [] -> Format.fprintf fmt "[]@."
| (what, ie) :: _ ->
- Cprint.print_init_expression fmt (A.COMPOUND_INIT [(what, ie)])
+ Cprint.print_init_expression fmt (Cabs.COMPOUND_INIT [(what, ie)])
);
match unrollType so.soTyp, allinitl with
(* No more initializers return *)
| _, [] -> acc, preinit, []
(* No more subobjects to initialize *)
- | _, (A.NEXT_INIT, _) :: _ when so.eof -> acc, preinit, allinitl
+ | _, (Cabs.NEXT_INIT, _) :: _ when so.eof -> acc, preinit, allinitl
(* 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, _, _ ),
- (A.NEXT_INIT,
- (A.SINGLE_INIT({ expr_node = A.CONSTANT (A.CONST_STRING s)} as e)|
- A.COMPOUND_INIT
- [(A.NEXT_INIT,
- A.SINGLE_INIT(
+ (Cabs.NEXT_INIT,
+ (Cabs.SINGLE_INIT({ expr_node = Cabs.CONSTANT (Cabs.CONST_STRING s)} as e)|
+ Cabs.COMPOUND_INIT
+ [(Cabs.NEXT_INIT,
+ Cabs.SINGLE_INIT(
{ expr_node =
- A.CONSTANT
- (A.CONST_STRING s)} as e))]))
+ Cabs.CONSTANT
+ (Cabs.CONST_STRING s)} as e))]))
:: restil
when (match unrollType bt with
| TInt((IChar|IUChar|ISChar), _) -> true
@@ -8138,9 +8135,9 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
->
let charinits =
let init c =
- A.NEXT_INIT,
- A.SINGLE_INIT
- { expr_node = A.CONSTANT (A.CONST_CHAR [c]);
+ Cabs.NEXT_INIT,
+ Cabs.SINGLE_INIT
+ { expr_node = Cabs.CONSTANT (Cabs.CONST_CHAR [c]);
expr_loc = e.expr_loc }
in
let collector =
@@ -8179,14 +8176,14 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
* Despite what the compiler says, this match case is used and it is
* important. *)
| TArray(bt, leno, _, _),
- (A.NEXT_INIT,
- (A.SINGLE_INIT({expr_node = A.CONSTANT (A.CONST_WSTRING s)} as e)|
- A.COMPOUND_INIT
- [(A.NEXT_INIT,
- A.SINGLE_INIT(
+ (Cabs.NEXT_INIT,
+ (Cabs.SINGLE_INIT({expr_node = Cabs.CONSTANT (Cabs.CONST_WSTRING s)} as e)|
+ Cabs.COMPOUND_INIT
+ [(Cabs.NEXT_INIT,
+ Cabs.SINGLE_INIT(
{expr_node =
- A.CONSTANT
- (A.CONST_WSTRING s)} as e))]))
+ Cabs.CONSTANT
+ (Cabs.CONST_WSTRING s)} as e))]))
:: restil
when
(let bt' = unrollType bt in
@@ -8214,9 +8211,9 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
if Int64.compare c maxWChar > 0 then (* if c > maxWChar *)
Kernel.error ~once:true ~current:true
"cab2cil:doInit:character 0x%Lx too big." c;
- A.NEXT_INIT,
- A.SINGLE_INIT
- { expr_node = A.CONSTANT (A.CONST_INT (Int64.to_string c));
+ Cabs.NEXT_INIT,
+ Cabs.SINGLE_INIT
+ { expr_node = Cabs.CONSTANT (Cabs.CONST_INT (Int64.to_string c));
expr_loc = e.expr_loc
}
in
@@ -8251,7 +8248,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, _, _), (A.NEXT_INIT, A.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;
@@ -8266,7 +8263,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* 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, _, _), (A.NEXT_INIT, A.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
@@ -8289,7 +8286,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
end
(* A scalar with a single initializer *)
- | _, (A.NEXT_INIT, A.SINGLE_INIT oneinit) :: restil ->
+ | _, (Cabs.NEXT_INIT, Cabs.SINGLE_INIT oneinit) :: restil ->
let r, se, oneinit', t' =
doExp (no_paren_local_env local_env) asconst oneinit (AExp(Some so.soTyp))
in
@@ -8308,7 +8305,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, _, _), (A.NEXT_INIT, A.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 *)
@@ -8340,10 +8337,10 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* We have a designator that tells us to select the matching union field.
* This is to support a GCC extension *)
| TComp(ci, _, _) as targ,
- [(A.NEXT_INIT,
- A.COMPOUND_INIT
- [(A.INFIELD_INIT ("___matching_field", A.NEXT_INIT),
- A.SINGLE_INIT oneinit)])]
+ [(Cabs.NEXT_INIT,
+ Cabs.COMPOUND_INIT
+ [(Cabs.INFIELD_INIT ("___matching_field", Cabs.NEXT_INIT),
+ Cabs.SINGLE_INIT oneinit)])]
when not ci.cstruct ->
(* Do the expression to find its type *)
let _, c, _, t' =
@@ -8362,17 +8359,17 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
if Typ.equal t'noattr (Cil.typeDeepDropAllAttributes targ) then
doInit
local_env asconst add_implicit_ensures preinit so acc
- [(A.NEXT_INIT, A.SINGLE_INIT oneinit)]
+ [(Cabs.NEXT_INIT, Cabs.SINGLE_INIT oneinit)]
else
(* If this is a GNU extension with field-to-union cast find the field *)
let fi = findField (Option.value ~default:[] ci.cfields) in
(* Change the designator and redo *)
doInit
local_env asconst add_implicit_ensures preinit so acc
- [A.INFIELD_INIT (fi.fname, A.NEXT_INIT), A.SINGLE_INIT oneinit]
+ [Cabs.INFIELD_INIT (fi.fname, Cabs.NEXT_INIT), Cabs.SINGLE_INIT oneinit]
(* A structure with a composite initializer. We initialize the fields*)
- | TComp (comp, _, _), (A.NEXT_INIT, A.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 *)
@@ -8395,12 +8392,12 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Continue *)
doInit local_env asconst add_implicit_ensures preinit' so acc' restil
(* A scalar with a initializer surrounded by a number of braces *)
- | t, (A.NEXT_INIT, next) :: restil ->
+ | t, (Cabs.NEXT_INIT, next) :: restil ->
begin
let rec find_one_init c =
match c with
- | A.COMPOUND_INIT [A.NEXT_INIT,next] -> find_one_init next
- | A.SINGLE_INIT oneinit -> oneinit
+ | Cabs.COMPOUND_INIT [Cabs.NEXT_INIT,next] -> find_one_init next
+ | Cabs.SINGLE_INIT oneinit -> oneinit
| _ -> raise Not_found
in
try
@@ -8422,19 +8419,19 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
Cil_printer.pp_typ t
end
(* We have a designator *)
- | _, (what, ie) :: restil when what != A.NEXT_INIT ->
+ | _, (what, ie) :: restil when what != Cabs.NEXT_INIT ->
(* Process a designator and position to the designated subobject *)
let addressSubobj
(so: subobj)
- (what: A.initwhat)
+ (what: Cabs.initwhat)
(acc: chunk) : chunk =
(* Always start from the current element *)
so.stack <- []; so.eof <- false;
normalSubobj so;
- let rec address (what: A.initwhat) (acc: chunk) : chunk =
+ let rec address (what: Cabs.initwhat) (acc: chunk) : chunk =
match what with
- | A.NEXT_INIT -> acc
- | A.INFIELD_INIT (fn, whatnext) -> begin
+ | Cabs.NEXT_INIT -> acc
+ | Cabs.INFIELD_INIT (fn, whatnext) -> begin
match unrollType so.soTyp with
| TComp (comp, _, _) ->
let toinit = fieldsToInit comp (Some fn) in
@@ -8446,7 +8443,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
"Field designator %s not in a struct " fn
end
- | A.ATINDEX_INIT(idx, whatnext) -> begin
+ | Cabs.ATINDEX_INIT(idx, whatnext) -> begin
match unrollType so.soTyp with
| TArray (bt, leno, _, _) ->
let ilen = integerArrayLength leno in
@@ -8474,17 +8471,17 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
| _ -> abort_context "INDEX designator for a non-array"
end
- | A.ATINDEXRANGE_INIT _ -> abort_context "addressSubobj: INDEXRANGE"
+ | Cabs.ATINDEXRANGE_INIT _ -> abort_context "addressSubobj: INDEXRANGE"
in
address what acc
in
(* First expand the INDEXRANGE by making copies *)
- let rec expandRange (top: A.initwhat -> A.initwhat) = function
- | A.INFIELD_INIT (fn, whatnext) ->
- expandRange (fun what -> top (A.INFIELD_INIT(fn, what))) whatnext
- | A.ATINDEX_INIT (idx, whatnext) ->
- expandRange (fun what -> top (A.ATINDEX_INIT(idx, what))) whatnext
- | A.ATINDEXRANGE_INIT (idxs, idxe) ->
+ let rec expandRange (top: Cabs.initwhat -> Cabs.initwhat) = function
+ | Cabs.INFIELD_INIT (fn, whatnext) ->
+ expandRange (fun what -> top (Cabs.INFIELD_INIT(fn, what))) whatnext
+ | Cabs.ATINDEX_INIT (idx, whatnext) ->
+ expandRange (fun what -> top (Cabs.ATINDEX_INIT(idx, what))) whatnext
+ | Cabs.ATINDEXRANGE_INIT (idxs, idxe) ->
let (rs, doidxs, idxs', _) =
doExp (no_paren_local_env local_env) CConst idxs (AExp(Some intType))
in
@@ -8508,19 +8505,19 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let rec loop (i: int) =
if i > last then restil
else
- (top (A.ATINDEX_INIT(
- { expr_node = A.CONSTANT(A.CONST_INT(string_of_int i));
+ (top (Cabs.ATINDEX_INIT(
+ { expr_node = Cabs.CONSTANT(Cabs.CONST_INT(string_of_int i));
expr_loc = fst idxs.expr_loc, snd idxe.expr_loc},
- A.NEXT_INIT)), ie)
+ Cabs.NEXT_INIT)), ie)
:: loop (i + 1)
in
doInit
local_env asconst add_implicit_ensures preinit so acc (loop first)
- | A.NEXT_INIT -> (* We have not found any RANGE *)
+ | Cabs.NEXT_INIT -> (* We have not found any RANGE *)
let acc' = addressSubobj so what acc in
doInit
local_env asconst add_implicit_ensures preinit so acc'
- ((A.NEXT_INIT, ie) :: restil)
+ ((Cabs.NEXT_INIT, ie) :: restil)
in
expandRange (fun x -> x) what
| t, (_what, _ie) :: _ ->
@@ -8528,8 +8525,8 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Create and add to the file (if not already added) a global. Return the
* varinfo *)
-and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A.attribute list))
- (((n,ndt,a,cloc), inite) : A.init_name) : varinfo =
+and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * Cabs.attribute list))
+ (((n,ndt,a,cloc), inite) : Cabs.init_name) : varinfo =
Kernel.debug ~dkey:Kernel.dkey_typing_global "createGlobal: %s" n;
(* If the global is a Frama-C builtin, set the generated flag *)
if is_stdlib_macro n && get_current_stdheader () = "" then begin
@@ -8538,11 +8535,11 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
It is supposed to be a macro name and cannot be declared. See CERT C \
coding rule MSC38-C" n
end;
- let is_fc_builtin {A.expr_node=enode} =
- match enode with A.VARIABLE "FC_BUILTIN" -> true | _ -> false
+ let is_fc_builtin {Cabs.expr_node=enode} =
+ match enode with Cabs.VARIABLE "FC_BUILTIN" -> true | _ -> false
in
- let is_fc_stdlib {A.expr_node=enode} =
- match enode with A.VARIABLE v when v = fc_stdlib -> true | _ -> false
+ let is_fc_stdlib {Cabs.expr_node=enode} =
+ match enode with Cabs.VARIABLE v when v = fc_stdlib -> true | _ -> false
in
let isgenerated =
List.exists (fun (_,el) -> List.exists is_fc_builtin el) a
@@ -8557,7 +8554,7 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
(* Add the variable to the environment before doing the initializer
* because it might refer to the variable itself *)
if isFunctionType vi.vtype then begin
- if inite != A.NO_INIT then
+ if inite != Cabs.NO_INIT then
Kernel.error ~once:true ~current:true
"Function declaration with initializer (%s)\n" vi.vname;
end else if Option.is_some logic_spec then begin
@@ -8567,7 +8564,7 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
end;
let isadef =
not (isFunctionType vi.vtype) &&
- (inite != A.NO_INIT
+ (inite != Cabs.NO_INIT
||
(* tentative definition, but definition nevertheless. *)
vi.vstorage = NoStorage || vi.vstorage = Static)
@@ -8575,7 +8572,7 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * A
let vi, alreadyInEnv = makeGlobalVarinfo isadef vi in
(* Do the initializer and complete the array type if necessary *)
let init : init option =
- if inite = A.NO_INIT then
+ if inite = Cabs.NO_INIT then
None
else
let se, ie', et, _ = doInitializer (ghost_local_env ghost) vi inite in
@@ -8785,8 +8782,8 @@ and cleanup_autoreference vi chunk =
(* Must catch the Static local variables. Make them global *)
and createLocal ghost ((_, sto, _, _) as specs)
- ((((n, ndt, a, cloc) : A.name),
- (inite: A.init_expression)) as init_name)
+ ((((n, ndt, a, cloc) : Cabs.name),
+ (inite: Cabs.init_expression)) as init_name)
: chunk =
let loc = convLoc cloc in
(* Check if we are declaring a function *)
@@ -8844,7 +8841,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
Cil.update_var_type vi (constFoldType vi.vtype);
let init : init option =
- if inite = A.NO_INIT then
+ if inite = Cabs.NO_INIT then
None
else begin
let se, ie', et, _ = doInitializer (ghost_local_env ghost) vi inite in
@@ -8919,7 +8916,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(* Register the length *)
IH.add varSizeArrays vi.vid alloca_size;
(* There can be no initializer for this *)
- if inite != A.NO_INIT then
+ if inite != Cabs.NO_INIT then
Kernel.error ~once:true ~current:true
"Variable-sized array cannot have initializer";
let se0 =
@@ -8995,7 +8992,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
end else empty
in
let se1 = local_var_chunk se1 vi in
- if inite = A.NO_INIT then
+ if inite = Cabs.NO_INIT then
se1 (* skipChunk *)
else begin
(* TODO: if vi occurs in se4, this is not a real initialization. *)
@@ -9034,17 +9031,17 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
let rt, formals, isva, _ = splitFunctionType vtype in
if isva then Kernel.error ~once:true ~current:true "alias unsupported with varargs";
let args = List.map
- (fun (n,_,_) -> { expr_loc = loc; expr_node = A.VARIABLE n})
+ (fun (n,_,_) -> { expr_loc = loc; expr_node = Cabs.VARIABLE n})
(argsToList formals) in
- let call = A.CALL ({expr_loc = loc; expr_node = A.VARIABLE othername}, args,[])
+ let call = Cabs.CALL ({expr_loc = loc; expr_node = Cabs.VARIABLE othername}, args,[])
in
let stmt = {stmt_ghost = false;
stmt_node = if isVoidType rt then
- A.COMPUTATION({expr_loc = loc; expr_node = call}, loc)
- else A.RETURN({expr_loc = loc; expr_node = call}, loc)}
+ Cabs.COMPUTATION({expr_loc = loc; expr_node = call}, loc)
+ else Cabs.RETURN({expr_loc = loc; expr_node = call}, loc)}
in
- let body = { A.blabels = []; A.battrs = []; A.bstmts = [stmt] } in
- let fdef = A.FUNDEF (None, sname, body, loc, loc) in
+ let body = { Cabs.blabels = []; Cabs.battrs = []; Cabs.bstmts = [stmt] } in
+ let fdef = Cabs.FUNDEF (None, sname, body, loc, loc) in
ignore (doDecl empty_local_env true fdef);
(* get the new function *)
let v,_ =
@@ -9055,8 +9052,8 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
(* Do one declaration *)
-and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
- | A.DECDEF (logic_spec, (s, nl), loc) ->
+and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
+ | Cabs.DECDEF (logic_spec, (s, nl), loc) ->
CurrentLoc.set (convLoc loc);
(* Do the specifiers exactly once *)
let sugg =
@@ -9073,7 +9070,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
let bt,_,_,attrs = spec_res in
let vtype, nattr =
doType local_env.is_ghost false
- (AttrName false) bt (A.PARENTYPE(attrs, ndt, a)) in
+ (AttrName false) bt (Cabs.PARENTYPE(attrs, ndt, a)) in
(match filterAttributes "alias" nattr with
| [] -> (* ordinary prototype. *)
ignore (createGlobal local_env.is_ghost logic_spec spec_res name)
@@ -9116,17 +9113,17 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
res
end
end
- | A.TYPEDEF (ng, loc) ->
+ | Cabs.TYPEDEF (ng, loc) ->
CurrentLoc.set (convLoc loc); doTypedef local_env.is_ghost ng; empty
- | A.ONLYTYPEDEF (s, loc) ->
+ | Cabs.ONLYTYPEDEF (s, loc) ->
CurrentLoc.set (convLoc loc); doOnlyTypedef local_env.is_ghost s; empty
- | A.GLOBASM (s,loc) when isglobal ->
+ | Cabs.GLOBASM (s,loc) when isglobal ->
CurrentLoc.set (convLoc loc);
cabsPushGlobal (GAsm (s, CurrentLoc.get ())); empty
- | A.PRAGMA (a, loc) when isglobal -> begin
+ | Cabs.PRAGMA (a, loc) when isglobal -> begin
CurrentLoc.set (convLoc loc);
match doAttr local_env.is_ghost ("dummy", [a]) with
| [Attr("dummy", [a'])] ->
@@ -9149,8 +9146,8 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
| _ -> Kernel.fatal ~current:true "Too many attributes in pragma"
end
- | A.FUNDEF (spec,((specs,(n,dt,a, _)) : A.single_name),
- (body : A.block), loc1, loc2) when isglobal ->
+ | Cabs.FUNDEF (spec,((specs,(n,dt,a, _)) : Cabs.single_name),
+ (body : Cabs.block), loc1, loc2) when isglobal ->
begin
let ghost = local_env.is_ghost in
let idloc = loc1 in
@@ -9180,12 +9177,12 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* Setup the environment. Add the formals to the locals. Maybe
* they need alpha-conv *)
enterScope (); (* Start the scope *)
- ignore (V.visitCabsBlock (new gatherLabelsClass) body);
+ ignore (Cabsvisit.visitCabsBlock (new gatherLabelsClass) body);
CurrentLoc.set idloc;
IH.clear varSizeArrays;
(* Enter all the function's labels into the alpha conversion table *)
- ignore (V.visitCabsBlock (new registerLabelsVisitor) body);
+ ignore (Cabsvisit.visitCabsBlock (new registerLabelsVisitor) body);
CurrentLoc.set idloc;
(* Do not process transparent unions in function definitions.
@@ -9196,7 +9193,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
!currentFunctionFDEC.svar.vinline <- inl;
let ftyp, funattr =
doType local_env.is_ghost false
- (AttrName false) bt (A.PARENTYPE(attrs, dt, a)) in
+ (AttrName false) bt (Cabs.PARENTYPE(attrs, dt, a)) in
if hasAttribute "thread" funattr then begin
let wkey = Kernel.wkey_inconsistent_specifier in
let source = fst funloc in
@@ -9542,7 +9539,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
dl;
empty
- | A.GLOBANNOT (decl) when isglobal ->
+ | Cabs.GLOBANNOT (decl) when isglobal ->
begin
List.iter
(fun decl ->
@@ -9564,7 +9561,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
end;
empty
- | A.CUSTOM (custom, name, location) when isglobal ->
+ | Cabs.CUSTOM (custom, name, location) when isglobal ->
begin
let loc = convLoc location in
CurrentLoc.set loc;
@@ -9578,19 +9575,19 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
"%s. Ignoring custom annotation" msg
end;
empty
- | A.CUSTOM _ | A.GLOBANNOT _ | A.PRAGMA _ | A.GLOBASM _ | A.FUNDEF _ ->
+ | Cabs.CUSTOM _ | Cabs.GLOBANNOT _ | Cabs.PRAGMA _ | Cabs.GLOBASM _ | Cabs.FUNDEF _ ->
Kernel.fatal ~current:true "this form of declaration must be global"
-and doTypedef ghost ((specs, nl): A.name_group) =
+and doTypedef ghost ((specs, nl): Cabs.name_group) =
(* Do the specifiers exactly once *)
let bt, sto, inl, attrs = doSpecList ghost (suggestAnonName nl) specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
"Storage or inline specifier not allowed in typedef";
- let createTypedef ((n,ndt,a,_) : A.name) =
+ let createTypedef ((n,ndt,a,_) : Cabs.name) =
(* E.s (error "doTypeDef") *)
let newTyp, tattr =
- doType ghost false AttrType bt (A.PARENTYPE(attrs, ndt, a)) in
+ doType ghost false AttrType bt (Cabs.PARENTYPE(attrs, ndt, a)) in
checkTypedefSize n newTyp;
let tattr = fc_stdlib_attribute tattr in
let newTyp' = cabsTypeAddAttributes tattr newTyp in
@@ -9681,13 +9678,13 @@ and doTypedef ghost ((specs, nl): A.name_group) =
in
List.iter createTypedef nl
-and doOnlyTypedef ghost (specs: A.spec_elem list) : unit =
+and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
let bt, sto, inl, attrs = doSpecList ghost "" specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
"Storage or inline specifier not allowed in typedef";
let restyp, nattr =
- doType ghost false AttrType bt (A.PARENTYPE(attrs, A.JUSTBASE, []))
+ doType ghost false AttrType bt (Cabs.PARENTYPE(attrs, Cabs.JUSTBASE, []))
in
if nattr <> [] then
Kernel.warning ~current:true "Ignoring identifier attribute";
@@ -9698,9 +9695,9 @@ and doOnlyTypedef ghost (specs: A.spec_elem list) : unit =
let isadef =
List.exists
(function
- A.SpecType(A.Tstruct(_, Some _, _)) -> true
- | A.SpecType(A.Tunion(_, Some _, _)) -> true
- | A.SpecType(A.Tenum(_, Some _, _)) -> true
+ Cabs.SpecType(Cabs.Tstruct(_, Some _, _)) -> true
+ | Cabs.SpecType(Cabs.Tunion(_, Some _, _)) -> true
+ | Cabs.SpecType(Cabs.Tenum(_, Some _, _)) -> true
| _ -> false) specs
in
match restyp with
@@ -9721,12 +9718,12 @@ and doOnlyTypedef ghost (specs: A.spec_elem list) : unit =
enumeration type"
(* Now define the processors for body and statement *)
-and doBody local_env (blk: A.block) : chunk =
+and doBody local_env (blk: Cabs.block) : chunk =
let ghost = local_env.is_ghost in
(* Rename the labels and add them to the environment *)
List.iter (fun l -> ignore (genNewLocalLabel ghost l)) blk.blabels;
(* See if we have some attributes *)
- let battrs = doAttributes ghost blk.A.battrs in
+ let battrs = doAttributes ghost blk.Cabs.battrs in
let bodychunk =
afterConversion ~ghost
@@ -9804,7 +9801,7 @@ and doBody local_env (blk: A.block) : chunk =
else prev @@ (res, ghost)
in ((new_behaviors, keep_next), chunk))
(([],false),empty)
- blk.A.bstmts))
+ blk.Cabs.bstmts))
in
if battrs == [] && bodychunk.locals == []
then begin
@@ -9823,7 +9820,7 @@ and doBody local_env (blk: A.block) : chunk =
and doBodyScope local_env blk =
enterScope (); let res = doBody local_env blk in exitScope (); res
-and doStatement local_env (s : A.statement) : chunk =
+and doStatement local_env (s : Cabs.statement) : chunk =
let mk_loop_annot a loc =
try
List.map
@@ -9838,10 +9835,10 @@ and doStatement local_env (s : A.statement) : chunk =
let ghost = s.stmt_ghost in
let local_env = { local_env with is_ghost = ghost } in
match s.stmt_node with
- | A.NOP loc ->
+ | Cabs.NOP loc ->
{ empty
with stmts = [mkEmptyStmt ~ghost ~valid_sid ~loc (), [],[],[],[]]}
- | A.COMPUTATION (e, loc) ->
+ | Cabs.COMPUTATION (e, loc) ->
CurrentLoc.set (convLoc loc);
let (lasts, data) = !gnu_body_result in
if lasts == s then begin (* This is the last in a GNU_BODY *)
@@ -9865,7 +9862,7 @@ and doStatement local_env (s : A.statement) : chunk =
s'
end
- | A.BLOCK (b, loc,_) ->
+ | Cabs.BLOCK (b, loc,_) ->
CurrentLoc.set (convLoc loc);
let c = doBodyScope local_env b in
let b = c2block ~ghost c in
@@ -9873,18 +9870,18 @@ and doStatement local_env (s : A.statement) : chunk =
let res = s2c (mkStmt ~ghost ~valid_sid (Block b)) in
{ res with cases = c.cases }
- | A.SEQUENCE (s1, s2, _) ->
+ | Cabs.SEQUENCE (s1, s2, _) ->
let c1 = doStatement local_env s1 in
let c2 = doStatement local_env s2 in
c1 @@ (c2, ghost)
- | A.IF(e,st,sf,loc) ->
+ | Cabs.IF(e,st,sf,loc) ->
let st' = doStatement local_env st in
let sf' = doStatement local_env sf in
CurrentLoc.set (convLoc loc);
doCondition local_env CNoConst e st' sf'
- | A.WHILE(a,e,s,loc) ->
+ | Cabs.WHILE(a,e,s,loc) ->
startLoop true;
let a = mk_loop_annot a loc in
let s' = doStatement local_env s in
@@ -9901,7 +9898,7 @@ and doStatement local_env (s : A.statement) : chunk =
((doCondition local_env CNoConst e skipChunk break_cond)
@@ (s', ghost))
- | A.DOWHILE(a, e,s,loc) ->
+ | Cabs.DOWHILE(a, e,s,loc) ->
startLoop false;
let a = mk_loop_annot a loc in
let s' = doStatement local_env s in
@@ -9934,7 +9931,7 @@ and doStatement local_env (s : A.statement) : chunk =
exitLoop ();
loopChunk ~ghost ~sattr:[Attr("dowhile",[])] a (s' @@ (s'', ghost))
- | A.FOR(a,fc1,e2,e3,s,loc) -> begin
+ | Cabs.FOR(a,fc1,e2,e3,s,loc) -> begin
let loc' = convLoc loc in
CurrentLoc.set loc';
enterScope (); (* Just in case we have a declaration *)
@@ -9956,7 +9953,7 @@ and doStatement local_env (s : A.statement) : chunk =
exitLoop ();
let res =
match e2.expr_node with
- | A.NOTHING -> (* This means true *)
+ | Cabs.NOTHING -> (* This means true *)
se1 @@ (loopChunk ~sattr:[Attr("for",[])] ~ghost a (s' @@ (s'', ghost)), ghost)
| _ ->
se1 @@
@@ -9973,17 +9970,17 @@ and doStatement local_env (s : A.statement) : chunk =
end else res
end
- | A.BREAK loc ->
+ | Cabs.BREAK loc ->
let loc' = convLoc loc in
CurrentLoc.set loc';
breakChunk ~ghost loc'
- | A.CONTINUE loc ->
+ | Cabs.CONTINUE loc ->
let loc' = convLoc loc in
CurrentLoc.set loc';
continueOrLabelChunk ~ghost loc'
- | A.RETURN ({ expr_node = A.NOTHING}, loc) ->
+ | Cabs.RETURN ({ expr_node = Cabs.NOTHING}, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
if not (isVoidType !currentReturnType) then
@@ -9992,7 +9989,7 @@ and doStatement local_env (s : A.statement) : chunk =
Cil_printer.pp_typ !currentReturnType;
returnChunk ~ghost None loc'
- | A.RETURN (e, loc) ->
+ | Cabs.RETURN (e, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
(* Sometimes we return the result of a void function call *)
@@ -10011,7 +10008,7 @@ and doStatement local_env (s : A.statement) : chunk =
se @@ (returnChunk ~ghost (Some e'') loc', ghost)
end
- | A.SWITCH (e, s, loc) ->
+ | Cabs.SWITCH (e, s, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
let (se, e', et) = doFullExp local_env CNoConst e (AExp None) in
@@ -10024,7 +10021,7 @@ and doStatement local_env (s : A.statement) : chunk =
exit_break_env ();
se @@ (switchChunk ~ghost e' s' loc', ghost)
- | A.CASE (e, s, loc) ->
+ | Cabs.CASE (e, s, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
let (se, e', _) = doFullExp local_env CConst e (AExp None) in
@@ -10040,7 +10037,7 @@ and doStatement local_env (s : A.statement) : chunk =
particular in the case of a sizeof with side-effects. *)
se @@ (chunk,ghost)
- | A.CASERANGE (el, eh, s, loc) ->
+ | Cabs.CASERANGE (el, eh, s, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc;
let (sel, el', _) = doFullExp local_env CNoConst el (AExp None) in
@@ -10063,11 +10060,11 @@ and doStatement local_env (s : A.statement) : chunk =
(caseRangeChunk ~ghost (mkAll il) loc' (doStatement local_env s),
ghost)
- | A.DEFAULT (s, loc) ->
+ | Cabs.DEFAULT (s, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
defaultChunk ~ghost loc' (doStatement local_env s)
- | A.LABEL (l, s, loc) ->
+ | Cabs.LABEL (l, s, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
add_label_env l;
@@ -10078,13 +10075,13 @@ and doStatement local_env (s : A.statement) : chunk =
in
C_logic_env.reset_current_label (); chunk
- | A.GOTO (l, loc) ->
+ | Cabs.GOTO (l, loc) ->
let loc' = convLoc loc in
CurrentLoc.set loc';
(* Maybe we need to rename this label *)
gotoChunk ~ghost (lookupLabel ghost l) loc'
- | A.COMPGOTO (e, loc) -> begin
+ | Cabs.COMPGOTO (e, loc) -> begin
let loc' = convLoc loc in
CurrentLoc.set loc';
(* Do the expression *)
@@ -10104,7 +10101,7 @@ and doStatement local_env (s : A.statement) : chunk =
let vchunk = createLocal
local_env.is_ghost
(intType, NoStorage, false, [])
- (("__compgoto", A.JUSTBASE, [], loc), A.NO_INIT)
+ (("__compgoto", Cabs.JUSTBASE, [], loc), Cabs.NO_INIT)
in
if not (isEmpty vchunk) then
Kernel.fatal ~current:true
@@ -10132,10 +10129,10 @@ and doStatement local_env (s : A.statement) : chunk =
end
end
- | A.DEFINITION d ->
+ | Cabs.DEFINITION d ->
doDecl local_env false d
- | A.ASM (asmattr, tmpls, details, loc) ->
+ | Cabs.ASM (asmattr, tmpls, details, loc) ->
(* Make sure all the outs are variables *)
let loc' = convLoc loc in
let attr' = doAttributes local_env.is_ghost asmattr in
@@ -10368,7 +10365,7 @@ let convFile (path, f) =
(fun name (resTyp, argTypes, isva) ->
ignore (setupBuiltin name (resTyp, ArgTypes argTypes, isva)));
let globalidx = ref 0 in
- let doOneGlobal (ghost,(d: A.definition)) =
+ let doOneGlobal (ghost,(d: Cabs.definition)) =
let local_env = ghost_local_env ghost in
let s = doDecl local_env true d in
if isNotEmpty s then