diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 14:24:03 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-03-27 14:24:03 +0100 |
commit | 33b742bb41725e47bd88dc12f2a4f40173023f83 (patch) | |
tree | 07f8c559aa58c9e4fcfb417a71e713665520e1c9 /backend/Selection.v | |
parent | ecbecdd399d0d685ffed2024e864dc4aaccdfbf6 (diff) | |
download | compcert-33b742bb41725e47bd88dc12f2a4f40173023f83.tar.gz compcert-33b742bb41725e47bd88dc12f2a4f40173023f83.zip |
Updated the Caml part. Added some more tests in annot1.c.
Diffstat (limited to 'backend/Selection.v')
-rw-r--r-- | backend/Selection.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 5cec6e00..ae9da0a7 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -203,12 +203,23 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +(** Annotations *) + Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool := match ef, optid with | EF_annot _ _, None => true | _, _ => false end. +Function sel_annot_arg (e: Cminor.expr) : AST.annot_arg expr := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => AA_addrglobal id ofs + | Cminor.Econst (Cminor.Oaddrstack ofs) => AA_addrstack ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrsymbol id ofs)) => AA_loadglobal chunk id ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrstack ofs)) => AA_loadstack chunk ofs + | _ => annot_arg (sel_expr e) + end. + (** Conversion of Cminor [switch] statements to decision trees. *) Parameter compile_switch: Z -> nat -> table -> comptree. @@ -270,7 +281,7 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := end) | Cminor.Sbuiltin optid ef args => OK (if builtin_is_annot ef optid - then Sannot ef (List.map (fun e => annot_arg (sel_expr e)) args) + then Sannot ef (List.map sel_annot_arg args) else Sbuiltin optid ef (sel_exprlist args)) | Cminor.Stailcall sg fn args => OK (match classify_call ge fn with |