From 906873ee165cbaabf36ca51792eb5a498a12bd72 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 12 Oct 2015 16:58:23 +0200 Subject: Move strip functions to Cutil. Since the strip functions might be useful in other context and is more general then the debug information. Bug 17392. --- cparser/Cutil.ml | 42 ++++++++++++++++++++++++++++++++++++++++++ cparser/Cutil.mli | 4 ++++ 2 files changed, 46 insertions(+) (limited to 'cparser') diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 0def347f..60bcc1a7 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -177,6 +177,48 @@ let remove_attributes_type env attr t = let erase_attributes_type env t = change_attributes_type env (fun a -> []) t +(* Remove all attributes from type that are not contained in attr *) +let strip_attributes_type t attr = + let strip = List.filter (fun a -> List.mem a attr) in + match t with + | TVoid at -> TVoid (strip at) + | TInt (k,at) -> TInt (k,strip at) + | TFloat (k,at) -> TFloat(k,strip at) + | TPtr (t,at) -> TPtr(t,strip at) + | TArray (t,s,at) -> TArray(t,s,strip at) + | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at) + | TNamed (n,at) -> TNamed(n,strip at) + | TStruct (n,at) -> TStruct(n,strip at) + | TUnion (n,at) -> TUnion(n,strip at) + | TEnum (n,at) -> TEnum(n,strip at) + +(* 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 + [] -> None,[] + | a::rest -> Some a,rest in + match typ with + | TVoid at -> let l,r = hd_opt at in + l,TVoid r + | TInt (k,at) -> let l,r = hd_opt at in + l,TInt (k,r) + | TFloat (k,at) -> let l,r = hd_opt at in + l,TFloat (k,r) + | TPtr (t,at) -> let l,r = hd_opt at in + l,TPtr(t,r) + | TArray (t,s,at) -> let l,r = hd_opt at in + l,TArray(t,s,r) + | TFun (t,arg,v,at) -> let l,r = hd_opt at in + l,TFun(t,arg,v,r) + | TNamed (n,at) -> let l,r = hd_opt at in + l,TNamed(n,r) + | TStruct (n,at) -> let l,r = hd_opt at in + l,TStruct(n,r) + | TUnion (n,at) -> let l,r = hd_opt at in + l,TUnion(n,r) + | TEnum (n,at) -> let l,r = hd_opt at in + l,TEnum(n,r) + (* Extracting alignment value from a set of attributes. Return 0 if none. *) let alignas_attribute al = diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index a322bfb1..a09316ad 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -56,6 +56,10 @@ val attr_is_type_related: attribute -> bool (* Is an attribute type-related (true) or variable-related (false)? *) val attr_inherited_by_members: attribute -> bool (* Is an attribute of a composite inherited by members of the composite? *) +val strip_attributes_type: typ -> attribute list -> typ + (* Remove all attributes from the given type that are not contained in the list *) +val strip_last_attribute: typ -> attribute option * typ + (* Remove the last top level attribute and return it *) (* Type compatibility *) -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- cparser/Bitfields.ml | 12 ++++++------ cparser/C.mli | 10 +++++----- cparser/Cabshelper.ml | 4 ++-- cparser/Ceval.ml | 10 +++++----- cparser/Cleanup.ml | 6 +++--- cparser/Cprint.ml | 8 ++++---- cparser/Cutil.ml | 38 +++++++++++++++++++------------------- cparser/Cutil.mli | 4 ++-- cparser/Elab.ml | 48 ++++++++++++++++++++++++------------------------ cparser/Env.ml | 12 ++++++------ cparser/ExtendedAsm.ml | 10 +++++----- cparser/GCC.ml | 16 ++++++++-------- cparser/PackedStructs.ml | 8 ++++---- cparser/Rename.ml | 16 ++++++++-------- cparser/StructReturn.ml | 10 +++++----- cparser/Transform.ml | 6 +++--- cparser/Transform.mli | 6 +++--- cparser/Unblock.ml | 20 ++++++++++---------- 18 files changed, 122 insertions(+), 122 deletions(-) (limited to 'cparser') diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index d064f4b1..223ee3ca 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -191,12 +191,12 @@ let transf_composite env su id attr ml = (* Bitfield manipulation expressions *) let left_shift_count bf = - intconst + intconst (Int64.of_int (8 * !config.sizeof_int - (bf.bf_pos + bf.bf_size))) IInt let right_shift_count bf = - intconst + intconst (Int64.of_int (8 * !config.sizeof_int - bf.bf_size)) IInt @@ -303,7 +303,7 @@ let bitfield_initializer bf i = (* Associate to the left so that it prints more nicely *) let or_expr_list = function - | [] -> intconst 0L IUInt + | [] -> intconst 0L IUInt | [e] -> e | e1 :: el -> List.fold_left @@ -409,7 +409,7 @@ let rec transf_exp env ctx e = | Some(ex, bf) -> transf_post env ctx (op_for_incr_decr op) ex bf e1.etyp end - | EUnop(op, e1) -> + | EUnop(op, e1) -> {edesc = EUnop(op, transf_exp env Val e1); etyp = e.etyp} | EBinop(Oassign, e1, e2, ty) -> @@ -433,7 +433,7 @@ let rec transf_exp env ctx e = transf_assignop env ctx (op_for_assignop op) ex bf e2 ty end | EBinop(Ocomma, e1, e2, ty) -> - {edesc = EBinop(Ocomma, transf_exp env Effects e1, + {edesc = EBinop(Ocomma, transf_exp env Effects e1, transf_exp env Val e2, ty); etyp = e.etyp} | EBinop(op, e1, e2, ty) -> @@ -534,5 +534,5 @@ let program p = Transform.program ~composite:transf_composite ~decl: transf_decl - ~fundef:transf_fundef + ~fundef:transf_fundef p diff --git a/cparser/C.mli b/cparser/C.mli index 72e1f787..8d8f2805 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -27,7 +27,7 @@ type ident = (* Kinds of integers *) -type ikind = +type ikind = | IBool (** [_Bool] *) | IChar (** [char] *) | ISChar (** [signed char] *) @@ -39,12 +39,12 @@ type ikind = | ILong (** [long] *) | IULong (** [unsigned long] *) | ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *) - | IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft + | IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft Visual C) *) (** Kinds of floating-point numbers*) -type fkind = +type fkind = FFloat (** [float] *) | FDouble (** [double] *) | FLongDouble (** [long double] *) @@ -73,7 +73,7 @@ type attr_arg = | AInt of int64 | AString of string -type attribute = +type attribute = | AConst | AVolatile | ARestrict @@ -216,7 +216,7 @@ and stmt_desc = | Sdecl of decl | Sasm of attributes * string * asm_operand list * asm_operand list * string list -and slabel = +and slabel = | Slabel of string | Scase of exp | Sdefault diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml index 5e6a19d0..890679b4 100644 --- a/cparser/Cabshelper.ml +++ b/cparser/Cabshelper.ml @@ -16,8 +16,8 @@ open Cabs -let cabslu = {lineno = -10; - filename = "cabs loc unknown"; +let cabslu = {lineno = -10; + filename = "cabs loc unknown"; byteno = -10; ident = 0} diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index ba7cdabc..74b535d4 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -124,7 +124,7 @@ let comparison env direction ptraction tyop ty1 v1 ty2 v2 = (* tyop = type at which the comparison is done *) let b = match cast env tyop ty1 v1, cast env tyop ty2 v2 with - | I n1, I n2 -> + | I n1, I n2 -> if is_signed env tyop then direction (compare n1 n2) 0 else direction (int64_unsigned_compare n1 n2) 0 (* including pointers *) @@ -162,7 +162,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = end | Odiv -> begin match cast env tyop ty1 v1, cast env tyop ty2 v2 with - | I n1, I n2 -> + | I n1, I n2 -> if n2 = 0L then raise Notconst else if is_signed env tyop then I (Int64.div n1 n2) else I (int64_unsigned_div n1 n2) @@ -170,7 +170,7 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = end | Omod -> begin match v1, v2 with - | I n1, I n2 -> + | I n1, I n2 -> if n2 = 0L then raise Notconst else if is_signed env tyop then I (Int64.rem n1 n2) else I (int64_unsigned_mod n1 n2) @@ -220,11 +220,11 @@ let binop env op tyop tyres ty1 v1 ty2 v2 = | Ocomma -> v2 | Ologand -> - if boolean_value v1 + if boolean_value v1 then if boolean_value v2 then I 1L else I 0L else I 0L | Ologor -> - if boolean_value v1 + if boolean_value v1 then I 1L else if boolean_value v2 then I 1L else I 0L | _ -> raise Notconst diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml index c81fd498..c8a900d5 100644 --- a/cparser/Cleanup.ml +++ b/cparser/Cleanup.ml @@ -92,7 +92,7 @@ let rec add_stmt s = | Sbreak -> () | Scontinue -> () | Sswitch(e, s1) -> add_exp e; add_stmt s1 - | Slabeled(lbl, s) -> + | Slabeled(lbl, s) -> begin match lbl with Scase e -> add_exp e | _ -> () end; add_stmt s | Sgoto lbl -> () @@ -187,7 +187,7 @@ let saturate p = let remove_unused_debug = function | Gdecl (_,id,_,_) -> Debug.remove_unused id | Gfundef f -> Debug.remove_unused f.fd_name - | _ -> () + | _ -> () let rec simpl_globdecls accu = function | [] -> accu @@ -212,6 +212,6 @@ let program p = let p' = simpl_globdecls [] p in referenced := IdentSet.empty; p' - + diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 1af5af1e..e80a4c8e 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -81,7 +81,7 @@ let const pp = function if c >= 32L && c <= 126L && c <> 34L && c <>92L then fprintf pp "%c" (Char.chr (Int64.to_int c)) else fprintf pp "\" \"\\x%02Lx\" \"" c) - l; + l; fprintf pp "\"" | CEnum(id, v) -> ident pp id @@ -216,7 +216,7 @@ let rec exp pp (prec, a) = if assoc = LtoR then (prec', prec' + 1) else (prec' + 1, prec') in - if prec' < prec + if prec' < prec then fprintf pp "@[(" else fprintf pp "@["; begin match a.edesc with @@ -329,7 +329,7 @@ let rec exp pp (prec, a) = begin match al with | [] -> () | a1 :: al -> - fprintf pp "%a" exp (2, a1); + fprintf pp "%a" exp (2, a1); List.iter (fun a -> fprintf pp ",@ %a" exp (2, a)) al end; fprintf pp ")@]" @@ -394,7 +394,7 @@ exception Not_expr let rec exp_of_stmt s = match s.sdesc with | Sdo e -> e - | Sseq(s1, s2) -> + | Sseq(s1, s2) -> {edesc = EBinop(Ocomma, exp_of_stmt s1, exp_of_stmt s2, TVoid []); etyp = TVoid []} | Sif(e, s1, s2) -> diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 60bcc1a7..a86c779f 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -44,7 +44,7 @@ let rec add_attributes (al1: attributes) (al2: attributes) = else if a1 > a2 then a2 :: add_attributes al1 al2' else a1 :: add_attributes al1' al2' -let rec remove_attributes (al1: attributes) (al2: attributes) = +let rec remove_attributes (al1: attributes) (al2: attributes) = (* viewed as sets: al1 \ al2 *) match al1, al2 with | [], _ -> [] @@ -91,7 +91,7 @@ let attr_is_type_related = function | Attr(("packed" | "__packed__"), _) -> true | _ -> false -(* Is an attribute applicable to a whole array (true) or only to +(* Is an attribute applicable to a whole array (true) or only to array elements (false)? *) let attr_array_applicable = function @@ -114,10 +114,10 @@ let rec add_attributes_type attr t = | TInt(ik, a) -> TInt(ik, add_attributes attr a) | TFloat(fk, a) -> TFloat(fk, add_attributes attr a) | TPtr(ty, a) -> TPtr(ty, add_attributes attr a) - | TArray(ty, sz, a) -> + | TArray(ty, sz, a) -> let (attr_arr, attr_elt) = List.partition attr_array_applicable attr in TArray(add_attributes_type attr_elt ty, sz, add_attributes attr_arr a) - | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr + | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr a) | TNamed(s, a) -> TNamed(s, add_attributes attr a) | TStruct(s, a) -> TStruct(s, add_attributes attr a) @@ -144,7 +144,7 @@ let rec attributes_of_type env t = | TArray(ty, sz, a) -> add_attributes a (attributes_of_type env ty) | TFun(ty, params, vararg, a) -> a | TNamed(s, a) -> attributes_of_type env (unroll env t) - | TStruct(s, a) -> + | TStruct(s, a) -> let ci = Env.find_struct env s in add_attributes ci.ci_attr a | TUnion(s, a) -> let ci = Env.find_union env s in add_attributes ci.ci_attr a @@ -179,7 +179,7 @@ let erase_attributes_type env t = (* Remove all attributes from type that are not contained in attr *) let strip_attributes_type t attr = - let strip = List.filter (fun a -> List.mem a attr) in + let strip = List.filter (fun a -> List.mem a attr) in match t with | TVoid at -> TVoid (strip at) | TInt (k,at) -> TInt (k,strip at) @@ -193,7 +193,7 @@ let strip_attributes_type t attr = | TEnum (n,at) -> TEnum(n,strip at) (* Remove the last attribute from the toplevel and return the changed type *) -let strip_last_attribute typ = +let strip_last_attribute typ = let rec hd_opt l = match l with [] -> None,[] | a::rest -> Some a,rest in @@ -306,9 +306,9 @@ let combine_types mode env t1 t2 = | _, TNamed _ -> comp m t1 (unroll env t2) | TStruct(s1, a1), TStruct(s2, a2) -> TStruct(comp_base s1 s2, comp_attr m a1 a2) - | TUnion(s1, a1), TUnion(s2, a2) -> + | TUnion(s1, a1), TUnion(s2, a2) -> TUnion(comp_base s1 s2, comp_attr m a1 a2) - | TEnum(s1, a1), TEnum(s2, a2) -> + | TEnum(s1, a1), TEnum(s2, a2) -> TEnum(comp_base s1 s2, comp_attr m a1 a2) | _, _ -> raise Incompat @@ -376,7 +376,7 @@ let pack_bitfields ml = in let (nbits, ml') = pack 0 ml in let (sz, al) = - (* A lone bitfield of width 0 consumes no space and aligns to 1 *) + (* A lone bitfield of width 0 consumes no space and aligns to 1 *) if nbits = 0 then (0, 1) else if nbits <= 8 then (1, 1) else if nbits <= 16 then (2, 2) else @@ -487,7 +487,7 @@ let rec sizeof env t = | TEnum(_, _) -> Some(sizeof_ikind enum_ikind) (* Compute the size of a union. - It is the size is the max of the sizes of fields. + It is the size is the max of the sizes of fields. Not done here but in composite_info_decl: rounding size to alignment. *) let sizeof_union env members = @@ -539,7 +539,7 @@ let struct_layout env members = end | m :: rem -> match alignof env m.fld_typ, sizeof env m.fld_typ with - | Some a, Some s -> + | Some a, Some s -> let offset = align ofs a in struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem | _, _ -> [] @@ -580,11 +580,11 @@ let composite_info_def env su attr m = let int_representable v nbits sgn = if nbits >= 64 then true else - if sgn then + if sgn then let p = Int64.shift_left 1L (nbits - 1) in Int64.neg p <= v && v < p else 0L <= v && v < Int64.shift_left 1L nbits - + (* Type of a function definition *) let fundef_typ fd = @@ -709,9 +709,9 @@ let pointer_decay env t = | TFun _ as ty -> TPtr(ty, []) | t -> t -(* The usual unary conversions (H&S 6.3.3) *) +(* The usual unary conversions (H&S 6.3.3) *) -let unary_conversion env t = +let unary_conversion env t = match unroll env t with (* Promotion of small integer types *) | TInt(kind, attr) -> @@ -774,7 +774,7 @@ let binary_conversion env t1 t2 = (* Conversion on function arguments (with protoypes) *) -let argument_conversion env t = +let argument_conversion env t = (* Arrays and functions degrade automatically to pointers *) (* Other types are not changed *) match unroll env t with @@ -970,7 +970,7 @@ let rec eaddrof e = match e.edesc with | EUnop(Oderef, e1) -> e1 | EBinop(Ocomma, e1, e2, _) -> ecomma e1 (eaddrof e2) - | EConditional(e1, e2, e3) -> + | EConditional(e1, e2, e3) -> { edesc = EConditional(e1, eaddrof e2, eaddrof e3); etyp = TPtr(e.etyp, []) } | _ -> { edesc = EUnop(Oaddrof, e); etyp = TPtr(e.etyp, []) } @@ -1092,7 +1092,7 @@ let rec subst_stmt phi s = | Sblock sl -> Sblock (List.map (subst_stmt phi) sl) | Sdecl d -> Sdecl (subst_decl phi d) | Sasm(attr, template, outputs, inputs, clob) -> - let subst_asm_operand (lbl, cstr, e) = + let subst_asm_operand (lbl, cstr, e) = (lbl, cstr, subst_expr phi e) in Sasm(attr, template, List.map subst_asm_operand outputs, diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index a09316ad..8b6c609b 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -69,7 +69,7 @@ type attr_handling = | AttrIgnoreAll val compatible_types : attr_handling -> Env.t -> typ -> typ -> bool - (* Check that the two given types are compatible. + (* Check that the two given types are compatible. The attributes in the types are compared according to the first argument: - [AttrCompat]: the types must have the same standard attributes ([const], [volatile], [restrict]) but may differ on custom attributes. @@ -229,7 +229,7 @@ val ecommalist : exp list -> exp -> exp val sskip: stmt (* The [skip] statement. No location. *) val sseq : location -> stmt -> stmt -> stmt - (* Return the statement [s1; s2], optimizing the cases + (* Return the statement [s1; s2], optimizing the cases where [s1] or [s2] is [skip], or [s2] is a block. *) val sassign : location -> exp -> exp -> stmt (* Return the statement [exp1 = exp2;] *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 4d3d1d02..0e445b9d 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -103,7 +103,7 @@ let elab_funbody_f : (C.typ -> Env.t -> statement -> C.stmt) ref (** * Elaboration of constants - C99 section 6.4.4 *) -let has_suffix s suff = +let has_suffix s suff = let ls = String.length s and lsuff = String.length suff in ls >= lsuff && String.sub s (ls - lsuff) lsuff = suff @@ -111,7 +111,7 @@ let chop_last s n = assert (String.length s >= n); String.sub s 0 (String.length s - n) -let has_prefix s pref = +let has_prefix s pref = let ls = String.length s and lpref = String.length pref in ls >= lpref && String.sub s 0 lpref = pref @@ -195,7 +195,7 @@ let elab_int_constant loc s0 = in (* Find smallest allowable type that fits *) let ty = - try List.find (fun ty -> integer_representable v ty) + try List.find (fun ty -> integer_representable v ty) (if base = 10 then dec_kinds else hex_kinds) with Not_found -> error loc "integer literal '%s' cannot be represented" s0; @@ -224,7 +224,7 @@ let elab_char_constant loc wide chars = let max_digit = Int64.shift_left 1L nbits in let max_val = Int64.shift_left 1L (64 - nbits) in let v = - List.fold_left + List.fold_left (fun acc d -> if acc < 0L || acc >= max_val then error loc "character constant overflows"; @@ -243,7 +243,7 @@ let elab_char_constant loc wide chars = IInt) let elab_string_literal loc wide chars = - let nbits = if wide then 8 * !config.sizeof_wchar else 8 in + let nbits = if wide then 8 * !config.sizeof_wchar else 8 in let char_max = Int64.shift_left 1L nbits in List.iter (fun c -> @@ -390,7 +390,7 @@ let rec elab_specifier ?(only = false) loc env specifier = let sto = ref Storage_default and inline = ref false and attr = ref [] - and tyspecs = ref [] + and tyspecs = ref [] and typedef = ref false in let do_specifier = function @@ -404,7 +404,7 @@ let rec elab_specifier ?(only = false) loc env specifier = | STATIC -> sto := Storage_static | EXTERN -> sto := Storage_extern | REGISTER -> sto := Storage_register - | TYPEDEF -> + | TYPEDEF -> if !typedef then error loc "multiple uses of 'typedef'"; typedef := true @@ -590,7 +590,7 @@ and elab_name env spec (Name (id, decl, attr, loc)) = let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in if tydef then error loc "'typedef' is forbidden here"; - let (ty, env'') = elab_type_declarator loc env' bty decl in + let (ty, env'') = elab_type_declarator loc env' bty decl in let a = elab_attributes env attr in (id, sto, inl, add_attributes_type a ty, env'') @@ -605,7 +605,7 @@ and elab_name_group loc env (spec, namelist) = error loc "'inline' is forbidden here"; let elab_one_name env (Name (id, decl, attr, loc)) = let (ty, env1) = - elab_type_declarator loc env bty decl in + elab_type_declarator loc env bty decl in let a = elab_attributes env attr in ((id, add_attributes_type a ty), env1) in (mmap elab_one_name env' namelist, sto) @@ -617,7 +617,7 @@ and elab_init_name_group loc env (spec, namelist) = elab_specifier ~only:(namelist=[]) loc env spec in let elab_one_name env (Init_name (Name (id, decl, attr, loc), init)) = let (ty, env1) = - elab_type_declarator loc env bty decl in + elab_type_declarator loc env bty decl in let a = elab_attributes env attr in if inl && not (is_function_type env ty) then error loc "'inline' can only appear on functions"; @@ -681,7 +681,7 @@ and elab_field_group env (Field_group (spec, fieldlist, loc)) = error loc "bit size of '%s' is not a compile-time constant" id; None end in - { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } + { fld_name = id; fld_typ = ty; fld_bitfield = optbitsize' } in (List.map2 elab_bitfield fieldlist names, env') @@ -818,7 +818,7 @@ and elab_enum only loc tag optmembers attrs env = let elab_type loc env spec decl = let (sto, inl, tydef, bty, env') = elab_specifier loc env spec in - let (ty, env'') = elab_type_declarator loc env' bty decl in + let (ty, env'') = elab_type_declarator loc env' bty decl in if sto <> Storage_default || inl || tydef then error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast"; (ty, env'') @@ -977,7 +977,7 @@ module I = struct if fld.fld_name = fld1.fld_name then i else default_init env fld1.fld_typ) - end + end | (TStruct _ | TUnion _), Init_single a -> (* This is a previous whole-struct initialization that we are going to overwrite. Revert to the default initializer. *) @@ -990,7 +990,7 @@ module I = struct let index env (z, i as zi) n = match unroll env (typeof zi), i with | TArray(ty, sz, _), Init_array il -> - if n >= 0L && index_below n sz then begin + if n >= 0L && index_below n sz then begin let dfl = default_init env ty in let rec loop p before after = if p = n then @@ -1044,7 +1044,7 @@ end let rec elab_designator loc env zi desig = match desig with - | [] -> + | [] -> zi | INFIELD_INIT name :: desig' -> begin match I.member env zi name with @@ -1103,7 +1103,7 @@ let rec elab_list zi il first = and elab_item zi item il = let ty = I.typeof zi in match item, unroll env ty with - (* Special case char array = "string literal" + (* Special case char array = "string literal" or wchar array = L"wide string literal" *) | (SINGLE_INIT (CONSTANT (CONST_STRING(w, s))) | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_STRING(w, s)))]), @@ -1737,8 +1737,8 @@ let elab_expr loc env a = match args, params with | [], [] -> [] | [], _::_ -> err "not enough arguments in function call"; [] - | _::_, [] -> - if vararg + | _::_, [] -> + if vararg then args else (err "too many arguments in function call"; args) | arg1 :: argl, (_, ty_p) :: paraml -> @@ -1773,7 +1773,7 @@ let elab_for_expr loc env = function (* Handling of __func__ (section 6.4.2.2) *) -let __func__type_and_init s = +let __func__type_and_init s = (TArray(TInt(IChar, [AConst]), Some(Int64.of_int (String.length s + 1)), []), init_char_array_string None s) @@ -1894,7 +1894,7 @@ let elab_fundef env spec name body loc = (* Extract info from type *) let (ty_ret, params, vararg, attr) = match ty with - | TFun(ty_ret, Some params, vararg, attr) -> + | TFun(ty_ret, Some params, vararg, attr) -> if wrap incomplete_type loc env1 ty_ret && not (is_void_type env ty_ret) then fatal_error loc "return type is an incomplete type"; (ty_ret, params, vararg, attr) @@ -1997,7 +1997,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) (* "int x = 12, y[10], *z" *) | DECDEF(init_name_group, loc) -> - let ((dl, env1), sto, tydef) = + let ((dl, env1), sto, tydef) = elab_init_name_group loc env init_name_group in if tydef then let env2 = enter_typedefs loc env1 sto dl @@ -2101,7 +2101,7 @@ let rec elab_stmt env ctx s = if not (is_scalar_type env a'.etyp) then error loc "the condition of 'if' does not have scalar type"; let s1' = elab_stmt env ctx s1 in - let s2' = + let s2' = match s2 with | None -> sskip | Some s2 -> elab_stmt env ctx s2 @@ -2134,12 +2134,12 @@ let rec elab_stmt env ctx s = | Some (FC_DECL def) -> let (dcl, env') = elab_definition true (Env.new_scope env) def in let loc = elab_loc (get_definitionloc def) in - (sskip, env', + (sskip, env', Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in let a2' = match a2 with | None -> intconst 1L IInt - | Some a2 -> elab_expr loc env' a2 + | Some a2 -> elab_expr loc env' a2 in if not (is_scalar_type env' a2'.etyp) then error loc "the condition of 'for' does not have scalar type"; diff --git a/cparser/Env.ml b/cparser/Env.ml index 6610c159..65df6cb9 100644 --- a/cparser/Env.ml +++ b/cparser/Env.ml @@ -132,7 +132,7 @@ let lookup_struct env s = res with Not_found -> raise(Error(Unbound_tag(s, "struct"))) - + let lookup_union env s = try let (id, ci as res) = IdentMap.lookup s env.env_tag in @@ -141,7 +141,7 @@ let lookup_union env s = res with Not_found -> raise(Error(Unbound_tag(s, "union"))) - + let lookup_composite env s = try Some (IdentMap.lookup s env.env_tag) with Not_found -> None @@ -191,7 +191,7 @@ let find_union env id = ci with Not_found -> raise(Error(Unbound_tag(id.name, "union"))) - + let find_member ci m = List.find (fun f -> f.fld_name = m) ci @@ -258,7 +258,7 @@ let add_typedef env id info = let add_enum env id info = let add_enum_item env (id, v, exp) = { env with env_ident = IdentMap.add id (II_enum v) env.env_ident } in - List.fold_left add_enum_item + List.fold_left add_enum_item { env with env_enum = IdentMap.add id info env.env_enum } info.ei_members @@ -270,12 +270,12 @@ let composite_tag_name name = if name = "" then "" else name let error_message = function - | Unbound_identifier name -> + | Unbound_identifier name -> sprintf "Unbound identifier '%s'" name | Unbound_tag(name, kind) -> sprintf "Unbound %s '%s'" kind (composite_tag_name name) | Tag_mismatch(name, expected, actual) -> - sprintf "'%s' was declared as a %s but is used as a %s" + sprintf "'%s' was declared as a %s but is used as a %s" (composite_tag_name name) actual expected | Unbound_typedef name -> sprintf "Unbound typedef '%s'" name diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml index 05084561..94fcda31 100644 --- a/cparser/ExtendedAsm.ml +++ b/cparser/ExtendedAsm.ml @@ -18,7 +18,7 @@ (* The [transf_asm] function in this module takes a full GCC-style extended asm statement and puts it in the form supported by CompCert, namely: - - 0 or 1 output of kind "r" + - 0 or 1 output of kind "r" - 0, 1 or several inputs of kind "r". Inputs and outputs of kind "m" (memory location) are emulated by taking the address of the operand and treating it as @@ -116,7 +116,7 @@ let rec transf_inputs loc env accu pos pos' subst = function transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1) (set_label_reg lbl pos pos' subst) inputs end - + (* Transform the output operands: - outputs of kind "=m" become an input (equal to the address of the output) *) @@ -147,7 +147,7 @@ let transf_outputs loc env = function | outputs -> error "%aUnsupported feature: asm statement with 2 or more outputs" formatloc loc; - (* Bind the outputs so that we don't get another error + (* Bind the outputs so that we don't get another error when substituting the text *) let rec bind_outputs pos subst = function | [] -> (None, [], subst, pos, pos) @@ -165,7 +165,7 @@ let check_clobbers loc clob = || List.mem c' Machregsaux.scratch_register_names || c' = "MEMORY" || c' = "CC" then () - else error "%aError: unrecognized asm register clobber '%s'" + else error "%aError: unrecognized asm register clobber '%s'" formatloc loc c) clob @@ -174,7 +174,7 @@ let check_clobbers loc clob = let re_asm_placeholder = Str.regexp "\\(%[QR]?\\([0-9]+\\|\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\)\\|%%\\)" -let rename_placeholders loc template subst = +let rename_placeholders loc template subst = let rename p = if p = "%%" then p else try diff --git a/cparser/GCC.ml b/cparser/GCC.ml index 030f300b..f7f64a4e 100644 --- a/cparser/GCC.ml +++ b/cparser/GCC.ml @@ -65,7 +65,7 @@ let builtins = { "__builtin_acosl", (longDoubleType, [ longDoubleType ], false); "__builtin_alloca", (voidPtrType, [ uintType ], false); - + "__builtin_asin", (doubleType, [ doubleType ], false); "__builtin_asinf", (floatType, [ floatType ], false); "__builtin_asinl", (longDoubleType, [ longDoubleType ], false); @@ -76,7 +76,7 @@ let builtins = { "__builtin_atan2", (doubleType, [ doubleType; doubleType ], false); "__builtin_atan2f", (floatType, [ floatType; floatType ], false); - "__builtin_atan2l", (longDoubleType, [ longDoubleType; + "__builtin_atan2l", (longDoubleType, [ longDoubleType; longDoubleType ], false); "__builtin_ceil", (doubleType, [ doubleType ], false); @@ -133,12 +133,12 @@ let builtins = { "__builtin_frexp", (doubleType, [ doubleType; intPtrType ], false); "__builtin_frexpf", (floatType, [ floatType; intPtrType ], false); - "__builtin_frexpl", (longDoubleType, [ longDoubleType; + "__builtin_frexpl", (longDoubleType, [ longDoubleType; intPtrType ], false); "__builtin_ldexp", (doubleType, [ doubleType; intType ], false); "__builtin_ldexpf", (floatType, [ floatType; intType ], false); - "__builtin_ldexpl", (longDoubleType, [ longDoubleType; + "__builtin_ldexpl", (longDoubleType, [ longDoubleType; intType ], false); "__builtin_log", (doubleType, [ doubleType ], false); @@ -149,10 +149,10 @@ let builtins = { "__builtin_log10f", (floatType, [ floatType ], false); "__builtin_log10l", (longDoubleType, [ longDoubleType ], false); - "__builtin_modff", (floatType, [ floatType; + "__builtin_modff", (floatType, [ floatType; TPtr(floatType,[]) ], false); - "__builtin_modfl", (longDoubleType, [ longDoubleType; - TPtr(longDoubleType, []) ], + "__builtin_modfl", (longDoubleType, [ longDoubleType; + TPtr(longDoubleType, []) ], false); "__builtin_nan", (doubleType, [ charConstPtrType ], false); @@ -210,7 +210,7 @@ let builtins = { "__builtin_tanhl", (longDoubleType, [ longDoubleType ], false); "__builtin_va_end", (voidType, [ voidPtrType ], false); - "__builtin_varargs_start", + "__builtin_varargs_start", (voidType, [ voidPtrType ], false); (* When we elaborate builtin_stdarg_start/builtin_va_start, second argument is passed by address *) diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index ca6c9da5..c163989e 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -190,7 +190,7 @@ let bswap_write loc env lhs rhs = let (id, fty) = lookup_function loc 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); + let args = [ecast_opt env (TPtr(aty,[])) (eaddrof lhs); ecast_opt env aty rhs] in {edesc = ECall(fn, args); etyp = TVoid[]} end else begin @@ -216,7 +216,7 @@ let transf_expr loc env ctx e = let is_byteswapped_ptr ty fieldname = match unroll env ty with | TPtr(ty', _) -> is_byteswapped ty' fieldname - | _ -> false in + | _ -> false in (* Transformation of l-values. Return transformed expr plus [true] if l-value is a byte-swapped field and [false] otherwise. *) @@ -232,7 +232,7 @@ let transf_expr loc env ctx e = let (e1', swap) = lvalue e1 in ({edesc = EBinop(Oindex, e1', e2, tyres); etyp = e.etyp}, swap) | _ -> - (texp Val e, false) + (texp Val e, false) and texp ctx e = match e.edesc with @@ -401,7 +401,7 @@ let rec transf_globdecls env accu = function let attr' = match su with | Union -> attr - | Struct -> remove_custom_attributes ["packed";"__packed__"] attr in + | Struct -> remove_custom_attributes ["packed";"__packed__"] attr in transf_globdecls (Env.add_composite env id (composite_info_decl env su attr')) ({g with gdesc = Gcompositedecl(su, id, attr')} :: accu) diff --git a/cparser/Rename.ml b/cparser/Rename.ml index b0dc120f..4b387b0d 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -42,20 +42,20 @@ let enter_public env id = { re_id = IdentMap.add id id env.re_id; re_public = StringMap.add id.name id env.re_public; re_used = StringSet.add id.name env.re_used } - + let enter_static env id file = try let id' = StringMap.find id.name env.re_public in { env with re_id = IdentMap.add id id' env.re_id } with Not_found -> let file = String.map (fun a -> match a with 'a'..'z' | 'A'..'Z' | '0'..'9' -> a | _ -> '_') file in - let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in + let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in { re_id = IdentMap.add id id' env.re_id; re_public = env.re_public; re_used = StringSet.add id'.name env.re_used } (* For static or local identifiers, we make up a new name if needed *) -(* If the same identifier has already been declared, +(* If the same identifier has already been declared, don't rename a second time *) let rename env id = @@ -94,7 +94,7 @@ let ident env id = try IdentMap.find id env.re_id with Not_found -> - Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" + Cerrors.fatal_error "Internal error: Rename: %s__%d unbound" id.name id.stamp let rec typ env = function @@ -111,7 +111,7 @@ let rec typ env = function | ty -> ty and param env (id, ty) = - if id.name = "" then + if id.name = "" then ((id, typ env ty), env) else let (id', env') = rename env id in ((id', typ env' ty), env') @@ -216,7 +216,7 @@ let fundef env f = fd_body = stmt env2 f.fd_body }, env0 ) -let enum env (id, v, opte) = +let enum env (id, v, opte) = let (id', env') = rename env id in ((id', v, optexp env' opte), env') @@ -269,7 +269,7 @@ let rec reserve_public env file = function begin match sto with | Storage_default | Storage_extern -> enter_public env id | Storage_static -> if !Clflags.option_rename_static then - enter_static env id file + enter_static env id file else env | _ -> assert false @@ -292,4 +292,4 @@ let program p file = globdecls (reserve_public (reserve_builtins()) file p) [] p - + diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 5e5602f3..2c6fd1d2 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -71,7 +71,7 @@ let classify_param env ty = | SP_ref_caller -> Param_ref_caller | _ -> match sizeof env ty, alignof env ty with - | Some sz, Some al -> + | Some sz, Some al -> Param_flattened ((sz + 3) / 4, sz, al) | _, _ -> Param_unchanged (* should not happen *) @@ -306,7 +306,7 @@ let rec transf_expr env ctx e = We used to do a copy optimization: ctx = Effects: lv = f(...) -> f(&lv, ...) - but it is not correct in case of overlap (see test/regression/struct12.c) + but it is not correct in case of overlap (see test/regression/struct12.c) Function calls returning a composite by value: ctx = Effects: lv = f(...) -> newtemp = f(...), lv = newtemp @@ -521,8 +521,8 @@ let rec transf_funparams loc env params = let tpx = TPtr(tx', []) in let ex = { edesc = EVar x; etyp = tpx } in let estarx = { edesc = EUnop(Oderef, ex); etyp = tx' } in - ((x, tpx) :: params', - actions, + ((x, tpx) :: params', + actions, IdentMap.add x estarx subst) | Param_flattened(n, sz, al) -> let y = new_temp ~name:x.name (ty_buffer n) in @@ -562,7 +562,7 @@ let transf_fundef env f = | Ret_value(ty, sz, al) -> (f.fd_attrib, ty, - params, + params, transf_funbody env (subst_stmt subst f.fd_body) None) in let temps = get_temps() in {f with fd_attrib = attr1; diff --git a/cparser/Transform.ml b/cparser/Transform.ml index 6cdd8a6b..840234b8 100644 --- a/cparser/Transform.ml +++ b/cparser/Transform.ml @@ -81,7 +81,7 @@ let op_for_assignop = function | Odiv_assign -> Odiv | Omod_assign -> Omod | Oand_assign -> Oand - | Oor_assign -> Oor + | Oor_assign -> Oor | Oxor_assign -> Oxor | Oshl_assign -> Oshl | Oshr_assign -> Oshr @@ -118,7 +118,7 @@ let expand_assignop ~read ~write env ctx op l r ty = ecomma (eassign tmp res) (ecomma (write l tmp) tmp)) let expand_preincrdecr ~read ~write env ctx op l = - expand_assignop ~read ~write env ctx (assignop_for_incr_decr op) + expand_assignop ~read ~write env ctx (assignop_for_incr_decr op) l (intconst 1L IInt) (unary_conversion env l.etyp) let expand_postincrdecr ~read ~write env ctx op l = @@ -147,7 +147,7 @@ let stmt ~expr ?(decl = fun env decl -> assert false) env s = | Sskip -> s | Sdo e -> {s with sdesc = Sdo(expr s.sloc env Effects e)} - | Sseq(s1, s2) -> + | Sseq(s1, s2) -> {s with sdesc = Sseq(stm s1, stm s2)} | Sif(e, s1, s2) -> {s with sdesc = Sif(expr s.sloc env Val e, stm s1, stm s2)} diff --git a/cparser/Transform.mli b/cparser/Transform.mli index 57a4737b..a04896a9 100644 --- a/cparser/Transform.mli +++ b/cparser/Transform.mli @@ -64,11 +64,11 @@ val fundef : (Env.t -> C.stmt -> C.stmt) -> Env.t -> C.fundef -> C.fundef val program : ?decl:(Env.t -> C.decl -> C.decl) -> ?fundef:(Env.t -> C.fundef -> C.fundef) -> - ?composite:(Env.t -> C.struct_or_union -> - C.ident -> C.attributes -> C.field list -> + ?composite:(Env.t -> C.struct_or_union -> + C.ident -> C.attributes -> C.field list -> C.attributes * C.field list) -> ?typedef:(Env.t -> C.ident -> C.typ -> C.typ) -> - ?enum:(Env.t -> C.ident -> C.attributes -> C.enumerator list -> + ?enum:(Env.t -> C.ident -> C.attributes -> C.enumerator list -> C.attributes * C.enumerator list) -> ?pragma:(Env.t -> string -> string) -> C.program -> diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index c6646b5c..405cf755 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -49,7 +49,7 @@ let rec local_initializer env path init k = | Init_struct(id, fil) -> let field_init (fld, i) k = local_initializer env - { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } + { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } i k in List.fold_right field_init fil k | Init_union(id, fld, i) -> @@ -80,7 +80,7 @@ let add_inits_expr inits e = let local_variables = ref ([]: decl list) let global_variables = ref ([]: decl list) -(* Note: "const int x = y - 1;" is legal, but we turn it into +(* Note: "const int x = y - 1;" is legal, but we turn it into "const int x; x = y - 1;", which is not. Therefore, remove top-level 'const' attribute. Also remove it on element type of array type. *) @@ -128,7 +128,7 @@ let rec expand_expr islocal env e = let e2' = match op with | Ocomma | Ologand | Ologor -> expand_expr islocal env e2 - (* Make sure the initializers of [e2] are performed in + (* Make sure the initializers of [e2] are performed in sequential order, i.e. just before [e2] but after [e1]. *) | _ -> expand e2 in {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp} @@ -148,7 +148,7 @@ let rec expand_expr islocal env e = e' | ECall(e1, el) -> {edesc = ECall(expand e1, List.map expand el); etyp = e.etyp} - in + in let e' = expand e in ecommalist !inits e' (* Elimination of compound literals within an initializer. *) @@ -185,7 +185,7 @@ let debug_ty = let debug_annot kind args = { sloc = no_loc; - sdesc = Sdo { + sdesc = Sdo { etyp = TVoid []; edesc = ECall({edesc = EVar debug_id; etyp = debug_ty}, intconst kind IInt :: args) @@ -276,12 +276,12 @@ let rec unblock_stmt env ctx ploc s = | Sseq(s1, s2) -> {s with sdesc = Sseq(unblock_stmt env ctx ploc s1, unblock_stmt env ctx s1.sloc s2)} - | Sif(e, s1, s2) -> + | Sif(e, s1, s2) -> add_lineno ctx ploc s.sloc {s with sdesc = Sif(expand_expr true env e, unblock_stmt env ctx s.sloc s1, unblock_stmt env ctx s.sloc s2)} - | Swhile(e, s1) -> + | Swhile(e, s1) -> add_lineno ctx ploc s.sloc {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env ctx s.sloc s1)} @@ -301,7 +301,7 @@ let rec unblock_stmt env ctx ploc s = add_lineno ctx ploc s.sloc {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env ctx s.sloc s1)} - | Slabeled(lbl, s1) -> + | Slabeled(lbl, s1) -> add_lineno ctx ploc s.sloc {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)} | Sgoto lbl -> @@ -309,7 +309,7 @@ let rec unblock_stmt env ctx ploc s = | Sreturn None -> add_lineno ctx ploc s.sloc s | Sreturn (Some e) -> - add_lineno ctx ploc s.sloc + add_lineno ctx ploc s.sloc {s with sdesc = Sreturn(Some (expand_expr true env e))} | Sblock sl -> let ctx' = @@ -327,7 +327,7 @@ let rec unblock_stmt env ctx ploc s = | Sasm(attr, template, outputs, inputs, clob) -> let expand_asm_operand (lbl, cstr, e) = (lbl, cstr, expand_expr true env e) in - add_lineno ctx ploc s.sloc + add_lineno ctx ploc s.sloc {s with sdesc = Sasm(attr, template, List.map expand_asm_operand outputs, List.map expand_asm_operand inputs, clob)} -- cgit From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- cparser/Cabs.v | 6 ++--- cparser/validator/Alphabet.v | 4 +-- cparser/validator/Automaton.v | 4 +-- cparser/validator/Grammar.v | 12 ++++----- cparser/validator/Interpreter.v | 2 +- cparser/validator/Interpreter_complete.v | 42 ++++++++++++++++---------------- cparser/validator/Interpreter_correct.v | 6 ++--- cparser/validator/Validator_complete.v | 2 +- cparser/validator/Validator_safe.v | 2 +- 9 files changed, 40 insertions(+), 40 deletions(-) (limited to 'cparser') diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 6d9e95d5..e15f8694 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -86,18 +86,18 @@ with parameter := | PARAM : list spec_elem -> option string -> decl_type -> list attribute -> cabsloc -> parameter (* The optional expression is the bitfield *) -with field_group := +with field_group := | Field_group : list spec_elem -> list (option name * option expression) -> cabsloc -> field_group (* The decl_type is in the order in which they are printed. Only the name of * the declared identifier is pulled out. *) (* e.g: in "int *x", "*x" is the declarator; "x" will be pulled out as *) (* the string, and decl_type will be PTR([], JUSTBASE) *) -with name := +with name := | Name : string -> decl_type -> list attribute -> cabsloc -> name (* A variable declarator ("name") with an initializer *) -with init_name := +with init_name := | Init_name : name -> init_expression -> init_name (* diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v index 85a1689d..13718cd5 100644 --- a/cparser/validator/Alphabet.v +++ b/cparser/validator/Alphabet.v @@ -193,7 +193,7 @@ Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A := { AlphabetComparable := {| compare := fun x y => compare31 (inj x) (inj y) |}; AlphabetFinite := - {| all_list := fst (iter_int31 inj_bound _ + {| all_list := fst (iter_int31 inj_bound _ (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }. Next Obligation. apply Zcompare_antisym. Qed. Next Obligation. @@ -229,7 +229,7 @@ rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; refle replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega. rewrite Z_mod_same_full in H0. exfalso; omega. -exfalso; inversion Heqp; subst; +exfalso; inversion Heqp; subst; pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega. clear H. rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v index b15f87d2..98ab1246 100644 --- a/cparser/validator/Automaton.v +++ b/cparser/validator/Automaton.v @@ -113,7 +113,7 @@ Module Types(Import Init:AutInit). (** Types used for the annotations of the automaton. **) (** An item is a part of the annotations given to the validator. - It is acually a set of LR(1) items sharing the same core. It is needed + It is acually a set of LR(1) items sharing the same core. It is needed to validate completeness. **) Record item := { (** The pseudo-production of the item. **) @@ -136,7 +136,7 @@ Module Type T. Parameter start_nt: initstate -> nonterminal. (** The action table maps a state to either a map terminal -> action. **) - Parameter action_table: + Parameter action_table: state -> action. (** The goto table of an LR(1) automaton. **) Parameter goto_table: state -> forall nt:nonterminal, diff --git a/cparser/validator/Grammar.v b/cparser/validator/Grammar.v index d162892d..0768d647 100644 --- a/cparser/validator/Grammar.v +++ b/cparser/validator/Grammar.v @@ -96,8 +96,8 @@ Module Defs(Import G:T). Definition token := {t:terminal & symbol_semantic_type (T t)}. (** A grammar creates a relation between word of tokens and semantic values. - This relation is parametrized by the head symbol. It defines the - "semantics" of the grammar. This relation is defined by a notion of + This relation is parametrized by the head symbol. It defines the + "semantics" of the grammar. This relation is defined by a notion of parse tree. **) Inductive parse_tree: forall (head_symbol:symbol) (word:list token) @@ -110,9 +110,9 @@ Module Defs(Import G:T). parse_tree (T t) [existT (fun t => symbol_semantic_type (T t)) t sem] sem - (** Given a production, if a word has a list of semantic values for the - right hand side as head symbols, then this word has the semantic value - given by the semantic action of the production for the left hand side + (** Given a production, if a word has a list of semantic values for the + right hand side as head symbols, then this word has the semantic value + given by the semantic action of the production for the left hand side as head symbol.**) | Non_terminal_pt: forall {p:production} {word:list token} @@ -152,7 +152,7 @@ Module Defs(Import G:T). Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) := - match tree with + match tree with | Terminal_pt _ _ => 1 | Non_terminal_pt _ _ _ l => S (ptl_size l) end diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v index 16be3859..2242065c 100644 --- a/cparser/validator/Interpreter.v +++ b/cparser/validator/Interpreter.v @@ -98,7 +98,7 @@ Fixpoint pop (symbols_to_pop:list symbol) (stack_cur:stack): result (stack * A) := match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), _ with | [] => fun A action => OK (stack_cur, action) - | t::q => fun A action => + | t::q => fun A action => match stack_cur with | existT state_cur sem::stack_rec => match compare_eqdec (last_symb_of_non_init_state state_cur) t with diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index 3b922f7d..3d564c11 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -102,7 +102,7 @@ Variable buffer_end: Stream token. Variable full_sem: symbol_semantic_type (NT (start_nt init)). Inductive pt_zipper: - forall (hole_symb:symbol) (hole_word:list token) + forall (hole_symb:symbol) (hole_word:list token) (hole_sem:symbol_semantic_type hole_symb), Type := | Top_ptz: pt_zipper (NT (start_nt init)) (full_word) (full_sem) @@ -115,7 +115,7 @@ Inductive pt_zipper: {wordq:list token} {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, parse_tree_list head_symbolsq wordq semantic_valuesq -> - + ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq) (semantic_valuet,semantic_valuesq) -> @@ -134,11 +134,11 @@ with ptl_zipper: {wordt:list token} {semantic_valuet:symbol_semantic_type head_symbolt}, parse_tree head_symbolt wordt semantic_valuet -> - + forall {head_symbolsq:list symbol} {wordq:list token} {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, - + ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq) (semantic_valuet,semantic_valuesq) -> @@ -275,7 +275,7 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} (ptlz:ptl_zipper hole_symbs hole_word hole_sems) :pt_dot := match ptl in parse_tree_list hole_symbs hole_word hole_sems - return ptl_zipper hole_symbs hole_word hole_sems -> _ + return ptl_zipper hole_symbs hole_word hole_sems -> _ with | Nil_ptl => fun ptlz => Reduce_ptd ptlz @@ -292,7 +292,7 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} end ptlz. Lemma build_pt_dot_cost: - forall hole_symbs hole_word hole_sems + forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), ptd_cost (build_pt_dot ptl ptlz) = ptl_size ptl + ptlz_cost ptlz. @@ -307,7 +307,7 @@ simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity. Qed. Lemma build_pt_dot_buffer: - forall hole_symbs hole_word hole_sems + forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), ptd_buffer (build_pt_dot ptl ptlz) = hole_word ++ ptlz_buffer ptlz. @@ -321,7 +321,7 @@ simpl; rewrite build_pt_dot_buffer. apply app_str_app_assoc. Qed. -Lemma ptd_stack_compat_build_pt_dot: +Lemma ptd_stack_compat_build_pt_dot: forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems) @@ -354,8 +354,8 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems} { word:_ & { sem:_ & (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } := - match ptlz in ptl_zipper hole_symbs hole_word hole_sems - return parse_tree_list hole_symbs hole_word hole_sems -> + match ptlz in ptl_zipper hole_symbs hole_word hole_sems + return parse_tree_list hole_symbs hole_word hole_sems -> { word:_ & { sem:_ & (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } @@ -368,7 +368,7 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems} end ptl. Lemma pop_ptlz_cost: - forall hole_symbs hole_word hole_sems + forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in @@ -381,7 +381,7 @@ simpl; apply pop_ptlz_cost. Qed. Lemma pop_ptlz_buffer: - forall hole_symbs hole_word hole_sems + forall hole_symbs hole_word hole_sems (ptl:parse_tree_list hole_symbs hole_word hole_sems) (ptlz:ptl_zipper hole_symbs hole_word hole_sems), let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in @@ -414,14 +414,14 @@ Lemma pop_ptlz_pop_stack_compat: (stack:stack), ptlz_stack_compat ptlz stack -> - - let action' := - eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ + + let action' := + eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ (pop_ptlz_pop_stack_compat_converter _ _ _ _ _) in let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with - | OK (stack', sem') => + | OK (stack', sem') => ptz_stack_compat ptz stack' /\ sem = sem' | Err => True end. @@ -503,8 +503,8 @@ pose proof (pop_ptlz_buffer _ _ _ Nil_ptl ptlz). destruct (pop_ptlz Nil_ptl ptlz) as [word [sem [ptz pt]]]. rewrite H0; clear H0. revert H. -match goal with - |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end => +match goal with + |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end => replace p1 with p2; [destruct p2 as [|[]]; intros|] end. assumption. @@ -610,8 +610,8 @@ Qed. Variable full_pt: parse_tree (NT (start_nt init)) full_word full_sem. Definition init_ptd := - match full_pt in parse_tree head full_word full_sem return - pt_zipper head full_word full_sem -> + match full_pt in parse_tree head full_word full_sem return + pt_zipper head full_word full_sem -> match head return Type with | T _ => unit | NT _ => pt_dot end with | Terminal_pt _ _ => fun _ => () @@ -668,7 +668,7 @@ Qed. Theorem parse_complete n_steps: match parse init (full_word ++ buffer_end) n_steps with | OK (Parsed_pr sem_res buffer_end_res) => - sem_res = full_sem /\ buffer_end_res = buffer_end /\ + sem_res = full_sem /\ buffer_end_res = buffer_end /\ pt_size full_pt <= n_steps | OK Fail_pr => False | OK Timeout_pr => n_steps < pt_size full_pt diff --git a/cparser/validator/Interpreter_correct.v b/cparser/validator/Interpreter_correct.v index 095b26ca..3a285158 100644 --- a/cparser/validator/Interpreter_correct.v +++ b/cparser/validator/Interpreter_correct.v @@ -68,7 +68,7 @@ Qed. Lemma pop_invariant: forall (symbols_to_pop symbols_popped:list symbol) (stack_cur:stack) - (A:Type) + (A:Type) (action:arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A), forall word_stack word_popped, forall sem_popped, @@ -96,12 +96,12 @@ destruct e; simpl. dependent destruction H. destruct H0, H1. apply (Cons_ptl X), inhabits in X0. specialize (IHsymbols_to_pop _ _ _ action0 _ _ _ H X0). -match goal with +match goal with IHsymbols_to_pop:match ?p1 with Err => _ | OK _ => _ end |- match ?p2 with Err => _ | OK _ => _ end => replace p2 with p1; [destruct p1 as [|[]]|]; intuition end. destruct IHsymbols_to_pop as [word1res [word2res [sem_full []]]]; intuition; subst. -exists word1res. +exists word1res. eexists. exists sem_full. intuition. diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v index 98559305..90ab1b0c 100644 --- a/cparser/validator/Validator_complete.v +++ b/cparser/validator/Validator_complete.v @@ -497,7 +497,7 @@ Qed. (** The automaton is complete **) Definition complete := - nullable_stable /\ first_stable /\ start_future /\ terminal_shift + nullable_stable /\ first_stable /\ start_future /\ terminal_shift /\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed. Definition is_complete (_:unit) := diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v index 119f7337..c5229ac9 100644 --- a/cparser/validator/Validator_safe.v +++ b/cparser/validator/Validator_safe.v @@ -121,7 +121,7 @@ Qed. Definition goto_head_symbs := forall s nt, match goto_table s nt with - | Some (exist s2 _) => + | Some (exist s2 _) => prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) | None => True end. -- cgit