diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in index 4cb7ceebdc781357e9221147bad002aae4d4c284..a4aee4ac5c07f8d1596462e154ed1f4a874feb59 100644 --- a/src/plugins/loop_analysis/Makefile.in +++ b/src/plugins/loop_analysis/Makefile.in @@ -33,6 +33,7 @@ PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE) PLUGIN_NAME:= LoopAnalysis PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register PLUGIN_CMI:= region_analysis_sig +PLUGIN_DEPENDENCIES:= Eva PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org PLUGIN_TESTS_DIRS:=loop_analysis diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml index 39a8827dd6a6ccf49727ac1b7cdb7a18c4d32dde..a37f5ec6586e66fc2b74e11a11b627dc6b060d7a 100644 --- a/src/plugins/loop_analysis/loop_analysis.ml +++ b/src/plugins/loop_analysis/loop_analysis.ml @@ -340,37 +340,18 @@ module Store(* (B:sig *) Printer.pp_stmt stmt let value_min_max stmt vi = - if (Db.Value.is_computed ()) then + if (Eva.Analysis.is_computed ()) then begin Options.feedback ~dkey ~once:true "value analysis computed, trying results"; - if Db.Value.is_reachable_stmt stmt then - let state = Db.Value.get_stmt_state stmt in - try - let loc = Locations.loc_of_varinfo vi in - let v = Db.Value.find state loc in - let ival = Cvalue.V.project_ival v in - let omin, omax = Ival.min_and_max ival in - omin, omax - with - | Not_found -> - Options.feedback ~dkey "value_min_max: not found: %a@.\ - function: %a, stmt: %a" - Printer.pp_varinfo vi Kernel_function.pretty - (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt; - None, None - | Cvalue.V.Not_based_on_null -> - Options.feedback ~dkey "value_min_max: not based on null: %a@.\ - function: %a, stmt: %a" - Printer.pp_varinfo vi Kernel_function.pretty - (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt; - None, None - else - begin + let value = Eva.Results.(before stmt |> eval_var vi |> as_ival) in + match value with + | Result.Ok ival -> Ival.min_and_max ival + | Error e -> + if e = Eva.Results.Bottom then Options.feedback ~dkey "skipping unreachable stmt (function: %a)" Kernel_function.pretty (Kernel_function.find_englobing_kf stmt); - None, None - end + None, None end else begin @@ -490,7 +471,7 @@ module Store(* (B:sig *) with Not_found -> () end | c -> - if (Db.Value.is_computed ()) then + if (Eva.Analysis.is_computed ()) then begin let min_max_int = value_min_max stmt in match c with diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle index f2851d8cb74760ca575b38650701d31b54dcc5f9..b7db69d0c82a6d489540170eed6b3c41a2e97997 100644 --- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle +++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle @@ -433,6 +433,10 @@ with_value.i:26: 5 with_value.i:30: 5 with_value.i:34: 4 + with_value.i:38: 2147483648 + with_value.i:42: 2147483649 + with_value.i:46: 2147483649 + with_value.i:50: 2147483648 with_value.i:54: 2147483646 with_value.i:58: 2147483647 with_value.i:62: 2147483647