From cfee340dc514e2cfbc5df910f7aa687e78a54d41 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 2 Sep 2015 17:17:00 +0200
Subject: Added builtin for the icbtls instruction.

This commit adds a builtin for the icbtls instruction.
---
 powerpc/TargetPrinter.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'powerpc/TargetPrinter.ml')

diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 764ad8a3..6a583cca 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -536,6 +536,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fsel	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
       | Picbi (r1,r2) ->
           fprintf oc "	icbi	%a,%a\n" ireg r1 ireg r2
+      | Picbtls (n,r1) ->
+          fprintf oc "	icbtls	%ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1
       | Pisync ->
           fprintf oc "	isync\n"
       | Plwsync ->
-- 
cgit