|
|
@ -14,9 +14,6 @@ module L = Logging
|
|
|
|
module F = Format
|
|
|
|
module F = Format
|
|
|
|
open Utils
|
|
|
|
open Utils
|
|
|
|
|
|
|
|
|
|
|
|
let pvar_to_string pvar =
|
|
|
|
|
|
|
|
Mangled.to_string (Sil.pvar_get_name pvar)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** Check whether the hpred is a |-> representing a resource in the Racquire state *)
|
|
|
|
(** Check whether the hpred is a |-> representing a resource in the Racquire state *)
|
|
|
|
let hpred_is_open_resource prop = function
|
|
|
|
let hpred_is_open_resource prop = function
|
|
|
|
| Sil.Hpointsto(e, _, _) ->
|
|
|
|
| Sil.Hpointsto(e, _, _) ->
|
|
|
@ -32,7 +29,7 @@ let explain_context_leak pname context_typ fieldname error_path =
|
|
|
|
|
|
|
|
|
|
|
|
(** Explain a deallocate stack variable error *)
|
|
|
|
(** Explain a deallocate stack variable error *)
|
|
|
|
let explain_deallocate_stack_var pvar ra =
|
|
|
|
let explain_deallocate_stack_var pvar ra =
|
|
|
|
let pvar_str = pvar_to_string pvar in
|
|
|
|
let pvar_str = Sil.pvar_to_string pvar in
|
|
|
|
Localise.desc_deallocate_stack_variable pvar_str ra.Sil.ra_pname ra.Sil.ra_loc
|
|
|
|
Localise.desc_deallocate_stack_variable pvar_str ra.Sil.ra_pname ra.Sil.ra_loc
|
|
|
|
|
|
|
|
|
|
|
|
(** Explain a deallocate constant string error *)
|
|
|
|
(** Explain a deallocate constant string error *)
|
|
|
@ -186,19 +183,19 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
|
|
|
|
(** Check whether the program variable is a temporary one generated by CIL *)
|
|
|
|
(** Check whether the program variable is a temporary one generated by CIL *)
|
|
|
|
let pvar_is_cil_tmp pvar =
|
|
|
|
let pvar_is_cil_tmp pvar =
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
let name = pvar_to_string pvar in
|
|
|
|
let name = Sil.pvar_to_string pvar in
|
|
|
|
string_is_prefix "_tmp" name
|
|
|
|
string_is_prefix "_tmp" name
|
|
|
|
|
|
|
|
|
|
|
|
(** Check whether the program variable is a temporary one generated by EDG *)
|
|
|
|
(** Check whether the program variable is a temporary one generated by EDG *)
|
|
|
|
let pvar_is_edg_tmp pvar =
|
|
|
|
let pvar_is_edg_tmp pvar =
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
let name = pvar_to_string pvar in
|
|
|
|
let name = Sil.pvar_to_string pvar in
|
|
|
|
string_is_prefix "__T" name
|
|
|
|
string_is_prefix "__T" name
|
|
|
|
|
|
|
|
|
|
|
|
(** Check whether the program variable is a temporary one generated by sawja *)
|
|
|
|
(** Check whether the program variable is a temporary one generated by sawja *)
|
|
|
|
let pvar_is_sawja_tmp pvar =
|
|
|
|
let pvar_is_sawja_tmp pvar =
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
let name = pvar_to_string pvar in
|
|
|
|
let name = Sil.pvar_to_string pvar in
|
|
|
|
string_is_prefix "$irvar" name ||
|
|
|
|
string_is_prefix "$irvar" name ||
|
|
|
|
string_is_prefix "$T" name ||
|
|
|
|
string_is_prefix "$T" name ||
|
|
|
|
string_is_prefix "$bc" name
|
|
|
|
string_is_prefix "$bc" name
|
|
|
@ -208,7 +205,7 @@ let edg_native_tmp_var_name_prefix = "__temp_var_"
|
|
|
|
(** Check whether the program variable is a temporary one generated by EDG *)
|
|
|
|
(** Check whether the program variable is a temporary one generated by EDG *)
|
|
|
|
let pvar_is_edg_tmp pvar =
|
|
|
|
let pvar_is_edg_tmp pvar =
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
Sil.pvar_is_local pvar &&
|
|
|
|
let name = pvar_to_string pvar in
|
|
|
|
let name = Sil.pvar_to_string pvar in
|
|
|
|
string_is_prefix edg_native_tmp_var_name_prefix name
|
|
|
|
string_is_prefix edg_native_tmp_var_name_prefix name
|
|
|
|
|
|
|
|
|
|
|
|
(** Check whether the program variable is a temporary generated by the front-end *)
|
|
|
|
(** Check whether the program variable is a temporary generated by the front-end *)
|
|
|
@ -276,11 +273,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
|
|
|
|
if pvar_is_frontend_tmp pvar then
|
|
|
|
if pvar_is_frontend_tmp pvar then
|
|
|
|
begin
|
|
|
|
begin
|
|
|
|
match find_program_variable_assignment node pvar with
|
|
|
|
match find_program_variable_assignment node pvar with
|
|
|
|
| None ->
|
|
|
|
| None -> None
|
|
|
|
(*
|
|
|
|
|
|
|
|
L.err "exp_string_lv: Cannot find assignment of %s@." (pvar_to_string pvar);
|
|
|
|
|
|
|
|
exit(1) *)
|
|
|
|
|
|
|
|
None
|
|
|
|
|
|
|
|
| Some (node', id) ->
|
|
|
|
| Some (node', id) ->
|
|
|
|
begin
|
|
|
|
begin
|
|
|
|
match find_normal_variable_funcall node' id with
|
|
|
|
match find_normal_variable_funcall node' id with
|
|
|
@ -924,7 +917,7 @@ let explain_dereference_as_caller_expression
|
|
|
|
find 1 formal_params in
|
|
|
|
find 1 formal_params in
|
|
|
|
match find_pvar_with_exp spec_pre exp with
|
|
|
|
match find_pvar_with_exp spec_pre exp with
|
|
|
|
| Some (pv, pvar_off) ->
|
|
|
|
| Some (pv, pvar_off) ->
|
|
|
|
if !verbose then L.d_strln ("pvar: " ^ (pvar_to_string pv));
|
|
|
|
if !verbose then L.d_strln ("pvar: " ^ (Sil.pvar_to_string pv));
|
|
|
|
let pv_name = Sil.pvar_get_name pv in
|
|
|
|
let pv_name = Sil.pvar_get_name pv in
|
|
|
|
if Sil.pvar_is_global pv
|
|
|
|
if Sil.pvar_is_global pv
|
|
|
|
then
|
|
|
|
then
|
|
|
@ -936,7 +929,7 @@ let explain_dereference_as_caller_expression
|
|
|
|
explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off
|
|
|
|
explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off
|
|
|
|
else
|
|
|
|
else
|
|
|
|
if Prop.has_dangling_uninit_attribute spec_pre exp then
|
|
|
|
if Prop.has_dangling_uninit_attribute spec_pre exp then
|
|
|
|
Localise.desc_uninitialized_dangling_pointer_deref deref_str (pvar_to_string pv) loc
|
|
|
|
Localise.desc_uninitialized_dangling_pointer_deref deref_str (Sil.pvar_to_string pv) loc
|
|
|
|
else Localise.no_desc
|
|
|
|
else Localise.no_desc
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
if !verbose then (L.d_str "explain_dereference_as_caller_expression "; Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ());
|
|
|
|
if !verbose then (L.d_str "explain_dereference_as_caller_expression "; Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ());
|
|
|
@ -1013,7 +1006,7 @@ let explain_stack_variable_address_escape loc pvar addr_dexp_opt =
|
|
|
|
Some "the caller via a return"
|
|
|
|
Some "the caller via a return"
|
|
|
|
| Some dexp -> Some (Sil.dexp_to_string dexp)
|
|
|
|
| Some dexp -> Some (Sil.dexp_to_string dexp)
|
|
|
|
| None -> None in
|
|
|
|
| None -> None in
|
|
|
|
Localise.desc_stack_variable_address_escape (pvar_to_string pvar) addr_dexp_str loc
|
|
|
|
Localise.desc_stack_variable_address_escape (Sil.pvar_to_string pvar) addr_dexp_str loc
|
|
|
|
|
|
|
|
|
|
|
|
(** explain unary minus applied to unsigned expression *)
|
|
|
|
(** explain unary minus applied to unsigned expression *)
|
|
|
|
let explain_unary_minus_applied_to_unsigned_expression exp typ node loc =
|
|
|
|
let explain_unary_minus_applied_to_unsigned_expression exp typ node loc =
|
|
|
|