aboutsummaryrefslogtreecommitdiffstats
path: root/backend/XTL.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-03-27 14:24:03 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-03-27 14:24:03 +0100
commit33b742bb41725e47bd88dc12f2a4f40173023f83 (patch)
tree07f8c559aa58c9e4fcfb417a71e713665520e1c9 /backend/XTL.ml
parentecbecdd399d0d685ffed2024e864dc4aaccdfbf6 (diff)
downloadcompcert-kvx-33b742bb41725e47bd88dc12f2a4f40173023f83.tar.gz
compcert-kvx-33b742bb41725e47bd88dc12f2a4f40173023f83.zip
Updated the Caml part. Added some more tests in annot1.c.
Diffstat (limited to 'backend/XTL.ml')
-rw-r--r--backend/XTL.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/XTL.ml b/backend/XTL.ml
index 30c09fdf..0e5ce0c4 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -125,10 +125,10 @@ let rec set_vars_type vl tyl =
let unify_var_type v1 v2 =
if typeof v1 <> typeof v2 then raise Type_error
-let type_annot_arg a ty =
+let rec type_annot_arg a ty =
match a with
| AA_base v -> set_var_type v ty
- | AA_longofwords(v1, v2) -> set_var_type v1 Tint; set_var_type v2 Tint
+ | AA_longofwords(a1, a2) -> type_annot_arg a1 Tint; type_annot_arg a2 Tint
| _ -> ()
let type_instr = function