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/Machregs.v | |
| 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/Machregs.v')
| -rw-r--r-- | powerpc/Machregs.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 62a4a0a5..14edb89d 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -207,6 +207,7 @@ Definition two_address_op (op: operation) : bool := Definition builtin_get_spr := ident_of_string "__builtin_get_spr". Definition builtin_set_spr := ident_of_string "__builtin_set_spr". Definition builtin_prefetch := ident_of_string "__builtin_prefetch". +Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls". Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := @@ -215,6 +216,7 @@ Definition builtin_constraints (ef: external_function) : if ident_eq id builtin_get_spr then OK_const :: nil else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil + else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil |