aboutsummaryrefslogtreecommitdiffstats
path: root/backend/XTL.mli
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2016-05-27 09:03:30 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2016-05-27 09:03:30 +0200
commit5087ec788016b719b4038be08cd55bccc22b3619 (patch)
tree58f0a26f4b02364c0823ba64a2de2df1a073e0a4 /backend/XTL.mli
parentb45cdb9dce7df376fd3cb27a32863af90b847b78 (diff)
parent8d3dbd3636fbb6a056f5506be8ee2d8839c1aea2 (diff)
downloadcompcert-5087ec788016b719b4038be08cd55bccc22b3619.tar.gz
compcert-5087ec788016b719b4038be08cd55bccc22b3619.zip
Merge pull request #99 from AbsInt/register-pairs
Introduce register pairs to describe calling conventions more precisely
Diffstat (limited to 'backend/XTL.mli')
-rw-r--r--backend/XTL.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/XTL.mli b/backend/XTL.mli
index 6bdcc8c6..54988d4b 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -64,6 +64,7 @@ val vloc: loc -> var
val vlocs: loc list -> var list
val vmreg: mreg -> var
val vmregs: mreg list -> var list
+val vlocpairs: loc rpair list -> var list
(* Tests over variables *)