diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 39 |
1 files changed, 34 insertions, 5 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 25d3654f..3c71718c 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -535,7 +535,7 @@ let checkFunctionType env tres targs = end end -let rec convertTyp env t = +let rec convertTyp env ?bitwidth t = match t with | C.TVoid a -> Tvoid | C.TInt(ik, a) -> @@ -566,7 +566,21 @@ let rec convertTyp env t = | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) | C.TEnum(id, a) -> - convertIkind Cutil.enum_ikind (convertAttr a) + let ik = + match bitwidth with + | None -> Cutil.enum_ikind + | Some w -> + let info = Env.find_enum env id in + let representable sg = + List.for_all (fun (_, v, _) -> Cutil.int_representable v w sg) + info.Env.ei_members in + if representable false then + Cutil.unsigned_ikind_of Cutil.enum_ikind + else if representable true then + Cutil.signed_ikind_of Cutil.enum_ikind + else + Cutil.enum_ikind in + convertIkind ik (convertAttr a) and convertParams env = function | [] -> Tnil @@ -602,9 +616,16 @@ let rec convertTypAnnotArgs env = function convertTypAnnotArgs env el) let convertField env f = - if f.fld_bitfield <> None then - unsupported "bit field in struct or union (consider adding option [-fbitfields])"; - (intern_string f.fld_name, convertTyp env f.fld_typ) + let id = intern_string f.fld_name + and ty = convertTyp env ?bitwidth: f.fld_bitfield f.fld_typ in + match f.fld_bitfield with + | None -> Member_plain(id, ty) + | Some w -> + match ty with + | Tint(sz, sg, attr) -> + Member_bitfield(id, sz, sg, attr, Z.of_uint w, f.fld_name = "") + | _ -> + fatal_error "bitfield must have type int" let convertCompositedef env su id attr members = if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then @@ -707,6 +728,11 @@ let convertFloat f kind = (** Expressions *) +let check_volatile_bitfield env e = + if Cutil.is_bitfield env e + && List.mem AVolatile (Cutil.attributes_of_type env e.etyp) then + warning Diagnostics.Unnamed "access to a volatile bit field, the 'volatile' qualifier is ignored" + let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) let ewrap = function @@ -721,6 +747,7 @@ let rec convertExpr env e = | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> let l = convertLvalue env e in + check_volatile_bitfield env e; ewrap (Ctyping.evalof l) | C.EConst(C.CInt(i, k, _)) -> @@ -790,6 +817,7 @@ let rec convertExpr env e = if Cutil.is_composite_type env e2.etyp && List.mem AVolatile (Cutil.attributes_of_type env e2.etyp) then warning Diagnostics.Unnamed "assignment of a value of volatile composite type, the 'volatile' qualifier is ignored"; + check_volatile_bitfield env e1; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| @@ -810,6 +838,7 @@ let rec convertExpr env e = | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in + check_volatile_bitfield env e1; ewrap (Ctyping.eassignop op' e1' e2') | C.EBinop(C.Ocomma, e1, e2, _) -> ewrap (Ctyping.ecomma (convertExpr env e1) (convertExpr env e2)) |