diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/Bitfields.ml | 8 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 8 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 4 | ||||
| -rw-r--r-- | cparser/Elab.ml | 8 | ||||
| -rw-r--r-- | cparser/validator/Automaton.v | 6 | ||||
| -rw-r--r-- | cparser/validator/Interpreter.v | 4 |
6 files changed, 19 insertions, 19 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 2431a0bd..35da5d4e 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -195,13 +195,17 @@ let right_shift_count bf = (Int64.of_int (8 * !config.sizeof_int - bf.bf_size)) IInt +let uintconst_hex v = + { edesc = EConst(CInt(v, IUInt, Printf.sprintf "0x%LXU" v)); + etyp = TInt(IUInt, []) } + let insertion_mask bf = let m = Int64.shift_left (Int64.pred (Int64.shift_left 1L bf.bf_size)) bf.bf_pos in (* Give the mask an hexadecimal string representation, nicer to read *) - intconst ~hex:true m IUInt + uintconst_hex m let eshift env op a b = let ty = unary_conversion env a.etyp in @@ -283,7 +287,7 @@ let bitfield_initializer bf i = let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in let e_cast = if bf.bf_bool then ecast (TInt(IBool,[])) e else e in - let e_mask = intconst ~hex:true m IUInt in + let e_mask = uintconst_hex m in let e_and = {edesc = EBinop(Oand, e_cast, e_mask, TInt(IUInt,[])); etyp = TInt(IUInt,[])} in diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 735dd99b..18088be7 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -1007,12 +1007,8 @@ let int_pointer_conversion env tfrom tto = (* Construct an integer constant *) -let intconst ?hex v ik = - let ist = match hex with - | Some hex when hex -> - Printf.sprintf "0x%LXU" v - | _ -> "" in - { edesc = EConst(CInt(v, ik, ist)); etyp = TInt(ik, []) } +let intconst v ik = + { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) } (* Construct the 0 float constant of double type *) diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index bd5a2c3e..a1b9cd26 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -238,8 +238,8 @@ val field_of_arrow_access: Env.t -> typ -> string -> field (* Constructors *) -val intconst : ?hex:bool -> int64 -> ikind -> exp - (* Build expression for given integer constant with optional hex string. *) +val intconst : int64 -> ikind -> exp + (* Build expression for given integer constant. *) val floatconst0 : exp (* Build expression for (double)0. *) val nullconst : exp diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 76f0c998..eb9ff560 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -835,7 +835,7 @@ and elab_struct_or_union_info keep_ty kind loc env members attrs = let m = List.flatten m in let m,_ = mmap (fun c fld -> if fld.fld_anonymous then - let name = Format.sprintf "<anon>_%d" c in + let name = Printf.sprintf "<anon>_%d" c in {fld with fld_name = name},c+1 else fld,c) 0 m in @@ -1103,11 +1103,11 @@ module I = struct let rec zipname = function | Ztop(name, ty) -> name | Zarray(z, ty, sz, dfl, before, idx, after) -> - Format.sprintf "%s[%Ld]" (zipname z) idx + Printf.sprintf "%s[%Ld]" (zipname z) idx | Zstruct(z, id, before, fld, after) -> - Format.sprintf "%s.%s" (zipname z) fld.fld_name + Printf.sprintf "%s.%s" (zipname z) fld.fld_name | Zunion(z, id, fld) -> - Format.sprintf "%s.%s" (zipname z) fld.fld_name + Printf.sprintf "%s.%s" (zipname z) fld.fld_name let name (z, i) = zipname z diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v index 98ab1246..fc995298 100644 --- a/cparser/validator/Automaton.v +++ b/cparser/validator/Automaton.v @@ -102,9 +102,9 @@ Module Types(Import Init:AutInit). T term = last_symb_of_non_init_state s -> lookahead_action term | Reduce_act: production -> lookahead_action term | Fail_act: lookahead_action term. - Implicit Arguments Shift_act [term]. - Implicit Arguments Reduce_act [term]. - Implicit Arguments Fail_act [term]. + Arguments Shift_act [term]. + Arguments Reduce_act [term]. + Arguments Fail_act [term]. Inductive action := | Default_reduce_act: production -> action diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v index a24362f8..4ac02693 100644 --- a/cparser/validator/Interpreter.v +++ b/cparser/validator/Interpreter.v @@ -26,8 +26,8 @@ Inductive result (A:Type) := | Err: result A | OK: A -> result A. -Implicit Arguments Err [A]. -Implicit Arguments OK [A]. +Arguments Err [A]. +Arguments OK [A]. Definition bind {A B: Type} (f: result A) (g: A -> result B): result B := match f with |