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/CBuiltins.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/CBuiltins.ml')
| -rw-r--r-- | powerpc/CBuiltins.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 701690b2..8dbf02e5 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -96,6 +96,8 @@ let builtins = { (TVoid [],[TPtr(TVoid [], [])],false); "__builtin_prefetch", (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false); + "__builtin_dcbtls", + (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false); (* Access to special registers *) "__builtin_get_spr", (TInt(IUInt, []), [TInt(IInt, [])], false); |