Add builtins for load with reservation and conditional store.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 20 insertions, 0 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index a9a5f02..f175f16 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -1664,6 +1664,16 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Plwarx(rd, r1, r2) ->
+          begin match ecode with
+          | LWARX(rD, rA, rB):: es ->
+              OK(fw)
+              >>= match_iregs rd rD
+              >>= match_iregs r1 rA
+              >>= match_iregs r2 rB
+              >>= recur_simpl
+          | _ -> error
+          end
       | Plwbrx(rd, r1, r2) ->
           begin match ecode with
           | LWBRX(rD, rA, rB):: es ->
@@ -2121,6 +2131,16 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pstwcx_(rd, r1, r2) ->
+          begin match ecode with
+          | STWCX_(rS, rA, rB) :: es ->
+              OK(fw)
+              >>= match_iregs rd rS
+              >>= match_iregs r1 rA
+              >>= match_iregs r2 rB
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pstwxu(rd, r1, r2) ->
           begin match ecode with
           | STWUX(rS, rA, rB) :: es ->