Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

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.