diff options
Diffstat (limited to 'cfrontend/SimplLocals.v')
| -rw-r--r-- | cfrontend/SimplLocals.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index f54aa60d..0a164e29 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -18,7 +18,7 @@ Require FSetAVL. Require Import Coqlib Ordered Errors. Require Import AST Linking. Require Import Ctypes Cop Clight. -Require Compopts. +Require Compopts Conventions1. Open Scope error_monad_scope. Open Scope string_scope. @@ -157,15 +157,20 @@ with simpl_lblstmt (cenv: compilenv) (ls: labeled_statements) : res labeled_stat end. (** Function parameters that are not lifted to temporaries must be - stored in the corresponding local variable at function entry. *) + stored in the corresponding local variable at function entry. + The other function parameters may need to be normalized to their types, + to support interoperability with code generated by other C compilers. *) Fixpoint store_params (cenv: compilenv) (params: list (ident * type)) (s: statement): statement := match params with | nil => s | (id, ty) :: params' => - if VSet.mem id cenv - then store_params cenv params' s + if VSet.mem id cenv then + if Conventions1.parameter_needs_normalization (rettype_of_type ty) + then Ssequence (Sset id (make_cast (Etempvar id ty) ty)) + (store_params cenv params' s) + else store_params cenv params' s else Ssequence (Sassign (Evar id ty) (Etempvar id ty)) (store_params cenv params' s) end. |