diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-02 13:50:24 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-02 13:50:24 +0200 |
| commit | db8e35c6abf58c82853b94f416aa76b33efc1f65 (patch) | |
| tree | dcd1a758de6234817c9947e9898c1bc87937e597 /powerpc/TargetPrinter.ml | |
| parent | 75d50c12ee220fecf955b1626c78b78636cbca92 (diff) | |
| download | compcert-kvx-db8e35c6abf58c82853b94f416aa76b33efc1f65.tar.gz compcert-kvx-db8e35c6abf58c82853b94f416aa76b33efc1f65.zip | |
Added builtin for dcbtls
THis commit adds a builtin function for the dcbtls instruction.
Additionaly it changes the printing of the dcbt and dcbtst instruction to
embedded mode and adds support for different address variants.
Diffstat (limited to 'powerpc/TargetPrinter.ml')
| -rw-r--r-- | powerpc/TargetPrinter.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b0f296ef..b5fa50dc 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -463,9 +463,11 @@ module Target (System : SYSTEM):TARGET = | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdcbt (c,r1) -> - fprintf oc " dcbt %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbt %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbtst %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + | Pdcbtls (c,r1) -> + fprintf oc " dcbtls %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> |