aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Bitfields.ml10
-rw-r--r--cparser/Ceval.ml41
-rw-r--r--cparser/Cutil.ml7
-rw-r--r--cparser/Cutil.mli4
-rw-r--r--cparser/Elab.ml34
-rw-r--r--cparser/Env.ml11
-rw-r--r--cparser/ExtendedAsm.ml1
-rw-r--r--cparser/Lexer.mll5
-rw-r--r--cparser/PackedStructs.ml12
-rw-r--r--cparser/StructReturn.ml2
-rw-r--r--cparser/Transform.ml4
-rw-r--r--cparser/Transform.mli2
-rw-r--r--cparser/Unblock.ml19
13 files changed, 58 insertions, 94 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index bbc39456..d55a6d36 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -19,7 +19,7 @@
open Printf
open Machine
-open C
+open !C
open Cutil
open Transform
@@ -60,12 +60,6 @@ let unsigned_ikind_for_carrier nbits =
if nbits <= 8 * !config.sizeof_longlong then IULongLong else
assert false
-let fits_unsigned v n =
- v >= 0L && v < Int64.shift_left 1L n
-
-let fits_signed v n =
- let p = Int64.shift_left 1L (n-1) in v >= Int64.neg p && v < p
-
let is_signed_enum_bitfield env sid fld eid n =
let info = Env.find_enum env eid in
if List.for_all (fun (_, v, _) -> int_representable v n false) info.Env.ei_members
@@ -73,7 +67,7 @@ let is_signed_enum_bitfield env sid fld eid n =
else if List.for_all (fun (_, v, _) -> int_representable v n true) info.Env.ei_members
then true
else begin
- Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.name n;
+ Cerrors.warning "Warning: not all values of type 'enum %s' can be represented in bit-field '%s' of struct '%s' (%d bits are not enough)" eid.name fld sid.C.name n;
false
end
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 74b535d4..c3d7eeeb 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -91,7 +91,7 @@ let is_signed env ty =
| TEnum(_, _) -> is_signed_ikind enum_ikind
| _ -> false
-let cast env ty_to ty_from v =
+let cast env ty_to v =
match unroll env ty_to, v with
| TInt(IBool, _), _ ->
if boolean_value v then I 1L else I 0L
@@ -118,12 +118,12 @@ let unop env op tyres ty v =
| Olognot, _, _ -> if boolean_value v then I 0L else I 1L
| Onot, _, I n -> I (Int64.lognot n)
| _ -> raise Notconst
- in cast env ty tyres res
+ in cast env ty res
-let comparison env direction ptraction tyop ty1 v1 ty2 v2 =
+let comparison env direction ptraction tyop v1 v2 =
(* tyop = type at which the comparison is done *)
let b =
- match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+ match cast env tyop v1, cast env tyop v2 with
| I n1, I n2 ->
if is_signed env tyop
then direction (compare n1 n2) 0
@@ -143,25 +143,25 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
match op with
| Oadd ->
if is_arith_type env ty1 && is_arith_type env ty2 then begin
- match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+ match cast env tyop v1, cast env tyop v2 with
| I n1, I n2 -> I (Int64.add n1 n2)
| _, _ -> raise Notconst
end else
raise Notconst
| Osub ->
if is_arith_type env ty1 && is_arith_type env ty2 then begin
- match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+ match cast env tyop v1, cast env tyop v2 with
| I n1, I n2 -> I (Int64.sub n1 n2)
| _, _ -> raise Notconst
end else
raise Notconst
| Omul ->
- begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+ begin match cast env tyop v1, cast env tyop v2 with
| I n1, I n2 -> I (Int64.mul n1 n2)
| _, _ -> raise Notconst
end
| Odiv ->
- begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with
+ begin match cast env tyop v1, cast env tyop v2 with
| I n1, I n2 ->
if n2 = 0L then raise Notconst else
if is_signed env tyop then I (Int64.div n1 n2)
@@ -206,17 +206,17 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
| _, _ -> raise Notconst
end
| Oeq ->
- comparison env (=) (Some false) tyop ty1 v1 ty2 v2
+ comparison env (=) (Some false) tyop v1 v2
| One ->
- comparison env (<>) (Some true) tyop ty1 v1 ty2 v2
+ comparison env (<>) (Some true) tyop v1 v2
| Olt ->
- comparison env (<) None tyop ty1 v1 ty2 v2
+ comparison env (<) None tyop v1 v2
| Ogt ->
- comparison env (>) None tyop ty1 v1 ty2 v2
+ comparison env (>) None tyop v1 v2
| Ole ->
- comparison env (<=) None tyop ty1 v1 ty2 v2
+ comparison env (<=) None tyop v1 v2
| Oge ->
- comparison env (>=) None tyop ty1 v1 ty2 v2
+ comparison env (>=) None tyop v1 v2
| Ocomma ->
v2
| Ologand ->
@@ -229,7 +229,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 =
else if boolean_value v2 then I 1L else I 0L
| _ -> raise Notconst
(* force normalization of result, e.g. of double to float *)
- in cast env tyres tyres res
+ in cast env tyres res
let rec expr env e =
match e.edesc with
@@ -253,11 +253,10 @@ let rec expr env e =
binop env op ty e.etyp e1.etyp (expr env e1) e2.etyp (expr env e2)
| EConditional(e1, e2, e3) ->
if boolean_value (expr env e1)
- then cast env e.etyp e2.etyp (expr env e2)
- else cast env e.etyp e3.etyp (expr env e3)
- (* | ECast(TInt (_, _), EConst (CFloat (_, _))) -> TODO *)
+ then cast env e.etyp (expr env e2)
+ else cast env e.etyp (expr env e3)
| ECast(ty, e1) ->
- cast env ty e1.etyp (expr env e1)
+ cast env ty (expr env e1)
| ECompound _ ->
raise Notconst
| ECall _ ->
@@ -265,14 +264,14 @@ let rec expr env e =
let integer_expr env e =
try
- match cast env (TInt(ILongLong, [])) e.etyp (expr env e) with
+ match cast env (TInt(ILongLong, [])) (expr env e) with
| I n -> Some n
| _ -> None
with Notconst -> None
let constant_expr env ty e =
try
- match unroll env ty, cast env ty e.etyp (expr env e) with
+ match unroll env ty, cast env ty (expr env e) with
| TInt(ik, _), I n -> Some(CInt(n, ik, ""))
| TPtr(_, _), I n -> Some(CInt(n, IInt, ""))
| TPtr(_, _), S s -> Some(CStr s)
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index c15a7adf..1bbb8e98 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -15,7 +15,6 @@
(* Operations on C types and abstract syntax *)
-open Printf
open Cerrors
open C
open Env
@@ -194,7 +193,7 @@ let strip_attributes_type t attr =
(* Remove the last attribute from the toplevel and return the changed type *)
let strip_last_attribute typ =
- let rec hd_opt l = match l with
+ let hd_opt l = match l with
[] -> None,[]
| a::rest -> Some a,rest in
match typ with
@@ -561,7 +560,7 @@ let incomplete_type env t =
(* Computing composite_info records *)
-let composite_info_decl env su attr =
+let composite_info_decl su attr =
{ ci_kind = su; ci_members = [];
ci_alignof = None; ci_sizeof = None;
ci_attr = attr }
@@ -892,7 +891,7 @@ let is_literal_0 e =
let is_debug_stmt s =
let is_debug_call = function
- | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug"
+ | (ECall ({edesc = EVar id; _},_)) -> id.C.name = "__builtin_debug"
| _ -> false in
match s.sdesc with
| Sdo {edesc = e;_} ->
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b353cba3..3dcfe4aa 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -102,13 +102,11 @@ val sizeof_ikind: ikind -> int
(* Return the size of the given integer kind. *)
val sizeof_fkind: fkind -> int
(* Return the size of the given float kind. *)
-val is_signed_ikind: ikind -> bool
- (* Return true if the given integer kind is signed, false if unsigned. *)
(* Computing composite_info records *)
val composite_info_decl:
- Env.t -> struct_or_union -> attributes -> Env.composite_info
+ struct_or_union -> attributes -> Env.composite_info
val composite_info_def:
Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
val struct_layout:
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index d7a1212a..130f37cd 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -19,9 +19,9 @@
open Format
open Machine
-open Cabs
+open !Cabs
open Cabshelper
-open C
+open !C
open Cutil
open Env
@@ -203,7 +203,7 @@ let elab_int_constant loc s0 =
in
(v, ty)
-let elab_float_constant loc f =
+let elab_float_constant f =
let ty = match f.suffix_FI with
| Some ("l"|"L") -> FLongDouble
| Some ("f"|"F") -> FFloat
@@ -253,11 +253,11 @@ let elab_string_literal loc wide chars =
if wide then
CWStr chars
else begin
- let res = String.create (List.length chars) in
+ let res = Bytes.create (List.length chars) in
List.iteri
- (fun i c -> res.[i] <- Char.unsafe_chr (Int64.to_int c))
+ (fun i c -> Bytes.set res i (Char.unsafe_chr (Int64.to_int c)))
chars;
- CStr res
+ CStr (Bytes.to_string res)
end
let elab_constant loc = function
@@ -265,7 +265,7 @@ let elab_constant loc = function
let (v, ik) = elab_int_constant loc s in
CInt(v, ik, s)
| CONST_FLOAT f ->
- let (v, fk) = elab_float_constant loc f in
+ let (v, fk) = elab_float_constant f in
CFloat(v, fk)
| CONST_CHAR(wide, s) ->
CInt(elab_char_constant loc wide s, IInt, "")
@@ -319,7 +319,7 @@ let elab_gcc_attr loc env = function
warning loc "cannot parse '%s' attribute, ignored" v; []
end
-let is_power_of_two n = n > 0L && Int64.(logand n (pred n)) = 0L
+let is_power_of_two n = n > 0L && Int64.logand n (Int64.pred n) = 0L
let extract_alignas loc a =
match a with
@@ -569,7 +569,7 @@ and elab_parameters env params =
let (vars, _) = mmap elab_parameter (Env.new_scope env) params in
(* Catch special case f(t) where t is void or a typedef to void *)
match vars with
- | [ ( {name=""}, t) ] when is_void_type env t -> []
+ | [ ( {C.name=""}, t) ] when is_void_type env t -> []
| _ -> vars
(* Elaboration of a function parameter *)
@@ -578,7 +578,7 @@ and elab_parameter env (PARAM (spec, id, decl, attr, loc)) =
let (sto, inl, tydef, bty, env1) = elab_specifier loc env spec in
if tydef then
error loc "'typedef' used in function parameter";
- let ((ty, _), env2) = elab_type_declarator loc env1 bty false decl in
+ let ((ty, _), _) = elab_type_declarator loc env1 bty false decl in
let ty = add_attributes_type (elab_attributes env attr) ty in
if sto <> Storage_default && sto <> Storage_register then
error loc
@@ -753,7 +753,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* declaration of an incomplete struct or union *)
if tag = "" then
error loc "anonymous, incomplete struct or union";
- let ci = composite_info_decl env kind attrs in
+ let ci = composite_info_decl kind attrs in
(* enter it with a new name *)
let (tag', env') = Env.enter_composite env tag ci in
(* emit it *)
@@ -761,7 +761,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(tag', env')
| _, Some members ->
(* definition of a complete struct or union *)
- let ci1 = composite_info_decl env kind attrs in
+ let ci1 = composite_info_decl kind attrs in
(* enter it, incomplete, with a new name *)
let (tag', env') = Env.enter_composite env tag ci1 in
(* emit a declaration so that inner structs and unions can refer to it *)
@@ -900,8 +900,6 @@ module I = struct
* ident (* union type *)
* field (* current member *)
- type state = zipinit * init (* current point & init for this point *)
-
(* The initial state: default initialization, current point at top *)
let top env name ty = (Ztop(name, ty), default_init env ty)
@@ -1727,7 +1725,7 @@ let elab_expr loc env a =
| (TInt _ | TEnum _), TPtr _ ->
warning "comparison between integer and pointer";
EBinop(op, b1, b2, TPtr(TVoid [], []))
- | ty1, ty2 ->
+ | _, _ ->
error "illegal comparison between types@ %a@ and %a"
Cprint.typ b1.etyp Cprint.typ b2.etyp in
{ edesc = resdesc; etyp = TInt(IInt, []) }
@@ -1860,7 +1858,7 @@ let enter_decdefs local loc env sto dl =
fatal_error loc "'register' on global declaration";
if sto <> Storage_default && dl = [] then
warning loc "Storage class specifier on empty declaration";
- let rec enter_decdef (decls, env) (s, ty, init) =
+ let enter_decdef (decls, env) (s, ty, init) =
let isfun = is_function_type env ty in
if sto = Storage_extern && init <> NO_INIT then
error loc "'extern' declaration cannot have an initializer";
@@ -1936,7 +1934,7 @@ let elab_fundef env spec name defs body loc =
"Illegal declaration of function parameter" in
let (kr_params_defs, env1) = mmap elab_kr_param_def env1 defs in
let kr_params_defs = List.concat kr_params_defs in
- let rec search_param_type param =
+ let search_param_type param =
match List.filter (fun (p, _) -> p = param) kr_params_defs with
| [] ->
(* Parameter is not declared, defaults to "int" in ISO C90,
@@ -1960,7 +1958,7 @@ let elab_fundef env spec name defs body loc =
(ty_ret, params, vararg, attr)
| _ -> fatal_error loc "wrong type for function definition" in
(* Enter function in the environment, for recursive references *)
- let (fun_id, sto1, env1,ty) = enter_or_refine_ident false loc env1 s sto ty in
+ let (fun_id, sto1, env1, _) = enter_or_refine_ident false loc env1 s sto ty in
(* Enter parameters in the environment *)
let env2 =
List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty)
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 65df6cb9..dae79ef2 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -118,12 +118,6 @@ let lookup_ident env s =
with Not_found ->
raise(Error(Unbound_identifier s))
-let lookup_tag env s =
- try
- IdentMap.lookup s env.env_tag
- with Not_found ->
- raise(Error(Unbound_tag(s, "tag")))
-
let lookup_struct env s =
try
let (id, ci as res) = IdentMap.lookup s env.env_tag in
@@ -169,11 +163,6 @@ let find_ident env id =
with Not_found ->
raise(Error(Unbound_identifier(id.name)))
-let find_tag env id =
- try IdentMap.find id env.env_tag
- with Not_found ->
- raise(Error(Unbound_tag(id.name, "tag")))
-
let find_struct env id =
try
let ci = IdentMap.find id env.env_tag in
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index 94fcda31..c3d80272 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -33,7 +33,6 @@ open Printf
open Machine
open C
open Cutil
-open Env
open Cerrors
(* Renaming of labeled and numbered operands *)
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index bcf2ada0..871f2bf9 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -17,8 +17,7 @@
open Lexing
open Pre_parser
open Pre_parser_aux
-open Cabshelper
-open Camlcoq
+open !Cabshelper
module SSet = Set.Make(String)
@@ -430,7 +429,7 @@ and singleline_comment = parse
open Streams
open Specif
open Parser
- open Aut.GramDefs
+ open !Aut.GramDefs
(* This is the main entry point to the lexer. *)
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 6ea5d121..aafa1caa 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -127,7 +127,7 @@ let transf_composite loc env su id attrs ml =
(* Accessor functions *)
-let lookup_function loc env name =
+let lookup_function env name =
match Env.lookup_ident env name with
| (id, II_ident(sto, ty)) -> (id, ty)
| (id, II_enum _) -> raise (Env.Error(Env.Unbound_identifier name))
@@ -161,14 +161,14 @@ let bswap_read loc env lval =
try
if !use_reversed then begin
let (id, fty) =
- lookup_function loc env (sprintf "__builtin_read%d_reversed" bsize) in
+ lookup_function env (sprintf "__builtin_read%d_reversed" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lval)] in
let call = {edesc = ECall(fn, args); etyp = aty} in
ecast_opt env ty call
end else begin
let (id, fty) =
- lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
+ lookup_function env (sprintf "__builtin_bswap%d" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env aty lval] in
let call = {edesc = ECall(fn, args); etyp = aty} in
@@ -188,14 +188,14 @@ let bswap_write loc env lhs rhs =
try
if !use_reversed then begin
let (id, fty) =
- lookup_function loc env (sprintf "__builtin_write%d_reversed" bsize) in
+ lookup_function env (sprintf "__builtin_write%d_reversed" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs);
ecast_opt env aty rhs] in
{edesc = ECall(fn, args); etyp = TVoid[]}
end else begin
let (id, fty) =
- lookup_function loc env (sprintf "__builtin_bswap%d" bsize) in
+ lookup_function env (sprintf "__builtin_bswap%d" bsize) in
let fn = {edesc = EVar id; etyp = fty} in
let args = [ecast_opt env aty rhs] in
let call = {edesc = ECall(fn, args); etyp = aty} in
@@ -403,7 +403,7 @@ let rec transf_globdecls env accu = function
| Union -> attr
| Struct -> remove_custom_attributes ["packed";"__packed__"] attr in
transf_globdecls
- (Env.add_composite env id (composite_info_decl env su attr'))
+ (Env.add_composite env id (composite_info_decl su attr'))
({g with gdesc = Gcompositedecl(su, id, attr')} :: accu)
gl
| Gcompositedef(su, id, attr, fl) ->
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 4e019380..04f0021a 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -19,7 +19,7 @@
open Machine
open Configuration
-open C
+open !C
open Cutil
open Transform
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 840234b8..0a2ce3bb 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -45,7 +45,7 @@ let new_temp ?(name = "t") ty =
let attributes_to_remove_from_temp = add_attributes [AConst] [AVolatile]
-let mk_temp env ?(name = "t") ty =
+let mk_temp env ty =
new_temp (remove_attributes_type env attributes_to_remove_from_temp ty)
(* Bind a l-value to a temporary variable if it is not invariant. *)
@@ -211,7 +211,7 @@ let program
Env.add_ident env f.fd_name f.fd_storage (fundef_typ f))
| Gcompositedecl(su, id, attr) ->
(Gcompositedecl(su, id, attr),
- Env.add_composite env id (composite_info_decl env su attr))
+ Env.add_composite env id (composite_info_decl su attr))
| Gcompositedef(su, id, attr, fl) ->
let (attr', fl') = composite env su id attr fl in
(Gcompositedef(su, id, attr', fl'),
diff --git a/cparser/Transform.mli b/cparser/Transform.mli
index a04896a9..dbd8e575 100644
--- a/cparser/Transform.mli
+++ b/cparser/Transform.mli
@@ -18,7 +18,7 @@ val reset_temps : unit -> unit
val get_temps : unit -> C.decl list
val new_temp_var : ?name:string -> C.typ -> C.ident
val new_temp : ?name:string -> C.typ -> C.exp
-val mk_temp : Env.t -> ?name:string -> C.typ -> C.exp
+val mk_temp : Env.t -> C.typ -> C.exp
(** Avoiding repeated evaluation of a l-value *)
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index ef8bc91c..0669be6e 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -64,17 +64,6 @@ let add_inits_stmt loc inits s =
(fun e s -> sseq loc {sdesc = Sdo e; sloc = loc} s)
inits s
-(* Prepend assignments to the given expression. *)
-(* Associate to the left so that it prints more nicely *)
-
-let add_inits_expr inits e =
- match inits with
- | [] -> e
- | i1 :: il ->
- let comma a b =
- { edesc = EBinop(Ocomma, a, b, b.etyp); etyp = b.etyp } in
- comma (List.fold_left comma i1 il) e
-
(* Record new variables to be locally or globally defined *)
let local_variables = ref ([]: decl list)
@@ -357,7 +346,7 @@ let unblock_fundef env f =
(* Simplification of compound literals within a top-level declaration *)
-let unblock_decl loc env ((sto, id, ty, optinit) as d) =
+let unblock_decl env ((sto, id, ty, optinit) as d) =
match optinit with
| None -> [d]
| Some init ->
@@ -375,8 +364,8 @@ let rec unblock_glob env accu = function
| [] -> List.rev accu
| g :: gl ->
match g.gdesc with
- | Gdecl((sto, id, ty, init) as d) ->
- let dl = unblock_decl g.gloc env d in
+ | Gdecl d ->
+ let dl = unblock_decl env d in
unblock_glob env
(List.rev_append
(List.map (fun d' -> {g with gdesc = Gdecl d'}) dl)
@@ -387,7 +376,7 @@ let rec unblock_glob env accu = function
unblock_glob env ({g with gdesc = Gfundef f'} :: accu) gl
| Gcompositedecl(su, id, attr) ->
unblock_glob
- (Env.add_composite env id (composite_info_decl env su attr))
+ (Env.add_composite env id (composite_info_decl su attr))
(g :: accu) gl
| Gcompositedef(su, id, attr, fl) ->
unblock_glob
generated by cgit (git 2.34.1) at 2024-07-09 19:21:00 +0000