|
|
@ -6,6 +6,7 @@
|
|
|
|
*)
|
|
|
|
*)
|
|
|
|
open! IStd
|
|
|
|
open! IStd
|
|
|
|
module F = Format
|
|
|
|
module F = Format
|
|
|
|
|
|
|
|
module L = Logging
|
|
|
|
open Result.Monad_infix
|
|
|
|
open Result.Monad_infix
|
|
|
|
|
|
|
|
|
|
|
|
let report summary diagnostic =
|
|
|
|
let report summary diagnostic =
|
|
|
@ -87,29 +88,32 @@ module PulseTransferFunctions = struct
|
|
|
|
| _ ->
|
|
|
|
| _ ->
|
|
|
|
Ok astate )
|
|
|
|
Ok astate )
|
|
|
|
| Direct callee_pname when Typ.Procname.is_constructor callee_pname -> (
|
|
|
|
| Direct callee_pname when Typ.Procname.is_constructor callee_pname -> (
|
|
|
|
match actuals with
|
|
|
|
L.d_printfln "constructor call detected@." ;
|
|
|
|
| AccessExpression constructor_access :: rest ->
|
|
|
|
match actuals with
|
|
|
|
let constructed_object = HilExp.AccessExpression.dereference constructor_access in
|
|
|
|
| AccessExpression constructor_access :: rest ->
|
|
|
|
PulseOperations.havoc [crumb] call_loc constructed_object astate >>= read_all rest
|
|
|
|
let constructed_object = HilExp.AccessExpression.dereference constructor_access in
|
|
|
|
| _ ->
|
|
|
|
PulseOperations.havoc [crumb] call_loc constructed_object astate >>= read_all rest
|
|
|
|
Ok astate )
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
Ok astate )
|
|
|
|
| Direct (Typ.Procname.ObjC_Cpp callee_pname)
|
|
|
|
| Direct (Typ.Procname.ObjC_Cpp callee_pname)
|
|
|
|
when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> (
|
|
|
|
when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> (
|
|
|
|
match actuals with
|
|
|
|
L.d_printfln "operator= detected@." ;
|
|
|
|
(* We want to assign *lhs to *rhs when rhs is materialized temporary created in constructor *)
|
|
|
|
match actuals with
|
|
|
|
| [AccessExpression lhs; HilExp.AccessExpression (AddressOf (Base rhs_base as rhs_exp))]
|
|
|
|
(* We want to assign *lhs to *rhs when rhs is materialized temporary created in constructor *)
|
|
|
|
when Var.is_cpp_temporary (fst rhs_base) ->
|
|
|
|
| [AccessExpression lhs; HilExp.AccessExpression (AddressOf (Base rhs_base as rhs_exp))]
|
|
|
|
let lhs_deref = HilExp.AccessExpression.dereference lhs in
|
|
|
|
when Var.is_cpp_temporary (fst rhs_base) ->
|
|
|
|
exec_assign summary lhs_deref (HilExp.AccessExpression rhs_exp) call_loc astate
|
|
|
|
let lhs_deref = HilExp.AccessExpression.dereference lhs in
|
|
|
|
(* copy assignment *)
|
|
|
|
exec_assign summary lhs_deref (HilExp.AccessExpression rhs_exp) call_loc astate
|
|
|
|
| [AccessExpression lhs; HilExp.AccessExpression rhs] ->
|
|
|
|
(* copy assignment *)
|
|
|
|
let lhs_deref = HilExp.AccessExpression.dereference lhs in
|
|
|
|
| [AccessExpression lhs; HilExp.AccessExpression rhs] ->
|
|
|
|
let rhs_deref = HilExp.AccessExpression.dereference rhs in
|
|
|
|
let lhs_deref = HilExp.AccessExpression.dereference lhs in
|
|
|
|
PulseOperations.havoc [crumb] call_loc lhs_deref astate
|
|
|
|
let rhs_deref = HilExp.AccessExpression.dereference rhs in
|
|
|
|
>>= fun astate -> PulseOperations.read call_loc rhs_deref astate >>| fst
|
|
|
|
PulseOperations.havoc [crumb] call_loc lhs_deref astate
|
|
|
|
| _ ->
|
|
|
|
>>= fun astate -> PulseOperations.read call_loc rhs_deref astate >>| fst
|
|
|
|
read_all actuals astate )
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
read_all actuals astate )
|
|
|
|
| _ ->
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
L.d_printfln "skipping unknown procedure@." ;
|
|
|
|
read_all actuals astate
|
|
|
|
read_all actuals astate
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|