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/AsmToJSON.ml | |
| parent | 2809e264a4c146b31b5009fba08f74d12126a1b3 (diff) | |
| download | compcert-0de3d126e70dfedfd6f74710da31c4b9636f900a.tar.gz compcert-0de3d126e70dfedfd6f74710da31c4b9636f900a.zip | |
Use the gcc version of atomic load.
Diffstat (limited to 'powerpc/AsmToJSON.ml')
| -rw-r--r-- | powerpc/AsmToJSON.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 7064ebdd..d23beaad 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -163,7 +163,8 @@ let p_instruction oc ic = | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}" p_atom_constant i - | Pbne (lbl) -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl + | Pbne lbl -> fprintf oc "{\"Instruction Name\":\"Pbne\",\"Args\":[%a]}" p_label lbl + | Pbne_rel ofs -> fprintf oc"{\"Instruction Name\":\"Pbne_rel\",\"Args\":[%a]}" p_int_constant ofs | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}" p_atom_constant i | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l |