From 3f260952f67871f0d15444d28448420dcbb472cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 25 Mar 2021 10:14:22 +0100
Subject: [PATCH] [LoopAnalysis] Removes the slevel analysis and the related
options.
Only prints the maximum number of iterations by loop.
---
headers/header_spec.txt | 1 -
src/plugins/loop_analysis/Makefile.in | 2 +-
src/plugins/loop_analysis/README.org | 47 +--
src/plugins/loop_analysis/loop_analysis.ml | 11 +-
src/plugins/loop_analysis/loop_analysis.mli | 2 +
src/plugins/loop_analysis/options.ml | 31 +-
src/plugins/loop_analysis/options.mli | 3 -
src/plugins/loop_analysis/register.ml | 15 +-
src/plugins/loop_analysis/slevel_analysis.ml | 310 ------------------
.../oracle/mixed_output.res.oracle | 133 ++++----
.../tests/loop_analysis/oracle/ne.res.oracle | 84 +----
.../oracle/non_natural_loop.res.oracle | 3 +-
.../oracle/non_natural_loop2.res.oracle | 2 +-
.../oracle/slevel_overflow.res.oracle | 11 -
.../oracle/small_loop.0.res.oracle | 4 -
.../oracle/small_loop.1.res.oracle | 4 -
.../oracle/small_loop.res.oracle | 3 +
.../loop_analysis/oracle/test.0.res.oracle | 21 --
.../loop_analysis/oracle/test.1.res.oracle | 23 --
.../loop_analysis/oracle/test.res.oracle | 8 +
.../oracle/with_value.res.oracle | 104 +++---
.../tests/loop_analysis/slevel_overflow.c | 62 ----
.../tests/loop_analysis/small_loop.i | 4 -
.../loop_analysis/tests/loop_analysis/test.i | 5 -
24 files changed, 156 insertions(+), 737 deletions(-)
delete mode 100644 src/plugins/loop_analysis/slevel_analysis.ml
delete mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/slevel_overflow.res.oracle
delete mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.0.res.oracle
delete mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.1.res.oracle
create mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.res.oracle
delete mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/test.0.res.oracle
delete mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/test.1.res.oracle
create mode 100644 src/plugins/loop_analysis/tests/loop_analysis/oracle/test.res.oracle
delete mode 100644 src/plugins/loop_analysis/tests/loop_analysis/slevel_overflow.c
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d1e4b57004f..04a39712977 100644
--- a/headers/header_spec.txt
+++ b/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
diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in
index 002dfe843f1..74a6af00dbb 100644
--- a/src/plugins/loop_analysis/Makefile.in
+++ b/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
diff --git a/src/plugins/loop_analysis/README.org b/src/plugins/loop_analysis/README.org
index 6e4388ee4b5..79197bc191c 100644
--- a/src/plugins/loop_analysis/README.org
+++ b/src/plugins/loop_analysis/README.org
@@ -1,20 +1,9 @@
-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.
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index 2a55ef055c8..b97bd62b23f 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/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 ()
diff --git a/src/plugins/loop_analysis/loop_analysis.mli b/src/plugins/loop_analysis/loop_analysis.mli
index 3141ee73f68..a9072b072f0 100644
--- a/src/plugins/loop_analysis/loop_analysis.mli
+++ b/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
diff --git a/src/plugins/loop_analysis/options.ml b/src/plugins/loop_analysis/options.ml
index 54ca3514d2a..b7947aa7464 100644
--- a/src/plugins/loop_analysis/options.ml
+++ b/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)
diff --git a/src/plugins/loop_analysis/options.mli b/src/plugins/loop_analysis/options.mli
index 85a4f9918b6..d48830ac209 100644
--- a/src/plugins/loop_analysis/options.mli
+++ b/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
diff --git a/src/plugins/loop_analysis/register.ml b/src/plugins/loop_analysis/register.ml
index a6b1a69cc7c..47c4967b273 100644
--- a/src/plugins/loop_analysis/register.ml
+++ b/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
;;
diff --git a/src/plugins/loop_analysis/slevel_analysis.ml b/src/plugins/loop_analysis/slevel_analysis.ml
deleted file mode 100644
index 2e70c946c7a..00000000000
--- a/src/plugins/loop_analysis/slevel_analysis.ml
+++ /dev/null
@@ -1,310 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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;
-
-;;
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/mixed_output.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/mixed_output.res.oracle
index ca741cf1c77..ba2c662bb6b 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/mixed_output.res.oracle
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/mixed_output.res.oracle
@@ -1,73 +1,62 @@
[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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/ne.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/ne.res.oracle
index 415f11cf56c..fd4a4804d12 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/ne.res.oracle
+++ b/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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop.res.oracle
index 9da39d23e3e..a43fb8865f9 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop.res.oracle
+++ b/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:
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop2.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop2.res.oracle
index fdef320cf5e..f3ebfae4c8d 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/non_natural_loop2.res.oracle
+++ b/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:
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/slevel_overflow.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/slevel_overflow.res.oracle
deleted file mode 100644
index c12264a63be..00000000000
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/slevel_overflow.res.oracle
+++ /dev/null
@@ -1,11 +0,0 @@
-[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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.0.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.0.res.oracle
deleted file mode 100644
index 5ab62cc0696..00000000000
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.0.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.1.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.1.res.oracle
deleted file mode 100644
index 5ab62cc0696..00000000000
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.1.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.res.oracle
new file mode 100644
index 00000000000..82ab70bc037
--- /dev/null
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/small_loop.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/loop_analysis/small_loop.i (no preprocessing)
+[loop] Maximum number of iterations by loop:
+ tests/loop_analysis/small_loop.i:5: 10
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.0.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.0.res.oracle
deleted file mode 100644
index 923695413d0..00000000000
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.0.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.1.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.1.res.oracle
deleted file mode 100644
index 887aa01c9d3..00000000000
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.1.res.oracle
+++ /dev/null
@@ -1,23 +0,0 @@
-[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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.res.oracle
new file mode 100644
index 00000000000..4e45cc92bf4
--- /dev/null
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/test.res.oracle
@@ -0,0 +1,8 @@
+[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
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 2532c0705de..475629e9d00 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
@@ -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
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/slevel_overflow.c b/src/plugins/loop_analysis/tests/loop_analysis/slevel_overflow.c
deleted file mode 100644
index 1f0c8d3d3fb..00000000000
--- a/src/plugins/loop_analysis/tests/loop_analysis/slevel_overflow.c
+++ /dev/null
@@ -1,62 +0,0 @@
-/* run.config
- STDOPT: #"-loop-max-slevel 999999999999999999"
-*/
-
-#define ABS(a) ((a < 0) ? -a : a)
-
-void f1() {
- long i, j, k, err;
- for(i = 0; i < 1000000; i++) {
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- }
-}
-
-void f2() {
- long i, j, k, err;
- for(i = 0; i < 1000000000000000; i++) {
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- }
-}
-
-void f3() {
- long i, j, k, err;
- for(i = 0; i < 64*64*64*64*64; i++) {
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- for(j = 0; j < 64; j++)
- for(k = 0; k < 64; k++)
- if(ABS(err) > 1);
- }
-}
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/small_loop.i b/src/plugins/loop_analysis/tests/loop_analysis/small_loop.i
index b9ef8cd5ae0..274c1440a1a 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/small_loop.i
+++ b/src/plugins/loop_analysis/tests/loop_analysis/small_loop.i
@@ -1,7 +1,3 @@
-/* run.config
- STDOPT: #"-loop-max-slevel 20"
- STDOPT:
-*/
volatile int nondet;
int main() {
int i;
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/test.i b/src/plugins/loop_analysis/tests/loop_analysis/test.i
index 329da8e1f49..3a5a260b930 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/test.i
+++ b/src/plugins/loop_analysis/tests/loop_analysis/test.i
@@ -1,8 +1,3 @@
-/*run.config
-STDOPT:
-STDOPT: #"-loop-no-branches"
-*/
-
void main(void)
{
int i; int j;
--
GitLab