diff options
Diffstat (limited to 'cfrontend/SimplLocals.v')
| -rw-r--r-- | cfrontend/SimplLocals.v | 2 |
1 files changed, 1 insertions, 1 deletions
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). |