[infer] Do not treat static locals as stack-allocated in the biabduction analysis

Reviewed By: jeremydubreil

Differential Revision: D5214422

fbshipit-source-id: f8adb6d
master
Jia Chen 8 years ago committed by Facebook Github Bot
parent 468ed8a9c7
commit 938425020d

@ -283,12 +283,15 @@ let deallocate_stack_vars tenv (p: 'a Prop.t) pvars =
let res = ref p' in
let p'_fav = Prop.prop_fav p' in
let do_var (v, freshv) =
if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
begin
stack_vars_address_in_post := v :: !stack_vars_address_in_post;
let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in
res := add_or_replace tenv !res pred
end in
(* static locals are not stack-allocated *)
if not (Pvar.is_static_local v) then
(* the address of a de-allocated stack var in in the post *)
if Sil.fav_mem p'_fav freshv then
begin
stack_vars_address_in_post := v :: !stack_vars_address_in_post;
let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in
res := add_or_replace tenv !res pred
end in
List.iter ~f:do_var !fresh_address_vars;
!res in
!stack_vars_address_in_post, List.fold ~f:(Prop.prop_atom_and tenv) ~init:p'' pi

@ -60,6 +60,7 @@ SOURCES = \
shared/types/struct_pass_by_value.cpp \
shared/types/typeid_expr.cpp \
$(wildcard smart_ptr/*.cpp) \
$(wildcard static_local/*.cpp) \
$(wildcard subtyping/*.cpp) \
$(wildcard vector/*.cpp) \

@ -118,6 +118,8 @@ codetoanalyze/cpp/errors/smart_ptr/unique_ptr_deref.cpp, unique_ptr::unique_ptr_
codetoanalyze/cpp/errors/smart_ptr/unique_ptr_deref.cpp, unique_ptr::unique_ptr_move_null_deref, 3, NULL_DEREFERENCE, [start of procedure unique_ptr::unique_ptr_move_null_deref()]
codetoanalyze/cpp/errors/smart_ptr/unique_ptr_deref.cpp, unique_ptr::unique_ptr_move_ok_deref, 3, UNINITIALIZED_VALUE, [start of procedure unique_ptr::unique_ptr_move_ok_deref()]
codetoanalyze/cpp/errors/smart_ptr/unique_ptr_deref.cpp, unique_ptr::unique_ptr_move_ok_deref, 4, MEMORY_LEAK, [start of procedure unique_ptr::unique_ptr_move_ok_deref(),return from a call to unique_ptr::unique_ptr_move_ok_deref]
codetoanalyze/cpp/errors/static_local/nonstatic_local_bad.cpp, nonstatic_local_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, [start of procedure nonstatic_local_bad(),return from a call to nonstatic_local_bad]
codetoanalyze/cpp/errors/static_local/nonstatic_local_bad.cpp, nonstatic_local_caller, 2, DANGLING_POINTER_DEREFERENCE, [start of procedure nonstatic_local_caller(),start of procedure nonstatic_local_bad(),return from a call to nonstatic_local_bad]
codetoanalyze/cpp/errors/subtyping/cast_with_enforce.cpp, cast_with_enforce::cast_with_npe, 3, NULL_DEREFERENCE, [start of procedure cast_with_enforce::cast_with_npe(),start of procedure Base,return from a call to cast_with_enforce::Base_Base]
codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp, dynamic__cast::rightPointerCast, 4, DIVIDE_BY_ZERO, [start of procedure dynamic__cast::rightPointerCast(),start of procedure Derived,start of procedure Base,return from a call to dynamic__cast::Base_Base,return from a call to dynamic__cast::Derived_Derived,Condition is true]
codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp, dynamic__cast::rightPointerCast, 4, MEMORY_LEAK, [start of procedure dynamic__cast::rightPointerCast(),start of procedure Derived,start of procedure Base,return from a call to dynamic__cast::Base_Base,return from a call to dynamic__cast::Derived_Derived,Condition is true]

@ -0,0 +1,17 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
int* nonstatic_local_bad() {
int x = 1;
return &x;
}
int nonstatic_local_caller() {
int* p = nonstatic_local_bad();
return *p;
}

@ -0,0 +1,17 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
int* static_local_ok() {
static int x = 1;
return &x;
}
int static_local_caller() {
int* p = static_local_ok();
return *p;
}
Loading…
Cancel
Save