diff --git a/doc/eva/examples/parametrizing/pragma-widen-hints.c b/doc/eva/examples/parametrizing/pragma-widen-hints.c
deleted file mode 100644
index 1e829bf9757fb58a22d79318d5dbec16e7e3c4f3..0000000000000000000000000000000000000000
--- a/doc/eva/examples/parametrizing/pragma-widen-hints.c
+++ /dev/null
@@ -1,9 +0,0 @@
-int i,j;
-
-void main(void)
-{
- int n = 13;
- /*@ loop pragma WIDEN_HINTS i, 12, 13; */
- for (i=0; i<n; i++)
- j = 4 * i + 7;
-}
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 507d379936c598fde52ff744f40907bfd039ac1a..76628e4e00deb03c73726dddb65a3185d6edb710 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -3844,28 +3844,6 @@ thresholds.
Dynamic hints are automatically global; the \lstinline|global| prefix must not
be applied to them.
-\subsubsection*{Deprecated: \texttt{WIDEN\_HINTS} loop pragma}
-
-\begin{important}
- This syntax has been deprecated in favor of the previous one
- and it is kept here only for reference.
-\end{important}
-
-The \lstinline|loop widen_hints| annotation above has an obsoleted syntax: \\
-\lstinline|//@ loop pragma WIDEN_HINTS $v_1,\ldots,v_n$, $e_1,\ldots,e_m$ ;|\\
-which serves the same purpose but has a few differences:
-
-\begin{itemize}
-\item it is restricted to loop annotations;
-\item more than one variable ($v_1,\ldots,v_n$) can be specified in a single hint;
-\item if no variables are specified, it works as the special value \lstinline|"all"|,
- that is, all variables in the loop are affected;
-\item it does not accept the \lstinline|global| label.
-\end{itemize}
-
-Example:
-\csource{examples/parametrizing/pragma-widen-hints.c}
-
\subsubsection{Loop invariants}
A last technique consists in using the loop invariant construct of ACSL.
@@ -3915,7 +3893,7 @@ within bounds\footnote{And more precisely between \lstinline+t[1]+ and
\lstinline+t[9]+, since \lstinline+p+
is incremented before the affectation to \lstinline+*p+.}.
Thus, this technique is complementary to the use of
-\lstinline+WIDEN_HINTS+, which only accepts integers --- hence not
+\lstinline+widen_hints+, which only accepts integers --- hence not
\lstinline+&t[N-1]+. Compared to the use
of \lstinline+-eva-slevel+ or \lstinline+-ulevel+,
the technique above does not unroll the loop; thus the overall results
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index cafa0e96b6bf360f0c103ca51cdb542520381f07..5793c2feb49aabde87b7f8ef4e4ade646c1f5b87 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1464,10 +1464,6 @@ loop_pragma:
(if $3 <> "UNROLL" then
Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
Unroll_specs $4)
- else if $3 = "WIDEN_VARIABLES" then
- Widen_variables $4
- else if $3 = "WIDEN_HINTS" then
- Widen_hints $4
else raise (Not_well_formed (loc $sloc,"Unknown loop pragma")) }
;
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 4bc1d09e3912cfc2307e68172b2237329b35579d..9a3077594832805d91a225cca66de4852d2434fd 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -82,7 +82,6 @@ let extract_from_pragmas global_find_init s =
match a.annot_content with
| APragma (Loop_pragma (Unroll_specs specs)) ->
List.fold_left (update_info global_find_init e) info specs
- | APragma (Loop_pragma _) -> info
| _ -> assert false (* should have been filtered above. *)
in
List.fold_left get_infos empty_info pragmas
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 874fb84942604f9d0ea8c9a8d6806d6b4926a8e4..65883a64ce26715463f3aa69166f17dff78a4b14 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -478,9 +478,7 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
| AVariant (term,_) ->
(* to preserve the interpretation of the variant *)
get_zone_from_term (Option.get loop_body_opt) term results
- | APragma (Loop_pragma (Unroll_specs terms))
- | APragma (Loop_pragma (Widen_hints terms))
- | APragma (Loop_pragma (Widen_variables terms)) ->
+ | APragma (Loop_pragma (Unroll_specs terms)) ->
(* to select the declaration of the variables *)
List.fold_left
(fun results term -> {
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 0b27f448cc4937d02c715c9f40ba63603e12ac99..0ae3f376d5ac98e2a2fb00a3cd2649de377df45c 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1738,8 +1738,6 @@ and behavior = {
(** Pragmas for the value analysis plugin of Frama-C. *)
and loop_pragma =
| Unroll_specs of term list
- | Widen_hints of term list
- | Widen_variables of term list
(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a9d7c98103737e6c3f99048062c7ff2a5af3647a..31b287429f816c944a15ba5bd08533f4dcafd02c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3164,12 +3164,6 @@ class cil_printer () = object (self)
(pp_list false self#disjoint_behaviors) disjoint
method private loop_pragma fmt = function
- | Widen_hints terms ->
- fprintf fmt "WIDEN_HINTS @[%a@]"
- (Pretty_utils.pp_list ~sep:",@ " self#term) terms
- | Widen_variables terms ->
- fprintf fmt "WIDEN_VARIABLES @[%a@]"
- (Pretty_utils.pp_list ~sep:",@ " self#term) terms
| Unroll_specs terms ->
fprintf fmt "UNROLL @[%a@]"
(Pretty_utils.pp_list ~sep:",@ " self#term) terms
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index bdd64597f8619aa9e107a96a7c81671aebfdff2c..ed13828430d9dd900638e11bcc8df886892228ac 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -932,10 +932,6 @@ and pp_termination_kind fmt = function
and pp_loop_pragma fmt = function
| Unroll_specs(term_list) ->
Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
- | Widen_hints(term_list) ->
- Format.fprintf fmt "Widen_hints(%a)" (pp_list pp_term) term_list
- | Widen_variables(term_list) ->
- Format.fprintf fmt "Widen_variables(%a)" (pp_list pp_term) term_list
and pp_slice_pragma fmt = function
| SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 9509cb045c44331814e5fa1af17e9fa7769da74f..f0aeef687bad114badea91a4fd70bc0170de689e 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -453,10 +453,6 @@ let print_spec fmt spec =
let print_loop_pragma fmt p =
match p with
Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
- | Widen_hints l ->
- fprintf fmt "WIDEN_HINTS@ %a" (pp_list ~sep:",@ " print_lexpr) l
- | Widen_variables l ->
- fprintf fmt "WIDEN_VARIABLES@ %a" (pp_list ~sep:",@ " print_lexpr) l
let print_slice_pragma fmt p =
match p with
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 58fe0aa05cd35e230ab82958356a766b3c2961f3..35206eb8bd56bf238238d2225f58100c2b6d0f43 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -702,11 +702,7 @@ and is_same_variant (v,m) (v',m') env =
and is_same_loop_pragma p p' env =
match p, p' with
- | Unroll_specs l, Unroll_specs l'
- | Widen_hints l, Widen_hints l'
- | Widen_variables l, Widen_variables l' ->
- is_same_list is_same_term l l' env
- | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
+ | Unroll_specs l, Unroll_specs l' -> is_same_list is_same_term l l' env
and is_same_slice_pragma p p' env =
match p, p' with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 891b2fb3a4be7fafa4dad423808b06e8dae0d002..7eb80e74d5a03dbb1bf3bb1771ae9c88a7adc34e 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2049,10 +2049,6 @@ and childrenLoopPragma vis p =
match p with
| Unroll_specs lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
if lt' != lt then Unroll_specs lt' else p
- | Widen_hints lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
- if lt' != lt then Widen_hints lt' else p
- | Widen_variables lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
- if lt' != lt then Widen_variables lt' else p
and childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 3377cdbb68d9e20a77b0aecff2ded641130ea2be..9c5eddcfe4c9e0491a19a30ddcb18c113e06fb6b 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3632,29 +3632,9 @@ struct
let plain_logic_type loc env t = logic_type (base_ctxt env) loc env t
- (* For Widen_hints and Widen_variables, we check that the arguments of the
- pragma can be understood later. Keep this code synchronized with
- src/plugins/eva/utils/widen.ml. *)
let loop_pragma env p =
- let accept_int = function
- { term_node = TConst (Integer _)} -> true | _ -> false
- in
- let accept_var = function
- { term_node = TLval (TVar {lv_origin = Some _}, _)} -> true | _ -> false
- in
- (* fail when the translation of [p] does not verify the predicate [accept]*)
- let term_accept accept p =
- let t = term env p in
- if not (accept t) then
- C.error t.term_loc "invalid pragma '%a'" Cil_printer.pp_term t;
- t
- in
match p with
| Unroll_specs l -> Cil_types.Unroll_specs (List.map (term env) l)
- | Widen_variables l -> Cil_types.Widen_variables (List.map (term_accept accept_var) l)
- | Widen_hints l ->
- let accept t = accept_int t || accept_var t in
- Cil_types.Widen_hints (List.map (term_accept accept) l)
let model_annot loc ti =
let env = Lenv.empty() in
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index cd74caa5993ca4a66e9c79f9fa9ec10fd9d103d1..6846b6e71144681376f1988aae766b0a4376282a 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1179,9 +1179,6 @@ let is_same_logic_type_info t1 t2 =
let is_same_loop_pragma p1 p2 =
match p1,p2 with
Unroll_specs l1, Unroll_specs l2 -> is_same_list is_same_term l1 l2
- | Widen_hints l1, Widen_hints l2 -> is_same_list is_same_term l1 l2
- | Widen_variables l1, Widen_variables l2 -> is_same_list is_same_term l1 l2
- | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
let is_same_slice_pragma p1 p2 =
match p1,p2 with
@@ -2302,7 +2299,7 @@ let is_trivial_annotation a =
-> false
let is_property_pragma = function
- | Loop_pragma (Unroll_specs _ | Widen_hints _ | Widen_variables _)
+ | Loop_pragma (Unroll_specs _)
| Slice_pragma (SPexpr _ | SPctrl | SPstmt)
| Impact_pragma (IPexpr _ | IPstmt) -> false
(* If at some time a pragma becomes something which should be proven,
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 0dfa48308069b1bc63f3554dbec3bb165539da0e..d123c416326462beb7a280287382364b46fe7872 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -323,8 +323,6 @@ type spec = {
type loop_pragma =
| Unroll_specs of lexpr list
- | Widen_hints of lexpr list
- | Widen_variables of lexpr list
(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 0394740c78769e2c9e72380ad634fc33ce81575a..f4caa9f5a6efd427cf6b2f9c33305a78ab0900e7 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -57,7 +57,7 @@ let update_global_hints new_hints =
let hints = Widen_type.join (Global_Static_Hints.get ()) new_hints in
Global_Static_Hints.set hints;
-class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
+class widen_visitor init_widen_hints init_enclosing_loops = object(self)
inherit Visitor.frama_c_inplace
val widen_hints = init_widen_hints
@@ -69,70 +69,17 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
then update_global_hints new_hints
else widen_hints := Widen_type.join new_hints !widen_hints
- method private add_float_thresholds ?base float_thresholds =
- let new_hints = Widen_type.float_hints None base float_thresholds in
- if Option.fold ~none:false ~some:Base.is_global base
- then update_global_hints new_hints
- else widen_hints := Widen_type.join new_hints !widen_hints
-
method private add_var_hints ~stmt hints =
widen_hints := Widen_type.join (Widen_type.var_hints stmt hints) !widen_hints
- method private process_loop_pragma stmt p =
- match p with
- | Widen_variables l -> begin
- let f (lv, lt) t = match t with
- | { term_node= TLval (TVar {lv_origin = Some vi}, _)} ->
- (Base.Set.add (Base.of_varinfo vi) lv, lt)
- | _ -> (lv, t::lt)
- in
- match List.fold_left f (Base.Set.empty, []) l with
- | (var_hints, []) ->
- (* the annotation is empty or contains only variables *)
- self#add_var_hints ~stmt var_hints
- | (_lv, _lt) ->
- Self.warning ~once:true
- "could not interpret loop pragma relative to widening variables"
- end
- | Widen_hints l -> begin
- let f (lv, lint, lfloat, lt) t = match t with
- | { term_node= TLval (TVar { lv_origin = Some vi}, _)} ->
- (Base.of_varinfo vi :: lv, lint, lfloat, lt)
- | { term_node= TConst (Integer(v,_))} ->
- (lv, IntSet.add v lint, lfloat, lt)
- | _ ->
- match constFoldTermToReal t.term_node with
- | Some f -> (lv, lint, FloatSet.add f lfloat, lt)
- | None -> (lv, lint, lfloat, t::lt)
- in
- match List.fold_left f ([], IntSet.empty, FloatSet.empty, []) l with
- | (vars, int_thresholds, float_thresholds, []) ->
- (* the annotation is empty or contains only variables *)
- if vars = [] then begin
- self#add_int_thresholds int_thresholds;
- self#add_float_thresholds float_thresholds
- end else
- List.iter (fun base ->
- self#add_int_thresholds ~base int_thresholds;
- self#add_float_thresholds ~base float_thresholds;
- ) vars
- | _ ->
- Self.warning ~once:true
- "could not interpret loop pragma relative to widening hint"
- end
- | _ -> ()
-
method! vstmt (s:stmt) =
match s.skind with
| Loop (_, bl, _, _, _) -> begin
(* ZZZ: this code does not handle loops that are created using gotos. We
could improve this by finding the relevant statements using a
traversal of the CFG. *)
- let annot = Annotations.code_annot s in
- let pragmas = Logic_utils.extract_loop_pragma annot in
- List.iter (self#process_loop_pragma s) pragmas;
let new_loop_info = s :: enclosing_loops in
- let visitor = new pragma_widen_visitor widen_hints new_loop_info in
+ let visitor = new widen_visitor widen_hints new_loop_info in
ignore (Visitor.visitFramacBlock visitor bl);
Cil.SkipChildren (* Otherwise the inner statements are visited multiple
times needlessly *)
@@ -408,7 +355,7 @@ let compute_global_static_hints () =
let per_function_static_hints fdec =
let widen_hints = ref Widen_type.empty in
- let visitor_pragma = new pragma_widen_visitor widen_hints [] in
+ let visitor_pragma = new widen_visitor widen_hints [] in
ignore (Visitor.visitFramacFunction visitor_pragma fdec);
let visitor_local = new hints_visitor widen_hints false in
ignore (Visitor.visitFramacFunction visitor_local fdec);
diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i
index 6b6ffcb301940eff3177b26a0915af06a0d4c488..bd7f5dc7b9a1dfab04bd50d4462e762751469cf9 100644
--- a/tests/slicing/loops.i
+++ b/tests/slicing/loops.i
@@ -173,7 +173,7 @@ int X, Y, Z ;
void loop (int cond) {
if (cond) {
int c = 0 ;
- /*@ loop pragma WIDEN_HINTS X, 10, 100 ; */ while (1) {
+ while (1) {
//@ slice pragma ctrl ;
if (c) {
X++;
diff --git a/tests/slicing/oracle/adpcm.res.oracle b/tests/slicing/oracle/adpcm.res.oracle
index a8be5b40a15dafe92bf571d5b5369d8f63effbe8..d064224755afa3c264138d1ff4795db2f1dc9feb 100644
--- a/tests/slicing/oracle/adpcm.res.oracle
+++ b/tests/slicing/oracle/adpcm.res.oracle
@@ -1531,6 +1531,7 @@ Slicing project worklist [default] =
[pdg] computing for function logscl
[pdg] done for function logscl
[slicing] applying actions: 3/3...
+[slicing] tests/test/adpcm.c:607: Warning: Dropping unsupported ACSL annotation
[sparecode] remove unused global declarations from project 'Sliced code tmp'
[sparecode] removed unused global declarations in new project 'Sliced code'
/* Generated by Frama-C */
@@ -2070,8 +2071,7 @@ void main(void)
{
int i;
i = 0;
- /*@ loop pragma UNROLL 11;
- loop pragma WIDEN_HINTS 32767; */
+ /*@ loop pragma UNROLL 11; */
while (i < 10) {
encode_slice_1(test_data[i],test_data[i + 1]);
i += 2;
diff --git a/tests/slicing/oracle/loops.10.res.oracle b/tests/slicing/oracle/loops.10.res.oracle
index 7ba1874acead31fd20c084a227d3c52fa55f6fac..45eccd8972e154ec7617ee9096d5175e2fc93cac 100644
--- a/tests/slicing/oracle/loops.10.res.oracle
+++ b/tests/slicing/oracle/loops.10.res.oracle
@@ -62,12 +62,10 @@
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
-int X;
void loop_slice_1(void)
{
{
int c;
- /*@ loop pragma WIDEN_HINTS X, 10, 100; */
while (1) {
/*@ slice pragma ctrl; */ ;
c = 1;
diff --git a/tests/slicing/oracle/loops.12.res.oracle b/tests/slicing/oracle/loops.12.res.oracle
index 2c137bfaa618dedb48af0d5cfed9c4b4ba115d4e..c37d8ec3ed854e405b20549e5ffa1785801170e4 100644
--- a/tests/slicing/oracle/loops.12.res.oracle
+++ b/tests/slicing/oracle/loops.12.res.oracle
@@ -37,14 +37,12 @@
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
-int X;
int Y;
int Z;
void loop(int cond)
{
if (cond) {
int c = 0;
- /*@ loop pragma WIDEN_HINTS X, 10, 100; */
while (1) {
/*@ slice pragma ctrl; */ ;
if (c) Y = Z;
diff --git a/tests/slicing/oracle/loops.13.res.oracle b/tests/slicing/oracle/loops.13.res.oracle
index c9ea2a26e605dedf95cec73b63722fcb776d90a5..19f0f0820f6248d904aa53a0a04e82b6bada7235 100644
--- a/tests/slicing/oracle/loops.13.res.oracle
+++ b/tests/slicing/oracle/loops.13.res.oracle
@@ -37,14 +37,12 @@
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
-int X;
int Y;
int Z;
void loop(int cond)
{
if (cond) {
int c = 0;
- /*@ loop pragma WIDEN_HINTS X, 10, 100; */
while (1) {
/*@ slice pragma ctrl; */ ;
if (c) Y = Z;
diff --git a/tests/slicing/oracle/loops.21.res.oracle b/tests/slicing/oracle/loops.21.res.oracle
index 8636ad07b17046ce79ca5ca1ab0eb519c01bf81c..060ea45f1d6604803fb3050b1fa840d9ee578064 100644
--- a/tests/slicing/oracle/loops.21.res.oracle
+++ b/tests/slicing/oracle/loops.21.res.oracle
@@ -72,7 +72,6 @@ void loop_slice_1(void)
{
{
int c = 0;
- /*@ loop pragma WIDEN_HINTS X, 10, 100; */
while (1) {
/*@ slice pragma ctrl; */ ;
if (c) Y = Z;
diff --git a/tests/slicing/oracle/loops.22.res.oracle b/tests/slicing/oracle/loops.22.res.oracle
index 3313fbc32d943908d3b6701ed97fdd379ff18096..9b53131b45d7694bd90cdce58f315e9bba6405cb 100644
--- a/tests/slicing/oracle/loops.22.res.oracle
+++ b/tests/slicing/oracle/loops.22.res.oracle
@@ -72,7 +72,6 @@ void loop_slice_1(void)
{
{
int c = 0;
- /*@ loop pragma WIDEN_HINTS X, 10, 100; */
while (1) {
/*@ slice pragma ctrl; */ ;
if (c) Y = Z;
diff --git a/tests/slicing/oracle/loops.9.res.oracle b/tests/slicing/oracle/loops.9.res.oracle
index a2caa35921cfccd62af77a1b13f943464086f2cd..b5fcf07545c01ddca66358df26b66993a5833357 100644
--- a/tests/slicing/oracle/loops.9.res.oracle
+++ b/tests/slicing/oracle/loops.9.res.oracle
@@ -62,10 +62,8 @@
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
-int X;
void loop_slice_1(void)
{
- /*@ loop pragma WIDEN_HINTS X, 10, 100; */
while (1)
/*@ slice pragma ctrl; */ ;
return;
diff --git a/tests/test/adpcm.c b/tests/test/adpcm.c
index 8fa00fc7aef5f28aa567dede0c341b635f7b14d6..0c8d7e005050cd9ac08c833ebc83666d3bebd5fb 100644
--- a/tests/test/adpcm.c
+++ b/tests/test/adpcm.c
@@ -603,7 +603,7 @@ int compressed[10]={0};
void main () //(int test_data[10], int compressed[10])
{
int i;
- /*@ loop pragma UNROLL 11; loop pragma WIDEN_HINTS 32767; */ /* Better bounds: loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */
+ /*@ loop pragma UNROLL 11; loop widen_hints "all", 32767; */ /* Better bounds: loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */
for(i = 0 ; i < 10 ; i += 2)
compressed[i/2] = encode(test_data[i],test_data[i+1]);
diff --git a/tests/value/loop_wvar.i b/tests/value/loop_wvar.i
index 892c3948c3b14d244e7ff27e122adeb37a1ed8ad..2e15f918229a722cfc1e1e4b950f24e001241964 100644
--- a/tests/value/loop_wvar.i
+++ b/tests/value/loop_wvar.i
@@ -9,9 +9,6 @@
void main(void)
{ int n = 13;
int i,j;
-// ceci était une annotation, mais on ne fait pas moins bien sans
-// maintenant:
-// loop pragma WIDEN_VARIABLES i;
/*@ loop widen_hints i, 12, 13; */
for (i=0; i<n; i++)
{
@@ -35,7 +32,6 @@ void main_err1(void)
void main_err2(void)
{ int n = 13;
int i,j;
- /*@ loop pragma WIDEN_VARIABLES 12; */
for (i=0; i<n; i++)
{
j = 4 * i + 7;
@@ -48,7 +44,7 @@ void main_unhelpful () {
int next = 0;
int i;
-/*@ loop widen_hints next, 24; */ // This pragma is unhelpful, but used to interfere with the bound for i.
+/*@ loop widen_hints next, 24; */ // This hint is unhelpful, but used to interfere with the bound for i.
for (i=0;i<30;i++) {
int vsize = max;
int vnext = next;
diff --git a/tests/value/oracle/loop_wvar.0.res.oracle b/tests/value/oracle/loop_wvar.0.res.oracle
index 26226e60686687c151d18c486b3720d62240eb42..e68a02c1d640c38b4a50754cf740d29700306e64 100644
--- a/tests/value/oracle/loop_wvar.0.res.oracle
+++ b/tests/value/oracle/loop_wvar.0.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:16: starting to merge loop iterations
+[eva] loop_wvar.i:13: starting to merge loop iterations
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -13,14 +13,12 @@
i ∈ [13..2147483647]
j ∈ [7..55],3%4 or UNINITIALIZED
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:16: starting to merge loop iterations
+[eva] loop_wvar.i:13: starting to merge loop iterations
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/loop_wvar.1.res.oracle b/tests/value/oracle/loop_wvar.1.res.oracle
index 2746763959e4c6a93f4fa969b654d2f6782347fb..edafe26a894ece635030e2ddc5c581b4b1e5f0b7 100644
--- a/tests/value/oracle/loop_wvar.1.res.oracle
+++ b/tests/value/oracle/loop_wvar.1.res.oracle
@@ -1,29 +1,27 @@
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main3
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] computing for function main_unhelpful <- main3.
- Called from loop_wvar.i:84.
-[eva] loop_wvar.i:52: starting to merge loop iterations
-[eva:alarm] loop_wvar.i:57: Warning:
+ Called from loop_wvar.i:80.
+[eva] loop_wvar.i:48: starting to merge loop iterations
+[eva:alarm] loop_wvar.i:53: Warning:
signed overflow. assert next + 1 ≤ 2147483647;
[eva] Recording results for main_unhelpful
[eva] Done for function main_unhelpful
[eva] computing for function main_multiple_hints <- main3.
- Called from loop_wvar.i:85.
-[eva] loop_wvar.i:71: Frama_C_show_each: {0}, {0}, {0}
-[eva] loop_wvar.i:69: starting to merge loop iterations
-[eva] loop_wvar.i:71: Frama_C_show_each: {0; 1}, {0; 1}, {0; 1}
-[eva] loop_wvar.i:71: Frama_C_show_each: {0; 1; 2}, {0; 1; 2}, {0; 1; 2}
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], {0; 1; 2; 3}, {0; 1; 2; 3}
-[eva] loop_wvar.i:71:
+ Called from loop_wvar.i:81.
+[eva] loop_wvar.i:67: Frama_C_show_each: {0}, {0}, {0}
+[eva] loop_wvar.i:65: starting to merge loop iterations
+[eva] loop_wvar.i:67: Frama_C_show_each: {0; 1}, {0; 1}, {0; 1}
+[eva] loop_wvar.i:67: Frama_C_show_each: {0; 1; 2}, {0; 1; 2}, {0; 1; 2}
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], {0; 1; 2; 3}, {0; 1; 2; 3}
+[eva] loop_wvar.i:67:
Frama_C_show_each: [0..9], {0; 1; 2; 3; 4}, {0; 1; 2; 3; 4}
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
[eva] Recording results for main_multiple_hints
[eva] Done for function main_multiple_hints
[eva] Recording results for main3
diff --git a/tests/value/oracle/loop_wvar.2.res.oracle b/tests/value/oracle/loop_wvar.2.res.oracle
index 709713eeae91d6c6eb02365c88d84b047a8a76d1..082af63bc9572d3b7e369c66975f441426ae5a62 100644
--- a/tests/value/oracle/loop_wvar.2.res.oracle
+++ b/tests/value/oracle/loop_wvar.2.res.oracle
@@ -1,12 +1,10 @@
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main_err1
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:27: starting to merge loop iterations
+[eva] loop_wvar.i:24: starting to merge loop iterations
[eva] Recording results for main_err1
[eva] Done for function main_err1
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/loop_wvar.3.res.oracle b/tests/value/oracle/loop_wvar.3.res.oracle
index 6f76e0e4fa90d798cf3cdd5fc9aefadc926abda5..720baa6ea243d944f3b86c78fcb31a2d5cad0152 100644
--- a/tests/value/oracle/loop_wvar.3.res.oracle
+++ b/tests/value/oracle/loop_wvar.3.res.oracle
@@ -1,12 +1,10 @@
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main_err2
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:39: starting to merge loop iterations
+[eva] loop_wvar.i:35: starting to merge loop iterations
[eva] Recording results for main_err2
[eva] Done for function main_err2
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/loop_wvar.1.res.oracle b/tests/value/oracle_apron/loop_wvar.1.res.oracle
index cdc969cce79a93ee24afdb37631ea544a1dee65d..33e7e93d67390e20559632cbd7f5eef7ca1a562c 100644
--- a/tests/value/oracle_apron/loop_wvar.1.res.oracle
+++ b/tests/value/oracle_apron/loop_wvar.1.res.oracle
@@ -1,18 +1,18 @@
-12,13d11
-< [eva:alarm] loop_wvar.i:57: Warning:
+10,11d9
+< [eva:alarm] loop_wvar.i:53: Warning:
< signed overflow. assert next + 1 ≤ 2147483647;
-25,26c23
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+23,24c21
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
---
-> [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-35,36c32,33
+> [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..9], [0..9]
+33,34c30,31
< j ∈ [0..18]
< k ∈ [0..12]
---
> j ∈ [0..17]
> k ∈ [0..11]
-39c36
+37c34
< next ∈ [0..2147483647]
---
> next ∈ [0..25]
diff --git a/tests/value/oracle_gauges/loop_wvar.1.res.oracle b/tests/value/oracle_gauges/loop_wvar.1.res.oracle
index 7920ef36bc252e10cd5bd47384f8680831e836bf..6eddd73a4dafcd87f275613ae16dd4413139168e 100644
--- a/tests/value/oracle_gauges/loop_wvar.1.res.oracle
+++ b/tests/value/oracle_gauges/loop_wvar.1.res.oracle
@@ -1,9 +1,9 @@
-25,26c25
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+23,24c23
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
---
-> [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-35,36c34,35
+> [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..9], [0..9]
+33,34c32,33
< j ∈ [0..18]
< k ∈ [0..12]
---
diff --git a/tests/value/oracle_octagon/loop_wvar.1.res.oracle b/tests/value/oracle_octagon/loop_wvar.1.res.oracle
index e88a9b98afba1b6cc723bae582a2c626fd005f55..402004713bdf960e211f87cbb2b622b800ecd27f 100644
--- a/tests/value/oracle_octagon/loop_wvar.1.res.oracle
+++ b/tests/value/oracle_octagon/loop_wvar.1.res.oracle
@@ -1,7 +1,7 @@
-12,13d11
-< [eva:alarm] loop_wvar.i:57: Warning:
+10,11d9
+< [eva:alarm] loop_wvar.i:53: Warning:
< signed overflow. assert next + 1 ≤ 2147483647;
-39c37
+37c35
< next ∈ [0..2147483647]
---
> next ∈ [0..25]