diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-11 12:05:31 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-11 12:05:31 +0200 |
| commit | 0de3d126e70dfedfd6f74710da31c4b9636f900a (patch) | |
| tree | 43b19f66ef97def541881bceebcbdac4cfca8fb2 /powerpc/Asm.v | |
| parent | 2809e264a4c146b31b5009fba08f74d12126a1b3 (diff) | |
| download | compcert-0de3d126e70dfedfd6f74710da31c4b9636f900a.tar.gz compcert-0de3d126e70dfedfd6f74710da31c4b9636f900a.zip | |
Use the gcc version of atomic load.
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 66bb4607..5fd40a27 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -154,6 +154,7 @@ Inductive instruction : Type := | Pbf: crbit -> label -> instruction (**r branch if false *) | Pbl: ident -> signature -> instruction (**r branch and link *) | Pbne: label -> instruction (**r branch not equal *) + | Pbne_rel: int -> instruction (**r branch not equal with relative offset *) | Pbs: ident -> signature -> instruction (**r branch to symbol *) | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) @@ -875,6 +876,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out directly by [Asmgen], so we do not model them. *) | Pbdnz _ | Pbne _ + | Pbne_rel _ | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ |