From bd725602ee34b51bd1cf93a5ba425e7cb8b9efc3 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 18 Jun 2018 01:49:35 -0700 Subject: [PATCH] Inferbo: size of arrayblk is unsigned Reviewed By: skcho Differential Revision: D8370803 fbshipit-source-id: 1276b7e --- infer/src/bufferoverrun/bufferOverrunChecker.ml | 2 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 5 ++--- infer/tests/codetoanalyze/java/performance/issues.exp | 4 ++-- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index c46b2836d..b8219492d 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -64,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let size = match length with | Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) -> - Some (Itv.make_sym pname new_sym_num) + None (* Will be made symbolic by [decl_sym_arr] *) | _ -> Option.map ~f:Itv.of_int_lit length in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index dae65a5a6..14a9c6167 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -60,9 +60,8 @@ module Exec = struct fun ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num ~new_sym_num ~new_alloc_num mem -> let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in - let itv_make_sym () = Itv.make_sym pname new_sym_num in - let offset = option_value offset itv_make_sym in - let size = option_value size itv_make_sym in + let offset = option_value offset (fun () -> Itv.make_sym pname new_sym_num) in + let size = option_value size (fun () -> Itv.make_sym ~unsigned:true pname new_sym_num) in let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in let arr = diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3b7c1a5f6..ec2b1d6a5 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -2,8 +2,8 @@ codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(i codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 882] codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 882] codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 889] -codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * s$7^2] -codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * s$7^2] +codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * u$7^2] +codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * u$7^2] codetoanalyze/java/performance/Break.java, int Break.break_constant(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * s$1] codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 7 * s$1] codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * s$1]