diff --git a/Changelog b/Changelog
index b35148dd49c1d72bf82366c745ec2459f9d32dda..75135d6742111c6a105df9cb651d10830b8a3b98 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,10 @@
Open Source Release <next-release>
###############################################################################
+- Kernel [2024-05-20] New ACSL extension loop unfold (replaces loop pragma UNROLL)
+-! Kernel [2024-05-20] Removed loop pragma UNROLL annotations
+o! Kernel [2024-05-20] Renamed module Unroll_loop into Unfold_loop
+
###############################################################################
Open Source Release 29.0 (Copper)
###############################################################################
diff --git a/bin/frama-c.debug b/bin/frama-c.debug
index 85747b96322ba453933b52fd7ac21d673061600c..0532109e44e79fb53c3b1e91939f7f6e024a3610 100755
--- a/bin/frama-c.debug
+++ b/bin/frama-c.debug
@@ -124,7 +124,6 @@ install_printer Cil_types_debug.pp_predicate
install_printer Cil_types_debug.pp_spec
install_printer Cil_types_debug.pp_acsl_extension
install_printer Cil_types_debug.pp_acsl_extension_kind
-install_printer Cil_types_debug.pp_loop_pragma
install_printer Cil_types_debug.pp_slice_pragma
install_printer Cil_types_debug.pp_impact_pragma
install_printer Cil_types_debug.pp_pragma
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 13521e3d5c25894cc60705fc550480620d063806..6950bc6fcbeba901e0a58fa3ad1aa52e91eec6d7 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -3784,8 +3784,11 @@ especially for nested loops. This may cause the analyzer to use more time and
memory.
It is possible to control syntactic unrolling for each loop in the analyzed code
-with the annotation \lstinline|//@loop pragma UNROLL n;|, placed before the loop.
-
+with the annotation \lstinline|//@loop unfold n;|, placed before the loop.
+You may also specify \lstinline|//@loop unfold "completely", n;| for a loop
+that shall be completely unrolled after $n$ steps. Although, consider that
+a loop that executes $n$ times before exiting will need $n+1$ unrolling steps,
+since the $n+1$ iteration need to be executed for terminating the loop.
\subsection{Widening hints and loop invariants}
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 96e49b547fa49983f7a3ddcd8e79a0cd10c8af5b..b2868d04b708fb8cd4ad4436f4ac9390f64af6f2 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -9,6 +9,11 @@ release. First we list changes of the last release.
\begin{itemize}
\item \textbf{Normalizing the Source Code:} document the possibility of
undefining builtin macros from the chosen \texttt{-machdep}.
+\item \textbf{Preparing the Sources:} loop pragmas are removed and replaced
+ by dedicated ACSL extension.
+ Use \verb+loop unfold+ in place of \verb+loop pragma UNROLL+.
+\item \textbf{Preparing the Sources:} add subsection on standard library about
+ portability considerations.
\end{itemize}
\section*{27.0 (Cobalt)}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 2acb9ad8ac4854369ae8127e59da1288d1523b95..2fb46c266137876d0d077ddf8f48286aba43cfee 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -304,26 +304,37 @@ underscores as prefix and suffix, \texttt{-UMACRO} will also undefine
\texttt{do ... while(0)}. This option is set by default.
\item \texttt{\optiondef{-}{ulevel} <n>} unrolls all loops n times. This is a
- purely syntactic operation. Loops can be unrolled individually, by
- inserting the \pragmadef{UNROLL} pragma just before the loop statement. Do
+ purely syntactic operation. Loops can be unfolded individually, by
+ inserting a \verb+loop unfold+ annotation just before the loop statement. Do
not confuse this option with plug-in-specific options that may also be called
- ``unrolling''~\cite{value}. Below is a typical example of use.
+ ``unrolling''~\cite{value}\footnote{
+ Historically, \textit{syntactic} loop unrolling was denoted by
+ \texttt{loop pragma UNROLL} annotations. Later on, \textsf{EVA} introduced
+ \textit{semantic} unrolling with \texttt{loop unroll} annotations.
+ Loop pragams was removed for Frama-C 29 (Copper) and it was
+ decided to introduce \texttt{loop unfold} annotations for \textit{syntactic}
+ unrolling and to reserve \texttt{loop unroll} annotations for \textit{semantic}
+ loop unrolling with \textsf{EVA}.
+ }. Below is a typical example of use:
\begin{ccode}
-/*@ loop pragma UNROLL 10; */
+/*@ loop unfold 10; */
for(i = 0; i < 9; i++) ...
\end{ccode}
-The transformation introduces an \pragmadef{UNROLL} pragma indicating that the unrolling process has been done:
+The transformation introduces an additional \verb+loop unfold+ annotation
+indicating that the unrolling process has been done:
\begin{ccode}
... // loop unrolled 10 times
-/*@ loop pragma UNROLL 10;
- loop pragma UNROLL "done", 10; */
+/*@ loop unfold 10;
+ loop unfold "done", 10; */
... // remaining loop
\end{ccode}
-That allows to disable unrolling transformation on such a loop when reusing \FramaC with a code obtained by a previous use of \FramaC tool.
-To ignore this disabling \pragmadef{UNROLL} pragma and force unrolling, the option \texttt{\optiondef{-}{ulevel-force}} has to be set.
+That allows to disable unrolling transformation on such a loop when reusing
+\FramaC with a code obtained by a previous use of \FramaC tool.
+To ignore this disabling \verb+loop unfold "done"+ and force unrolling,
+the option \texttt{\optiondef{-}{ulevel-force}} has to be set.
Passing a negative argument to \texttt{-ulevel} will disable unrolling, even
-in case of \texttt{UNROLL} pragma.
+in case of \verb+loop unfold+ annotations.
\end{description}
\section{Normalizing Contracts}\label{sec:normalize-contracts}
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index b9db2837074872f10b9edb2270edda1428f82ffe..7ef5a8430092b4ac0b9655693b1130ca260513a3 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -210,7 +210,6 @@ function filterKind(
case 'behavior': return filter('kind.behavior');
case 'reachable': return filter('kind.reachable');
case 'axiomatic': return filter('kind.axiomatic');
- case 'loop_pragma': return filter('kind.pragma');
case 'assumes': return filter('kind.assumes');
default: return filter('kind.others');
}
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 98eb7d5f505ebc7b9cdc5672f0d26fc10e591803..b793a002f499dcc035e0388103b471c23b88d6fa 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -447,11 +447,11 @@ the analysis is launched).
: syntactically unroll loops *n* times before the analysis. This can be quite
costly and some plugins (e.g. Eva) provide more efficient ways to perform the
same thing. See their respective manuals for more information. This can also be
-activated on a per-loop basis via the **loop pragma unroll <m>** directive.
+activated on a per-loop basis via the **loop unfold <m>** directive.
A negative value for *n* will inhibit such pragmas.
[-no]-ulevel-force
-: ignores **UNROLL** loop pragmas disabling unrolling.
+: ignores **loop unfold "done"** disabling syntactic loop unrolling.
[-no]-unicode
outputs ACSL formulas with UTF-8 characters. This is the default.
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index e43950a38e011a015cd04f8aff8500238c33b9d5..79d29dce4a3ee1387a36b0a55fe3cf9af7f7a028 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1402,8 +1402,6 @@ loop_annot_stack:
check_empty
(pos,"loop annotations can have at most one variant.") v ;
(i,fa,a,b,AVariant loop_variant::v,p,e) }
-| loop_pragma loop_annot_opt
- { let (i,fa,a,b,v,p,e) = $2 in (i,fa,a,b,v,APragma (Loop_pragma $1)::p,e) }
| loop_grammar_extension loop_annot_opt {
let (i,fa,a,b,v,p,e) = $2 in
(i,fa,a,b,v,p, $1::e)
@@ -1458,15 +1456,6 @@ loop_grammar_extension:
}
;
-loop_pragma:
-| LOOP PRAGMA any_identifier ne_lexpr_list SEMICOLON
- { if $3 = "UNROLL_LOOP" || $3 = "UNROLL" then
- (if $3 <> "UNROLL" then
- Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
- Unroll_specs $4)
- else raise (Not_well_formed (loc $sloc,"Unknown loop pragma")) }
-;
-
/*** code annotations ***/
beg_pragma_or_code_annotation:
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
similarity index 92%
rename from src/kernel_internals/typing/unroll_loops.ml
rename to src/kernel_internals/typing/unfold_loops.ml
index d2fc8966ec940080f8ef0e55afefdde3bb45a465..60d3ede0535983b5f740fc36331e4e246e1e16f6 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Syntactic loop unrolling. *)
+(** Syntactic loop unfolding. *)
open Cil_types
open Cil
@@ -41,7 +41,7 @@ let update_info global_find_init emitter info spec =
| {term_type=typ} when Logic_typing.is_integral_type typ ->
if Option.is_some info.unroll_number && not info.ignore_unroll then begin
Kernel.warning ~once:true ~current:true
- "ignoring unrolling directive (directive already defined)";
+ "ignoring unfolding directive (directive already defined)";
info
end else begin
try
@@ -54,37 +54,36 @@ let update_info global_find_init emitter info spec =
| Some _ as unroll_number -> { info with unroll_number }
| None ->
Kernel.warning ~once:true ~current:true
- "ignoring unrolling directive (not an understood constant \
+ "ignoring unfolding directive (not an understood constant \
expression)";
info
end
with Invalid_argument s ->
Kernel.warning ~once:true ~current:true
- "ignoring unrolling directive (%s)" s;
+ "ignoring unfolding directive (%s)" s;
info
end
| {term_node=TConst (LStr "done") } -> { info with ignore_unroll = true }
| {term_node=TConst (LStr "completely") } ->
if Option.is_some info.total_unroll then begin
Kernel.warning ~once:true ~current:true
- "found two total unroll pragmas";
+ "found two complete unfolding annotations";
info
end else { info with total_unroll = Some emitter }
| _ ->
Kernel.warning ~once:true ~current:true
- "ignoring invalid unrolling directive";
+ "ignoring invalid unfolding directive";
info
-let extract_from_pragmas global_find_init s =
- let filter _ a = Logic_utils.is_loop_pragma a in
- let pragmas = Annotations.code_annot_emitter ~filter s in
- let get_infos info (a,e) =
- match a.annot_content with
- | APragma (Loop_pragma (Unroll_specs specs)) ->
- List.fold_left (update_info global_find_init e) info specs
- | _ -> assert false (* should have been filtered above. *)
- in
- List.fold_left get_infos empty_info pragmas
+let extract_unroll_spec global_find_init s =
+ let infos = ref empty_info in
+ Annotations.iter_code_annot (fun e (ca: code_annotation) ->
+ match ca.annot_content with
+ | AExtended (_,_, { ext_name = "unfold" ; ext_kind = Ext_terms args }) ->
+ infos := List.fold_left (update_info global_find_init e) !infos args
+ | _ -> ()
+ ) s ;
+ !infos
let fresh_label =
let counter = ref (-1) in
@@ -95,7 +94,7 @@ let fresh_label =
| Some loc -> loc, true
and new_label_name =
let prefix = match label_name with None -> "" | Some s -> s ^ "_"
- in Format.sprintf "%sunrolling_%d_loop" prefix (- !counter)
+ in Format.sprintf "%sunfolding_%d_loop" prefix (- !counter)
in Label (new_label_name,
loc,
orig)
@@ -111,7 +110,7 @@ let copy_var =
decr counter;
fun vi ->
let vi' = Cil_const.copy_with_new_vid vi in
- let name = vi.vname ^ "_unroll_" ^ (string_of_int (- !counter)) in
+ let name = vi.vname ^ "_unfold_" ^ (string_of_int (- !counter)) in
Cil_const.change_varinfo_name vi' name;
vi'
@@ -190,7 +189,7 @@ let copy_annotations kf assoc labelled_stmt_tbl (break_continue_must_change, stm
with Not_found -> SkipChildren
| Invalid_argument _ ->
Kernel.abort
- "Loop unrolling: cannot find new representative for \
+ "Loop unfolding: cannot find new representative for \
local var %s"
vi.vname
end
@@ -603,14 +602,14 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
s
in
ChangeDoChildrenPost (s, update)
- | Loop _ ->
- let infos = extract_from_pragmas global_find_init s in
+ | Loop(_,_,loc,_,_) ->
+ let infos = extract_unroll_spec global_find_init s in
let number = Option.value ~default:times infos.unroll_number in
let total_unrolling = infos.total_unroll in
let is_ignored_unrolling = not force && infos.ignore_unroll in
let f sloop =
Kernel.debug ~dkey
- "Unrolling loop stmt %d (%d times) inside function %a@."
+ "unfolding loop stmt %d (%d times) inside function %a@."
sloop.sid number Kernel_function.pretty (Option.get self#current_kf);
file_has_unrolled_loop <- true ;
has_unrolled_loop <- true ;
@@ -692,13 +691,12 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
new_stmts
in
let h sloop new_stmts = (* To indicate that the unrolling has been done *)
- let specs = Unroll_specs [(Logic_const.term (TConst (LStr "done"))
- (Ctype Cil.charPtrType)) ;
- Logic_const.tinteger number
- ] in
- let annot =
- Logic_const.new_code_annotation (APragma (Loop_pragma specs))
- in
+ let kind = Ext_terms [
+ (Logic_const.term (TConst (LStr "done")) (Ctype Cil.charPtrType)) ;
+ Logic_const.tinteger number
+ ] in
+ let ext = Logic_const.new_acsl_extension "unfold" loc false kind in
+ let annot =Logic_const.new_code_annotation (AExtended([],true,ext)) in
Annotations.add_code_annot
Emitter.end_user ~kf:(Option.get self#current_kf) sloop annot;
new_stmts
@@ -722,39 +720,42 @@ end
(* Performs unrolling transformation without using -ulevel option.
Do not forget to apply [transformations_closure] afterwards. *)
let apply_transformation ?(force=true) nb file =
- (* [nb] default number of unrolling used when there is no UNROLL loop pragma.
- When [nb] is negative, no unrolling is done; all UNROLL loop pragmas
- are ignored. *)
+ (* [nb] default number of unrolling used when there is no loop unfold.
+ When [nb] is negative, no unrolling is done and all loop unfold
+ specifications are ignored. *)
if nb >= 0 then
let global_find_init vi =
try (Globals.Vars.find vi).init with Not_found -> None
in
let visitor = new do_it global_find_init (force, nb) in
- Kernel.debug ~dkey "Using -ulevel %d option and UNROLL loop pragmas@." nb;
+ Kernel.debug ~dkey "Using -ulevel %d option and loop unfold annotations@." nb;
visitFramacFileFunctions (visitor:>Visitor.frama_c_visitor) file;
if !ast_has_changed then Ast.mark_as_changed ()
else begin
Kernel.debug ~dkey
- "No unrolling is done; all UNROLL loop pragmas are ignored@."
+ "No unfolding is done; all loop unfold annotations are ignored@."
end
(* Performs and closes all syntactic transformations *)
let compute file =
- let nb = Kernel.UnrollingLevel.get () in
- let force = Kernel.UnrollingForce.get () in
+ let nb = Kernel.UnfoldingLevel.get () in
+ let force = Kernel.UnfoldingForce.get () in
apply_transformation ~force nb file
-let unroll_transform =
- File.register_code_transformation_category "loop unrolling"
+let transform =
+ File.register_code_transformation_category "loop unfolding"
let () =
File.add_code_transformation_after_cleanup
- ~deps:[(module Kernel.UnrollingLevel:Parameter_sig.S);
- (module Kernel.UnrollingForce:Parameter_sig.S)]
- unroll_transform compute
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
+ ~deps:[(module Kernel.UnfoldingLevel:Parameter_sig.S);
+ (module Kernel.UnfoldingForce:Parameter_sig.S)]
+ transform compute
+
+let unroll_typer (ctxt: Logic_typing.typing_context) (_loc:location) args =
+ let open Logic_typing in
+ let env =
+ Lenv.empty () |> append_here_label |> append_init_label |> append_pre_label
+ in Ext_terms (List.map (ctxt.type_term ctxt env) args)
+
+let () = Acsl_extension.register_code_annot_next_loop
+ ~plugin:"kernel" "unfold" unroll_typer false
diff --git a/src/kernel_internals/typing/unroll_loops.mli b/src/kernel_internals/typing/unfold_loops.mli
similarity index 92%
rename from src/kernel_internals/typing/unroll_loops.mli
rename to src/kernel_internals/typing/unfold_loops.mli
index 2f2c4a12fe61c76b562303f37a7f0dad1ea60d0d..a078e24300671da75cbb351bc43ae7fe759b6102 100644
--- a/src/kernel_internals/typing/unroll_loops.mli
+++ b/src/kernel_internals/typing/unfold_loops.mli
@@ -20,14 +20,14 @@
(* *)
(**************************************************************************)
-(** Syntactic loop unrolling.
+(** Syntactic loop unfolding.
Uses code transformation hook mechanism (after-cleanup phase)
of {!File} and exports nothing.
- Name of the transformation is "loop unrolling"
+ Name of the transformation is "loop unfolding"
*)
-val unroll_transform: File.code_transformation_category
+val transform: File.code_transformation_category
(*
Local Variables:
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 7d2e37eb6a89711bf080916dce98f4576070ab52..d416534d0ac42e7254ced76c440c4a2831b0e976 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -478,15 +478,6 @@ 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)) ->
- (* to select the declaration of the variables *)
- List.fold_left
- (fun results term -> {
- results with
- locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
- labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
- })
- results terms
| AAllocation (_,FreeAllocAny) -> results
| AAllocation (_,FreeAlloc(f,a)) ->
let get_zone results x =
@@ -509,6 +500,24 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
results l
| AStmtSpec _ -> (* TODO *)
raise (NYI "[logic_interp] statement contract")
+ | AExtended(_,_, { ext_kind = Ext_preds preds }) ->
+ (* to select the declaration of the variables *)
+ List.fold_left
+ (fun results pred -> {
+ results with
+ locals = Varinfo.Set.union (extract_locals_from_pred pred) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_pred pred) results.labels
+ })
+ results preds
+ | AExtended(_,_, { ext_kind = Ext_terms terms }) ->
+ (* to select the declaration of the variables *)
+ List.fold_left
+ (fun results term -> {
+ results with
+ locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
+ })
+ results terms
| AExtended _ -> raise (NYI "[logic_interp] extension")
(* Used by annotations entry points. *)
@@ -571,7 +580,7 @@ let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop
| AInvariant(_,false,_) -> others
| AAllocation _ -> others
| AAssigns _ -> others
- | APragma (Loop_pragma _)| APragma (Impact_pragma _) -> others
+ | APragma (Impact_pragma _) -> others
| AStmtSpec _ | AExtended _ (* TODO *) -> false
diff --git a/src/kernel_services/ast_data/ast.ml b/src/kernel_services/ast_data/ast.ml
index 0efd2a914145390064e50e7cec3d46b5cf62188d..5dbe5309e22766f5b5793b08ac3550a6761d88c8 100644
--- a/src/kernel_services/ast_data/ast.ml
+++ b/src/kernel_services/ast_data/ast.ml
@@ -38,7 +38,7 @@ include
Kernel.ReadAnnot.self;
Kernel.PreprocessAnnot.self;
Kernel.Files.self;
- Kernel.UnrollingLevel.self;
+ Kernel.UnfoldingLevel.self;
Kernel.Keep_unused_specified_functions.self;
Kernel.Keep_unused_types.self;
Cil.selfFormalsDecl ]
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index d1e72d54804411130ebad1ba9dd186f7b1bd39e9..aa3daab36e81dd122dbacefe4d25bf289e79b2a0 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1736,10 +1736,6 @@ and behavior = {
(** extensions *)
}
-(** Pragmas for the value analysis plugin of Frama-C. *)
-and loop_pragma =
- | Unroll_specs of term list
-
(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
| SPexpr of term
@@ -1753,7 +1749,6 @@ and impact_pragma =
(** The various kinds of pragmas. *)
and pragma =
- | Loop_pragma of loop_pragma
| Slice_pragma of slice_pragma
| Impact_pragma of impact_pragma
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 73feb757fad83a86ba8aaf052d28225b1a093f7d..0f1baeb7c2027fd32ee8f90aeb75ee9cc6f9145f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3179,11 +3179,6 @@ class cil_printer () = object (self)
(pp_list nl_complete self#complete_behaviors) complete
(pp_list false self#disjoint_behaviors) disjoint
- method private loop_pragma fmt = function
- | Unroll_specs terms ->
- fprintf fmt "UNROLL @[%a@]"
- (Pretty_utils.pp_list ~sep:",@ " self#term) terms
-
method private slice_pragma fmt = function
|SPexpr t -> fprintf fmt "expr @[%a@]" self#term t
| SPctrl -> Format.pp_print_string fmt "ctrl"
@@ -3217,10 +3212,6 @@ class cil_printer () = object (self)
fprintf fmt "@[%a@ %a;@]"
self#pp_acsl_keyword "impact pragma"
self#impact_pragma sp
- | APragma (Loop_pragma lp) ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword "loop pragma"
- self#loop_pragma lp
| AStmtSpec(for_bhv, spec) ->
fprintf fmt "@[<hv 2>%a%a@]"
pp_for_behavs for_bhv
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 92ec1921e219757f0eae6fc7b24594b85612de7a..05b20100bcd7fc590286082dd44ea4601035536d 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -929,10 +929,6 @@ and pp_termination_kind fmt = function
| Continues -> Format.fprintf fmt "Continues"
| Returns -> Format.fprintf fmt "Returns"
-and pp_loop_pragma fmt = function
- | Unroll_specs(term_list) ->
- Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
-
and pp_slice_pragma fmt = function
| SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
| SPctrl -> Format.fprintf fmt "SPctrl"
@@ -943,8 +939,6 @@ and pp_impact_pragma fmt = function
| IPstmt -> Format.fprintf fmt "IPstmt"
and pp_pragma fmt = function
- | Loop_pragma(term) ->
- Format.fprintf fmt "Loop_pragma(%a)" pp_loop_pragma term
| Slice_pragma(term) ->
Format.fprintf fmt "Slice_pragma(%a)" pp_slice_pragma term
| Impact_pragma(term) ->
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index f66f816f039c891ac5eda79c7e8d93add21cf401..7998dfb1d740497012a2c0be2ec4583b55d22937 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -140,8 +140,6 @@ val pp_acsl_extension_kind :
val pp_behavior : Format.formatter -> Cil_types.behavior -> unit
val pp_termination_kind :
Format.formatter -> Cil_types.termination_kind -> unit
-val pp_loop_pragma :
- Format.formatter -> Cil_types.loop_pragma -> unit
val pp_slice_pragma :
Format.formatter -> Cil_types.slice_pragma -> unit
val pp_impact_pragma :
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 08e3e2304e8f89474d0a39796130eff3f9b5e4a2..8eb0730f39d8f72b13c4bec441b2b97e141ab92c 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -450,10 +450,6 @@ let print_spec fmt spec =
~sep:"@\n" ~suf:"@\n" (pp_list ~sep:",@ " pp_print_string))
spec.spec_disjoint_behaviors
-let print_loop_pragma fmt p =
- match p with
- Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
-
let print_slice_pragma fmt p =
match p with
| SPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
@@ -467,7 +463,6 @@ let print_impact_pragma fmt p =
let print_pragma fmt p =
match p with
- Loop_pragma p -> fprintf fmt "loop@ pragma@ %a;" print_loop_pragma p
| Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
| Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 1c6eb15b7f70e459f651ddd8b7a710665142a40c..af74c4dd1fe05e464c10874b8088be4c8f54379a 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -713,10 +713,6 @@ and is_same_behavior b b' env =
and is_same_variant (v,m) (v',m') env =
is_same_term v v' env && is_same_opt is_matching_logic_info m m' env
-and is_same_loop_pragma p p' env =
- match p, p' with
- | 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
| SPexpr t, SPexpr t' -> is_same_term t t' env
@@ -732,10 +728,9 @@ and is_same_impact_pragma p p' env =
and is_same_pragma p p' env =
match p,p' with
- | Loop_pragma p, Loop_pragma p' -> is_same_loop_pragma p p' env
| Slice_pragma p, Slice_pragma p' -> is_same_slice_pragma p p' env
| Impact_pragma p, Impact_pragma p' -> is_same_impact_pragma p p' env
- | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
+ | (Slice_pragma _ | Impact_pragma _), _ -> false
and are_same_behaviors bhvs bhvs' env =
let treat_one_behavior acc b =
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 24d8d26e36fc42e6af21e74e0925beaf910a755c..2de503910f92d466c89b6d93f5c578c886090c12 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1017,8 +1017,6 @@ class type cilVisitor = object
method vallocation:
allocation -> allocation visitAction
- method vloop_pragma: loop_pragma -> loop_pragma visitAction
-
method vslice_pragma: slice_pragma -> slice_pragma visitAction
method vimpact_pragma: impact_pragma -> impact_pragma visitAction
@@ -1154,8 +1152,6 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor =
method vallocates _s = DoChildren
method vallocation _s = DoChildren
- method vloop_pragma _ = DoChildren
-
method vslice_pragma _ = DoChildren
method vimpact_pragma _ = DoChildren
@@ -2042,15 +2038,6 @@ and childrenImpactPragma vis p = match p with
| IPexpr t -> let t' = visitCilTerm vis t in if t' != t then IPexpr t' else p
| IPstmt -> p
-and visitCilLoopPragma vis p =
- doVisitCil vis
- id vis#vloop_pragma childrenLoopPragma p
-
-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
-
and childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
let base_type = visitCilType vis m.mi_base_type in
@@ -2169,9 +2156,6 @@ and childrenCodeAnnot vis ca =
| APragma (Slice_pragma t) ->
let t' = visitCilSlicePragma vis t in
if t' != t then change_content (APragma (Slice_pragma t')) else ca
- | APragma (Loop_pragma p) ->
- let p' = visitCilLoopPragma vis p in
- if p' != p then change_content (APragma (Loop_pragma p')) else ca
| AStmtSpec (behav,s) ->
let s' = vSpec s in
if s' != s then change_content (AStmtSpec (behav,s')) else ca
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 83a9b53210a943b23d890b72c2337b6548c27b8b..f39332dfbd8e58788cd8cf63424d606c16af3296 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2016,7 +2016,6 @@ class type cilVisitor = object
method vallocation: allocation -> allocation visitAction
(** @since Oxygen-20120901 *)
- method vloop_pragma: loop_pragma -> loop_pragma visitAction
method vslice_pragma: slice_pragma -> slice_pragma visitAction
method vimpact_pragma: impact_pragma -> impact_pragma visitAction
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 4d5cb71767ffa074a887700058a67cb373c06134..cb18e76893f995df9046975c33132ff4f1b9ca18 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3632,10 +3632,6 @@ struct
let plain_logic_type loc env t = logic_type (base_ctxt env) loc env t
- let loop_pragma env p =
- match p with
- | Unroll_specs l -> Cil_types.Unroll_specs (List.map (term env) l)
-
let model_annot loc ti =
let env = Lenv.empty() in
let model_for_type =
@@ -3870,9 +3866,6 @@ struct
| APragma (Slice_pragma sp) ->
Cil_types.APragma
(Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
- | APragma (Loop_pragma lp) ->
- Cil_types.APragma
- (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
| AStmtSpec (behav,s) ->
(* function behaviors and statement behaviors are not at the
same level. Do not mix them in a complete or disjoint clause
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index b8d91ce7909940a74860ace725f43a4a1ea41a10..7d43c5cb2aac0210cf28e992340746724eb7d86b 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -731,7 +731,7 @@ let is_annot_next_stmt c =
| AAssigns _ | AAllocation _
| APragma (Slice_pragma (SPctrl | SPexpr _))
| APragma (Impact_pragma (IPexpr _))
- | APragma (Loop_pragma _) -> false
+ -> false
let rec add_attribute_glob_annot a g =
match g with
@@ -1176,10 +1176,6 @@ let is_same_logic_type_info t1 t2 =
is_same_attributes t1.lt_attr t2.lt_attr &&
is_same_opt is_same_logic_type_def t1.lt_def t2.lt_def
-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
-
let is_same_slice_pragma p1 p2 =
match p1,p2 with
SPexpr t1, SPexpr t2 -> is_same_term t1 t2
@@ -1194,10 +1190,9 @@ let is_same_impact_pragma p1 p2 =
let is_same_pragma p1 p2 =
match p1,p2 with
- | Loop_pragma p1, Loop_pragma p2 -> is_same_loop_pragma p1 p2
| Slice_pragma p1, Slice_pragma p2 -> is_same_slice_pragma p1 p2
| Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
- | (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
+ | (Slice_pragma _ | Impact_pragma _), _ -> false
let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
@@ -2275,9 +2270,6 @@ let is_assigns ca =
let is_pragma ca =
match ca.annot_content with APragma _ -> true | _ -> false
-let is_loop_pragma ca =
- match ca.annot_content with APragma (Loop_pragma _) -> true | _ -> false
-
let is_slice_pragma ca =
match ca.annot_content with APragma (Slice_pragma _) -> true | _ -> false
@@ -2289,7 +2281,7 @@ let is_loop_extension ca =
let is_loop_annot s =
is_loop_invariant s || is_assigns s || is_allocation s ||
- is_variant s || is_loop_pragma s || is_loop_extension s
+ is_variant s || is_loop_extension s
let is_trivial_annotation a =
match a.annot_content with
@@ -2299,18 +2291,11 @@ let is_trivial_annotation a =
-> false
let is_property_pragma = function
- | 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,
update the pragma-related code in gui/property_navigator.ml *)
-
-let extract_loop_pragma l =
- List.fold_right
- (fun ca l -> match ca.annot_content with
- APragma (Loop_pragma lp) -> lp::l | _ -> l) l []
-
let extract_contract l =
List.fold_right
(fun ca l -> match ca.annot_content with
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 74ab761d28372d23cb414e0b897e165ace809c6e..62ace3c9ccfc6dec17e9c6f08ae0ae48a63a2e8f 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -373,7 +373,6 @@ val is_same_logic_type_def :
logic_type_def -> logic_type_def -> bool
val is_same_logic_type_info :
logic_type_info -> logic_type_info -> bool
-val is_same_loop_pragma : loop_pragma -> loop_pragma -> bool
val is_same_slice_pragma : slice_pragma -> slice_pragma -> bool
val is_same_impact_pragma : impact_pragma -> impact_pragma -> bool
val is_same_pragma : pragma -> pragma -> bool
@@ -460,7 +459,6 @@ val is_variant : code_annotation -> bool
val is_allocation: code_annotation -> bool
val is_assigns : code_annotation -> bool
val is_pragma : code_annotation -> bool
-val is_loop_pragma : code_annotation -> bool
val is_slice_pragma : code_annotation -> bool
val is_impact_pragma : code_annotation -> bool
val is_loop_annot : code_annotation -> bool
@@ -470,8 +468,6 @@ val is_trivial_annotation : code_annotation -> bool
val is_property_pragma : pragma -> bool
(** Should this pragma be proved by plugins *)
-val extract_loop_pragma :
- code_annotation list -> loop_pragma list
val extract_contract :
code_annotation list -> (string list * funspec) list
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 21e1f8edd631971ae9a3b60a82ae9cd7b5971bc4..aeb6da19615b9c4372765f8f6c82c4f47339f420 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -321,10 +321,6 @@ type spec = {
(** Pragmas for the value analysis plugin of Frama-C. *)
-type loop_pragma =
- | Unroll_specs of lexpr list
-
-(** Pragmas for the slicing plugin of Frama-C. *)
and slice_pragma =
| SPexpr of lexpr
| SPctrl
@@ -337,7 +333,6 @@ and impact_pragma =
(** The various kinds of pragmas. *)
and pragma =
- | Loop_pragma of loop_pragma
| Slice_pragma of slice_pragma
| Impact_pragma of impact_pragma
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index a347a92f2d5350e0d7906a5edf2c1f0e0937e627..73cf18ce7ce6c6d819a0edfd36438dda468d6fee 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1268,26 +1268,26 @@ module JsonCompilationDatabase =
let normalisation = add_group "Customizing Normalization"
let () = Parameter_customize.set_group normalisation
-module UnrollingLevel =
+module UnfoldingLevel =
Zero
(struct
- let module_name = "UnrollingLevel"
+ let module_name = "UnfoldingLevel"
let option_name = "-ulevel"
let arg_name = "l"
let help =
- "unroll loops n times (defaults to 0) before analyzes. \
- A negative value hides UNROLL loop pragmas."
+ "unfold loops n times (defaults to 0) before analyzes. \
+ A negative value hides loop unfold annotations."
end)
let () = Parameter_customize.set_group normalisation
-module UnrollingForce =
+module UnfoldingForce =
Bool
(struct
- let module_name = "UnrollingForce"
+ let module_name = "UnfoldingForce"
let default = false
let option_name = "-ulevel-force"
let help =
- "ignore UNROLL loop pragmas disabling unrolling."
+ "ignore loop unfold \"done\" specifications (force unfolding)."
end)
let () = Parameter_customize.set_group normalisation
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 8d4f1b47e79dd226d3e29c18508bedf45e474369..2e8856d2e52a1be2828459e7d8946faeacd7d2f3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -438,10 +438,10 @@ module Set_project_as_default: Parameter_sig.Bool
(** {2 Customizing Normalization and parsing} *)
(* ************************************************************************* *)
-module UnrollingLevel: Parameter_sig.Int
+module UnfoldingLevel: Parameter_sig.Int
(** Behavior of option "-ulevel" *)
-module UnrollingForce: Parameter_sig.Bool
+module UnfoldingForce: Parameter_sig.Bool
(** Behavior of option "-ulevel-force"
@since Neon-20140301 *)
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 5933b01e0d7115f04757693a8b9737445ca686cf..ad4dd73a4323a618db05592d560f038ce6552947 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -390,7 +390,6 @@ class full_visitor = object(self)
method! vfrees _ = Cil.DoChildren
method! vallocates _ = Cil.DoChildren
method! vallocation _ = Cil.DoChildren
- method! vloop_pragma _ = Cil.DoChildren
method! vslice_pragma _ = Cil.DoChildren
method! vimpact_pragma _ = Cil.DoChildren
method! vdeps _ = Cil.DoChildren
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index ee163be3d8bdcfd80379cab23740d51545ee704a..8d84bb2874a334504e69b69415ce4f252d27f479 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -70,7 +70,7 @@ struct
let t_loop_assigns = t_loop "assigns"
let t_loop_variant = t_loop "variant"
let t_loop_allocates = t_loop "allocates"
- let t_loop_pragma = t_loop "pragma"
+ let t_pragma = t_loop "pragma"
let t_reachable = t_kind "reachable" "Reachable statement"
let t_code_contract = t_kind "code_contract" "Statement contract"
@@ -119,7 +119,7 @@ struct
| AVariant _ -> t_loop_variant
| AAssigns _ -> t_loop_assigns
| AAllocation _ -> t_loop_allocates
- | APragma _ -> t_loop_pragma
+ | APragma _ -> t_pragma
| AExtended(_,_,{ext_name=_}) -> t_ext
end
| IPAllocation _ -> t_allocates
diff --git a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
index 6efec9870ea80f65d22584419bd259c372760eae..ec0cd665edef6bc4a3c6c325ef178fb1f9df928d 100644
--- a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
@@ -7,12 +7,12 @@
out of bounds read. assert \valid_read((int *)*list);
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow.
- assert -2147483648 ≤ ret + tmp_unroll_5;
- (tmp_unroll_5 from vararg)
+ assert -2147483648 ≤ ret + tmp_unfold_5;
+ (tmp_unfold_5 from vararg)
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow.
- assert ret + tmp_unroll_5 ≤ 2147483647;
- (tmp_unroll_5 from vararg)
+ assert ret + tmp_unfold_5 ≤ 2147483647;
+ (tmp_unfold_5 from vararg)
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
out of bounds read. assert \valid_read(list);
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
@@ -43,20 +43,20 @@ int sum(int n, void * const *__va_params)
int ret = 0;
list = __va_params;
i = 0;
- if (! (i < n)) goto unrolling_2_loop;
+ if (! (i < n)) goto unfolding_2_loop;
{
- int tmp_unroll_5;
+ int tmp_unfold_5;
/*@ assert Eva: mem_access: \valid_read(list); */
/*@ assert Eva: mem_access: \valid_read((int *)*list); */
- tmp_unroll_5 = *((int *)*list);
+ tmp_unfold_5 = *((int *)*list);
list ++;
- /*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unroll_5; */
- /*@ assert Eva: signed_overflow: ret + tmp_unroll_5 ≤ 2147483647; */
- ret += tmp_unroll_5;
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unfold_5; */
+ /*@ assert Eva: signed_overflow: ret + tmp_unfold_5 ≤ 2147483647; */
+ ret += tmp_unfold_5;
}
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL "done", 1; */
+ unfolding_3_loop: ;
+ /*@ loop unfold "done", 1; */
while (i < n) {
{
int tmp;
@@ -70,7 +70,7 @@ int sum(int n, void * const *__va_params)
}
i ++;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return ret;
}
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 5bb7e1aedb8d6ff21d28bf35c1dbf7e8184a75ad..ef3514c844b85d222bb7e2cb5142a3b9dca67e02 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -649,7 +649,6 @@ let cfun_code env kf = (* Visits term/pred of code annotations and C exp *)
method !vpredicate p = do_pred p ; Cil.SkipChildren
method !vterm t = do_term t ; Cil.SkipChildren
(* speed up: skip non interesting subtrees *)
- method! vloop_pragma _ = Cil.SkipChildren (* no need *)
method! vvdec _ = Cil.SkipChildren (* done via stmt *)
method! vexpr _ = Cil.SkipChildren (* done via stmt *)
method! vlval _ = Cil.SkipChildren (* done via stmt *)
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
index adf1cd46980a48d06b602788891e478a86547cc9..d268d14ff6ed86c8c252cab81a59d2809a2e783a 100644
--- a/src/plugins/wp/RegionAccess.ml
+++ b/src/plugins/wp/RegionAccess.ml
@@ -392,7 +392,6 @@ class visitor map =
(* vpredicate and vterm are called from vcode_annot *)
(* speed up: skip non interesting subtrees *)
- method! vloop_pragma _ = Cil.SkipChildren (* no need *)
method! vvdec _ = Cil.SkipChildren (* done via stmt *)
method! vexpr _ = Cil.SkipChildren (* done via stmt *)
method! vlval _ = Cil.SkipChildren (* done via stmt *)
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_unroll.i b/src/plugins/wp/tests/wp_plugin/doomed_unroll.i
index dd025d4817a97adde1279711cbce88670b0e1f58..bfcaec734b26c6420e7a17b56fbf50a7bad36a1c 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/doomed_unroll.i
@@ -10,7 +10,7 @@ void foo(void)
{
int n = 3 ;
/*@
- loop pragma UNROLL "completely", 4 ;
+ loop unfold "completely", 4 ;
*/
while (n>0) n--;
}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
index 43b1f1173ae426387f7cac5252f94d1e3e2a3dc3..116eea855dee981d0162fc96b0eed3fac3e6f375 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
@@ -45,24 +45,24 @@ Prove: true.
void foo(void)
{
int n = 3;
- if (! (n > 0)) goto unrolling_2_loop;
+ if (! (n > 0)) goto unfolding_2_loop;
n --;
- unrolling_6_loop: ;
- if (! (n > 0)) goto unrolling_2_loop;
+ unfolding_6_loop: ;
+ if (! (n > 0)) goto unfolding_2_loop;
n --;
- unrolling_5_loop: ;
- if (! (n > 0)) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! (n > 0)) goto unfolding_2_loop;
n --;
- unrolling_4_loop: ;
- if (! (n > 0)) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! (n > 0)) goto unfolding_2_loop;
n --;
- unrolling_3_loop: ;
+ unfolding_3_loop: ;
/*@ loop invariant \false;
- loop pragma UNROLL "completely", 4;
- loop pragma UNROLL "done", 4;
+ loop unfold "completely", 4;
+ loop unfold "done", 4;
*/
while (n > 0) n --;
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return;
}
diff --git a/src/plugins/wp/tests/wp_plugin/repeat.c b/src/plugins/wp/tests/wp_plugin/repeat.c
index a060cc7c0ab55e49e68776f029670c66126ca8a7..cd53430a6b83885db09a8996ab2897ce01020138 100644
--- a/src/plugins/wp/tests/wp_plugin/repeat.c
+++ b/src/plugins/wp/tests/wp_plugin/repeat.c
@@ -43,7 +43,7 @@ void master(void)
*/
void unroll(void)
{
- /*@ loop pragma UNROLL "completely", U; */
+ /*@ loop unfold "completely", U; */
for (int i = 0; i < N; i++)
{ f(); g(); }
return;
@@ -57,7 +57,7 @@ void unroll(void)
*/
void induction(int n)
{
- /*@
+ /*@
loop invariant 0 <= i <= n;
loop invariant CALL == [| F , G |] *^ i;
loop assigns i,calls;
@@ -77,8 +77,8 @@ void induction(int n)
void shifted(int n)
{
f();
-
- /*@
+
+ /*@
loop invariant 0 <= i <= n;
loop invariant CALL == ([| F , G |] *^ i ^ [| F |]);
loop assigns i,calls;
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index f6feda1b587b987794cc4103c1e4e3ea853c7af4..54a94e25d7bf95a639bdea492a9113593b170982 100644
--- a/src/plugins/wp/tests/wp_plugin/unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/unroll.i
@@ -17,6 +17,6 @@ enum {Max = 16};
@ ensures zero: zeroed(t,0,Max-1);
*/
void unrolled_loop(unsigned *t){
- //@ loop pragma UNROLL "completely", Max+1;
+ //@ loop unfold "completely", Max+1;
for (unsigned i=0; i<Max; i++) t[i] = 0;
}
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 2bc3cb504a7ee920be8ddad29d379c172dbfcde0..ac962eda030ce5310ef4f0deb0fe8a4457cfaebc 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -59,11 +59,6 @@ let node () =
(* --- Unrolled Loop --- *)
(* -------------------------------------------------------------------------- *)
-let is_unrolled_completely spec =
- match spec.term_node with
- | TConst (LStr "completely") -> true
- | _ -> false
-
let rec is_predicate cond p =
match p.pred_content with
| Pfalse -> not cond
@@ -88,8 +83,6 @@ let rec is_predicate cond p =
let is_dead_annot ca =
match ca.annot_content with
- | APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
- is_unrolled_completely spec
| AAssert([],p)
| AInvariant([],_,p) ->
Logic_utils.use_predicate p.tp_kind && is_predicate false p.tp_statement
diff --git a/tests/cil/comments.c b/tests/cil/comments.c
index ed0252e15d2097202b8de8897ba5d035f0a5b774..0c0e9d3efd8115687494a5daeaa72a8febc93414 100644
--- a/tests/cil/comments.c
+++ b/tests/cil/comments.c
@@ -19,7 +19,7 @@ int bts_2176() {
1 */
r = /* comment 2 */ 1;
- //@ loop pragma UNROLL 10;
+ //@ loop unfold 10;
for(i=0; i<10; i++) {
r += 1;
}
diff --git a/tests/cil/oracle/comments.res.oracle b/tests/cil/oracle/comments.res.oracle
index fd7b14f4298869cf6f9b582765cbae96ae941a3a..479418c36083c669ce17c0711d3dbf87a31e0963 100644
--- a/tests/cil/oracle/comments.res.oracle
+++ b/tests/cil/oracle/comments.res.oracle
@@ -30,53 +30,53 @@ int bts_2176(void)
// comment 2
r = 1;
i = 0;
- if (! (i < 10)) goto unrolling_2_loop;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_12_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_12_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_11_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_11_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_10_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_10_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_9_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_9_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_8_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_8_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_7_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_7_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_6_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_6_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_5_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_4_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL 10;
- loop pragma UNROLL "done", 10; */
+ unfolding_3_loop: ;
+ /*@ loop unfold 10;
+ loop unfold "done", 10; */
while (i < 10) {
r ++;
i ++;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
// comment 3
return r;
}
diff --git a/tests/float/round10d.i b/tests/float/round10d.i
index 4dfa2710f349811eb8a9063e035a7a5041fee846..30b33d4d7f5f5a7a7b0b9f3637e6c9481f1db014 100644
--- a/tests/float/round10d.i
+++ b/tests/float/round10d.i
@@ -7,12 +7,12 @@ int main()
double t=0.0;
int i;
Frama_C_show_each_dixieme(0.1);
- //@ loop pragma UNROLL 10;
- for(i=0;i<10;i++)
- {
+ //@ loop unfold 10;
+ for(i=0;i<10;i++)
+ {
t = t + 0.1;
Frama_C_show_each_t(t);
- }
+ }
//@ assert t>=1.0;
return 0;
}
diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c
index 90bc2edd2edd91cf7500e146ca51c0e12603245a..a7083537cbc36424e79c3b63d55ddddaa65ab29e 100644
--- a/tests/idct/ieee_1180_1990.c
+++ b/tests/idct/ieee_1180_1990.c
@@ -173,7 +173,7 @@ int main()
long i, j, k, m1[8][8], m2[8][8], m3[8][8], m4[8][8], succ, omse, ome, err;
succ = 1;
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
for(i = 0; i < 6; i++)
for(j = 0; j < 8; j++)
for(k = 0; k < 8; k++)
@@ -198,7 +198,7 @@ int main()
}
/*fprintf(stderr, "------------------------------------------------->\n");*/
-/* loop pragma UNROLL 0 */
+/* loop unfold 0 */
for(i = 0; i < 10000; i++)
{
if((i + 1) % 200 == 0)
diff --git a/tests/metrics/cabs.i b/tests/metrics/cabs.i
index 0d86a7db0f7fdebb32f0b437cb5eeda624530b5b..e910d23f0dfe3852b537c10803c1ce52eb683abe 100644
--- a/tests/metrics/cabs.i
+++ b/tests/metrics/cabs.i
@@ -4,7 +4,7 @@
void main() {
int j = 1;
- //@ loop pragma UNROLL 6;
+ //@ loop unfold 6;
for (int i=0; i<6; i++) {
j += 2;
}
diff --git a/tests/misc/oracle/bts1135_ulevel.res.oracle b/tests/misc/oracle/bts1135_ulevel.res.oracle
index bb6bb5dec9af88ecf46b59b0cb968ef27a89db6e..22da8c05b0c9c9d81797a6ac1ac96773eeb594c7 100644
--- a/tests/misc/oracle/bts1135_ulevel.res.oracle
+++ b/tests/misc/oracle/bts1135_ulevel.res.oracle
@@ -4,23 +4,23 @@ int X;
void main(int c)
{
int i = 0;
- if (! (i < 10)) goto unrolling_2_loop;
+ if (! (i < 10)) goto unfolding_2_loop;
if (c)
/*@ ensures \false; */
- goto there_unrolling_6_loop;
+ goto there_unfolding_6_loop;
X ++;
- there_unrolling_6_loop: i ++;
- /*@ assert c ≡ 0 ⇒ \at(X,there_unrolling_6_loop) ≡ i + 1; */ ;
- unrolling_5_loop: ;
- if (! (i < 10)) goto unrolling_2_loop;
+ there_unfolding_6_loop: i ++;
+ /*@ assert c ≡ 0 ⇒ \at(X,there_unfolding_6_loop) ≡ i + 1; */ ;
+ unfolding_5_loop: ;
+ if (! (i < 10)) goto unfolding_2_loop;
if (c)
/*@ ensures \false; */
- goto there_unrolling_4_loop;
+ goto there_unfolding_4_loop;
X ++;
- there_unrolling_4_loop: i ++;
- /*@ assert c ≡ 0 ⇒ \at(X,there_unrolling_4_loop) ≡ i + 1; */ ;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL "done", 2; */
+ there_unfolding_4_loop: i ++;
+ /*@ assert c ≡ 0 ⇒ \at(X,there_unfolding_4_loop) ≡ i + 1; */ ;
+ unfolding_3_loop: ;
+ /*@ loop unfold "done", 2; */
while (i < 10) {
if (c)
/*@ ensures \false; */
@@ -29,7 +29,7 @@ void main(int c)
there: i ++;
/*@ assert c ≡ 0 ⇒ \at(X,there) ≡ i + 1; */ ;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return;
}
diff --git a/tests/misc/ulevel.i b/tests/misc/ulevel.i
index dbfc67d7c9082ea9ccc854eab15ae0d2e7743a6e..d18729eb2637afa1611d8b065d735d6a746497d3 100644
--- a/tests/misc/ulevel.i
+++ b/tests/misc/ulevel.i
@@ -8,7 +8,7 @@
void main(void) {
int i, j;
- /*@ loop pragma UNROLL 1; */
+ /*@ loop unfold 1; */
for(i = 0; i < 4; i++)
for(j = 0; j < 3; j++)
;
diff --git a/tests/slicing/oracle/adpcm.res.oracle b/tests/slicing/oracle/adpcm.res.oracle
index d064224755afa3c264138d1ff4795db2f1dc9feb..496702e3225a91eec1fefa182c52b11213beb6cf 100644
--- a/tests/slicing/oracle/adpcm.res.oracle
+++ b/tests/slicing/oracle/adpcm.res.oracle
@@ -1531,7 +1531,6 @@ 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 */
@@ -1822,7 +1821,7 @@ void encode_slice_1(int xin1, int xin2)
h_ptr ++;
xb = (long)*tmp_1 * (long)*tmp_2;
i = 0;
- /*@ loop pragma UNROLL 11; */
+ /*@ loop unfold 11; */
while (i < 10) {
{
int *tmp_3;
@@ -1851,7 +1850,7 @@ void encode_slice_1(int xin1, int xin2)
xb += (long)*tqmf_ptr * (long)*tmp_9;
tqmf_ptr1 = tqmf_ptr - 2;
i = 0;
- /*@ loop pragma UNROLL 23; */
+ /*@ loop unfold 23; */
while (i < 22) {
int *tmp_10;
int *tmp_11;
@@ -1921,7 +1920,7 @@ int filtez_slice_1(int *bpl, int *dlt_0)
dlt_0 ++;
zl = (long)*tmp * (long)*tmp_0;
i = 1;
- /*@ loop pragma UNROLL 7; */
+ /*@ loop unfold 7; */
while (i < 6) {
int *tmp_1;
int *tmp_2;
@@ -1958,7 +1957,7 @@ int quantl_slice_1(int el_0, int detl_0)
wd = (long)abs_slice_1(el_0);
mil = 0;
decis = (long)decis_levl[mil] * (long)detl_0 >> 15L;
- /*@ loop pragma UNROLL 30; */
+ /*@ loop unfold 30; */
while (1) {
if (wd <= decis) {
if (! (mil < 29)) break;
@@ -2001,7 +2000,7 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
int wd3;
if (dlt_0 == 0) {
i = 0;
- /*@ loop pragma UNROLL 7; */
+ /*@ loop unfold 7; */
while (i < 6) {
*(bli + i) = (int)(255L * (long)*(bli + i) >> 8L);
i ++;
@@ -2009,7 +2008,7 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
}
else {
i = 0;
- /*@ loop pragma UNROLL 7; */
+ /*@ loop unfold 7; */
while (i < 6) {
if ((long)dlt_0 * (long)*(dlti + i) >= (long)0) wd2 = 128;
else wd2 = -128;
@@ -2071,7 +2070,8 @@ void main(void)
{
int i;
i = 0;
- /*@ loop pragma UNROLL 11; */
+ /*@ loop unfold 11;
+ loop \eva::widen_hints "all", 32767; */
while (i < 10) {
encode_slice_1(test_data[i],test_data[i + 1]);
i += 2;
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 9fd462bcb24a07984cbe4e86e1297a9fd5df86cd..5b0f79536b0e31e7e140417b4a7f0d9fc16631d2 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -226,7 +226,7 @@ void main(void)
lecture_slice_1();
fsm_transition_slice_1();
step ++;
- /*@ loop pragma UNROLL "done", 10; */
+ /*@ loop unfold "done", 10; */
while (1) {
lecture_slice_1();
fsm_transition_slice_1();
diff --git a/tests/spec/breaks_continues_unroll.i b/tests/spec/breaks_continues_unroll.i
index fed8f02091708994c1d2897d15f0ed8264547130..e5f7bf977dfc3bdb42c074ed39fc9a176c846c5b 100644
--- a/tests/spec/breaks_continues_unroll.i
+++ b/tests/spec/breaks_continues_unroll.i
@@ -3,13 +3,13 @@
// Semantics of unrolling
int unroll (int c) {
int x = 0;
- //@ loop pragma UNROLL 1;
+ //@ loop unfold 1;
while (1) {
/*@ breaks \false;
continues x == \old(x) + 1; */
switch (x) {
/*@ breaks x == 13; */
- {
+ {
case 11: x++; continue;
case 12: x++;
case 13: break;
@@ -24,4 +24,4 @@ int unroll (int c) {
}
}
return x;
-}
+}
diff --git a/tests/spec/loop_labels_unroll.i b/tests/spec/loop_labels_unroll.i
index cec4e93183fa944c5ac2ff6e2c929177fb1d8287..30df6b4f1be74c2a71f2213239cddb26ad91dca5 100644
--- a/tests/spec/loop_labels_unroll.i
+++ b/tests/spec/loop_labels_unroll.i
@@ -2,8 +2,8 @@ int main () {
int x = 0;
- /*@
- loop pragma UNROLL 4;
+ /*@
+ loop unfold 4;
loop invariant \at(x,LoopEntry) == 0;
loop invariant \at(x,LoopCurrent) <= 15;
*/
diff --git a/tests/spec/oracle/breaks_continues_unroll.res.oracle b/tests/spec/oracle/breaks_continues_unroll.res.oracle
index 245cc34841f9d3bcf3bad7daa9ca820a8614bd41..cdb607de3549603aab89e51163d10e4093c7bb8a 100644
--- a/tests/spec/oracle/breaks_continues_unroll.res.oracle
+++ b/tests/spec/oracle/breaks_continues_unroll.res.oracle
@@ -7,7 +7,7 @@ int unroll(int c)
/*@ breaks x ≡ 13; */
{
case 11: x ++;
- goto unrolling_3_loop;
+ goto unfolding_3_loop;
case 12: x ++;
case 13: break;
default: ;
@@ -15,12 +15,12 @@ int unroll(int c)
}
if (x < c) {
x ++;
- goto unrolling_3_loop;
+ goto unfolding_3_loop;
}
- goto unrolling_2_loop;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL 1;
- loop pragma UNROLL "done", 1; */
+ goto unfolding_2_loop;
+ unfolding_3_loop: ;
+ /*@ loop unfold 1;
+ loop unfold "done", 1; */
while (1) {
/*@ breaks \false;
continues x ≡ \old(x) + 1; */
@@ -44,7 +44,7 @@ int unroll(int c)
break;
}
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return x;
}
diff --git a/tests/spec/oracle/loop_labels_unroll.res.oracle b/tests/spec/oracle/loop_labels_unroll.res.oracle
index 84a3ca289907e1062d26b481dbadf834211b3eec..998a9bb7d2336ed96da0c577700868acad763250 100644
--- a/tests/spec/oracle/loop_labels_unroll.res.oracle
+++ b/tests/spec/oracle/loop_labels_unroll.res.oracle
@@ -4,63 +4,63 @@ int main(void)
{
int __retres;
int x = 0;
- unrolling_7_loop: ;
- if (! (x < 15)) goto unrolling_2_loop;
+ unfolding_7_loop: ;
+ if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
- /*@ assert x ≡ \at(x,unrolling_7_loop) + 1; */ ;
- int i_unroll_32 = 0;
- /*@ loop invariant \at(i_unroll_32,LoopEntry) ≡ 0; */
- while (i_unroll_32 < 4) {
- i_unroll_32 ++;
- /*@ assert \at(i_unroll_32,LoopCurrent) ≡ i_unroll_32 - 1; */ ;
+ /*@ assert x ≡ \at(x,unfolding_7_loop) + 1; */ ;
+ int i_unfold_32 = 0;
+ /*@ loop invariant \at(i_unfold_32,LoopEntry) ≡ 0; */
+ while (i_unfold_32 < 4) {
+ i_unfold_32 ++;
+ /*@ assert \at(i_unfold_32,LoopCurrent) ≡ i_unfold_32 - 1; */ ;
}
- /*@ assert i_unroll_32 > 0; */ ;
+ /*@ assert i_unfold_32 > 0; */ ;
}
- unrolling_6_loop: ;
- if (! (x < 15)) goto unrolling_2_loop;
+ unfolding_6_loop: ;
+ if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
- /*@ assert x ≡ \at(x,unrolling_6_loop) + 1; */ ;
- int i_unroll_24 = 0;
- /*@ loop invariant \at(i_unroll_24,LoopEntry) ≡ 0; */
- while (i_unroll_24 < 4) {
- i_unroll_24 ++;
- /*@ assert \at(i_unroll_24,LoopCurrent) ≡ i_unroll_24 - 1; */ ;
+ /*@ assert x ≡ \at(x,unfolding_6_loop) + 1; */ ;
+ int i_unfold_24 = 0;
+ /*@ loop invariant \at(i_unfold_24,LoopEntry) ≡ 0; */
+ while (i_unfold_24 < 4) {
+ i_unfold_24 ++;
+ /*@ assert \at(i_unfold_24,LoopCurrent) ≡ i_unfold_24 - 1; */ ;
}
- /*@ assert i_unroll_24 > 0; */ ;
+ /*@ assert i_unfold_24 > 0; */ ;
}
- unrolling_5_loop: ;
- if (! (x < 15)) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
- /*@ assert x ≡ \at(x,unrolling_5_loop) + 1; */ ;
- int i_unroll_16 = 0;
- /*@ loop invariant \at(i_unroll_16,LoopEntry) ≡ 0; */
- while (i_unroll_16 < 4) {
- i_unroll_16 ++;
- /*@ assert \at(i_unroll_16,LoopCurrent) ≡ i_unroll_16 - 1; */ ;
+ /*@ assert x ≡ \at(x,unfolding_5_loop) + 1; */ ;
+ int i_unfold_16 = 0;
+ /*@ loop invariant \at(i_unfold_16,LoopEntry) ≡ 0; */
+ while (i_unfold_16 < 4) {
+ i_unfold_16 ++;
+ /*@ assert \at(i_unfold_16,LoopCurrent) ≡ i_unfold_16 - 1; */ ;
}
- /*@ assert i_unroll_16 > 0; */ ;
+ /*@ assert i_unfold_16 > 0; */ ;
}
- unrolling_4_loop: ;
- if (! (x < 15)) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
- /*@ assert x ≡ \at(x,unrolling_4_loop) + 1; */ ;
- int i_unroll_8 = 0;
- /*@ loop invariant \at(i_unroll_8,LoopEntry) ≡ 0; */
- while (i_unroll_8 < 4) {
- i_unroll_8 ++;
- /*@ assert \at(i_unroll_8,LoopCurrent) ≡ i_unroll_8 - 1; */ ;
+ /*@ assert x ≡ \at(x,unfolding_4_loop) + 1; */ ;
+ int i_unfold_8 = 0;
+ /*@ loop invariant \at(i_unfold_8,LoopEntry) ≡ 0; */
+ while (i_unfold_8 < 4) {
+ i_unfold_8 ++;
+ /*@ assert \at(i_unfold_8,LoopCurrent) ≡ i_unfold_8 - 1; */ ;
}
- /*@ assert i_unroll_8 > 0; */ ;
+ /*@ assert i_unfold_8 > 0; */ ;
}
- unrolling_3_loop: ;
+ unfolding_3_loop: ;
/*@ loop invariant \at(x,LoopEntry) ≡ 0;
loop invariant \at(x,LoopCurrent) ≤ 15;
- loop pragma UNROLL 4;
- loop pragma UNROLL "done", 4;
+ loop unfold 4;
+ loop unfold "done", 4;
*/
while (x < 15) {
x ++;
@@ -73,7 +73,7 @@ int main(void)
}
/*@ assert i > 0; */ ;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
__retres = 0;
return __retres;
}
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
index b621427cab8dac8e73a195e76afd3ecc0c369df9..9e7552621ea4658d179135a9ccc80236d75d9088 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
@@ -174,61 +174,61 @@ void main(void)
tmp_0 = gen_nondet(68);
if (tmp_0) goto L1;
{
- int tmp_1_unroll_41;
- case 1: tmp_1_unroll_41 = gen_nondet(71);
- if (tmp_1_unroll_41) goto L1_unrolling_11_loop;
- L_unrolling_8_loop: x = y;
+ int tmp_1_unfold_41;
+ case 1: tmp_1_unfold_41 = gen_nondet(71);
+ if (tmp_1_unfold_41) goto L1_unfolding_11_loop;
+ L_unfolding_8_loop: x = y;
case 2:
{
- int j_unroll_40;
- int i_unroll_40 = 0;
- if (! (i_unroll_40 < 4)) goto unrolling_2_loop_unrolling_12_loop;
+ int j_unfold_40;
+ int i_unfold_40 = 0;
+ if (! (i_unfold_40 < 4)) goto unfolding_2_loop_unfolding_12_loop;
{
- int tmp_2_unroll_12_unroll_26;
- int tmp_3_unroll_12_unroll_26;
- int tmp_4_unroll_12_unroll_26;
- int tmp_5_unroll_12_unroll_26;
- L1_unrolling_4_loop_unrolling_9_loop: j_unroll_40 = gen_nondet(76);
- tmp_2_unroll_12_unroll_26 = gen_nondet(77);
- if (tmp_2_unroll_12_unroll_26 > 10) i_unroll_40 = 10;
- else i_unroll_40 = 0;
- Frama_C_show_each_i_(i_unroll_40);
- tmp_3_unroll_12_unroll_26 = gen_nondet(79);
- if (tmp_3_unroll_12_unroll_26) goto L_unrolling_8_loop;
- tmp_4_unroll_12_unroll_26 = gen_nondet(80);
- if (tmp_4_unroll_12_unroll_26) goto L0;
- tmp_5_unroll_12_unroll_26 = gen_nondet(81);
- if (tmp_5_unroll_12_unroll_26) goto L3;
+ int tmp_2_unfold_12_unfold_26;
+ int tmp_3_unfold_12_unfold_26;
+ int tmp_4_unfold_12_unfold_26;
+ int tmp_5_unfold_12_unfold_26;
+ L1_unfolding_4_loop_unfolding_9_loop: j_unfold_40 = gen_nondet(76);
+ tmp_2_unfold_12_unfold_26 = gen_nondet(77);
+ if (tmp_2_unfold_12_unfold_26 > 10) i_unfold_40 = 10;
+ else i_unfold_40 = 0;
+ Frama_C_show_each_i_(i_unfold_40);
+ tmp_3_unfold_12_unfold_26 = gen_nondet(79);
+ if (tmp_3_unfold_12_unfold_26) goto L_unfolding_8_loop;
+ tmp_4_unfold_12_unfold_26 = gen_nondet(80);
+ if (tmp_4_unfold_12_unfold_26) goto L0;
+ tmp_5_unfold_12_unfold_26 = gen_nondet(81);
+ if (tmp_5_unfold_12_unfold_26) goto L3;
}
- i_unroll_40 ++;
- unrolling_3_loop_unrolling_10_loop: ;
- /*@ loop pragma UNROLL "done", 1; */
- while (i_unroll_40 < 4) {
+ i_unfold_40 ++;
+ unfolding_3_loop_unfolding_10_loop: ;
+ /*@ loop unfold "done", 1; */
+ while (i_unfold_40 < 4) {
{
- int tmp_2_unroll_37;
- int tmp_3_unroll_37;
- int tmp_4_unroll_37;
- int tmp_5_unroll_37;
- L1_unrolling_11_loop: j_unroll_40 = gen_nondet(76);
- tmp_2_unroll_37 = gen_nondet(77);
- if (tmp_2_unroll_37 > 10) i_unroll_40 = 10; else i_unroll_40 = 0;
- Frama_C_show_each_i_(i_unroll_40);
- tmp_3_unroll_37 = gen_nondet(79);
- if (tmp_3_unroll_37) goto L_unrolling_8_loop;
- tmp_4_unroll_37 = gen_nondet(80);
- if (tmp_4_unroll_37) goto L0;
- tmp_5_unroll_37 = gen_nondet(81);
- if (tmp_5_unroll_37) goto L3;
+ int tmp_2_unfold_37;
+ int tmp_3_unfold_37;
+ int tmp_4_unfold_37;
+ int tmp_5_unfold_37;
+ L1_unfolding_11_loop: j_unfold_40 = gen_nondet(76);
+ tmp_2_unfold_37 = gen_nondet(77);
+ if (tmp_2_unfold_37 > 10) i_unfold_40 = 10; else i_unfold_40 = 0;
+ Frama_C_show_each_i_(i_unfold_40);
+ tmp_3_unfold_37 = gen_nondet(79);
+ if (tmp_3_unfold_37) goto L_unfolding_8_loop;
+ tmp_4_unfold_37 = gen_nondet(80);
+ if (tmp_4_unfold_37) goto L0;
+ tmp_5_unfold_37 = gen_nondet(81);
+ if (tmp_5_unfold_37) goto L3;
}
- i_unroll_40 ++;
+ i_unfold_40 ++;
}
- unrolling_2_loop_unrolling_12_loop: ;
+ unfolding_2_loop_unfolding_12_loop: ;
}
}
n --;
- if (! (n > 0)) goto unrolling_6_loop;
- unrolling_7_loop: ;
- /*@ loop pragma UNROLL "done", 1; */
+ if (! (n > 0)) goto unfolding_6_loop;
+ unfolding_7_loop: ;
+ /*@ loop unfold "done", 1; */
while (1) {
{
int tmp_1;
@@ -238,26 +238,26 @@ void main(void)
{
int j;
int i = 0;
- if (! (i < 4)) goto unrolling_2_loop;
+ if (! (i < 4)) goto unfolding_2_loop;
{
- int tmp_2_unroll_12;
- int tmp_3_unroll_12;
- int tmp_4_unroll_12;
- int tmp_5_unroll_12;
- L1_unrolling_4_loop: j = gen_nondet(76);
- tmp_2_unroll_12 = gen_nondet(77);
- if (tmp_2_unroll_12 > 10) i = 10; else i = 0;
+ int tmp_2_unfold_12;
+ int tmp_3_unfold_12;
+ int tmp_4_unfold_12;
+ int tmp_5_unfold_12;
+ L1_unfolding_4_loop: j = gen_nondet(76);
+ tmp_2_unfold_12 = gen_nondet(77);
+ if (tmp_2_unfold_12 > 10) i = 10; else i = 0;
Frama_C_show_each_i_(i);
- tmp_3_unroll_12 = gen_nondet(79);
- if (tmp_3_unroll_12) goto L;
- tmp_4_unroll_12 = gen_nondet(80);
- if (tmp_4_unroll_12) goto L0;
- tmp_5_unroll_12 = gen_nondet(81);
- if (tmp_5_unroll_12) goto L3;
+ tmp_3_unfold_12 = gen_nondet(79);
+ if (tmp_3_unfold_12) goto L;
+ tmp_4_unfold_12 = gen_nondet(80);
+ if (tmp_4_unfold_12) goto L0;
+ tmp_5_unfold_12 = gen_nondet(81);
+ if (tmp_5_unfold_12) goto L3;
}
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL "done", 1; */
+ unfolding_3_loop: ;
+ /*@ loop unfold "done", 1; */
while (i < 4) {
{
int tmp_2;
@@ -277,13 +277,13 @@ void main(void)
}
i ++;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
}
}
n --;
if (! (n > 0)) break;
}
- unrolling_6_loop: ;
+ unfolding_6_loop: ;
Frama_C_show_each_y_(y);
Frama_C_show_each_x_(x);
}
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
index 85a47d4d093e1f69a954b43b88513bd9b84e05c6..d19de9df259672fab55369c3409b3c4ac24876ff 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
@@ -174,160 +174,160 @@ void main(void)
tmp_0 = gen_nondet(68);
if (tmp_0) goto L1;
{
- int tmp_1_unroll_106;
- case 1: tmp_1_unroll_106 = gen_nondet(71);
- if (tmp_1_unroll_106) goto L1_unrolling_23_loop;
- L_unrolling_18_loop: x = y;
+ int tmp_1_unfold_106;
+ case 1: tmp_1_unfold_106 = gen_nondet(71);
+ if (tmp_1_unfold_106) goto L1_unfolding_23_loop;
+ L_unfolding_18_loop: x = y;
case 2:
{
- int j_unroll_105;
- int i_unroll_105 = 0;
- if (! (i_unroll_105 < 4)) goto unrolling_2_loop_unrolling_24_loop;
+ int j_unfold_105;
+ int i_unfold_105 = 0;
+ if (! (i_unfold_105 < 4)) goto unfolding_2_loop_unfolding_24_loop;
{
- int tmp_2_unroll_24_unroll_80;
- int tmp_3_unroll_24_unroll_80;
- int tmp_4_unroll_24_unroll_80;
- int tmp_5_unroll_24_unroll_80;
- L1_unrolling_6_loop_unrolling_19_loop:
- j_unroll_105 = gen_nondet(76);
- tmp_2_unroll_24_unroll_80 = gen_nondet(77);
- if (tmp_2_unroll_24_unroll_80 > 10) i_unroll_105 = 10;
- else i_unroll_105 = 0;
- Frama_C_show_each_i_(i_unroll_105);
- tmp_3_unroll_24_unroll_80 = gen_nondet(79);
- if (tmp_3_unroll_24_unroll_80) goto L_unrolling_18_loop;
- tmp_4_unroll_24_unroll_80 = gen_nondet(80);
- if (tmp_4_unroll_24_unroll_80) goto L0;
- tmp_5_unroll_24_unroll_80 = gen_nondet(81);
- if (tmp_5_unroll_24_unroll_80) goto L3;
+ int tmp_2_unfold_24_unfold_80;
+ int tmp_3_unfold_24_unfold_80;
+ int tmp_4_unfold_24_unfold_80;
+ int tmp_5_unfold_24_unfold_80;
+ L1_unfolding_6_loop_unfolding_19_loop:
+ j_unfold_105 = gen_nondet(76);
+ tmp_2_unfold_24_unfold_80 = gen_nondet(77);
+ if (tmp_2_unfold_24_unfold_80 > 10) i_unfold_105 = 10;
+ else i_unfold_105 = 0;
+ Frama_C_show_each_i_(i_unfold_105);
+ tmp_3_unfold_24_unfold_80 = gen_nondet(79);
+ if (tmp_3_unfold_24_unfold_80) goto L_unfolding_18_loop;
+ tmp_4_unfold_24_unfold_80 = gen_nondet(80);
+ if (tmp_4_unfold_24_unfold_80) goto L0;
+ tmp_5_unfold_24_unfold_80 = gen_nondet(81);
+ if (tmp_5_unfold_24_unfold_80) goto L3;
}
- i_unroll_105 ++;
- unrolling_5_loop_unrolling_20_loop: ;
- if (! (i_unroll_105 < 4)) goto unrolling_2_loop_unrolling_24_loop;
+ i_unfold_105 ++;
+ unfolding_5_loop_unfolding_20_loop: ;
+ if (! (i_unfold_105 < 4)) goto unfolding_2_loop_unfolding_24_loop;
{
- int tmp_2_unroll_12_unroll_91;
- int tmp_3_unroll_12_unroll_91;
- int tmp_4_unroll_12_unroll_91;
- int tmp_5_unroll_12_unroll_91;
- L1_unrolling_4_loop_unrolling_21_loop:
- j_unroll_105 = gen_nondet(76);
- tmp_2_unroll_12_unroll_91 = gen_nondet(77);
- if (tmp_2_unroll_12_unroll_91 > 10) i_unroll_105 = 10;
- else i_unroll_105 = 0;
- Frama_C_show_each_i_(i_unroll_105);
- tmp_3_unroll_12_unroll_91 = gen_nondet(79);
- if (tmp_3_unroll_12_unroll_91) goto L_unrolling_18_loop;
- tmp_4_unroll_12_unroll_91 = gen_nondet(80);
- if (tmp_4_unroll_12_unroll_91) goto L0;
- tmp_5_unroll_12_unroll_91 = gen_nondet(81);
- if (tmp_5_unroll_12_unroll_91) goto L3;
+ int tmp_2_unfold_12_unfold_91;
+ int tmp_3_unfold_12_unfold_91;
+ int tmp_4_unfold_12_unfold_91;
+ int tmp_5_unfold_12_unfold_91;
+ L1_unfolding_4_loop_unfolding_21_loop:
+ j_unfold_105 = gen_nondet(76);
+ tmp_2_unfold_12_unfold_91 = gen_nondet(77);
+ if (tmp_2_unfold_12_unfold_91 > 10) i_unfold_105 = 10;
+ else i_unfold_105 = 0;
+ Frama_C_show_each_i_(i_unfold_105);
+ tmp_3_unfold_12_unfold_91 = gen_nondet(79);
+ if (tmp_3_unfold_12_unfold_91) goto L_unfolding_18_loop;
+ tmp_4_unfold_12_unfold_91 = gen_nondet(80);
+ if (tmp_4_unfold_12_unfold_91) goto L0;
+ tmp_5_unfold_12_unfold_91 = gen_nondet(81);
+ if (tmp_5_unfold_12_unfold_91) goto L3;
}
- i_unroll_105 ++;
- unrolling_3_loop_unrolling_22_loop: ;
- /*@ loop pragma UNROLL "done", 2; */
- while (i_unroll_105 < 4) {
+ i_unfold_105 ++;
+ unfolding_3_loop_unfolding_22_loop: ;
+ /*@ loop unfold "done", 2; */
+ while (i_unfold_105 < 4) {
{
- int tmp_2_unroll_102;
- int tmp_3_unroll_102;
- int tmp_4_unroll_102;
- int tmp_5_unroll_102;
- L1_unrolling_23_loop: j_unroll_105 = gen_nondet(76);
- tmp_2_unroll_102 = gen_nondet(77);
- if (tmp_2_unroll_102 > 10) i_unroll_105 = 10;
- else i_unroll_105 = 0;
- Frama_C_show_each_i_(i_unroll_105);
- tmp_3_unroll_102 = gen_nondet(79);
- if (tmp_3_unroll_102) goto L_unrolling_18_loop;
- tmp_4_unroll_102 = gen_nondet(80);
- if (tmp_4_unroll_102) goto L0;
- tmp_5_unroll_102 = gen_nondet(81);
- if (tmp_5_unroll_102) goto L3;
+ int tmp_2_unfold_102;
+ int tmp_3_unfold_102;
+ int tmp_4_unfold_102;
+ int tmp_5_unfold_102;
+ L1_unfolding_23_loop: j_unfold_105 = gen_nondet(76);
+ tmp_2_unfold_102 = gen_nondet(77);
+ if (tmp_2_unfold_102 > 10) i_unfold_105 = 10;
+ else i_unfold_105 = 0;
+ Frama_C_show_each_i_(i_unfold_105);
+ tmp_3_unfold_102 = gen_nondet(79);
+ if (tmp_3_unfold_102) goto L_unfolding_18_loop;
+ tmp_4_unfold_102 = gen_nondet(80);
+ if (tmp_4_unfold_102) goto L0;
+ tmp_5_unfold_102 = gen_nondet(81);
+ if (tmp_5_unfold_102) goto L3;
}
- i_unroll_105 ++;
+ i_unfold_105 ++;
}
- unrolling_2_loop_unrolling_24_loop: ;
+ unfolding_2_loop_unfolding_24_loop: ;
}
}
n --;
- if (! (n > 0)) goto unrolling_8_loop;
- unrolling_17_loop: ;
+ if (! (n > 0)) goto unfolding_8_loop;
+ unfolding_17_loop: ;
{
- int tmp_1_unroll_64;
- tmp_1_unroll_64 = gen_nondet(71);
- if (tmp_1_unroll_64) goto L1_unrolling_15_loop;
- L_unrolling_10_loop: x = y;
+ int tmp_1_unfold_64;
+ tmp_1_unfold_64 = gen_nondet(71);
+ if (tmp_1_unfold_64) goto L1_unfolding_15_loop;
+ L_unfolding_10_loop: x = y;
{
- int j_unroll_63;
- int i_unroll_63 = 0;
- if (! (i_unroll_63 < 4)) goto unrolling_2_loop_unrolling_16_loop;
+ int j_unfold_63;
+ int i_unfold_63 = 0;
+ if (! (i_unfold_63 < 4)) goto unfolding_2_loop_unfolding_16_loop;
{
- int tmp_2_unroll_24_unroll_38;
- int tmp_3_unroll_24_unroll_38;
- int tmp_4_unroll_24_unroll_38;
- int tmp_5_unroll_24_unroll_38;
- L1_unrolling_6_loop_unrolling_11_loop:
- j_unroll_63 = gen_nondet(76);
- tmp_2_unroll_24_unroll_38 = gen_nondet(77);
- if (tmp_2_unroll_24_unroll_38 > 10) i_unroll_63 = 10;
- else i_unroll_63 = 0;
- Frama_C_show_each_i_(i_unroll_63);
- tmp_3_unroll_24_unroll_38 = gen_nondet(79);
- if (tmp_3_unroll_24_unroll_38) goto L_unrolling_10_loop;
- tmp_4_unroll_24_unroll_38 = gen_nondet(80);
- if (tmp_4_unroll_24_unroll_38) goto L0;
- tmp_5_unroll_24_unroll_38 = gen_nondet(81);
- if (tmp_5_unroll_24_unroll_38) goto L3;
+ int tmp_2_unfold_24_unfold_38;
+ int tmp_3_unfold_24_unfold_38;
+ int tmp_4_unfold_24_unfold_38;
+ int tmp_5_unfold_24_unfold_38;
+ L1_unfolding_6_loop_unfolding_11_loop:
+ j_unfold_63 = gen_nondet(76);
+ tmp_2_unfold_24_unfold_38 = gen_nondet(77);
+ if (tmp_2_unfold_24_unfold_38 > 10) i_unfold_63 = 10;
+ else i_unfold_63 = 0;
+ Frama_C_show_each_i_(i_unfold_63);
+ tmp_3_unfold_24_unfold_38 = gen_nondet(79);
+ if (tmp_3_unfold_24_unfold_38) goto L_unfolding_10_loop;
+ tmp_4_unfold_24_unfold_38 = gen_nondet(80);
+ if (tmp_4_unfold_24_unfold_38) goto L0;
+ tmp_5_unfold_24_unfold_38 = gen_nondet(81);
+ if (tmp_5_unfold_24_unfold_38) goto L3;
}
- i_unroll_63 ++;
- unrolling_5_loop_unrolling_12_loop: ;
- if (! (i_unroll_63 < 4)) goto unrolling_2_loop_unrolling_16_loop;
+ i_unfold_63 ++;
+ unfolding_5_loop_unfolding_12_loop: ;
+ if (! (i_unfold_63 < 4)) goto unfolding_2_loop_unfolding_16_loop;
{
- int tmp_2_unroll_12_unroll_49;
- int tmp_3_unroll_12_unroll_49;
- int tmp_4_unroll_12_unroll_49;
- int tmp_5_unroll_12_unroll_49;
- L1_unrolling_4_loop_unrolling_13_loop:
- j_unroll_63 = gen_nondet(76);
- tmp_2_unroll_12_unroll_49 = gen_nondet(77);
- if (tmp_2_unroll_12_unroll_49 > 10) i_unroll_63 = 10;
- else i_unroll_63 = 0;
- Frama_C_show_each_i_(i_unroll_63);
- tmp_3_unroll_12_unroll_49 = gen_nondet(79);
- if (tmp_3_unroll_12_unroll_49) goto L_unrolling_10_loop;
- tmp_4_unroll_12_unroll_49 = gen_nondet(80);
- if (tmp_4_unroll_12_unroll_49) goto L0;
- tmp_5_unroll_12_unroll_49 = gen_nondet(81);
- if (tmp_5_unroll_12_unroll_49) goto L3;
+ int tmp_2_unfold_12_unfold_49;
+ int tmp_3_unfold_12_unfold_49;
+ int tmp_4_unfold_12_unfold_49;
+ int tmp_5_unfold_12_unfold_49;
+ L1_unfolding_4_loop_unfolding_13_loop:
+ j_unfold_63 = gen_nondet(76);
+ tmp_2_unfold_12_unfold_49 = gen_nondet(77);
+ if (tmp_2_unfold_12_unfold_49 > 10) i_unfold_63 = 10;
+ else i_unfold_63 = 0;
+ Frama_C_show_each_i_(i_unfold_63);
+ tmp_3_unfold_12_unfold_49 = gen_nondet(79);
+ if (tmp_3_unfold_12_unfold_49) goto L_unfolding_10_loop;
+ tmp_4_unfold_12_unfold_49 = gen_nondet(80);
+ if (tmp_4_unfold_12_unfold_49) goto L0;
+ tmp_5_unfold_12_unfold_49 = gen_nondet(81);
+ if (tmp_5_unfold_12_unfold_49) goto L3;
}
- i_unroll_63 ++;
- unrolling_3_loop_unrolling_14_loop: ;
- /*@ loop pragma UNROLL "done", 2; */
- while (i_unroll_63 < 4) {
+ i_unfold_63 ++;
+ unfolding_3_loop_unfolding_14_loop: ;
+ /*@ loop unfold "done", 2; */
+ while (i_unfold_63 < 4) {
{
- int tmp_2_unroll_60;
- int tmp_3_unroll_60;
- int tmp_4_unroll_60;
- int tmp_5_unroll_60;
- L1_unrolling_15_loop: j_unroll_63 = gen_nondet(76);
- tmp_2_unroll_60 = gen_nondet(77);
- if (tmp_2_unroll_60 > 10) i_unroll_63 = 10; else i_unroll_63 = 0;
- Frama_C_show_each_i_(i_unroll_63);
- tmp_3_unroll_60 = gen_nondet(79);
- if (tmp_3_unroll_60) goto L_unrolling_10_loop;
- tmp_4_unroll_60 = gen_nondet(80);
- if (tmp_4_unroll_60) goto L0;
- tmp_5_unroll_60 = gen_nondet(81);
- if (tmp_5_unroll_60) goto L3;
+ int tmp_2_unfold_60;
+ int tmp_3_unfold_60;
+ int tmp_4_unfold_60;
+ int tmp_5_unfold_60;
+ L1_unfolding_15_loop: j_unfold_63 = gen_nondet(76);
+ tmp_2_unfold_60 = gen_nondet(77);
+ if (tmp_2_unfold_60 > 10) i_unfold_63 = 10; else i_unfold_63 = 0;
+ Frama_C_show_each_i_(i_unfold_63);
+ tmp_3_unfold_60 = gen_nondet(79);
+ if (tmp_3_unfold_60) goto L_unfolding_10_loop;
+ tmp_4_unfold_60 = gen_nondet(80);
+ if (tmp_4_unfold_60) goto L0;
+ tmp_5_unfold_60 = gen_nondet(81);
+ if (tmp_5_unfold_60) goto L3;
}
- i_unroll_63 ++;
+ i_unfold_63 ++;
}
- unrolling_2_loop_unrolling_16_loop: ;
+ unfolding_2_loop_unfolding_16_loop: ;
}
}
n --;
- if (! (n > 0)) goto unrolling_8_loop;
- unrolling_9_loop: ;
- /*@ loop pragma UNROLL "done", 2; */
+ if (! (n > 0)) goto unfolding_8_loop;
+ unfolding_9_loop: ;
+ /*@ loop unfold "done", 2; */
while (1) {
{
int tmp_1;
@@ -337,45 +337,45 @@ void main(void)
{
int j;
int i = 0;
- if (! (i < 4)) goto unrolling_2_loop;
+ if (! (i < 4)) goto unfolding_2_loop;
{
- int tmp_2_unroll_24;
- int tmp_3_unroll_24;
- int tmp_4_unroll_24;
- int tmp_5_unroll_24;
- L1_unrolling_6_loop: j = gen_nondet(76);
- tmp_2_unroll_24 = gen_nondet(77);
- if (tmp_2_unroll_24 > 10) i = 10; else i = 0;
+ int tmp_2_unfold_24;
+ int tmp_3_unfold_24;
+ int tmp_4_unfold_24;
+ int tmp_5_unfold_24;
+ L1_unfolding_6_loop: j = gen_nondet(76);
+ tmp_2_unfold_24 = gen_nondet(77);
+ if (tmp_2_unfold_24 > 10) i = 10; else i = 0;
Frama_C_show_each_i_(i);
- tmp_3_unroll_24 = gen_nondet(79);
- if (tmp_3_unroll_24) goto L;
- tmp_4_unroll_24 = gen_nondet(80);
- if (tmp_4_unroll_24) goto L0;
- tmp_5_unroll_24 = gen_nondet(81);
- if (tmp_5_unroll_24) goto L3;
+ tmp_3_unfold_24 = gen_nondet(79);
+ if (tmp_3_unfold_24) goto L;
+ tmp_4_unfold_24 = gen_nondet(80);
+ if (tmp_4_unfold_24) goto L0;
+ tmp_5_unfold_24 = gen_nondet(81);
+ if (tmp_5_unfold_24) goto L3;
}
i ++;
- unrolling_5_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
{
- int tmp_2_unroll_12;
- int tmp_3_unroll_12;
- int tmp_4_unroll_12;
- int tmp_5_unroll_12;
- L1_unrolling_4_loop: j = gen_nondet(76);
- tmp_2_unroll_12 = gen_nondet(77);
- if (tmp_2_unroll_12 > 10) i = 10; else i = 0;
+ int tmp_2_unfold_12;
+ int tmp_3_unfold_12;
+ int tmp_4_unfold_12;
+ int tmp_5_unfold_12;
+ L1_unfolding_4_loop: j = gen_nondet(76);
+ tmp_2_unfold_12 = gen_nondet(77);
+ if (tmp_2_unfold_12 > 10) i = 10; else i = 0;
Frama_C_show_each_i_(i);
- tmp_3_unroll_12 = gen_nondet(79);
- if (tmp_3_unroll_12) goto L;
- tmp_4_unroll_12 = gen_nondet(80);
- if (tmp_4_unroll_12) goto L0;
- tmp_5_unroll_12 = gen_nondet(81);
- if (tmp_5_unroll_12) goto L3;
+ tmp_3_unfold_12 = gen_nondet(79);
+ if (tmp_3_unfold_12) goto L;
+ tmp_4_unfold_12 = gen_nondet(80);
+ if (tmp_4_unfold_12) goto L0;
+ tmp_5_unfold_12 = gen_nondet(81);
+ if (tmp_5_unfold_12) goto L3;
}
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL "done", 2; */
+ unfolding_3_loop: ;
+ /*@ loop unfold "done", 2; */
while (i < 4) {
{
int tmp_2;
@@ -395,13 +395,13 @@ void main(void)
}
i ++;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
}
}
n --;
if (! (n > 0)) break;
}
- unrolling_8_loop: ;
+ unfolding_8_loop: ;
Frama_C_show_each_y_(y);
Frama_C_show_each_x_(x);
}
diff --git a/tests/syntax/oracle/unroll_const.res.oracle b/tests/syntax/oracle/unroll_const.res.oracle
index add94fa163ae3fc3072359d080e92e25b6ebd985..8f17a08e2914d6515a2fb8be09a0528bb8e915bb 100644
--- a/tests/syntax/oracle/unroll_const.res.oracle
+++ b/tests/syntax/oracle/unroll_const.res.oracle
@@ -21,156 +21,154 @@ int volatile c;
void main(void)
{
unsigned int i = (unsigned int)0;
- if (! c) goto unrolling_2_loop;
+ if (! c) goto unfolding_2_loop;
i ++;
- unrolling_6_loop: ;
- if (! c) goto unrolling_2_loop;
+ unfolding_6_loop: ;
+ if (! c) goto unfolding_2_loop;
i ++;
- unrolling_5_loop: ;
- if (! c) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! c) goto unfolding_2_loop;
i ++;
- unrolling_4_loop: ;
- if (! c) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! c) goto unfolding_2_loop;
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL sizeof(t) / sizeof(t[0]);
- loop pragma UNROLL "done", 4;
- */
+ unfolding_3_loop: ;
+ /*@ loop unfold sizeof(t) / sizeof(t[0]);
+ loop unfold "done", 4; */
while (c) i ++;
- unrolling_2_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_2_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_20_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_20_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_19_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_19_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_18_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_18_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_17_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_17_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_16_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_16_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_15_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_15_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_14_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_14_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_13_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_13_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_12_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_12_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_11_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_11_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_10_loop: ;
- if (! c) goto unrolling_8_loop;
+ unfolding_10_loop: ;
+ if (! c) goto unfolding_8_loop;
i ++;
- unrolling_9_loop: ;
- /*@ loop pragma UNROLL \offset(&s.v.l);
- loop pragma UNROLL "done", 12; */
+ unfolding_9_loop: ;
+ /*@ loop unfold \offset(&s.v.l);
+ loop unfold "done", 12; */
while (c) i ++;
- unrolling_8_loop: ;
- if (! c) goto unrolling_22_loop;
+ unfolding_8_loop: ;
+ if (! c) goto unfolding_22_loop;
i ++;
- unrolling_27_loop: ;
- if (! c) goto unrolling_22_loop;
+ unfolding_27_loop: ;
+ if (! c) goto unfolding_22_loop;
i ++;
- unrolling_26_loop: ;
- if (! c) goto unrolling_22_loop;
+ unfolding_26_loop: ;
+ if (! c) goto unfolding_22_loop;
i ++;
- unrolling_25_loop: ;
- if (! c) goto unrolling_22_loop;
+ unfolding_25_loop: ;
+ if (! c) goto unfolding_22_loop;
i ++;
- unrolling_24_loop: ;
- if (! c) goto unrolling_22_loop;
+ unfolding_24_loop: ;
+ if (! c) goto unfolding_22_loop;
i ++;
- unrolling_23_loop: ;
- /*@ loop pragma UNROLL s.i + s.v.l;
- loop pragma UNROLL "done", 5; */
+ unfolding_23_loop: ;
+ /*@ loop unfold s.i + s.v.l;
+ loop unfold "done", 5; */
while (c) i ++;
- unrolling_22_loop: ;
- if (! c) goto unrolling_29_loop;
+ unfolding_22_loop: ;
+ if (! c) goto unfolding_29_loop;
i ++;
- unrolling_33_loop: ;
- if (! c) goto unrolling_29_loop;
+ unfolding_33_loop: ;
+ if (! c) goto unfolding_29_loop;
i ++;
- unrolling_32_loop: ;
- if (! c) goto unrolling_29_loop;
+ unfolding_32_loop: ;
+ if (! c) goto unfolding_29_loop;
i ++;
- unrolling_31_loop: ;
- if (! c) goto unrolling_29_loop;
+ unfolding_31_loop: ;
+ if (! c) goto unfolding_29_loop;
i ++;
- unrolling_30_loop: ;
- /*@ loop pragma UNROLL \max(t[..]);
- loop pragma UNROLL "done", 4; */
+ unfolding_30_loop: ;
+ /*@ loop unfold \max(t[..]);
+ loop unfold "done", 4; */
while (c) i ++;
- unrolling_29_loop: ;
- /*@ loop pragma UNROLL \min(t[..]); */
+ unfolding_29_loop: ;
+ /*@ loop unfold \min(t[..]); */
while (c) i ++;
- if (! c) goto unrolling_35_loop;
+ if (! c) goto unfolding_35_loop;
i ++;
- unrolling_41_loop: ;
- if (! c) goto unrolling_35_loop;
+ unfolding_41_loop: ;
+ if (! c) goto unfolding_35_loop;
i ++;
- unrolling_40_loop: ;
- if (! c) goto unrolling_35_loop;
+ unfolding_40_loop: ;
+ if (! c) goto unfolding_35_loop;
i ++;
- unrolling_39_loop: ;
- if (! c) goto unrolling_35_loop;
+ unfolding_39_loop: ;
+ if (! c) goto unfolding_35_loop;
i ++;
- unrolling_38_loop: ;
- if (! c) goto unrolling_35_loop;
+ unfolding_38_loop: ;
+ if (! c) goto unfolding_35_loop;
i ++;
- unrolling_37_loop: ;
- if (! c) goto unrolling_35_loop;
+ unfolding_37_loop: ;
+ if (! c) goto unfolding_35_loop;
i ++;
- unrolling_36_loop: ;
- /*@ loop pragma UNROLL \max({1, 1 + s.i});
- loop pragma UNROLL "done", 6; */
+ unfolding_36_loop: ;
+ /*@ loop unfold \max({1, 1 + s.i});
+ loop unfold "done", 6; */
while (c) i ++;
- unrolling_35_loop: ;
- if (! c) goto unrolling_43_loop;
+ unfolding_35_loop: ;
+ if (! c) goto unfolding_43_loop;
i ++;
- unrolling_45_loop: ;
- if (! c) goto unrolling_43_loop;
+ unfolding_45_loop: ;
+ if (! c) goto unfolding_43_loop;
i ++;
- unrolling_44_loop: ;
- /*@ loop pragma UNROLL \min(t[{1, 3}]) + \max(t[{1, 3}]);
- loop pragma UNROLL "done", 2;
- */
+ unfolding_44_loop: ;
+ /*@ loop unfold \min(t[{1, 3}]) + \max(t[{1, 3}]);
+ loop unfold "done", 2; */
while (c) i ++;
- unrolling_43_loop: ;
- if (! c) goto unrolling_47_loop;
+ unfolding_43_loop: ;
+ if (! c) goto unfolding_47_loop;
i ++;
- unrolling_53_loop: ;
- if (! c) goto unrolling_47_loop;
+ unfolding_53_loop: ;
+ if (! c) goto unfolding_47_loop;
i ++;
- unrolling_52_loop: ;
- if (! c) goto unrolling_47_loop;
+ unfolding_52_loop: ;
+ if (! c) goto unfolding_47_loop;
i ++;
- unrolling_51_loop: ;
- if (! c) goto unrolling_47_loop;
+ unfolding_51_loop: ;
+ if (! c) goto unfolding_47_loop;
i ++;
- unrolling_50_loop: ;
- if (! c) goto unrolling_47_loop;
+ unfolding_50_loop: ;
+ if (! c) goto unfolding_47_loop;
i ++;
- unrolling_49_loop: ;
- if (! c) goto unrolling_47_loop;
+ unfolding_49_loop: ;
+ if (! c) goto unfolding_47_loop;
i ++;
- unrolling_48_loop: ;
- /*@ loop pragma UNROLL \min(u[.. 1].i1) * \max(u[.. 1].i1);
- loop pragma UNROLL "done", 6;
+ unfolding_48_loop: ;
+ /*@ loop unfold \min(u[.. 1].i1) * \max(u[.. 1].i1);
+ loop unfold "done", 6;
*/
while (c) i ++;
- unrolling_47_loop: ;
+ unfolding_47_loop: ;
return;
}
diff --git a/tests/syntax/oracle/unroll_labels.0.res.oracle b/tests/syntax/oracle/unroll_labels.0.res.oracle
index 783cbed13c8bc550ce424f8f44cddbbebf330997..b4bf202e0196a60e2d7f5e338888f790ee8eaa7a 100644
--- a/tests/syntax/oracle/unroll_labels.0.res.oracle
+++ b/tests/syntax/oracle/unroll_labels.0.res.oracle
@@ -23,7 +23,7 @@ void main(void)
int j = 0;
{
int i = 1;
- if (! (i < 4)) goto unrolling_2_loop;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -36,8 +36,8 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_6_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_6_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -50,8 +50,8 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_5_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -64,8 +64,8 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_4_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -78,10 +78,10 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_3_loop: ;
+ unfolding_3_loop: ;
/*@ loop invariant \false;
- loop pragma UNROLL "completely", 4;
- loop pragma UNROLL "done", 4;
+ loop unfold "completely", 4;
+ loop unfold "done", 4;
*/
while (i < 4) {
switch (i) {
@@ -97,63 +97,63 @@ void main(void)
}
i ++;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
}
{
int x = 0;
L:
{
- if (! (x < 5)) goto unrolling_8_loop;
+ if (! (x < 5)) goto unfolding_8_loop;
{
- int y_unroll_32 = 0;
+ int y_unfold_32 = 0;
x ++;
- y_unroll_32 ++;
+ y_unfold_32 ++;
}
- unrolling_11_loop: ;
- if (! (x < 5)) goto unrolling_8_loop;
+ unfolding_11_loop: ;
+ if (! (x < 5)) goto unfolding_8_loop;
{
- int y_unroll_28 = 0;
+ int y_unfold_28 = 0;
x ++;
- y_unroll_28 ++;
+ y_unfold_28 ++;
}
- unrolling_10_loop: ;
- if (! (x < 5)) goto unrolling_8_loop;
+ unfolding_10_loop: ;
+ if (! (x < 5)) goto unfolding_8_loop;
{
- int y_unroll_24 = 0;
+ int y_unfold_24 = 0;
x ++;
- y_unroll_24 ++;
+ y_unfold_24 ++;
}
- unrolling_9_loop: ;
- /*@ loop pragma UNROLL 3;
- loop pragma UNROLL "done", 3; */
+ unfolding_9_loop: ;
+ /*@ loop unfold 3;
+ loop unfold "done", 3; */
while (x < 5) {
int y = 0;
x ++;
y ++;
}
- unrolling_8_loop: ;
+ unfolding_8_loop: ;
}
}
j = 0;
- if (! foo) goto unrolling_18_loop;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
j ++;
- unrolling_16_loop_unrolling_45_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+ unfolding_16_loop_unfolding_45_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
j ++;
- unrolling_15_loop_unrolling_46_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+ unfolding_15_loop_unfolding_46_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
j ++;
- unrolling_14_loop_unrolling_47_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_47_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_48_loop: ;
+ unfolding_13_loop_unfolding_48_loop: ;
}
break;
case 5: j = -1;
@@ -161,26 +161,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_44_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_44_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
j ++;
- unrolling_16_loop_unrolling_40_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+ unfolding_16_loop_unfolding_40_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
j ++;
- unrolling_15_loop_unrolling_41_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+ unfolding_15_loop_unfolding_41_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
j ++;
- unrolling_14_loop_unrolling_42_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_42_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_43_loop: ;
+ unfolding_13_loop_unfolding_43_loop: ;
}
break;
case 5: j = -1;
@@ -188,26 +188,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_39_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_39_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
j ++;
- unrolling_16_loop_unrolling_35_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+ unfolding_16_loop_unfolding_35_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
j ++;
- unrolling_15_loop_unrolling_36_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+ unfolding_15_loop_unfolding_36_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
j ++;
- unrolling_14_loop_unrolling_37_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_37_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_38_loop: ;
+ unfolding_13_loop_unfolding_38_loop: ;
}
break;
case 5: j = -1;
@@ -215,26 +215,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_34_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_34_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
j ++;
- unrolling_16_loop_unrolling_30_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+ unfolding_16_loop_unfolding_30_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
j ++;
- unrolling_15_loop_unrolling_31_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+ unfolding_15_loop_unfolding_31_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
j ++;
- unrolling_14_loop_unrolling_32_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_32_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_33_loop: ;
+ unfolding_13_loop_unfolding_33_loop: ;
}
break;
case 5: j = -1;
@@ -242,26 +242,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_29_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_29_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
j ++;
- unrolling_16_loop_unrolling_25_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+ unfolding_16_loop_unfolding_25_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
j ++;
- unrolling_15_loop_unrolling_26_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+ unfolding_15_loop_unfolding_26_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
j ++;
- unrolling_14_loop_unrolling_27_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_27_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_28_loop: ;
+ unfolding_13_loop_unfolding_28_loop: ;
}
break;
case 5: j = -1;
@@ -269,26 +269,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_24_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_24_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
j ++;
- unrolling_16_loop_unrolling_20_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+ unfolding_16_loop_unfolding_20_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
j ++;
- unrolling_15_loop_unrolling_21_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+ unfolding_15_loop_unfolding_21_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
j ++;
- unrolling_14_loop_unrolling_22_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_22_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_23_loop: ;
+ unfolding_13_loop_unfolding_23_loop: ;
}
break;
case 5: j = -1;
@@ -296,28 +296,28 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_19_loop: ;
- /*@ loop pragma UNROLL SIX;
- loop pragma UNROLL "done", 6; */
+ unfolding_19_loop: ;
+ /*@ loop unfold SIX;
+ loop unfold "done", 6; */
while (foo)
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop;
+ if (! (j < 5)) goto unfolding_13_loop;
j ++;
- unrolling_16_loop: ;
- if (! (j < 5)) goto unrolling_13_loop;
+ unfolding_16_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop;
j ++;
- unrolling_15_loop: ;
- if (! (j < 5)) goto unrolling_13_loop;
+ unfolding_15_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop;
j ++;
- unrolling_14_loop: ;
- /*@ loop pragma UNROLL 3;
- loop pragma UNROLL "done", 3; */
+ unfolding_14_loop: ;
+ /*@ loop unfold 3;
+ loop unfold "done", 3; */
while (j < 5) j ++;
- unrolling_13_loop: ;
+ unfolding_13_loop: ;
}
break;
case 5: j = -1;
@@ -325,25 +325,25 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_18_loop: ;
+ unfolding_18_loop: ;
if (j == 0) goto zero;
if (j == 1) goto un;
goto return_label;
zero:
{
- if (! (j < 5)) goto unrolling_50_loop;
- un_unrolling_56_loop: j ++;
- unrolling_55_loop: ;
- if (! (j < 5)) goto unrolling_50_loop;
- un_unrolling_54_loop: j ++;
- unrolling_53_loop: ;
- if (! (j < 5)) goto unrolling_50_loop;
- un_unrolling_52_loop: j ++;
- unrolling_51_loop: ;
- /*@ loop pragma UNROLL 3;
- loop pragma UNROLL "done", 3; */
+ if (! (j < 5)) goto unfolding_50_loop;
+ un_unfolding_56_loop: j ++;
+ unfolding_55_loop: ;
+ if (! (j < 5)) goto unfolding_50_loop;
+ un_unfolding_54_loop: j ++;
+ unfolding_53_loop: ;
+ if (! (j < 5)) goto unfolding_50_loop;
+ un_unfolding_52_loop: j ++;
+ unfolding_51_loop: ;
+ /*@ loop unfold 3;
+ loop unfold "done", 3; */
while (j < 5) un: j ++;
- unrolling_50_loop: ;
+ unfolding_50_loop: ;
}
return_label: return;
}
@@ -351,34 +351,34 @@ void main(void)
void main2(void)
{
int i = 0;
- if (! (i < 2)) goto unrolling_58_loop;
+ if (! (i < 2)) goto unfolding_58_loop;
{
- int j_unroll_192 = 0;
- while (j_unroll_192 < 2) {
+ int j_unfold_192 = 0;
+ while (j_unfold_192 < 2) {
i ++;
- goto foo_unrolling_62_loop;
+ goto foo_unfolding_62_loop;
i ++;
- foo_unrolling_62_loop: ;
- j_unroll_192 ++;
+ foo_unfolding_62_loop: ;
+ j_unfold_192 ++;
}
}
i ++;
- unrolling_61_loop: ;
- if (! (i < 2)) goto unrolling_58_loop;
+ unfolding_61_loop: ;
+ if (! (i < 2)) goto unfolding_58_loop;
{
- int j_unroll_184 = 0;
- while (j_unroll_184 < 2) {
+ int j_unfold_184 = 0;
+ while (j_unfold_184 < 2) {
i ++;
- goto foo_unrolling_60_loop;
+ goto foo_unfolding_60_loop;
i ++;
- foo_unrolling_60_loop: ;
- j_unroll_184 ++;
+ foo_unfolding_60_loop: ;
+ j_unfold_184 ++;
}
}
i ++;
- unrolling_59_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ unfolding_59_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (i < 2) {
{
int j = 0;
@@ -392,34 +392,34 @@ void main2(void)
}
i ++;
}
- unrolling_58_loop: ;
+ unfolding_58_loop: ;
return;
}
void main2_done(void)
{
int i = 0;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (i < 2) {
{
int j = 0;
- if (! (j < 2)) goto unrolling_64_loop;
+ if (! (j < 2)) goto unfolding_64_loop;
i ++;
- goto foo_unrolling_68_loop;
+ goto foo_unfolding_68_loop;
i ++;
- foo_unrolling_68_loop: ;
+ foo_unfolding_68_loop: ;
j ++;
- unrolling_67_loop: ;
- if (! (j < 2)) goto unrolling_64_loop;
+ unfolding_67_loop: ;
+ if (! (j < 2)) goto unfolding_64_loop;
i ++;
- goto foo_unrolling_66_loop;
+ goto foo_unfolding_66_loop;
i ++;
- foo_unrolling_66_loop: ;
+ foo_unfolding_66_loop: ;
j ++;
- unrolling_65_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ unfolding_65_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (j < 2) {
i ++;
goto foo;
@@ -427,7 +427,7 @@ void main2_done(void)
foo: ;
j ++;
}
- unrolling_64_loop: ;
+ unfolding_64_loop: ;
}
i ++;
}
@@ -438,46 +438,46 @@ void main3(int c)
{
int i = 0;
if (c == 0) goto foo;
- if (! (i < 5)) goto unrolling_70_loop;
+ if (! (i < 5)) goto unfolding_70_loop;
{
- int j_unroll_244 = 0;
- if (i == j_unroll_244) goto foo_unrolling_77_loop;
- if (i == 1) goto unrolling_70_loop;
- if (i == 2) goto __Cont_unrolling_80_loop;
- while (j_unroll_244 < 5) {
- if (i == j_unroll_244) break;
- if (i < j_unroll_244) goto foo_unrolling_77_loop;
- if (i == j_unroll_244 + 1) goto __Cont_0_unrolling_78_loop;
- if (i == j_unroll_244 + 2) goto up_unrolling_79_loop;
+ int j_unfold_244 = 0;
+ if (i == j_unfold_244) goto foo_unfolding_77_loop;
+ if (i == 1) goto unfolding_70_loop;
+ if (i == 2) goto __Cont_unfolding_80_loop;
+ while (j_unfold_244 < 5) {
+ if (i == j_unfold_244) break;
+ if (i < j_unfold_244) goto foo_unfolding_77_loop;
+ if (i == j_unfold_244 + 1) goto __Cont_0_unfolding_78_loop;
+ if (i == j_unfold_244 + 2) goto up_unfolding_79_loop;
i ++;
- foo_unrolling_77_loop: i ++;
- __Cont_0_unrolling_78_loop: j_unroll_244 ++;
+ foo_unfolding_77_loop: i ++;
+ __Cont_0_unfolding_78_loop: j_unfold_244 ++;
}
- up_unrolling_79_loop: ;
+ up_unfolding_79_loop: ;
}
- __Cont_unrolling_80_loop: i ++;
- unrolling_76_loop: ;
- if (! (i < 5)) goto unrolling_70_loop;
+ __Cont_unfolding_80_loop: i ++;
+ unfolding_76_loop: ;
+ if (! (i < 5)) goto unfolding_70_loop;
{
- int j_unroll_222 = 0;
- if (i == j_unroll_222) goto foo_unrolling_72_loop;
- if (i == 1) goto unrolling_70_loop;
- if (i == 2) goto __Cont_unrolling_75_loop;
- while (j_unroll_222 < 5) {
- if (i == j_unroll_222) break;
- if (i < j_unroll_222) goto foo_unrolling_72_loop;
- if (i == j_unroll_222 + 1) goto __Cont_0_unrolling_73_loop;
- if (i == j_unroll_222 + 2) goto up_unrolling_74_loop;
+ int j_unfold_222 = 0;
+ if (i == j_unfold_222) goto foo_unfolding_72_loop;
+ if (i == 1) goto unfolding_70_loop;
+ if (i == 2) goto __Cont_unfolding_75_loop;
+ while (j_unfold_222 < 5) {
+ if (i == j_unfold_222) break;
+ if (i < j_unfold_222) goto foo_unfolding_72_loop;
+ if (i == j_unfold_222 + 1) goto __Cont_0_unfolding_73_loop;
+ if (i == j_unfold_222 + 2) goto up_unfolding_74_loop;
i ++;
- foo_unrolling_72_loop: i ++;
- __Cont_0_unrolling_73_loop: j_unroll_222 ++;
+ foo_unfolding_72_loop: i ++;
+ __Cont_0_unfolding_73_loop: j_unfold_222 ++;
}
- up_unrolling_74_loop: ;
+ up_unfolding_74_loop: ;
}
- __Cont_unrolling_75_loop: i ++;
- unrolling_71_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ __Cont_unfolding_75_loop: i ++;
+ unfolding_71_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (i < 5) {
{
int j = 0;
@@ -497,7 +497,7 @@ void main3(int c)
}
__Cont: i ++;
}
- unrolling_70_loop: ;
+ unfolding_70_loop: ;
return;
}
diff --git a/tests/syntax/oracle/unroll_labels.1.res.oracle b/tests/syntax/oracle/unroll_labels.1.res.oracle
index 0c625a01ef43c99e768623b0906f85096315b8e6..8a9d1c82f7aae87f25994c943465209eb2d93be7 100644
--- a/tests/syntax/oracle/unroll_labels.1.res.oracle
+++ b/tests/syntax/oracle/unroll_labels.1.res.oracle
@@ -19,7 +19,7 @@ void main(void)
int j = 0;
{
int i = 1;
- if (! (i < 4)) goto unrolling_2_loop;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -32,8 +32,8 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_6_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_6_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -46,8 +46,8 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_5_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_5_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -60,8 +60,8 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_4_loop: ;
- if (! (i < 4)) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! (i < 4)) goto unfolding_2_loop;
switch (i) {
case 1: j ++;
break;
@@ -74,10 +74,10 @@ void main(void)
default: j = 0;
}
i ++;
- unrolling_3_loop: ;
+ unfolding_3_loop: ;
/*@ loop invariant \false;
- loop pragma UNROLL "completely", 4;
- loop pragma UNROLL "done", 4;
+ loop unfold "completely", 4;
+ loop unfold "done", 4;
*/
while (i < 4) {
switch (i) {
@@ -93,63 +93,63 @@ void main(void)
}
i ++;
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
}
{
int x = 0;
L:
{
- if (! (x < 5)) goto unrolling_8_loop;
+ if (! (x < 5)) goto unfolding_8_loop;
{
- int y_unroll_32 = 0;
+ int y_unfold_32 = 0;
x ++;
- y_unroll_32 ++;
+ y_unfold_32 ++;
}
- unrolling_11_loop: ;
- if (! (x < 5)) goto unrolling_8_loop;
+ unfolding_11_loop: ;
+ if (! (x < 5)) goto unfolding_8_loop;
{
- int y_unroll_28 = 0;
+ int y_unfold_28 = 0;
x ++;
- y_unroll_28 ++;
+ y_unfold_28 ++;
}
- unrolling_10_loop: ;
- if (! (x < 5)) goto unrolling_8_loop;
+ unfolding_10_loop: ;
+ if (! (x < 5)) goto unfolding_8_loop;
{
- int y_unroll_24 = 0;
+ int y_unfold_24 = 0;
x ++;
- y_unroll_24 ++;
+ y_unfold_24 ++;
}
- unrolling_9_loop: ;
- /*@ loop pragma UNROLL 3;
- loop pragma UNROLL "done", 3; */
+ unfolding_9_loop: ;
+ /*@ loop unfold 3;
+ loop unfold "done", 3; */
while (x < 5) {
int y = 0;
x ++;
y ++;
}
- unrolling_8_loop: ;
+ unfolding_8_loop: ;
}
}
j = 0;
- if (! foo) goto unrolling_18_loop;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
j ++;
- unrolling_16_loop_unrolling_45_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+ unfolding_16_loop_unfolding_45_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
j ++;
- unrolling_15_loop_unrolling_46_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+ unfolding_15_loop_unfolding_46_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
j ++;
- unrolling_14_loop_unrolling_47_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_47_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_48_loop: ;
+ unfolding_13_loop_unfolding_48_loop: ;
}
break;
case 5: j = -1;
@@ -157,26 +157,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_44_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_44_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
j ++;
- unrolling_16_loop_unrolling_40_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+ unfolding_16_loop_unfolding_40_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
j ++;
- unrolling_15_loop_unrolling_41_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+ unfolding_15_loop_unfolding_41_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
j ++;
- unrolling_14_loop_unrolling_42_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_42_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_43_loop: ;
+ unfolding_13_loop_unfolding_43_loop: ;
}
break;
case 5: j = -1;
@@ -184,26 +184,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_39_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_39_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
j ++;
- unrolling_16_loop_unrolling_35_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+ unfolding_16_loop_unfolding_35_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
j ++;
- unrolling_15_loop_unrolling_36_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+ unfolding_15_loop_unfolding_36_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
j ++;
- unrolling_14_loop_unrolling_37_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_37_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_38_loop: ;
+ unfolding_13_loop_unfolding_38_loop: ;
}
break;
case 5: j = -1;
@@ -211,26 +211,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_34_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_34_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
j ++;
- unrolling_16_loop_unrolling_30_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+ unfolding_16_loop_unfolding_30_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
j ++;
- unrolling_15_loop_unrolling_31_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+ unfolding_15_loop_unfolding_31_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
j ++;
- unrolling_14_loop_unrolling_32_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_32_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_33_loop: ;
+ unfolding_13_loop_unfolding_33_loop: ;
}
break;
case 5: j = -1;
@@ -238,26 +238,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_29_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_29_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
j ++;
- unrolling_16_loop_unrolling_25_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+ unfolding_16_loop_unfolding_25_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
j ++;
- unrolling_15_loop_unrolling_26_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+ unfolding_15_loop_unfolding_26_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
j ++;
- unrolling_14_loop_unrolling_27_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_27_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_28_loop: ;
+ unfolding_13_loop_unfolding_28_loop: ;
}
break;
case 5: j = -1;
@@ -265,26 +265,26 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_24_loop: ;
- if (! foo) goto unrolling_18_loop;
+ unfolding_24_loop: ;
+ if (! foo) goto unfolding_18_loop;
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
j ++;
- unrolling_16_loop_unrolling_20_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+ unfolding_16_loop_unfolding_20_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
j ++;
- unrolling_15_loop_unrolling_21_loop: ;
- if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+ unfolding_15_loop_unfolding_21_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
j ++;
- unrolling_14_loop_unrolling_22_loop: ;
- /*@ loop pragma UNROLL "done", 3;
- loop pragma UNROLL 3; */
+ unfolding_14_loop_unfolding_22_loop: ;
+ /*@ loop unfold "done", 3;
+ loop unfold 3; */
while (j < 5) j ++;
- unrolling_13_loop_unrolling_23_loop: ;
+ unfolding_13_loop_unfolding_23_loop: ;
}
break;
case 5: j = -1;
@@ -292,28 +292,28 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_19_loop: ;
- /*@ loop pragma UNROLL SIX;
- loop pragma UNROLL "done", 6; */
+ unfolding_19_loop: ;
+ /*@ loop unfold SIX;
+ loop unfold "done", 6; */
while (foo)
switch (j) {
case -1: j ++;
break;
case 0:
{
- if (! (j < 5)) goto unrolling_13_loop;
+ if (! (j < 5)) goto unfolding_13_loop;
j ++;
- unrolling_16_loop: ;
- if (! (j < 5)) goto unrolling_13_loop;
+ unfolding_16_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop;
j ++;
- unrolling_15_loop: ;
- if (! (j < 5)) goto unrolling_13_loop;
+ unfolding_15_loop: ;
+ if (! (j < 5)) goto unfolding_13_loop;
j ++;
- unrolling_14_loop: ;
- /*@ loop pragma UNROLL 3;
- loop pragma UNROLL "done", 3; */
+ unfolding_14_loop: ;
+ /*@ loop unfold 3;
+ loop unfold "done", 3; */
while (j < 5) j ++;
- unrolling_13_loop: ;
+ unfolding_13_loop: ;
}
break;
case 5: j = -1;
@@ -321,25 +321,25 @@ void main(void)
default: ;
goto return_label;
}
- unrolling_18_loop: ;
+ unfolding_18_loop: ;
if (j == 0) goto zero;
if (j == 1) goto un;
goto return_label;
zero:
{
- if (! (j < 5)) goto unrolling_50_loop;
- un_unrolling_56_loop: j ++;
- unrolling_55_loop: ;
- if (! (j < 5)) goto unrolling_50_loop;
- un_unrolling_54_loop: j ++;
- unrolling_53_loop: ;
- if (! (j < 5)) goto unrolling_50_loop;
- un_unrolling_52_loop: j ++;
- unrolling_51_loop: ;
- /*@ loop pragma UNROLL 3;
- loop pragma UNROLL "done", 3; */
+ if (! (j < 5)) goto unfolding_50_loop;
+ un_unfolding_56_loop: j ++;
+ unfolding_55_loop: ;
+ if (! (j < 5)) goto unfolding_50_loop;
+ un_unfolding_54_loop: j ++;
+ unfolding_53_loop: ;
+ if (! (j < 5)) goto unfolding_50_loop;
+ un_unfolding_52_loop: j ++;
+ unfolding_51_loop: ;
+ /*@ loop unfold 3;
+ loop unfold "done", 3; */
while (j < 5) un: j ++;
- unrolling_50_loop: ;
+ unfolding_50_loop: ;
}
return_label: return;
}
@@ -347,34 +347,34 @@ void main(void)
void main2(void)
{
int i = 0;
- if (! (i < 2)) goto unrolling_58_loop;
+ if (! (i < 2)) goto unfolding_58_loop;
{
- int j_unroll_192 = 0;
- while (j_unroll_192 < 2) {
+ int j_unfold_192 = 0;
+ while (j_unfold_192 < 2) {
i ++;
- goto foo_unrolling_62_loop;
+ goto foo_unfolding_62_loop;
i ++;
- foo_unrolling_62_loop: ;
- j_unroll_192 ++;
+ foo_unfolding_62_loop: ;
+ j_unfold_192 ++;
}
}
i ++;
- unrolling_61_loop: ;
- if (! (i < 2)) goto unrolling_58_loop;
+ unfolding_61_loop: ;
+ if (! (i < 2)) goto unfolding_58_loop;
{
- int j_unroll_184 = 0;
- while (j_unroll_184 < 2) {
+ int j_unfold_184 = 0;
+ while (j_unfold_184 < 2) {
i ++;
- goto foo_unrolling_60_loop;
+ goto foo_unfolding_60_loop;
i ++;
- foo_unrolling_60_loop: ;
- j_unroll_184 ++;
+ foo_unfolding_60_loop: ;
+ j_unfold_184 ++;
}
}
i ++;
- unrolling_59_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ unfolding_59_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (i < 2) {
{
int j = 0;
@@ -388,34 +388,34 @@ void main2(void)
}
i ++;
}
- unrolling_58_loop: ;
+ unfolding_58_loop: ;
return;
}
void main2_done(void)
{
int i = 0;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (i < 2) {
{
int j = 0;
- if (! (j < 2)) goto unrolling_64_loop;
+ if (! (j < 2)) goto unfolding_64_loop;
i ++;
- goto foo_unrolling_68_loop;
+ goto foo_unfolding_68_loop;
i ++;
- foo_unrolling_68_loop: ;
+ foo_unfolding_68_loop: ;
j ++;
- unrolling_67_loop: ;
- if (! (j < 2)) goto unrolling_64_loop;
+ unfolding_67_loop: ;
+ if (! (j < 2)) goto unfolding_64_loop;
i ++;
- goto foo_unrolling_66_loop;
+ goto foo_unfolding_66_loop;
i ++;
- foo_unrolling_66_loop: ;
+ foo_unfolding_66_loop: ;
j ++;
- unrolling_65_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ unfolding_65_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (j < 2) {
i ++;
goto foo;
@@ -423,7 +423,7 @@ void main2_done(void)
foo: ;
j ++;
}
- unrolling_64_loop: ;
+ unfolding_64_loop: ;
}
i ++;
}
@@ -434,46 +434,46 @@ void main3(int c)
{
int i = 0;
if (c == 0) goto foo;
- if (! (i < 5)) goto unrolling_70_loop;
+ if (! (i < 5)) goto unfolding_70_loop;
{
- int j_unroll_244 = 0;
- if (i == j_unroll_244) goto foo_unrolling_77_loop;
- if (i == 1) goto unrolling_70_loop;
- if (i == 2) goto __Cont_unrolling_80_loop;
- while (j_unroll_244 < 5) {
- if (i == j_unroll_244) break;
- if (i < j_unroll_244) goto foo_unrolling_77_loop;
- if (i == j_unroll_244 + 1) goto __Cont_0_unrolling_78_loop;
- if (i == j_unroll_244 + 2) goto up_unrolling_79_loop;
+ int j_unfold_244 = 0;
+ if (i == j_unfold_244) goto foo_unfolding_77_loop;
+ if (i == 1) goto unfolding_70_loop;
+ if (i == 2) goto __Cont_unfolding_80_loop;
+ while (j_unfold_244 < 5) {
+ if (i == j_unfold_244) break;
+ if (i < j_unfold_244) goto foo_unfolding_77_loop;
+ if (i == j_unfold_244 + 1) goto __Cont_0_unfolding_78_loop;
+ if (i == j_unfold_244 + 2) goto up_unfolding_79_loop;
i ++;
- foo_unrolling_77_loop: i ++;
- __Cont_0_unrolling_78_loop: j_unroll_244 ++;
+ foo_unfolding_77_loop: i ++;
+ __Cont_0_unfolding_78_loop: j_unfold_244 ++;
}
- up_unrolling_79_loop: ;
+ up_unfolding_79_loop: ;
}
- __Cont_unrolling_80_loop: i ++;
- unrolling_76_loop: ;
- if (! (i < 5)) goto unrolling_70_loop;
+ __Cont_unfolding_80_loop: i ++;
+ unfolding_76_loop: ;
+ if (! (i < 5)) goto unfolding_70_loop;
{
- int j_unroll_222 = 0;
- if (i == j_unroll_222) goto foo_unrolling_72_loop;
- if (i == 1) goto unrolling_70_loop;
- if (i == 2) goto __Cont_unrolling_75_loop;
- while (j_unroll_222 < 5) {
- if (i == j_unroll_222) break;
- if (i < j_unroll_222) goto foo_unrolling_72_loop;
- if (i == j_unroll_222 + 1) goto __Cont_0_unrolling_73_loop;
- if (i == j_unroll_222 + 2) goto up_unrolling_74_loop;
+ int j_unfold_222 = 0;
+ if (i == j_unfold_222) goto foo_unfolding_72_loop;
+ if (i == 1) goto unfolding_70_loop;
+ if (i == 2) goto __Cont_unfolding_75_loop;
+ while (j_unfold_222 < 5) {
+ if (i == j_unfold_222) break;
+ if (i < j_unfold_222) goto foo_unfolding_72_loop;
+ if (i == j_unfold_222 + 1) goto __Cont_0_unfolding_73_loop;
+ if (i == j_unfold_222 + 2) goto up_unfolding_74_loop;
i ++;
- foo_unrolling_72_loop: i ++;
- __Cont_0_unrolling_73_loop: j_unroll_222 ++;
+ foo_unfolding_72_loop: i ++;
+ __Cont_0_unfolding_73_loop: j_unfold_222 ++;
}
- up_unrolling_74_loop: ;
+ up_unfolding_74_loop: ;
}
- __Cont_unrolling_75_loop: i ++;
- unrolling_71_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ __Cont_unfolding_75_loop: i ++;
+ unfolding_71_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while (i < 5) {
{
int j = 0;
@@ -493,7 +493,7 @@ void main3(int c)
}
__Cont: i ++;
}
- unrolling_70_loop: ;
+ unfolding_70_loop: ;
return;
}
diff --git a/tests/syntax/oracle/unroll_visit.res.oracle b/tests/syntax/oracle/unroll_visit.res.oracle
index c65c2723ab53a495d5f822b511d9741d8e1fcb5f..4768a2906b4d130538dab116a8c659800c461649 100644
--- a/tests/syntax/oracle/unroll_visit.res.oracle
+++ b/tests/syntax/oracle/unroll_visit.res.oracle
@@ -27,27 +27,27 @@ typedef char i8;
void main(void)
{
i8 i = (i8)0;
- if (! ((int)i < 100)) goto unrolling_2_loop;
+ if (! ((int)i < 100)) goto unfolding_2_loop;
i = (i8)((int)i - 1);
/*@ assert i < 100; */ ;
i = (i8)((int)i + 1);
i = (i8)((int)i + 1);
- unrolling_4_loop: ;
- if (! ((int)i < 100)) goto unrolling_2_loop;
+ unfolding_4_loop: ;
+ if (! ((int)i < 100)) goto unfolding_2_loop;
i = (i8)((int)i - 1);
/*@ assert i < 100; */ ;
i = (i8)((int)i + 1);
i = (i8)((int)i + 1);
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL 2;
- loop pragma UNROLL "done", 2; */
+ unfolding_3_loop: ;
+ /*@ loop unfold 2;
+ loop unfold "done", 2; */
while ((int)i < 100) {
i = (i8)((int)i - 1);
/*@ assert i < 100; */ ;
i = (i8)((int)i + 1);
i = (i8)((int)i + 1);
}
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return;
}
diff --git a/tests/syntax/oracle/very_large_integers.17.res.oracle b/tests/syntax/oracle/very_large_integers.17.res.oracle
index 3358d5f03d550e6db60ecd6b91ac10cfbcfe4eca..952d0b178160cf63405a6d5e13e63727487b832c 100644
--- a/tests/syntax/oracle/very_large_integers.17.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.17.res.oracle
@@ -5,7 +5,7 @@
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:141: Warning:
- ignoring unrolling directive (not an understood constant expression)
+ ignoring unfolding directive (not an understood constant expression)
/* Generated by Frama-C */
int volatile nondet;
/*@ logic ℤ too_large_integer= 9999999999999999999;
@@ -13,7 +13,7 @@ int volatile nondet;
int main(void)
{
int __retres;
- /*@ loop pragma UNROLL 99999999999999999999; */
+ /*@ loop unfold 99999999999999999999; */
while (nondet) ;
__retres = 0;
return __retres;
diff --git a/tests/syntax/unroll_const.i b/tests/syntax/unroll_const.i
index 715210a9bf3d1b178a0f9cdf214251984047532b..46e21c26fe2f8b975c530dad74f24558b2b1aaaa 100644
--- a/tests/syntax/unroll_const.i
+++ b/tests/syntax/unroll_const.i
@@ -17,44 +17,44 @@ volatile int c;
void main() {
unsigned int i = 0;
- //@ loop pragma UNROLL sizeof(t)/sizeof(t[0]); // 4
+ //@ loop unfold sizeof(t)/sizeof(t[0]); // 4
while (c) {
i++;
}
- //@ loop pragma UNROLL \offset(&s.v.l); // 12
+ //@ loop unfold \offset(&s.v.l); // 12
while (c) {
i++;
}
- //@ loop pragma UNROLL s.i + s.v.l; // 5+0
+ //@ loop unfold s.i + s.v.l; // 5+0
while (c) {
i++;
}
- //@ loop pragma UNROLL \max(t[..]); // 4
+ //@ loop unfold \max(t[..]); // 4
while (c) {
i++;
}
- //@ loop pragma UNROLL \min(t[..]); // 0 because of missing initializer
+ //@ loop unfold \min(t[..]); // 0 because of missing initializer
while (c) {
i++;
}
- //@ loop pragma UNROLL \max(\union(1, 1+s.i)); // 6
+ //@ loop unfold \max(\union(1, 1+s.i)); // 6
while (c) {
i++;
}
- //@ loop pragma UNROLL \min(t[\union(1, 3)]) + \max(t[\union(1, 3)]); // 2+0
+ //@ loop unfold \min(t[\union(1, 3)]) + \max(t[\union(1, 3)]); // 2+0
while (c) {
i++;
}
- //@ loop pragma UNROLL \min(u[..1].i1) * \max(u[..1].i1); // 2*3
+ //@ loop unfold \min(u[..1].i1) * \max(u[..1].i1); // 2*3
while (c) {
i++;
}
@@ -62,5 +62,3 @@ void main() {
}
-
-
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 7747244a7ae8b6e13488bb985d673736de6a9c04..cc85b245b77bb2e776294faefd15b949b7905117 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -7,7 +7,7 @@ enum { SIX = 6 } ;
volatile foo;
void main () {
int j = 0;
- /*@ loop pragma UNROLL "completely", 4; */
+ /*@ loop unfold "completely", 4; */
for (int i=1;i<4;i++) {
switch (i) {
case 1: j+=1; break;
@@ -21,7 +21,7 @@ void main () {
{
int x = 0;
L:
- //@ loop pragma UNROLL 3;
+ //@ loop unfold 3;
while(x<5) {
int y=0;
x++; y++;
@@ -29,13 +29,13 @@ void main () {
}
j = 0;
- //@ loop pragma UNROLL SIX;
+ //@ loop unfold SIX;
while(foo) {
switch(j) {
case -1: j++;
break;
case 0:
- //@ loop pragma UNROLL 3;
+ //@ loop unfold 3;
while (j<5) {j++;}
break;
case 5:
@@ -44,19 +44,19 @@ void main () {
}
}
- {
+ {
if (j==0) goto zero;
if (j==1) goto un;
return;
zero:
- //@ loop pragma UNROLL 3;
+ //@ loop unfold 3;
while (j<5) { un: j++;}
}
}
void main2 () {
- /*@ loop pragma UNROLL 2; */
+ /*@ loop unfold 2; */
for (int i=0;i<2;i++) {
for (int j=0;j<2;j++){
i += 1;
@@ -68,10 +68,10 @@ void main2 () {
}
void main2_done () {
- /*@ loop pragma UNROLL 2;
- @ loop pragma UNROLL "done", 2; */
+ /*@ loop unfold 2;
+ @ loop unfold "done", 2; */
for (int i=0;i<2;i++) {
- /*@ loop pragma UNROLL 2; */
+ /*@ loop unfold 2; */
for (int j=0;j<2;j++){
i += 1;
goto foo;
@@ -84,7 +84,7 @@ void main2_done () {
void main3 (int c) {
int i=0;
if (c == 0) goto foo;
- /*@ loop pragma UNROLL 2; */
+ /*@ loop unfold 2; */
for (;i<5;i++) {
int j = 0 ;
if (i == j) goto foo;
@@ -102,4 +102,3 @@ void main3 (int c) {
up:;
}
}
-
diff --git a/tests/syntax/unroll_property_status_bts1442.i b/tests/syntax/unroll_property_status_bts1442.i
index 0a8970b5b8990d77268c0b7a7e2b8d8f54512e28..a9939128704514da39f2369ed8ed0be0584779fb 100644
--- a/tests/syntax/unroll_property_status_bts1442.i
+++ b/tests/syntax/unroll_property_status_bts1442.i
@@ -7,7 +7,7 @@ int u(void);
char *strcpy(char*dst, char*src) {
char* ldst=dst;
- /*@ loop pragma UNROLL 20; */
+ /*@ loop unfold 20; */
while (*ldst++ = *src++)
;
return dst;
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index f4d949c53ef9a94e93a366b61bbb2a14caf8356c..60bbf94abb1261e78a9178043356b61f68728616 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -6,7 +6,7 @@ PLUGIN: eva,scope,from,inout
typedef char i8; // ideally, pretty-printing should keep 'i8' for some casts
void main() {
- /*@ loop pragma UNROLL 2; */
+ /*@ loop unfold 2; */
for(i8 i=0; i<100; i++) {
i--;
//@ assert i<100;
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 7a203185712a92c869d46f16732c07bfe07cc798..aac454ade3a457ecfb8d55f97b3b578991b02628 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -136,7 +136,7 @@ int main() {
do { } while (09);
#endif
#ifdef UNROLL_PRAGMA
- //@ loop pragma UNROLL 99999999999999999999;
+ //@ loop unfold 99999999999999999999;
#endif
while (nondet);
return 0;
diff --git a/tests/test/adpcm.c b/tests/test/adpcm.c
index 0c8d7e005050cd9ac08c833ebc83666d3bebd5fb..0cbd5960dd71649650af4ec3c55b3c6992f35a40 100644
--- a/tests/test/adpcm.c
+++ b/tests/test/adpcm.c
@@ -272,7 +272,7 @@ int encode(int xin1,int xin2)
tqmf_ptr = tqmf;
xa = (long)(*tqmf_ptr++) * (*h_ptr++);
xb = (long)(*tqmf_ptr++) * (*h_ptr++);
-/*@ loop pragma UNROLL 11; */
+/*@ loop unfold 11; */
/* main multiply accumulate loop for samples and coefficients */
for(i = 0 ; i < 10 ; i++) {
xa += (long)(*tqmf_ptr++) * (*h_ptr++);
@@ -284,7 +284,7 @@ int encode(int xin1,int xin2)
/* update delay line tqmf */
tqmf_ptr1 = tqmf_ptr - 2;
-/*@ loop pragma UNROLL 23; */
+/*@ loop unfold 23; */
for(i = 0 ; i < 22 ; i++) *tqmf_ptr-- = *tqmf_ptr1--;
*tqmf_ptr-- = xin1;
*tqmf_ptr = xin2;
@@ -414,7 +414,7 @@ int filtez(int *bpl,int *dlt)
int i;
long int zl;
zl = (long)(*bpl++) * (*dlt++);
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
for(i = 1 ; i < 6 ; i++)
zl += (long)(*bpl++) * (*dlt++);
@@ -449,7 +449,7 @@ int quantl(int el,int detl)
}*/
mil = 0;
decis = (decis_levl[mil]*(long)detl) >> 15L;
-/*@ loop pragma UNROLL 30; */
+/*@ loop unfold 30; */
while(wd <= decis && mil < 29) { /* FOR/BREAK 662 : 30 possibilities */
mil++;
decis = (decis_levl[mil]*(long)detl) >> 15L;
@@ -502,13 +502,13 @@ void upzero(int dlt,int *dlti,int *bli)
int i,wd2,wd3;
/*if dlt is zero, then no sum into bli */
if(dlt == 0) { /* CONDITION 711 */
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
for(i = 0 ; i < 6 ; i++) {
bli[i] = (int)((255L*bli[i]) >> 8L); /* leak factor of 255/256 */
}
}
else {
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
for(i = 0 ; i < 6 ; i++) {
if((long)dlt*dlti[i] >= 0) wd2 = 128; else wd2 = -128; /* CONDITION 718 : 2exp6 possibs */
wd3 = (int)((255L*bli[i]) >> 8L); /* leak factor of 255/256 */
@@ -603,7 +603,7 @@ int compressed[10]={0};
void main () //(int test_data[10], int compressed[10])
{
int i;
- /*@ loop pragma UNROLL 11; loop widen_hints "all", 32767; */ /* Better bounds: loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */
+ /*@ loop unfold 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/test/oracle/adpcm.res.oracle b/tests/test/oracle/adpcm.res.oracle
index 20799a40a8be991c8d9203ef0536131043d8b2f0..7aff5b9c985a6cf322b88737f9b19592e2828b21 100644
--- a/tests/test/oracle/adpcm.res.oracle
+++ b/tests/test/oracle/adpcm.res.oracle
@@ -1679,10 +1679,10 @@
[inout] Inputs for function filtep:
\nothing
[inout] Out (internal) for function filtez:
- bpl; dlt_0; i; zl; tmp; tmp_0; __retres; tmp_1_unroll_123;
- tmp_2_unroll_123; tmp_1_unroll_126; tmp_2_unroll_126; tmp_1_unroll_129;
- tmp_2_unroll_129; tmp_1_unroll_132; tmp_2_unroll_132; tmp_1_unroll_135;
- tmp_2_unroll_135
+ bpl; dlt_0; i; zl; tmp; tmp_0; __retres; tmp_1_unfold_123;
+ tmp_2_unfold_123; tmp_1_unfold_126; tmp_2_unfold_126; tmp_1_unfold_129;
+ tmp_2_unfold_129; tmp_1_unfold_132; tmp_2_unfold_132; tmp_1_unfold_135;
+ tmp_2_unfold_135
[inout] Inputs for function filtez:
delay_bpl[0..5]; delay_dltx[0..5]; delay_dhx[0..5]; delay_bph[0..5]
[inout] Out (internal) for function logsch:
@@ -1720,28 +1720,28 @@
rlt1; rlt2; detl; deth; sh; eh; dh; ih; nbh; szh; sph; ph; yh;
delay_dhx{[0..1]; [3..5]}; delay_bph[0..5]; ah1; ah2; ph1; ph2; rh1;
rh2; i; h_ptr; tqmf_ptr; tqmf_ptr1; xa; xb; decis; tmp; tmp_0; tmp_1;
- tmp_2; tmp_7; tmp_8; tmp_9; tmp_12; tmp_13; __retres; tmp_3_unroll_8;
- tmp_4_unroll_8; tmp_5_unroll_8; tmp_6_unroll_8; tmp_3_unroll_12;
- tmp_4_unroll_12; tmp_5_unroll_12; tmp_6_unroll_12; tmp_3_unroll_16;
- tmp_4_unroll_16; tmp_5_unroll_16; tmp_6_unroll_16; tmp_3_unroll_20;
- tmp_4_unroll_20; tmp_5_unroll_20; tmp_6_unroll_20; tmp_3_unroll_24;
- tmp_4_unroll_24; tmp_5_unroll_24; tmp_6_unroll_24; tmp_3_unroll_28;
- tmp_4_unroll_28; tmp_5_unroll_28; tmp_6_unroll_28; tmp_3_unroll_32;
- tmp_4_unroll_32; tmp_5_unroll_32; tmp_6_unroll_32; tmp_3_unroll_36;
- tmp_4_unroll_36; tmp_5_unroll_36; tmp_6_unroll_36; tmp_3_unroll_40;
- tmp_4_unroll_40; tmp_5_unroll_40; tmp_6_unroll_40; tmp_3_unroll_44;
- tmp_4_unroll_44; tmp_5_unroll_44; tmp_6_unroll_44; tmp_10_unroll_51;
- tmp_11_unroll_51; tmp_10_unroll_54; tmp_11_unroll_54; tmp_10_unroll_57;
- tmp_11_unroll_57; tmp_10_unroll_60; tmp_11_unroll_60; tmp_10_unroll_63;
- tmp_11_unroll_63; tmp_10_unroll_66; tmp_11_unroll_66; tmp_10_unroll_69;
- tmp_11_unroll_69; tmp_10_unroll_72; tmp_11_unroll_72; tmp_10_unroll_75;
- tmp_11_unroll_75; tmp_10_unroll_78; tmp_11_unroll_78; tmp_10_unroll_81;
- tmp_11_unroll_81; tmp_10_unroll_84; tmp_11_unroll_84; tmp_10_unroll_87;
- tmp_11_unroll_87; tmp_10_unroll_90; tmp_11_unroll_90; tmp_10_unroll_93;
- tmp_11_unroll_93; tmp_10_unroll_96; tmp_11_unroll_96; tmp_10_unroll_99;
- tmp_11_unroll_99; tmp_10_unroll_102; tmp_11_unroll_102; tmp_10_unroll_105;
- tmp_11_unroll_105; tmp_10_unroll_108; tmp_11_unroll_108; tmp_10_unroll_111;
- tmp_11_unroll_111; tmp_10_unroll_114; tmp_11_unroll_114
+ tmp_2; tmp_7; tmp_8; tmp_9; tmp_12; tmp_13; __retres; tmp_3_unfold_8;
+ tmp_4_unfold_8; tmp_5_unfold_8; tmp_6_unfold_8; tmp_3_unfold_12;
+ tmp_4_unfold_12; tmp_5_unfold_12; tmp_6_unfold_12; tmp_3_unfold_16;
+ tmp_4_unfold_16; tmp_5_unfold_16; tmp_6_unfold_16; tmp_3_unfold_20;
+ tmp_4_unfold_20; tmp_5_unfold_20; tmp_6_unfold_20; tmp_3_unfold_24;
+ tmp_4_unfold_24; tmp_5_unfold_24; tmp_6_unfold_24; tmp_3_unfold_28;
+ tmp_4_unfold_28; tmp_5_unfold_28; tmp_6_unfold_28; tmp_3_unfold_32;
+ tmp_4_unfold_32; tmp_5_unfold_32; tmp_6_unfold_32; tmp_3_unfold_36;
+ tmp_4_unfold_36; tmp_5_unfold_36; tmp_6_unfold_36; tmp_3_unfold_40;
+ tmp_4_unfold_40; tmp_5_unfold_40; tmp_6_unfold_40; tmp_3_unfold_44;
+ tmp_4_unfold_44; tmp_5_unfold_44; tmp_6_unfold_44; tmp_10_unfold_51;
+ tmp_11_unfold_51; tmp_10_unfold_54; tmp_11_unfold_54; tmp_10_unfold_57;
+ tmp_11_unfold_57; tmp_10_unfold_60; tmp_11_unfold_60; tmp_10_unfold_63;
+ tmp_11_unfold_63; tmp_10_unfold_66; tmp_11_unfold_66; tmp_10_unfold_69;
+ tmp_11_unfold_69; tmp_10_unfold_72; tmp_11_unfold_72; tmp_10_unfold_75;
+ tmp_11_unfold_75; tmp_10_unfold_78; tmp_11_unfold_78; tmp_10_unfold_81;
+ tmp_11_unfold_81; tmp_10_unfold_84; tmp_11_unfold_84; tmp_10_unfold_87;
+ tmp_11_unfold_87; tmp_10_unfold_90; tmp_11_unfold_90; tmp_10_unfold_93;
+ tmp_11_unfold_93; tmp_10_unfold_96; tmp_11_unfold_96; tmp_10_unfold_99;
+ tmp_11_unfold_99; tmp_10_unfold_102; tmp_11_unfold_102; tmp_10_unfold_105;
+ tmp_11_unfold_105; tmp_10_unfold_108; tmp_11_unfold_108; tmp_10_unfold_111;
+ tmp_11_unfold_111; tmp_10_unfold_114; tmp_11_unfold_114
[inout] Inputs for function encode:
tqmf[0..23]; h[0..23]; xl; xh; il; szl; spl; sl; el;
qq4_code4_table{[1]; [8]; [15]}; delay_bpl[0..5]; delay_dltx[0..5];
diff --git a/tests/value/f2.i b/tests/value/f2.i
index 476765a83d193f2a90332a57d4fa24edb59d940e..88bd0e9b50ac5979f934ad5ede3c98ceef96abb7 100644
--- a/tests/value/f2.i
+++ b/tests/value/f2.i
@@ -1,10 +1,10 @@
/* run.config*
-
+
STDOPT: #"-main f"
*/
int f(int x) {
/* Here we are */
-/*@ loop pragma UNROLL 10; */
+/*@ loop unfold 10; */
while(1) { return 0 ;}
return 2;
}
diff --git a/tests/value/ghost.i b/tests/value/ghost.i
index 6e602983f0bf0cb8d833469da4b37cd393922909..e8836c6e2a8a520d90c0c24f570de756e84da504 100644
--- a/tests/value/ghost.i
+++ b/tests/value/ghost.i
@@ -12,7 +12,7 @@ int main () {
G = 0;
/*@ghost GHOST=G+G ; */
/* Commentaire avant loop */
- /*@ loop pragma UNROLL 0; */
+ /*@ loop unfold 0; */
for(i=0; i<=10; i++)
G++;
diff --git a/tests/value/local_slevel.i b/tests/value/local_slevel.i
index d40c3caf0477abdabcdbefad413537242c25ce91..7c127424f77fc006e54230fd5e7abc64082dea8c 100644
--- a/tests/value/local_slevel.i
+++ b/tests/value/local_slevel.i
@@ -24,7 +24,7 @@ void main1() {
}
void g() {// Do not crash when loop unrolling clears the dependencies of the AST
- //@ loop pragma UNROLL 1;
+ //@ loop unfold 1;
for (int i=0; i<5; i++) {
}
}
diff --git a/tests/value/oracle/local_slevel.res.oracle b/tests/value/oracle/local_slevel.res.oracle
index 2022cd839a084f2561dfe73db96230c219eec2c3..cb2e9dae5e0e8997cc780bf104b75a7fc9185a40 100644
--- a/tests/value/oracle/local_slevel.res.oracle
+++ b/tests/value/oracle/local_slevel.res.oracle
@@ -200,13 +200,13 @@ void main1(void)
void g(void)
{
int i = 0;
- if (! (i < 5)) goto unrolling_2_loop;
+ if (! (i < 5)) goto unfolding_2_loop;
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL 1;
- loop pragma UNROLL "done", 1; */
+ unfolding_3_loop: ;
+ /*@ loop unfold 1;
+ loop unfold "done", 1; */
while (i < 5) i ++;
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return;
}
@@ -266,13 +266,13 @@ void main1(void)
void g(void)
{
int i = 0;
- if (! (i < 5)) goto unrolling_2_loop;
+ if (! (i < 5)) goto unfolding_2_loop;
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL 1;
- loop pragma UNROLL "done", 1; */
+ unfolding_3_loop: ;
+ /*@ loop unfold 1;
+ loop unfold "done", 1; */
while (i < 5) i ++;
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return;
}
@@ -332,13 +332,13 @@ void main1(void)
void g(void)
{
int i = 0;
- if (! (i < 5)) goto unrolling_2_loop;
+ if (! (i < 5)) goto unfolding_2_loop;
i ++;
- unrolling_3_loop: ;
- /*@ loop pragma UNROLL 1;
- loop pragma UNROLL "done", 1; */
+ unfolding_3_loop: ;
+ /*@ loop unfold 1;
+ loop unfold "done", 1; */
while (i < 5) i ++;
- unrolling_2_loop: ;
+ unfolding_2_loop: ;
return;
}
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
index 17a53f17bdc53a87de17f235c7ae66c7f93e46f1..e07c92d0d5dcf8d5efe1fc2b5ae5b8d42e44b112 100644
--- a/tests/value/oracle/strings.res.oracle
+++ b/tests/value/oracle/strings.res.oracle
@@ -69,8 +69,8 @@
Called from strings.i:53.
[eva:alarm] strings.i:23: Warning:
out of bounds write.
- assert \valid(tmp_unroll_46);
- (tmp_unroll_46 from ldst++)
+ assert \valid(tmp_unfold_46);
+ (tmp_unfold_46 from ldst++)
[kernel] strings.i:23: Warning:
all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for strcpy
@@ -387,11 +387,11 @@
[inout] Inputs for function long_chain:
ANYTHING(origin:Unknown)
[inout] Out (internal) for function strcpy:
- src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
- tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
- tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
- tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
- tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
+ src; ldst; b[0..4]; tmp_unfold_46; tmp_1_unfold_46; tmp_0_unfold_46;
+ tmp_unfold_49; tmp_1_unfold_49; tmp_0_unfold_49; tmp_unfold_52;
+ tmp_1_unfold_52; tmp_0_unfold_52; tmp_unfold_55; tmp_1_unfold_55;
+ tmp_0_unfold_55; tmp_unfold_58; tmp_1_unfold_58; tmp_0_unfold_58;
+ tmp_unfold_61; tmp_1_unfold_61; tmp_0_unfold_61
[inout] Inputs for function strcpy:
a[0..5]
[inout] Out (internal) for function string_writes:
@@ -399,8 +399,8 @@
[inout] Inputs for function string_writes:
nondet; s3; s4; s5; s6; cc; "tutu"[bits 0 to 7]
[inout] Out (internal) for function strlen:
- s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
- tmp_unroll_118; tmp_unroll_121
+ s; l; tmp_unfold_106; tmp_unfold_109; tmp_unfold_112; tmp_unfold_115;
+ tmp_unfold_118; tmp_unfold_121
[inout] Inputs for function strlen:
s1[0..5]
[inout] Out (internal) for function string_comparison:
diff --git a/tests/value/oracle/unroll.res.oracle b/tests/value/oracle/unroll.res.oracle
index 7bba5131c292d633f107952fbaf5ded1860b83d2..c36bdf2bce155daeb3624c34432aba55098370b2 100644
--- a/tests/value/oracle/unroll.res.oracle
+++ b/tests/value/oracle/unroll.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing unroll.i (no preprocessing)
[kernel] unroll.i:49: Warning:
- ignoring unrolling directive (not an understood constant expression)
-[kernel] unroll.i:54: Warning: ignoring invalid unrolling directive
+ ignoring unfolding directive (not an understood constant expression)
+[kernel] unroll.i:54: Warning: ignoring invalid unfolding directive
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -32,8 +32,8 @@
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- c; G; i; MAX; JMAX; j; k; S; tmp; tmp_unroll_3752; tmp_unroll_3760;
- tmp_unroll_3768; tmp_unroll_3776; tmp_unroll_3784; tmp_unroll_3792;
- tmp_unroll_3800; tmp_unroll_3808; tmp_unroll_3816; tmp_unroll_3824
+ c; G; i; MAX; JMAX; j; k; S; tmp; tmp_unfold_3752; tmp_unfold_3760;
+ tmp_unfold_3768; tmp_unfold_3776; tmp_unfold_3784; tmp_unfold_3792;
+ tmp_unfold_3800; tmp_unfold_3808; tmp_unfold_3816; tmp_unfold_3824
[inout] Inputs for function main:
\nothing
diff --git a/tests/value/oracle/unroll_simple.res.oracle b/tests/value/oracle/unroll_simple.res.oracle
index c2a14ecd291d27223b0b2cbdd656c3c19ad75c35..503c58f70d4d7da6f10ede70c1c62bf1c38896fc 100644
--- a/tests/value/oracle/unroll_simple.res.oracle
+++ b/tests/value/oracle/unroll_simple.res.oracle
@@ -27,8 +27,8 @@
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
- c; G; i; MAX; JMAX; j; tmp; tmp_unroll_774; tmp_unroll_782; tmp_unroll_790;
- tmp_unroll_798; tmp_unroll_806; tmp_unroll_814; tmp_unroll_822;
- tmp_unroll_830; tmp_unroll_838; tmp_unroll_846
+ c; G; i; MAX; JMAX; j; tmp; tmp_unfold_774; tmp_unfold_782; tmp_unfold_790;
+ tmp_unfold_798; tmp_unfold_806; tmp_unfold_814; tmp_unfold_822;
+ tmp_unfold_830; tmp_unfold_838; tmp_unfold_846
[inout] Inputs for function main:
\nothing
diff --git a/tests/value/strings.i b/tests/value/strings.i
index 0f6087161602aca84fc72009a38b18e5ccb75272..fbb7d4654212d35b89d08a8ad9aca758caa09ab0 100644
--- a/tests/value/strings.i
+++ b/tests/value/strings.i
@@ -19,7 +19,7 @@ char Q, R, S, T, U, V, W, X, Y, Z;
char *strcpy(char*dst, char*src) {
char* ldst=dst;
- /*@ loop pragma UNROLL 20; */
+ /*@ loop unfold 20; */
while (*ldst++ = *src++)
;
return dst;
@@ -27,7 +27,7 @@ char *strcpy(char*dst, char*src) {
unsigned int strlen(char *s) {
unsigned int l=0;
- /*@ loop pragma UNROLL 20; */
+ /*@ loop unfold 20; */
while(*s++ != 0)
l++;
return l;
diff --git a/tests/value/unroll.i b/tests/value/unroll.i
index e85280c3f7a13802263a86e813bf110a7310c1b7..30e8d256760cb5facc015d9c22814914654fac1e 100644
--- a/tests/value/unroll.i
+++ b/tests/value/unroll.i
@@ -5,21 +5,21 @@ void main (int c) {
int MAX = 12;
int JMAX=5;
int j,k,S;
- /*@ loop pragma UNROLL 14; */ // first loop unrolled 14 times
+ /*@ loop unfold 14; */ // first loop unrolled 14 times
for (i=0; i<=MAX; i++)
{
G+=i;
}
- /*@ loop pragma UNROLL 124; */
+ /*@ loop unfold 124; */
for (i=0; i<=10*MAX; i++)
{
G+=i;
}
- /*@ loop pragma UNROLL 12+2; */ // loop unrolled 14 times
+ /*@ loop unfold 12+2; */ // loop unrolled 14 times
for (i=0; i<=MAX; i++)
{
j=0;
- /*@ loop pragma UNROLL FIFTY_TIMES; */
+ /*@ loop unfold FIFTY_TIMES; */
while (j<=JMAX)
{
G+=i;
@@ -27,7 +27,7 @@ void main (int c) {
}
}
-//@ loop pragma UNROLL 128*sizeof(char);
+//@ loop unfold 128*sizeof(char);
do {
G += i;
i++;
@@ -35,7 +35,7 @@ void main (int c) {
}
while (i<=256 || j>=0);
-//@ loop pragma UNROLL 10;
+//@ loop unfold 10;
do
{ if(c) continue;
@@ -45,17 +45,17 @@ void main (int c) {
}
while(c);
-//@ loop pragma UNROLL c;
+//@ loop unfold c;
while(0);
S=1;
k=1;
- //@ loop pragma UNROLL "completly", NB_TIMES;
+ //@ loop unfold "completly", NB_TIMES;
do {
S=S*k;
- k++;
+ k++;
} while (k <= NB_TIMES) ;
-
+
}
#if 0
@@ -69,7 +69,7 @@ int main2(int c,signed char nr_map) {
biosmap = g_biosmap;
if (nr_map<2) return (-1);
-//@ loop pragma UNROLL 200;
+//@ loop unfold 200;
do {
unsigned long long start = biosmap->addr;
unsigned long long size = biosmap->size;
diff --git a/tests/value/unroll_simple.i b/tests/value/unroll_simple.i
index 1a97949fa5cfff01cee54d6547f5a2974d0ae4e5..b0d0ff00e1885936732b34415d446d01e1827c05 100644
--- a/tests/value/unroll_simple.i
+++ b/tests/value/unroll_simple.i
@@ -4,7 +4,7 @@ void main (int c) {
int JMAX=5;
int j=3;
-//@ loop pragma UNROLL 128;
+//@ loop unfold 128;
do {
G += i;
i++;
@@ -12,7 +12,7 @@ void main (int c) {
}
while (i<=256 || j>=0);
-//@ loop pragma UNROLL 10;
+//@ loop unfold 10;
do
{ if(c) continue;
diff --git a/tests/value/with_comment.i b/tests/value/with_comment.i
index 61839445263bd8194a3584407fe62cea50942efc..19fc0e342d7779c387b0d73c03bb4f22220c1e05 100644
--- a/tests/value/with_comment.i
+++ b/tests/value/with_comment.i
@@ -1,5 +1,5 @@
/* run.config*
-
+
STDOPT: #"-main main2"
*/
/* Commentaire avant G comment*/ /* Commentaire avant G2 comment*/
@@ -16,7 +16,7 @@ int main2 () {
G = 0;
/* Commentaire avant loop comment*/
- /*@ loop pragma UNROLL 0; */
+ /*@ loop unfold 0; */
for(i=0; i<=10; i++)
G++;