diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-07-09 11:15:06 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-07-09 11:15:06 +0200 |
| commit | 0d783f1aa5e4f94b713588fb272ecca6a1bc23ca (patch) | |
| tree | 4567faa2a5c71e906db559ba57d1e811daf9cc65 /cfrontend/SimplLocals.v | |
| parent | a8a59e25447e61f4250d54187854cc3a36038c37 (diff) | |
| download | compcert-kvx-0d783f1aa5e4f94b713588fb272ecca6a1bc23ca.tar.gz compcert-kvx-0d783f1aa5e4f94b713588fb272ecca6a1bc23ca.zip | |
SimlLocals.Sdebug_var: wrong type for 64-bit platforms
Fixes: Github issue #190.
Tint was used instead of the correct Tptr.
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). |