diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-01 13:51:45 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-01 13:51:45 +0100 |
| commit | b0c6449c57a92fa0ba67dd7c9a98ffcc8e5d8bb6 (patch) | |
| tree | 76a9e7f0bbfd4b334c2ce22e389b965b84970f58 /cfrontend | |
| parent | 8675997219a5883ca639429639b2ab0edff16aa2 (diff) | |
| parent | 9d3521b4db46773239a2c5f9f6970de826075508 (diff) | |
| download | compcert-kvx-b0c6449c57a92fa0ba67dd7c9a98ffcc8e5d8bb6.tar.gz compcert-kvx-b0c6449c57a92fa0ba67dd7c9a98ffcc8e5d8bb6.zip | |
Merge remote-tracking branch 'absint/master' into merge_absint
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 502108f8..3dc40a1e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -619,19 +619,21 @@ let convertFkind k a : coq_type = if not !Clflags.option_flongdouble then unsupported "'long double' type"; Tfloat (F64, a) +let checkResultType env ty = + if (not !Clflags.option_fstruct_passing) && Cutil.is_composite_type env ty + then unsupported "function returning a struct or union \ + (consider adding option [-fstruct-passing])" + +let checkArgumentType env ty = + if (not !Clflags.option_fstruct_passing) && Cutil.is_composite_type env ty + then unsupported "function parameter of struct or union type \ + (consider adding option [-fstruct-passing])" + 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])"; - 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])") - l - end + checkResultType env tres; + begin match targs with + | None -> () + | Some l -> List.iter (fun (id, ty) -> checkArgumentType env ty) l end let rec convertTyp env ?bitwidth t = @@ -1072,12 +1074,13 @@ let rec convertExpr env e = | None -> error "wrong type for function part of a call" | Some(tres, targs, va) -> - checkFunctionType env tres targs; if targs = None && not !Clflags.option_funprototyped then unsupported "call to unprototyped function (consider adding option [-funprototyped])"; if va && not !Clflags.option_fvararg_calls then unsupported "call to variable-argument function (consider adding option [-fvararg-calls])" end; + checkResultType env e.etyp; + List.iter (fun arg -> checkArgumentType env arg.etyp) args; ewrap (Ctyping.ecall (convertExpr env fn) (convertExprList env args)) and convertLvalue env e = |