[LoopAnalysis] Removes the slevel analysis and the related options.

Only prints the maximum number of iterations by loop.

headers/header_spec.txt

@@ -917,7 +917,6 @@ src/plugins/loop_analysis/region_analysis_sig.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/slevel_analysis.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/markdown-report/configure.ac: CEA_LGPL
 src/plugins/markdown-report/eva_info.ml: CEA_LGPL
 src/plugins/markdown-report/eva_info.mli: CEA_LGPL

src/plugins/loop_analysis/Makefile.in

@@ -31,7 +31,7 @@ PLUGIN_ENABLE:=@ENABLE_LOOP_ANALYSIS@
 PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
 
 PLUGIN_NAME:= LoopAnalysis
-PLUGIN_CMO:=  options region_analysis_sig region_analysis region_analysis_stmt loop_analysis slevel_analysis register
+PLUGIN_CMO:=  options region_analysis_sig region_analysis region_analysis_stmt loop_analysis register
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
 PLUGIN_TESTS_DIRS:=loop_analysis
 

src/plugins/loop_analysis/README.org

-Loop and "slevel" analysis.
-
-Note: this plug-in has been deprecated in favor of newer Eva features, such as
-      `-eva-auto-loop-unroll`, `//@ loop unroll` annotations and trace
-      partitioning. It will be removed in a future release.
+Loop analysis.
 
 * Overview
 
-This plugin performs two analyses.
-
- - Loop analysis :: Tries to compute an upper bound on the number of
-                    iterations in a loop.
- - Slevel analysis :: Based on loop analysis, tries to compute a
-      sensible per-function "slevel" in Value.
-
-The analysis proceeds in two steps: first the loop analysis is done,
-then using its results, the slevel analysis is performed.
+This plugin tries to compute an upper bound on the number of
+iterations in a loop.
 
 * Installation
 
@@ -35,36 +24,6 @@ instance:
 
 : frama-c -loop test.c
 
-The final pass of the analysis, the =slevel= path, outputs:
-
-:  Add this to your command line:
-:          -val-slevel-merge-after-loop main \
-:          -val-slevel-merge-after-loop g \
-:          -val-slevel-merge-after-loop h3 \
-:          -val-slevel-merge-after-loop h4 \
-:          -val-slevel-merge-after-loop h5 \
-:          -val-slevel-merge-after-loop h6 \
-:          -slevel-function main:40 \
-:          -slevel-function k:2 \
-:          -slevel-function f:8 \
-:          -slevel-function g:0 \
-:          -slevel-function h:9 \
-:          -slevel-function h2:9 \
-:          -slevel-function h3:80 \
-:          -slevel-function h4:40 \
-:          -slevel-function h5:40 \
-:          -slevel-function h6:0
-
-These options are ready to be copy-and-pasted into a shell script or a Makefile.
-
-The =-slevel-function=, when found, gives a value that can be used to
-unroll loops and avoid merging paths; in addition it can detect when
-Value should merge analysis paths with the option
-=-val-slevel-merge-after-loop=. A value of 0 means that no reasonable bound
-has been found, and therefore it might be better to avoid spending time in that
-function. Note that this is just an initial recommendation, to be later refined
-by the user.
-
 The loop analysis path is silent, but its results can be read
 programmatically in the =Loop_Max_Iteration= table for use by other
 plugins.

src/plugins/loop_analysis/loop_analysis.ml

@@ -572,7 +572,6 @@ module Store(* (B:sig *)
             () (* no value => cannot infer anything *)
       ) final_conds;
 
-    (* TODO: Use this table in a second pass, for the slevel analysis. *)
     if not !success then
       Options.debug "no success %a init %a body %a result %a"
         Cil_datatype.Stmt.pretty stmt pretty (value,conds)
@@ -642,3 +641,13 @@ let get_bounds stmt =
 
 let fold_bounds f acc =
   Loop_Max_Iteration.fold_sorted ~cmp:Cil_datatype.Stmt.compare f acc
+
+let display_results () =
+  let pretty_hashtbl fmt () =
+    Loop_Max_Iteration.iter_sorted
+      (fun stmt max ->
+         let loc = Cil_datatype.Stmt.loc stmt in
+         Format.fprintf fmt "%a: %i@," Printer.pp_location loc max)
+  in
+  Options.result "Maximum number of iterations by loop:@\n@[<v>%a@]"
+    pretty_hashtbl ()

src/plugins/loop_analysis/loop_analysis.mli

@@ -30,3 +30,5 @@ val analyze: Kernel_function.t -> unit
 val get_bounds: stmt -> int option
 
 val fold_bounds: (stmt -> int -> 'a -> 'a) -> 'a -> 'a
+
+val display_results: unit -> unit

src/plugins/loop_analysis/options.ml

