diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 42 |
1 files changed, 24 insertions, 18 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c4772688..d6bf76f3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -16,7 +16,7 @@ open C open Camlcoq -open Floats +open! Floats open Values open Ctypes open Csyntax @@ -307,18 +307,18 @@ let builtins = (** ** The known attributes *) let attributes = [ - (* type-related *) - ("aligned", Cutil.Attr_type); + (* type-related -- currently none *) (* struct-related *) ("packed", Cutil.Attr_struct); (* function-related *) ("noreturn", Cutil.Attr_function); ("noinline",Cutil.Attr_function); (* name-related *) + ("aligned", Cutil.Attr_name); ("section", Cutil.Attr_name); ("unused", Cutil.Attr_name) ] - + (** ** Functions used to handle string literals *) @@ -546,14 +546,14 @@ let convertFkind k a : coq_type = let checkFunctionType env tres targs = if not !Clflags.option_fstruct_passing then begin if Cutil.is_composite_type env tres then - unsupported "function returning a struct or union (consider adding option -fstruct-passing)"; + unsupported "function returning a struct or union (consider adding option [-fstruct-passing])"; begin match targs with | None -> () | Some l -> List.iter (fun (id, ty) -> if Cutil.is_composite_type env ty then - unsupported "function parameter of struct or union type (consider adding option -fstruct-passing)") + unsupported "function parameter of struct or union type (consider adding option [-fstruct-passing])") l end end @@ -606,13 +606,15 @@ let rec convertTypArgs env tl el = let convertField env f = if f.fld_bitfield <> None then - unsupported "bit field in struct or union (consider adding option -fbitfields)"; + unsupported "bit field in struct or union (consider adding option [-fbitfields])"; (intern_string f.fld_name, convertTyp env f.fld_typ) let convertCompositedef env su id attr members = + if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then + unsupported "packed struct (consider adding option [-fpacked-structs])"; let t = match su with | C.Struct -> - let layout = Cutil.struct_layout env members in + let layout = Cutil.struct_layout env attr members in List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; TStruct (id,attr) | C.Union -> TUnion (id,attr) in @@ -717,6 +719,7 @@ let ewrap = function let rec convertExpr env e = match e.edesc with + | C.EConst (C.CStr _ | C.CWStr _) | C.EVar _ | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> @@ -732,12 +735,6 @@ let rec convertExpr env e = if k = C.FLongDouble && not !Clflags.option_flongdouble then unsupported "'long double' floating-point constant"; convertFloat f k - | C.EConst(C.CStr s) -> - let ty = typeStringLiteral s in - Evalof(Evar(name_for_string_literal s, ty), ty) - | C.EConst(C.CWStr s) -> - let ty = typeWideStringLiteral s in - Evalof(Evar(name_for_wide_string_literal s, ty), ty) | C.EConst(C.CEnum(id, i)) -> Ctyping.econst_int (convertInt32 i) Signed | C.ESizeof ty1 -> @@ -793,6 +790,9 @@ let rec convertExpr env e = if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then warning Diagnostics.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored"; + 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"; 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| @@ -829,10 +829,10 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 -> + error "too few arguments to function call, expected at least 2, have 0"; + ezero | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> - let len = List.length args in - if len < 2 then - error "too few arguments to function call, expected at least 2, have 0"; let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 when n <> 0L-> (n, args1) @@ -957,6 +957,12 @@ and convertLvalue env e = let e1' = convertExpr env e1 and e2' = convertExpr env e2 in let e3' = ewrap (Ctyping.ebinop Cop.Oadd e1' e2') in ewrap (Ctyping.ederef e3') + | C.EConst(C.CStr s) -> + let ty = typeStringLiteral s in + Evar(name_for_string_literal s, ty) + | C.EConst(C.CWStr s) -> + let ty = typeWideStringLiteral s in + Evar(name_for_wide_string_literal s, ty) | _ -> error "illegal lvalue"; ezero @@ -1002,7 +1008,7 @@ type switchbody = let rec flattenSwitch = function | {sdesc = C.Sseq(s1, s2)} -> flattenSwitch s1 @ flattenSwitch s2 - | {sdesc = C.Slabeled(C.Scase e, s1)} -> + | {sdesc = C.Slabeled(C.Scase(e, _), s1)} -> Label(Case e) :: flattenSwitch s1 | {sdesc = C.Slabeled(C.Sdefault, s1)} -> Label Default :: flattenSwitch s1 |