From ea23f1260ff7d587b0db05090580efd8f56d617a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 31 May 2008 08:50:20 +0000
Subject: Utilisation de intoffloatu.  Ajout du cas int + ptr.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@652 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Csyntax.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'cfrontend/Csyntax.v')

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 6680efe2..ee1b8617 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -396,6 +396,7 @@ Inductive classify_add_cases : Set :=
   | add_case_ii: classify_add_cases         (**r int , int *)
   | add_case_ff: classify_add_cases         (**r float , float *)
   | add_case_pi: type -> classify_add_cases (**r ptr or array, int *)
+  | add_case_ip: type -> classify_add_cases (**r int, ptr or array *)
   | add_default: classify_add_cases.        (**r other *)
 
 Definition classify_add (ty1: type) (ty2: type) :=
@@ -404,6 +405,8 @@ Definition classify_add (ty1: type) (ty2: type) :=
   | Tfloat _, Tfloat _ => add_case_ff
   | Tpointer ty, Tint _ _ => add_case_pi ty
   | Tarray ty _, Tint _ _ => add_case_pi ty 
+  | Tint _ _, Tpointer ty => add_case_ip ty
+  | Tint _ _, Tarray ty _ => add_case_ip ty 
   | _, _ => add_default
   end.
 
-- 
cgit