@@ -24,38 +24,11 @@ include Plugin.Register
     (struct
       let name = "loop"
       let shortname = "loop"
-      let help = "[DEPRECATED: use Eva's loop unroll annotations and options] \
-                  Find number of iterations in loops, and slevel value"
+      let help = "Find maximum number of iterations in loops"
     end)
 
 module Run = False
     (struct
       let option_name = "-loop"
-      let help = "[deprecated: use Eva loop unroll annotations or \
-                  -eva-auto-loop-unroll] Launch loop analysis"
-    end)
-
-module MaxIterations = Int
-    (struct
-      let option_name = "-loop-max-iterations"
-      let arg_name = "num"
-      let default = 1000
-      let help = "If slevel is found to be higher than this number in a loop"
-                 ^ "force the use of merge-after-loop (default: 1000)"
-    end)
-
-module MaxSlevel = Int
-    (struct
-      let option_name = "-loop-max-slevel"
-      let arg_name = "num"
-      let default = 10000
-      let help = "If slevel is found to be higher than this number,"
-                 ^ "set slevel to 0 instead (default: 10000)"
-    end)
-
-module NoBranches = False
-    (struct
-      let option_name = "-loop-no-branches"
-      let help = "Modify the algorithm use to estimate the slevel: ignore \
-                  branching due to ifs and always merge after loops"
+      let help = "Launch loop analysis"
     end)

src/plugins/loop_analysis/options.mli

@@ -23,6 +23,3 @@
 include Plugin.S
 
 module Run:Parameter_sig.Bool
-module MaxIterations:Parameter_sig.Int
-module MaxSlevel:Parameter_sig.Int
-module NoBranches:Parameter_sig.Bool

src/plugins/loop_analysis/register.ml

@@ -20,26 +20,21 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* [nobranches] defines whether this function will compute a full slevel
-   analysis (by default), or estimate loop bounds without
-   branching analysis (if [nobranches = true]). *)
-let analyze ?(nobranches=false) kf =
+let analyze kf =
   if Kernel_function.is_definition kf
   then
     if Cil_datatype.Stmt.Set.is_empty (Loop.get_non_naturals kf)
-    then (Loop_analysis.analyze kf;
-          Slevel_analysis.analyze ~nobranches kf)
+    then Loop_analysis.analyze kf
     else
       Options.warning "Could not analyze function %a;@ \
                        it contains a non-natural loop"
         Kernel_function.pretty kf
 ;;
 
-
-let main() =
+let main () =
   if Options.Run.get() then begin
-    Globals.Functions.iter (analyze ~nobranches:(Options.NoBranches.get()));
-    Slevel_analysis.display_results()
+    Globals.Functions.iter analyze;
+    Loop_analysis.display_results ();
   end
 ;;
 

