From 0d783f1aa5e4f94b713588fb272ecca6a1bc23ca Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 9 Jul 2017 11:15:06 +0200
Subject: SimlLocals.Sdebug_var: wrong type for 64-bit platforms

Fixes: Github issue #190.

Tint was used instead of the correct Tptr.
---
 cfrontend/SimplLocals.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cfrontend/SimplLocals.v')

diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index c0086a38..b142d3cc 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -59,7 +59,7 @@ Definition Sdebug_temp (id: ident) (ty: type) :=
                 (Etempvar id ty :: nil).
 
 Definition Sdebug_var (id: ident) (ty: type) :=
-  Sbuiltin None (EF_debug 5%positive id (AST.Tint :: nil))
+  Sbuiltin None (EF_debug 5%positive id (AST.Tptr :: nil))
                 (Tcons (Tpointer ty noattr) Tnil)
                 (Eaddrof (Evar id ty) (Tpointer ty noattr) :: nil).
 
-- 
cgit