|
|
@ -273,14 +273,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
| False ->
|
|
|
|
| False ->
|
|
|
|
(* precondition can't be satisfied *)
|
|
|
|
(* precondition can't be satisfied *)
|
|
|
|
acc
|
|
|
|
acc
|
|
|
|
| Conjunction actual_indexes -> (
|
|
|
|
| Conjunction actual_indexes ->
|
|
|
|
match List.nth actuals actual_index with
|
|
|
|
List.nth actuals actual_index
|
|
|
|
| Some actual ->
|
|
|
|
(* optional args can result into missing actuals so simply ignore *)
|
|
|
|
conjoin_ownership_precondition actual actual_indexes
|
|
|
|
|> Option.value_map ~default:acc ~f:(fun actual ->
|
|
|
|
| None ->
|
|
|
|
conjoin_ownership_precondition actual actual_indexes )
|
|
|
|
L.internal_error "Bad actual index %d for callee %a with %d actuals." actual_index
|
|
|
|
|
|
|
|
Typ.Procname.pp callee_pname (List.length actuals) ;
|
|
|
|
|
|
|
|
acc )
|
|
|
|
|
|
|
|
in
|
|
|
|
in
|
|
|
|
let update_callee_access (snapshot : AccessSnapshot.t) acc =
|
|
|
|
let update_callee_access (snapshot : AccessSnapshot.t) acc =
|
|
|
|
let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in
|
|
|
|
let access = TraceElem.with_callsite snapshot.access (CallSite.make callee_pname loc) in
|
|
|
|