src/plugins/loop_analysis/slevel_analysis.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2021                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* Note: this does not represent exactly the weird slevel consumption
-   strategy. *)
-
-module Needs_Merge_After_Loop =
-  Kernel_function.Make_Table
-    (Datatype.Bool)
-    (struct
-      let size = 97
-      let name = "Needs_Merge_After_Loop"
-      let dependencies = [Ast.self]
-    end)
-module Suggested_Slevel =
-  Kernel_function.Make_Table
-    (Datatype.Integer)
-    (struct
-      let size = 97
-      let name = "Suggested_Slevel"
-      let dependencies = [Ast.self]
-    end)
-module Functions_With_Unknown_Loop =
-  Kernel_function.Make_Table
-    (Datatype.Bool)
-    (struct
-      let size = 97
-      let name = "Functions_With_Unknown_Loop"
-      let dependencies = [Ast.self]
-    end)
-
-let max_slevel_encountered = ref Integer.zero;;
-let update_max_slevel_encountered x = match x, !max_slevel_encountered with
-  | None, _ -> ()
-  | Some a, b -> max_slevel_encountered := Integer.max a b
-;;
-
-type path_bound = Integer.t option  (* None = infinite *)
-
-module Specific(KF:sig val kf: Kernel_function.t end) = struct
-
-  let join2_stmts stmt1 stmt2 =
-    (* Cil.dummyStmt is bottom for statements. *)
-    if Cil_datatype.Stmt.equal stmt1 stmt2
-    then stmt1
-    else if Cil_datatype.Stmt.equal stmt1 Cil.dummyStmt
-    then stmt2
-    else if Cil_datatype.Stmt.equal stmt2 Cil.dummyStmt
-    then stmt1
-    else assert false
-  ;;
-
-  let add_path_bounds a b = match (a,b) with
-    | None, _ | _, None -> None
-    | Some a, Some b -> Some (Integer.add a b)
-
-  type abstract_value = path_bound * Cil_types.stmt
-
-  let join2 (a1,s1) (a2,s2) = (add_path_bounds a1 a2,join2_stmts s1 s2);;
-
-  let join = function
-    | [] -> (Some Integer.zero,Cil.dummyStmt)
-    | [x] -> x
-    | a::b -> List.fold_left join2 a b
-  ;;
-
-  let mu f (entry,loop) =
-    let max_iteration =
-      try Some(Loop_analysis.Loop_Max_Iteration.find loop)
-      with Not_found -> Functions_With_Unknown_Loop.replace KF.kf true; None
-    in
-    let (in_loop,_) = f (Some Integer.one,loop) in
-    let result =
-      match (max_iteration,in_loop, entry) with
-      (* If merge_after_loop, set to 1 after the loop. *)
-      | None, _,_ | _, None,_ | _,_,None ->
-        Needs_Merge_After_Loop.replace KF.kf true; Some Integer.one
-      | Some max_iteration, Some in_loop, Some entry ->
-        (* Kernel.feedback "max_iteration %d in_loop %a entry %a" *)
-        (*   max_iteration (Integer.pretty ~hexa:false) in_loop *)
-        (*   (Integer.pretty ~hexa:false) entry; *)
-        try
-          let in_loop_i = Integer.to_int in_loop in
-          match in_loop_i with
-          | 1 -> Some(Integer.mul entry (Integer.of_int max_iteration))
-          | _ ->
-            (* Ignoring entry, we have 1 state at the loop entry, then q,
-               then q^2, etc.
-               Sum i=0 to n q^n = (q^{n+1} - 1)/(q - 1)). *)
-            let s = if in_loop_i > 1 && (max_iteration + 1) > 100 then
-                raise (Invalid_argument "exponent too large for slevel")
-              else
-                Integer.power_int_positive_int in_loop_i (max_iteration + 1)
-            in
-            let slevel_inside_loop =
-              Integer.e_div (Integer.pred s) (Integer.pred in_loop)
-            in
-            let result = Integer.mul entry slevel_inside_loop in
-            (* Kernel.feedback "s %a slevel_inside_loop %a result %a" *)
-            (*   (Integer.pretty ~hexa:false) s *)
-            (*   (Integer.pretty ~hexa:false) slevel_inside_loop *)
-            (*   (Integer.pretty ~hexa:false) result; *)
-            if Integer.le result (Integer.of_int (Options.MaxIterations.get()))
-            then Some result
-            else raise Exit
-        with
-        | Invalid_argument _ (* Possible negative exponent *)
-        | Z.Overflow         (* Integer too big *)
-        | Exit  ->           (* Above MaxIterations. *)
-          update_max_slevel_encountered
-            (Some (Integer.mul entry (Integer.mul in_loop
-                                        (Integer.of_int max_iteration))));
-          Needs_Merge_After_Loop.replace KF.kf true; Some Integer.one
-    in
-    (* (match result with *)
-    (*  | None -> () *)
-    (*  | Some res -> *)
-    (*    Kernel.feedback "final result %a" (Integer.pretty ~hexa:false) res); *)
-    (result,loop)
-
-  let kf = KF.kf
-
-  let compile_node stmt (num,stmt2) =
-    let stmt = join2_stmts stmt stmt2 in
-    let open Cil_types in
-    let map_on_all_succs (value) =
-      List.map (fun x -> (Region_analysis.Edge(stmt,x),(value,x))) stmt.succs in
-    map_on_all_succs num
-
-end
-
-(* does not compute branches, and sets -merge-after-loop for all functions *)
-module SpecificNoBranches(KF:sig val kf: Kernel_function.t end) = struct
-
-  type abstract_value = path_bound * Cil_types.stmt
-
-  let join2_stmts stmt1 stmt2 =
-    (* Cil.dummyStmt is bottom for statements. *)
-    if Cil_datatype.Stmt.equal stmt1 stmt2 then stmt1
-    else if Cil_datatype.Stmt.equal stmt1 Cil.dummyStmt then stmt2
-    else if Cil_datatype.Stmt.equal stmt2 Cil.dummyStmt then stmt1
-    else assert false
-
-  let join2 (a1,s1) (a2,s2) =
-    let path_bounds =
-      match a1, a2 with
-      | None, None -> None
-      | Some a, None | None, Some a -> Some a
-      | Some a1, Some a2 -> Some (Integer.max a1 a2)
-    in
-    path_bounds, join2_stmts s1 s2;;
-
-  let join = function
-    | [] -> (Some Integer.zero, Cil.dummyStmt)
-    | [x] -> x
-    | a::b -> List.fold_left join2 a b
-  ;;
-
-  let mu f (entry,loop) =
-    let max_iteration =
-      try Some (Loop_analysis.Loop_Max_Iteration.find loop)
-      with Not_found -> Functions_With_Unknown_Loop.replace KF.kf true; None
-    in
-    let (in_loop,_) = f (Some Integer.one, loop) in
-    let result =
-      match (max_iteration, in_loop, entry) with
-      (* If merge_after_loop, set to 1 after the loop. *)
-      | None, _, _ | _, None, _ | _, _, None -> Some Integer.one
-      | Some max_iteration, Some in_loop, Some entry ->
-        try
-          let in_loop_i = Integer.to_int in_loop in
-          match in_loop_i with
-          | 1 -> Some Integer.(max entry (of_int max_iteration))
-          | _ ->
-            (* We only want the loop iteration count, so just multiply bounds;
-               add 1 to avoid issues with slevel counting of first/last
-               iterations in nested loops *)
-            Some Integer.(pred (mul (succ (of_int in_loop_i))
-                                  (of_int max_iteration)))
-        with
-        | Z.Overflow         (* Integer too big *)
-          -> update_max_slevel_encountered
-               (Some (Integer.mul entry (Integer.mul in_loop
-                                           (Integer.of_int max_iteration))));
-          Some Integer.one
-    in
-    Needs_Merge_After_Loop.replace KF.kf true;
-    (result, loop)
-
-  let kf = KF.kf
-
-  let compile_node stmt (num,stmt2) =
-    let stmt = join2_stmts stmt stmt2 in
-    let map_on_all_succs (value) =
-      List.map (fun x -> Region_analysis.Edge(stmt, x), (value, x))
-        stmt.Cil_types.succs
-    in
-    map_on_all_succs num
-
-end
-
-module type M' = Region_analysis_stmt.M with
-  type abstract_value = path_bound * Cil_types.stmt
-
-(* [nobranches] defines whether this function will compute a full slevel
-   analysis (by default), or estimate loop bounds without branching
-   analysis (if [nobranches = true]). *)
-let analyze ?(nobranches=false) kf =
-  max_slevel_encountered := Integer.zero;
-  Options.debug "slevel analysis of function %a" Kernel_function.pretty kf;
-  let m =
-    if nobranches then
-      (module SpecificNoBranches(struct let kf = kf end) : M')
-    else
-      (module Specific(struct let kf = kf end) : M')
-  in
-  let module M = (val m : M') in
-  let module Node = Region_analysis_stmt.MakeNode(M) in
-  let module Result = Region_analysis.Make(Node) in
-  let after = Result.after in
-  let dict = after (Some Integer.one, (Kernel_function.find_first_stmt kf)) in
-  Node.Edge_Dict.iter dict (fun _ (x,_) -> update_max_slevel_encountered x);
-  Suggested_Slevel.replace kf !max_slevel_encountered
-;;
-
-let cmp_kf_by_name kf1 kf2 =
-  String.compare (Kernel_function.get_name kf1) (Kernel_function.get_name kf2)
-
-let display_results() =
-  let display_functions_without_bounds fmt =
-    Functions_With_Unknown_Loop.iter_sorted ~cmp:cmp_kf_by_name (fun kf _ ->
-        Format.fprintf fmt "%a@\n" Kernel_function.pretty kf) in
-  if Functions_With_Unknown_Loop.length () > 0 then
-    Options.result "Functions with loops whose bounds we could not find:@\n%t"
-      display_functions_without_bounds;
-  let display_merge_after_loop fmt =
-    Needs_Merge_After_Loop.iter_sorted ~cmp:cmp_kf_by_name (fun kf _ ->
-        Format.fprintf fmt "-val-slevel-merge-after-loop %a \\@\n"
-          Kernel_function.pretty kf)
-  in
-  let max_slevel_opt = Integer.of_int (Options.MaxSlevel.get ()) in
-  let bounds_over_max_slevel =
-    List.rev (
-      Suggested_Slevel.fold_sorted ~cmp:cmp_kf_by_name
-        (fun kf i acc ->
-           if Integer.gt i max_slevel_opt then (kf, i) :: acc else acc)
-        [])
-  in
-  let display_slevel_function fmt (kf, i) =
-    Format.fprintf fmt "-slevel-function %a:%a"
-      Kernel_function.pretty kf (Integer.pretty ~hexa:false) i
-  in
-  if bounds_over_max_slevel <> [] then
-    Options.result "Functions with loops whose estimated bounds \
-                    were larger than %s@ (we recommend setting \
-                    their slevel to 0 to avoid wasting time):@\n%a"
-      Options.MaxSlevel.name
-      (Pretty_utils.pp_list ~sep:"@\n"
-         (Pretty_utils.pp_pair ~sep:" " Kernel_function.pretty
-            (fun fmt i -> Format.fprintf fmt "(estimated bounds: %a)"
-                (Integer.pretty ~hexa:false) i)))
-      bounds_over_max_slevel;
-  let functions_with_bounds =
-    List.rev (
-      Suggested_Slevel.fold_sorted ~cmp:cmp_kf_by_name
-        (fun kf i acc ->
-           (* Do not report -slevel-function for functions whose bounds
-              were not found or were larger than -max-slevel-loop *)
-           let slevel =
-             if Integer.le i max_slevel_opt &&
-                not (Functions_With_Unknown_Loop.mem kf) then i
-             else Integer.zero
-           in
-           (kf, slevel) :: acc
-        ) [])
-  in
-  (* for a more usable output, in case the user does not want functions
-     with bounds equal to 0, sort them before the others *)
-  let functions_with_bounds_0, functions_with_bounds_pos =
-    List.partition (fun (_kf, i) -> Integer.equal i Integer.zero)
-      functions_with_bounds
-  in
-  let display_slevel fmt =
-    Format.fprintf fmt "%a"
-      (Pretty_utils.pp_list ~sep:" \\@\n" display_slevel_function)
-      (functions_with_bounds_0 @ functions_with_bounds_pos)
-  in
-  Options.result "Add this to your command line:@\n%t%t @\n"
-    display_merge_after_loop display_slevel;
-
-;;

src/plugins/loop_analysis/tests/loop_analysis/oracle/mixed_output.res.oracle

 [kernel] Parsing tests/loop_analysis/mixed_output.i (no preprocessing)
-[loop] Functions with loops whose bounds we could not find:
-  loop_inf
-  loop_inf2
-[loop] Functions with loops whose estimated bounds were larger than -loop-max-slevel
-  (we recommend setting their slevel to 0 to avoid wasting time):
-  loop_large (estimated bounds: 4000000000000000000)
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop loop108 \
-  -val-slevel-merge-after-loop loop_inf \
-  -val-slevel-merge-after-loop loop_inf2 \
-  -val-slevel-merge-after-loop loop_large \
-  -slevel-function loop_inf:0 \
-  -slevel-function loop_inf2:0 \
-  -slevel-function loop_large:0 \
-  -slevel-function loop0:1 \
-  -slevel-function loop1:1 \
-  -slevel-function loop10:10 \
-  -slevel-function loop108:400 \
-  -slevel-function loop10init:7 \
-  -slevel-function loop10initneg:13 \
-  -slevel-function loop10initnegle:14 \
-  -slevel-function m01:7 \
-  -slevel-function m02:8 \
-  -slevel-function m03:7 \
-  -slevel-function m04:7 \
-  -slevel-function m05:7 \
-  -slevel-function m06:7 \
-  -slevel-function m07:7 \
-  -slevel-function m08:8 \
-  -slevel-function m09:7 \
-  -slevel-function m10:8 \
-  -slevel-function m11:7 \
-  -slevel-function m12:7 \
-  -slevel-function m13:7 \
-  -slevel-function m14:7 \
-  -slevel-function m15:7 \
-  -slevel-function m16:8 \
-  -slevel-function m17:1 \
-  -slevel-function m18:1 \
-  -slevel-function m19:1 \
-  -slevel-function m20:1 \
-  -slevel-function m21:1 \
-  -slevel-function m22:1 \
-  -slevel-function m23:1 \
-  -slevel-function m24:1 \
-  -slevel-function m_01:7 \
-  -slevel-function m_02:8 \
-  -slevel-function m_03:7 \
-  -slevel-function m_04:7 \
-  -slevel-function m_05:7 \
-  -slevel-function m_06:7 \
-  -slevel-function m_07:7 \
-  -slevel-function m_08:8 \
-  -slevel-function m_09:7 \
-  -slevel-function m_10:8 \
-  -slevel-function m_11:7 \
-  -slevel-function m_12:7 \
-  -slevel-function m_13:7 \
-  -slevel-function m_14:7 \
-  -slevel-function m_15:7 \
-  -slevel-function m_16:8 \
-  -slevel-function m_17:1 \
-  -slevel-function m_18:1 \
-  -slevel-function m_19:1 \
-  -slevel-function m_20:1 \
-  -slevel-function m_21:1 \
-  -slevel-function m_22:1 \
-  -slevel-function m_23:1 \
-  -slevel-function m_24:1 \
-  -slevel-function main:1 \
-  -slevel-function straight_line:1 \
-  -slevel-function with_if:2
+[loop] Maximum number of iterations by loop:
+  tests/loop_analysis/mixed_output.i:19: 0
+  tests/loop_analysis/mixed_output.i:24: 1
+  tests/loop_analysis/mixed_output.i:29: 10
+  tests/loop_analysis/mixed_output.i:34: 7
+  tests/loop_analysis/mixed_output.i:39: 13
+  tests/loop_analysis/mixed_output.i:45: 14
+  tests/loop_analysis/mixed_output.i:64: 10
+  tests/loop_analysis/mixed_output.i:68: 10
+  tests/loop_analysis/mixed_output.i:80: 1000000
+  tests/loop_analysis/mixed_output.i:84: 1000000
+  tests/loop_analysis/mixed_output.i:88: 1000000
+  tests/loop_analysis/mixed_output.i:92: 1000000
+  tests/loop_analysis/mixed_output.i:103: 7
+  tests/loop_analysis/mixed_output.i:107: 8
+  tests/loop_analysis/mixed_output.i:111: 7
+  tests/loop_analysis/mixed_output.i:115: 7
+  tests/loop_analysis/mixed_output.i:119: 7
+  tests/loop_analysis/mixed_output.i:123: 7
+  tests/loop_analysis/mixed_output.i:127: 7
+  tests/loop_analysis/mixed_output.i:131: 8
+  tests/loop_analysis/mixed_output.i:135: 7
+  tests/loop_analysis/mixed_output.i:139: 8
+  tests/loop_analysis/mixed_output.i:143: 7
+  tests/loop_analysis/mixed_output.i:147: 7
+  tests/loop_analysis/mixed_output.i:151: 7
+  tests/loop_analysis/mixed_output.i:155: 7
+  tests/loop_analysis/mixed_output.i:159: 7
+  tests/loop_analysis/mixed_output.i:163: 8
+  tests/loop_analysis/mixed_output.i:167: 1
+  tests/loop_analysis/mixed_output.i:171: 1
+  tests/loop_analysis/mixed_output.i:175: 1
+  tests/loop_analysis/mixed_output.i:179: 1
+  tests/loop_analysis/mixed_output.i:183: 1
+  tests/loop_analysis/mixed_output.i:187: 1
+  tests/loop_analysis/mixed_output.i:191: 1
+  tests/loop_analysis/mixed_output.i:195: 1
+  tests/loop_analysis/mixed_output.i:199: 7
+  tests/loop_analysis/mixed_output.i:203: 8
+  tests/loop_analysis/mixed_output.i:207: 7
+  tests/loop_analysis/mixed_output.i:211: 7
+  tests/loop_analysis/mixed_output.i:215: 7
+  tests/loop_analysis/mixed_output.i:219: 7
+  tests/loop_analysis/mixed_output.i:223: 7
+  tests/loop_analysis/mixed_output.i:227: 8
+  tests/loop_analysis/mixed_output.i:231: 7
+  tests/loop_analysis/mixed_output.i:235: 8
+  tests/loop_analysis/mixed_output.i:239: 7
+  tests/loop_analysis/mixed_output.i:243: 7
+  tests/loop_analysis/mixed_output.i:247: 7
+  tests/loop_analysis/mixed_output.i:251: 7
+  tests/loop_analysis/mixed_output.i:255: 7
+  tests/loop_analysis/mixed_output.i:259: 8
+  tests/loop_analysis/mixed_output.i:263: 1
+  tests/loop_analysis/mixed_output.i:267: 1
+  tests/loop_analysis/mixed_output.i:271: 1
+  tests/loop_analysis/mixed_output.i:275: 1
+  tests/loop_analysis/mixed_output.i:279: 1
+  tests/loop_analysis/mixed_output.i:283: 1
+  tests/loop_analysis/mixed_output.i:287: 1
+  tests/loop_analysis/mixed_output.i:291: 1

src/plugins/loop_analysis/tests/loop_analysis/oracle/ne.res.oracle

@@ -35,70 +35,20 @@
 [loop] tests/loop_analysis/ne.i:127: Warning: 
   termination condition may not be reached (infinite loop?)
   loop amounts to: for (i = 0; i != -5; i += 15)
-[loop] Functions with loops whose bounds we could not find:
-  f02
-  f04
-  f06
-  f08
-  f10
-  f12
-  f14
-  f16
-  no_iter01
-  no_iter02
-  no_iter03
-  no_iter04
-  no_iter05
-  no_iter06
-  no_iter07
-  no_iter08
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop f02 \
-  -val-slevel-merge-after-loop f04 \
-  -val-slevel-merge-after-loop f06 \
-  -val-slevel-merge-after-loop f08 \
-  -val-slevel-merge-after-loop f10 \
-  -val-slevel-merge-after-loop f12 \
-  -val-slevel-merge-after-loop f14 \
-  -val-slevel-merge-after-loop f16 \
-  -val-slevel-merge-after-loop no_iter01 \
-  -val-slevel-merge-after-loop no_iter02 \
-  -val-slevel-merge-after-loop no_iter03 \
-  -val-slevel-merge-after-loop no_iter04 \
-  -val-slevel-merge-after-loop no_iter05 \
-  -val-slevel-merge-after-loop no_iter06 \
-  -val-slevel-merge-after-loop no_iter07 \
-  -val-slevel-merge-after-loop no_iter08 \
-  -slevel-function f02:0 \
-  -slevel-function f04:0 \
-  -slevel-function f06:0 \
-  -slevel-function f08:0 \
-  -slevel-function f10:0 \
-  -slevel-function f12:0 \
-  -slevel-function f14:0 \
-  -slevel-function f16:0 \
-  -slevel-function no_iter01:0 \
-  -slevel-function no_iter02:0 \
-  -slevel-function no_iter03:0 \
-  -slevel-function no_iter04:0 \
-  -slevel-function no_iter05:0 \
-  -slevel-function no_iter06:0 \
-  -slevel-function no_iter07:0 \
-  -slevel-function no_iter08:0 \
-  -slevel-function a1:43 \
-  -slevel-function a2:146 \
-  -slevel-function a3:51 \
-  -slevel-function a4:154 \
-  -slevel-function a5:46 \
-  -slevel-function a6:46 \
-  -slevel-function a7:54 \
-  -slevel-function a8:54 \
-  -slevel-function f01:4 \
-  -slevel-function f03:4 \
-  -slevel-function f05:1 \
-  -slevel-function f07:1 \
-  -slevel-function f09:1 \
-  -slevel-function f11:6 \
-  -slevel-function f13:4 \
-  -slevel-function f15:1 \
-  -slevel-function main:1
+[loop] Maximum number of iterations by loop:
+  tests/loop_analysis/ne.i:2: 43
+  tests/loop_analysis/ne.i:6: 146
+  tests/loop_analysis/ne.i:10: 51
+  tests/loop_analysis/ne.i:14: 154
+  tests/loop_analysis/ne.i:18: 46
+  tests/loop_analysis/ne.i:22: 46
+  tests/loop_analysis/ne.i:26: 54
+  tests/loop_analysis/ne.i:30: 54
+  tests/loop_analysis/ne.i:34: 4
+  tests/loop_analysis/ne.i:42: 4
+  tests/loop_analysis/ne.i:50: 1
+  tests/loop_analysis/ne.i:58: 1
+  tests/loop_analysis/ne.i:66: 1
+  tests/loop_analysis/ne.i:74: 6
+  tests/loop_analysis/ne.i:82: 4
+  tests/loop_analysis/ne.i:90: 1

src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop.res.oracle

@@ -3,5 +3,4 @@
   Non-natural loop detected.
 [loop] Warning: Could not analyze function duff;
   it contains a non-natural loop
-[loop] Add this to your command line:
-  -slevel-function f:1
+[loop] Maximum number of iterations by loop:

src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop2.res.oracle

@@ -3,4 +3,4 @@
   Non-natural loop detected.
 [loop] Warning: Could not analyze function main;
   it contains a non-natural loop
-[loop] Add this to your command line:
+[loop] Maximum number of iterations by loop:

src/plugins/loop_analysis/tests/loop_analysis/oracle/slevel_overflow.res.oracle

-[kernel] Parsing tests/loop_analysis/slevel_overflow.c (with preprocessing)
-[loop] Functions with loops whose estimated bounds were larger than -loop-max-slevel
-  (we recommend setting their slevel to 0 to avoid wasting time):
-  f2 (estimated bounds: 16777216000000000000000)
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop f1 \
-  -val-slevel-merge-after-loop f2 \
-  -val-slevel-merge-after-loop f3 \
-  -slevel-function f2:0 \
-  -slevel-function f1:1073741824000000 \
-  -slevel-function f3:18014398509481984

src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.1.res.oracle

-[kernel] Parsing tests/loop_analysis/small_loop.i (no preprocessing)
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop main \
-  -slevel-function main:20

src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.0.res.oracle → src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.res.oracle

 [kernel] Parsing tests/loop_analysis/small_loop.i (no preprocessing)
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop main \
-  -slevel-function main:20
+[loop] Maximum number of iterations by loop:
+  tests/loop_analysis/small_loop.i:5: 10

src/plugins/loop_analysis/tests/loop_analysis/oracle/test.0.res.oracle

-[kernel] Parsing tests/loop_analysis/test.i (no preprocessing)
-[loop] Functions with loops whose bounds we could not find:
-  g
-  h6
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop g \
-  -val-slevel-merge-after-loop h3 \
-  -val-slevel-merge-after-loop h4 \
-  -val-slevel-merge-after-loop h5 \
-  -val-slevel-merge-after-loop h6 \
-  -val-slevel-merge-after-loop main \
-  -slevel-function g:0 \
-  -slevel-function h6:0 \
-  -slevel-function f:8 \
-  -slevel-function h:9 \
-  -slevel-function h2:9 \
-  -slevel-function h3:40 \
-  -slevel-function h4:20 \
-  -slevel-function h5:20 \
-  -slevel-function k:2 \
-  -slevel-function main:20

src/plugins/loop_analysis/tests/loop_analysis/oracle/test.1.res.oracle

-[kernel] Parsing tests/loop_analysis/test.i (no preprocessing)
-[loop] Functions with loops whose bounds we could not find:
-  g
-  h6
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop g \
-  -val-slevel-merge-after-loop h \
-  -val-slevel-merge-after-loop h2 \
-  -val-slevel-merge-after-loop h3 \
-  -val-slevel-merge-after-loop h4 \
-  -val-slevel-merge-after-loop h5 \
-  -val-slevel-merge-after-loop h6 \
-  -val-slevel-merge-after-loop main \
-  -slevel-function g:0 \
-  -slevel-function h6:0 \
-  -slevel-function f:1 \
-  -slevel-function h:9 \
-  -slevel-function h2:9 \
-  -slevel-function h3:20 \
-  -slevel-function h4:10 \
-  -slevel-function h5:10 \
-  -slevel-function k:1 \
-  -slevel-function main:10

src/plugins/loop_analysis/tests/loop_analysis/oracle/test.res.oracle

+[kernel] Parsing tests/loop_analysis/test.i (no preprocessing)
+[loop] Maximum number of iterations by loop:
+  tests/loop_analysis/test.i:8: 10
+  tests/loop_analysis/test.i:39: 9
+  tests/loop_analysis/test.i:44: 9
+  tests/loop_analysis/test.i:49: 20
+  tests/loop_analysis/test.i:55: 10
+  tests/loop_analysis/test.i:61: 10

src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle

@@ -424,65 +424,45 @@
   ----------------------------------------------------------------------------
   No logical properties have been reached by the analysis.
   ----------------------------------------------------------------------------
-[loop] Functions with loops whose bounds we could not find:
-  g1
-  g2
-  g3
-  g4
-[loop] Functions with loops whose estimated bounds were larger than -loop-max-slevel
-  (we recommend setting their slevel to 0 to avoid wasting time):
-  g5 (estimated bounds: 2147483646)
-  g6 (estimated bounds: 2147483647)
-  g7 (estimated bounds: 2147483647)
-  g8 (estimated bounds: 2147483646)
-[loop] Add this to your command line:
-  -val-slevel-merge-after-loop g1 \
-  -val-slevel-merge-after-loop g2 \
-  -val-slevel-merge-after-loop g3 \
-  -val-slevel-merge-after-loop g4 \
-  -slevel-function g1:0 \
-  -slevel-function g2:0 \
-  -slevel-function g3:0 \
-  -slevel-function g4:0 \
-  -slevel-function g5:0 \
-  -slevel-function g6:0 \
-  -slevel-function g7:0 \
-  -slevel-function g8:0 \
-  -slevel-function f1:6 \
-  -slevel-function f2:7 \
-  -slevel-function f2_u_const:7 \
-  -slevel-function f3:7 \
-  -slevel-function f4:6 \
-  -slevel-function f5:4 \
-  -slevel-function f6:5 \
-  -slevel-function f7:5 \
-  -slevel-function f8:4 \
-  -slevel-function h1:21 \
-  -slevel-function h2:22 \
-  -slevel-function h3:22 \
-  -slevel-function h4:21 \
-  -slevel-function h5:21 \
-  -slevel-function h6:22 \
-  -slevel-function h7:22 \
-  -slevel-function h8:21 \
-  -slevel-function i1:13 \
-  -slevel-function i2:14 \
-  -slevel-function i3:3 \
-  -slevel-function i4:4 \
-  -slevel-function j1:41 \
-  -slevel-function j2:42 \
-  -slevel-function j3:19 \
-  -slevel-function j4:20 \
-  -slevel-function main:1 \
-  -slevel-function ne1:43 \
-  -slevel-function ne2:146 \
-  -slevel-function ne3:46 \
-  -slevel-function ne4:46 \
-  -slevel-function nev1:43 \
-  -slevel-function nev2:146 \
-  -slevel-function nev3:46 \
-  -slevel-function nev4:46 \
-  -slevel-function nev5:43 \
-  -slevel-function nev6:146 \
-  -slevel-function nev7:46 \
-  -slevel-function nev8:46
+[loop] Maximum number of iterations by loop:
+  tests/loop_analysis/with_value.i:6: 6
+  tests/loop_analysis/with_value.i:10: 7
+  tests/loop_analysis/with_value.i:14: 7
+  tests/loop_analysis/with_value.i:18: 6
+  tests/loop_analysis/with_value.i:22: 4
+  tests/loop_analysis/with_value.i:26: 5
+  tests/loop_analysis/with_value.i:30: 5
+  tests/loop_analysis/with_value.i:34: 4
+  tests/loop_analysis/with_value.i:54: 2147483646
+  tests/loop_analysis/with_value.i:58: 2147483647
+  tests/loop_analysis/with_value.i:62: 2147483647
+  tests/loop_analysis/with_value.i:66: 2147483646
+  tests/loop_analysis/with_value.i:70: 21
+  tests/loop_analysis/with_value.i:74: 22
+  tests/loop_analysis/with_value.i:78: 22
+  tests/loop_analysis/with_value.i:82: 21
+  tests/loop_analysis/with_value.i:86: 21
+  tests/loop_analysis/with_value.i:90: 22
+  tests/loop_analysis/with_value.i:94: 22
+  tests/loop_analysis/with_value.i:98: 21
+  tests/loop_analysis/with_value.i:102: 13
+  tests/loop_analysis/with_value.i:106: 14
+  tests/loop_analysis/with_value.i:110: 3
+  tests/loop_analysis/with_value.i:114: 4
+  tests/loop_analysis/with_value.i:118: 41
+  tests/loop_analysis/with_value.i:122: 42
+  tests/loop_analysis/with_value.i:126: 19
+  tests/loop_analysis/with_value.i:130: 20
+  tests/loop_analysis/with_value.i:134: 7
+  tests/loop_analysis/with_value.i:138: 43
+  tests/loop_analysis/with_value.i:142: 146
+  tests/loop_analysis/with_value.i:146: 46
+  tests/loop_analysis/with_value.i:150: 46
+  tests/loop_analysis/with_value.i:154: 43
+  tests/loop_analysis/with_value.i:158: 146
+  tests/loop_analysis/with_value.i:162: 46
+  tests/loop_analysis/with_value.i:166: 46
+  tests/loop_analysis/with_value.i:170: 43
+  tests/loop_analysis/with_value.i:174: 146
+  tests/loop_analysis/with_value.i:178: 46
+  tests/loop_analysis/with_value.i:182: 46