summaryrefslogtreecommitdiff
path: root/checklink/Asm_printers.ml
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-17 14:36:18 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-17 14:36:18 +0000
commitc29871c2d5c7860c6c6c53e8d5c8a9fe434742d2 (patch)
tree9e002b414d3fb3a899deb43f9f6e14d02507121a /checklink/Asm_printers.ml
parent26bb5772c75efe1e4617fb9c4f2b8522989fac6d (diff)
powerpc/: new unary operation "addsymbol"
Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Asm_printers.ml')
-rw-r--r--checklink/Asm_printers.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index 794d47a..5b3abe8 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -109,6 +109,8 @@ let string_of_constant = function
| Csymbol_low (i0, i1) -> "Csymbol_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
| Csymbol_high (i0, i1) -> "Csymbol_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
| Csymbol_sda (i0, i1) -> "Csymbol_sda(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
+| Csymbol_rel_low (i0, i1) -> "Csymbol_rel_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
+| Csymbol_rel_high (i0, i1) -> "Csymbol_rel_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")"
let string_of_crbit = function
| CRbit_0 -> "CRbit_0"