diff --git a/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java b/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java index 813f52eb5..2bbdea56b 100644 --- a/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java +++ b/infer/models/java/builtins/com/facebook/infer/builtins/InferBuiltins.java @@ -16,12 +16,8 @@ public class InferBuiltins { public native static void __set_mem_attribute(Object o); - public native static void __set_lock_attribute(Object o); - public native static void __set_locked_attribute(Object o); - public native static void __set_unlocked_attribute(Object o); - public native static void __delete_locked_attribute(Object o); public native static void _exit(); diff --git a/infer/src/IR/BUILTINS.ml b/infer/src/IR/BUILTINS.ml index 49fede7b5..6f8584b6f 100644 --- a/infer/src/IR/BUILTINS.ml +++ b/infer/src/IR/BUILTINS.ml @@ -85,16 +85,12 @@ module type S = sig val __set_hidden_field : t - val __set_lock_attribute : t - val __set_locked_attribute : t val __set_mem_attribute : t val __set_observer_attribute : t - val __set_unlocked_attribute : t - val __set_unsubscribed_observer_attribute : t val __set_wont_leak_attribute : t diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index 88450f2dc..7f788f473 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -112,16 +112,12 @@ let __set_file_attribute = create_procname "__set_file_attribute" let __set_hidden_field = create_procname "__set_hidden_field" -let __set_lock_attribute = create_procname "__set_lock_attribute" - let __set_locked_attribute = create_procname "__set_locked_attribute" let __set_mem_attribute = create_procname "__set_mem_attribute" let __set_observer_attribute = create_procname "__set_observer_attribute" -let __set_unlocked_attribute = create_procname "__set_unlocked_attribute" - let __set_unsubscribed_observer_attribute = create_procname "__set_unsubscribed_observer_attribute" let __set_wont_leak_attribute = create_procname "__set_wont_leak_attribute" diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index ad6e7b797..a9048fe26 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -372,19 +372,6 @@ let execute___set_file_attribute {Builtin.tenv; pdesc; prop_; path; ret_id; args | _ -> raise (Exceptions.Wrong_argument_number __POS__) - -(** Set the attibute of the value as lock *) -let execute___set_lock_attribute {Builtin.tenv; pdesc; prop_; path; ret_id; args; loc} - : Builtin.ret_typ = - match (args, ret_id) with - | [(lexp, _)], _ -> - let pname = Procdesc.get_proc_name pdesc in - let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in - set_resource_attribute tenv prop path n_lexp loc PredSymb.Rlock - | _ -> - raise (Exceptions.Wrong_argument_number __POS__) - - (** Set the resource attribute of the first real argument of method as ignore, the first argument is assumed to be "this" *) let execute___method_set_ignore_attribute {Builtin.tenv; pdesc; prop_; path; ret_id; args; loc} @@ -591,20 +578,6 @@ let execute___set_locked_attribute builtin_args : Builtin.ret_typ = execute___set_attr PredSymb.Alocked builtin_args -(** Set the attibute of the value as resource/unlocked*) -let execute___set_unlocked_attribute ({Builtin.pdesc; loc} as builtin_args) : Builtin.ret_typ = - let pname = Procdesc.get_proc_name pdesc in - (* ra_kind = Rrelease in following indicates unlocked *) - let ra = - { PredSymb.ra_kind= PredSymb.Rrelease - ; ra_res= PredSymb.Rlock - ; ra_pname= pname - ; ra_loc= loc - ; ra_vpath= None } - in - execute___set_attr (PredSymb.Aresource ra) builtin_args - - (** Set the attibute of the value as wont leak*) let execute___set_wont_leak_attribute builtin_args : Builtin.ret_typ = execute___set_attr PredSymb.Awont_leak builtin_args @@ -1117,9 +1090,6 @@ let __set_file_attribute = (* set a hidden field in the struct to the given value *) let __set_hidden_field = Builtin.register BuiltinDecl.__set_hidden_field execute___set_hidden_field -let __set_lock_attribute = - Builtin.register BuiltinDecl.__set_lock_attribute execute___set_lock_attribute - let __set_locked_attribute = Builtin.register BuiltinDecl.__set_locked_attribute execute___set_locked_attribute @@ -1133,10 +1103,6 @@ let __set_observer_attribute = Builtin.register BuiltinDecl.__set_observer_attribute (execute___set_attr PredSymb.Aobserver) -let __set_unlocked_attribute = - Builtin.register BuiltinDecl.__set_unlocked_attribute execute___set_unlocked_attribute - - let __set_unsubscribed_observer_attribute = Builtin.register BuiltinDecl.__set_unsubscribed_observer_attribute (execute___set_attr PredSymb.Aunsubscribed_observer)