From 6f951e70d339cfa5d713cef5414541206ce4f434 Mon Sep 17 00:00:00 2001
From: Peter O'Hearn <peteroh@fb.com>
Date: Thu, 19 May 2016 05:38:35 -0700
Subject: [PATCH] Non-resource model for locks

Reviewed By: sblackshear

Differential Revision: D3317912

fbshipit-source-id: b2c7339
---
 infer/src/backend/modelBuiltins.ml | 34 ++++++++----------------------
 1 file changed, 9 insertions(+), 25 deletions(-)

diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index 81c7bff44..00e103a09 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -601,35 +601,19 @@ let execute___set_attr attr { Builtin.pdesc; prop_; path; args; }
   | [(lexp, _)] -> set_attr pdesc prop_ path lexp attr
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
-(** Set the attibute of the value as resource/locked*)
-let execute___set_locked_attribute
-    ({ Builtin.pdesc; loc; } as builtin_args)
-  : Builtin.ret_typ =
-  let pname = Cfg.Procdesc.get_proc_name pdesc in
-  (* ra_kind = Racquire in following indicates locked *)
-  let ra = {
-    Sil.ra_kind = Sil.Racquire;
-    ra_res = Sil.Rlock;
-    ra_pname = pname;
-    ra_loc = loc;
-    ra_vpath = None; } in
-  execute___set_attr (Sil.Aresource ra) builtin_args
-
-(** Delete the resource/locked attibute of the value, if it is locked*)
-let execute___delete_locked_attribute { Builtin.pdesc; loc; prop_; path; args; }
+(** Delete the locked attibute of the value*)
+let execute___delete_locked_attribute { Builtin.prop_; pdesc; path; args; }
   : Builtin.ret_typ =
-  let pname = Cfg.Procdesc.get_proc_name pdesc in
-  (* ra_kind = Racquire in following indicates locked *)
-  let ra = {
-    Sil.ra_kind = Sil.Racquire;
-    ra_res = Sil.Rlock;
-    ra_pname = pname;
-    ra_loc = loc;
-    ra_vpath = None; } in
   match args with
-  | [(lexp, _)] -> delete_attr pdesc prop_ path lexp (Sil.Aresource ra)
+  | [(lexp, _)] -> delete_attr pdesc prop_ path lexp Sil.Alocked
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
+
+(** Set the attibute of the value as locked*)
+let execute___set_locked_attribute builtin_args
+  : Builtin.ret_typ =
+  execute___set_attr (Sil.Alocked) builtin_args
+
 (** Set the attibute of the value as resource/unlocked*)
 let execute___set_unlocked_attribute
     ({ Builtin.pdesc; loc; } as builtin_args)