diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-07 09:40:24 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-07 09:40:24 +0200 |
| commit | a168d6a141e77a5fa98017b23ab2aadc5748fe94 (patch) | |
| tree | 95dc6301836fbd445094f5070c35eb9f1e4ab62f /powerpc/Machregs.v | |
| parent | 47d0e5256ab79b402faae14260fa2fabc1d24dcb (diff) | |
| download | compcert-kvx-a168d6a141e77a5fa98017b23ab2aadc5748fe94.tar.gz compcert-kvx-a168d6a141e77a5fa98017b23ab2aadc5748fe94.zip | |
Simplified generation of builtins for cache instructions.
The cache instructions need no special constraint on the address
argument. Therefore also the generation of the address is no longer
needed.
Diffstat (limited to 'powerpc/Machregs.v')
| -rw-r--r-- | powerpc/Machregs.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 402f07d1..a2017dca 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -217,9 +217,9 @@ Definition builtin_constraints (ef: external_function) : | EF_builtin id sg => 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 if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil + else if ident_eq id builtin_prefetch then OK_default :: OK_const :: OK_const :: nil + else if ident_eq id builtin_dcbtls then OK_default::OK_const::nil + else if ident_eq id builtin_icbtls then OK_default::OK_const::nil else if ident_eq id builtin_mbar then OK_const::nil else nil | EF_vload _ => OK_addrany :: nil |