Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate type

for Epostincr operations.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 9 insertions, 0 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 7bda1b13..f2550ef3 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -902,6 +902,15 @@ Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) :=
   | Decr => sem_sub v ty (Vint Int.one) type_int32s
   end.
 
+Definition incrdecr_type (ty: type) :=
+  match typeconv ty with
+  | Tpointer ty a => Tpointer ty a
+  | Tint sz sg a => Tint sz sg noattr
+  | Tlong sg a => Tlong sg noattr
+  | Tfloat sz a => Tfloat sz noattr
+  | _ => Tvoid
+  end.
+
 (** * Compatibility with extensions and injections *)
 
 Section GENERIC_INJECTION.