From 72ec9516d479df29511415a8b7e21db40a1f8a1d Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 8 Mar 2018 14:26:22 -0800 Subject: [PATCH] [inferbo][trace] Show some SymAssigns Summary: Show some `SymAssign`s (corresponding to parameters) in the trace. Depends on D7194448 Reviewed By: skcho Differential Revision: D7194479 fbshipit-source-id: 0deff6c --- infer/src/bufferoverrun/absLoc.ml | 9 ++++ .../src/bufferoverrun/bufferOverrunChecker.ml | 12 ++++-- infer/src/bufferoverrun/bufferOverrunTrace.ml | 7 ++-- infer/src/bufferoverrun/bufferOverrunUtils.ml | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 16 +++---- .../cpp/bufferoverrun/issues.exp | 42 +++++++++---------- 6 files changed, 51 insertions(+), 37 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index fc306d3dc..c33805ca5 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -49,6 +49,15 @@ module Loc = struct let is_var = function Var _ -> true | _ -> false + let rec contains_allocsite = function + | Var _ -> + false + | Allocsite _ -> + true + | Field (loc, _) -> + contains_allocsite loc + + let of_var v = Var v let of_allocsite a = Allocsite a diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 7334e6402..f2715c6ea 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -53,13 +53,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let unsigned = Typ.ikind_is_unsigned ikind in let v = Dom.Val.make_sym ~unsigned pname new_sym_num - |> Dom.Val.add_trace_elem (Trace.SymAssign location) + |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) in Dom.Mem.add_heap loc v mem | Typ.Tfloat _ -> let v = Dom.Val.make_sym pname new_sym_num - |> Dom.Val.add_trace_elem (Trace.SymAssign location) + |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) in Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> @@ -502,8 +502,12 @@ module Report = struct (Errlog.make_trace_element depth location "Call" [] :: trace, depth + 1) | Trace.Return location -> (Errlog.make_trace_element (depth - 1) location "Return" [] :: trace, depth - 1) - | Trace.SymAssign _ -> - (trace, depth) + | Trace.SymAssign (loc, location) -> + if Loc.contains_allocsite loc then (* ugly, don't show *) + (trace, depth) + else + let desc = Format.asprintf "Parameter: %a" Loc.pp loc in + (Errlog.make_trace_element depth location desc [] :: trace, depth) in List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index abe2514db..691bac1be 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -8,6 +8,7 @@ *) open! IStd +open AbsLoc module F = Format module BoTrace = struct @@ -17,7 +18,7 @@ module BoTrace = struct | Assign of Location.t | Call of Location.t | Return of Location.t - | SymAssign of Location.t + | SymAssign of Loc.t * Location.t [@@deriving compare] type t = {length: int; trace: elem list} [@@deriving compare] @@ -43,8 +44,8 @@ module BoTrace = struct F.fprintf fmt "Call (%a)" Location.pp_file_pos location | Return location -> F.fprintf fmt "Return (%a)" Location.pp_file_pos location - | SymAssign location -> - F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos location + | SymAssign (loc, location) -> + F.fprintf fmt "SymAssign (%a, %a)" Loc.pp loc Location.pp_file_pos location let pp : F.formatter -> t -> unit = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index fc643b14e..498cc512b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -123,7 +123,7 @@ module Make (CFG : ProcCfg.S) = struct let offset = option_value offset itv_make_sym in let size = option_value size itv_make_sym in let alloc_num = new_alloc_num () in - let elem = Trace.SymAssign location in + let elem = Trace.SymAssign (loc, location) in let arr = Sem.eval_array_alloc pname node typ offset size inst_num alloc_num |> Dom.Val.add_trace_elem elem diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 72ad9caf9..0311c6f87 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -7,18 +7,18 @@ codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/cast.c, cast2_Good_FP, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [4, 4] Size: [4, 4]] -codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,Call,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call to `do_while_sub()` ] -codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:11:7 by call to `two_accesses()` ] -codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, [Call,ArrayDeclaration,ArrayAccess: Offset: [3, 3] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ] -codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, [Call,ArrayDeclaration,ArrayAccess: Offset: [-1, -1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:24:3 by call to `two_symbolic_accesses()` ] -codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, [Call,ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ] +codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN_L4, [ArrayDeclaration,Assignment,Call,Parameter: a,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call to `do_while_sub()` ] +codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:11:7 by call to `two_accesses()` ] +codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [3, 3] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ] +codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [-1, -1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:24:3 by call to `two_symbolic_accesses()` ] +codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/duplicates.c:23:3 by call to `two_symbolic_accesses()` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]] codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:21:3 by call to `arr_access()` ] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:21:3 by call to `arr_access()` ] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, [] @@ -31,8 +31,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFER codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, [Call,Assignment,Return] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [max(10, s$0), s$1] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [s$0, min(-1, s$1)] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, s$0), s$1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [s$0, min(-1, s$1)] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: [9, 9]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: [10, 10]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 88efd7fea..cc002b4d0 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,17 +1,17 @@ -codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [15, 15] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/class.cpp:28:34 by call to `my_class_access_nth()` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, [Call,Parameter: n,ArrayAccess: Offset: [15, 15] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/class.cpp:28:34 by call to `my_class_access_nth()` ] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] -codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Return,Call,ArrayAccess: Offset: [5, 5] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call to `Tree_set_child()` ] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Return,Call,Parameter: nth,ArrayAccess: Offset: [5, 5] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call to `Tree_set_child()` ] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [3, 3] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:165:50 by call to `flexible_array_param_access()` ] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Parameter: n,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Parameter: n,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, [Return,ArrayAccess: Offset: [5, 5] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [5, 5] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]] @@ -21,23 +21,23 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVER codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, [] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_u_FP, 5, BUFFER_OVERRUN_S2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `my_vector_oob_Bad()` ] -codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `int_vector_access_at()` ] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_u_FP, 5, BUFFER_OVERRUN_S2, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN_L1, [Call,Parameter: newsize,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `my_vector_oob_Bad()` ] +codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call to `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [6, 6] Size: [5, 5]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [4, 4] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, -1] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, [ArrayDeclaration,Call,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] -codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [6, 6] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [4, 4] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Parameter: __n,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, -1] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Assignment,Call,Call,Assignment,Return,ArrayAccess: Offset: [-1, 0] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/vector.cpp:206:3 by call to `access_minus_one()` ] +codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [1, 1] Size: [1, 1]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, 0] Size: [0, 0]] codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, []