diff --git a/Changelog b/Changelog
index 1fce0e648c7720200b9138388a449e1b2b6768c1..f94504f038b925e104129f96a39f86f1820d65c0 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,11 @@
Open Source Release <next-release>
###############################################################################
+o! Kernel [2024-09-13] Pragma nodes in the AST have been removed
+- Slicing [2024-09-13] -slice-pragma is now -slice-annot
+- Slicing [2024-09-13] `slice pragma <elem>` is now `slice_preserve_<elem>`
+- Impact [2024-09-13] -impact-pragma is now -impact-annot
+- Impact [2024-09-13] `impact pragma stmt` is now `impact_stmt`
- Kernel [2024-09-03] Place noreturn attribute on types instead of vars
- Alias [2024-08-22] no longer classify virtually all casts as unsafe
o! Kernel [2024-08-08] New Machine module to manage theMachine and machdeps.
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 770627e22ec1fc35553ea74e5755bdbd1fb2d24d..0858a650b5b9ed5ab10b845468d977b3f62b5b82 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -2765,17 +2765,17 @@ module Print: Parameter_sig.Bool
\end{ocamlcode}
Another example is the parameter corresponding to the option
-\texttt{-impact-pragma} of the plug-in \texttt{impact}. This parameter is
-defined by the module \texttt{Pragma} (defined in the file
+\texttt{-impact-annot} of the plug-in \texttt{impact}. This parameter is
+defined by the module \texttt{Annot} (defined in the file
\texttt{src/plugins/impact/options.ml}). It is implemented as follows.
\sscodeidx{Parameter\_sig}{Builder}{Kernel\_function\_set}
\begin{ocamlcode}
-module Pragma =
+module Annot =
Kernel_function_set
(struct
- let option_name = "-impact-pragma"
+ let option_name = "-impact-annot"
let arg_name = "f1, ..., fn"
- let help = "use the impact pragmas in the code of functions f1,...,fn"
+ let help = "use the impact annotations in the code of functions f1,...,fn"
end)
\end{ocamlcode}
Thus it is a set of \texttt{kernel\_function}s initialized by default to
@@ -2785,7 +2785,7 @@ displaying help. The field \texttt{help} is the help message itself. The
Interface for this module is simple:
\scodeidx{Parameter\_sig}{Kernel\_function\_set}
\begin{ocamlcode}
-module Pragma: Parameter_sig.Kernel_function_set
+module Annot: Parameter_sig.Kernel_function_set
\end{ocamlcode}
\end{example}
diff --git a/doc/slicing/user-manual-fr/slicing.tex b/doc/slicing/user-manual-fr/slicing.tex
index a02ac602fcb44e249c37ae4ce71faa2801be1ebe..0b7552514f338f65dab072bd90ef15038c7263f9 100644
--- a/doc/slicing/user-manual-fr/slicing.tex
+++ b/doc/slicing/user-manual-fr/slicing.tex
@@ -49,8 +49,8 @@ effectuer en précisant ce en quoi l'utilisateur est intéressé~:
{\sl select the loop invariants of functions {\tt f1},...,{\tt fn}.}
\item {\tt -slice-loop-var f1,...,fn} :
{\sl select the loop variants of functions {\tt f1},...,{\tt fn}.}
-\item {\tt -slice-pragma f1,...,fn} :
- {\sl use the slicing pragmas in the code of functions {\tt f1},...,{\tt fn} as slicing criteria.}
+\item {\tt -slice-annot f1,...,fn} :
+ {\sl use the slicing annotations in the code of functions {\tt f1},...,{\tt fn} as slicing criteria.}
\item {\tt -slice-return f1,...,fn} :
{\sl select the result (returned value) of functions {\tt f1},...,{\tt fn}.}
@@ -84,30 +84,25 @@ Notons que l'ordre n'intervient pas dans le résultat final.
Les annotations destinées à spécifier des requêtes
de slicing se situe, comme toutes les autres annotations, dans des commentaires
-C commençant par \verb!@!. Leur identification est \verb!slice pragma!,
-et elles sont prises en compte si l'option \verb!-slice-pragma! mentionnée
+C commençant par \verb!@!. Elles sont préfixées par \verb!slice!,
+et elles sont prises en compte si l'option \verb!-slice-annot! mentionnée
ci-dessus est utilisée.\\
Il existe trois requêtes de slicing~:
\begin{quote}
\begin{description}
- \item[]\verb!//@ slice pragma expr! {\it expr\_desc} \verb!;!
+ \item[]\verb!//@ slice_preserve_expr! {\it expr\_desc} \verb!;!
correspond au critère traditionnel de slicing, à savoir préserver le passage
au point de programme et la valeur de l'expression à ce point. Exemple~:
\begin{center}
- \verb!//@slice pragma expr S.a;!
+ \verb!//@slice_preserve_expr S.a;!
\end{center}
- \item[]\verb!//@ slice pragma ctrl;!
+ \item[]\verb!//@ slice_preserve_ctrl;!
permet de s'intéresser uniquement au passage à un point de programme
(sélection des dépendances de contrôle),
- \item[]\verb!//@ slice pragma stmt;!
+ \item[]\verb!//@ slice_preserve_stmt;!
sélectionne l'instruction (et donc de tout ce qui permet de l'atteindre et
de la calculer).
Cette dernière requête est expérimentale.
\end{description}
\end{quote}
-
-
-
-
-
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 537af0103aacfd18826560b0927c959574c9f469..445ecb3af1c68ec02aac544802e0469b9cb2efec 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -142,7 +142,6 @@
"for", (fun _ -> FOR);
"global", (fun _ -> GLOBAL);
"if", (fun _ -> IF);
- "impact", (fun _ -> IMPACT);
"inductive", (fun _ -> INDUCTIVE);
"include", (fun _ -> INCLUDE);
(* ACSL extension for external spec file *)
@@ -159,7 +158,6 @@
(* ACSL extension for model fields *)
"module", (fun _ -> MODULE);
(* ACSL extension for external spec file *)
- "pragma", (fun _ -> PRAGMA);
"predicate", (fun _ -> PREDICATE);
"reads", (fun _ -> READS);
"requires", (fun _ -> REQUIRES);
@@ -167,7 +165,6 @@
"short", (fun _ -> SHORT);
"signed", (fun _ -> SIGNED);
"sizeof", (fun _ -> SIZEOF);
- "slice", (fun _ -> SLICE);
"struct", (fun _ -> STRUCT);
"terminates", (fun _ -> TERMINATES);
"type", (fun _ -> TYPE);
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 79d29dce4a3ee1387a36b0a55fe3cf9af7f7a028..4e8987cc60448820622a9b4d855f9b9e4d432edf 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -270,7 +270,7 @@
%token ALLOCABLE FREEABLE FRESH
%token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK ADMIT SEMICOLON NULL EMPTY
-%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
+%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING FROM
%token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
%token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
@@ -895,7 +895,6 @@ full_identifier:
| FREES { "frees" }
| FUNCTION { "function" }
| GLOBAL { "global" }
-| IMPACT { "impact" }
| INDUCTIVE { "inductive" }
| INCLUDE { "include" }
| INVARIANT { "invariant" }
@@ -905,11 +904,9 @@ full_identifier:
| LOOP { "loop" }
| MODEL { "model" }
| MODULE { "module" }
-| PRAGMA { "pragma" }
| PREDICATE { "predicate" }
| REQUIRES { "requires" }
| RETURNS { "returns" }
-| SLICE { "slice" }
| TERMINATES { "terminates" }
| TYPE { "type" }
| VARIANT { "variant" }
@@ -1322,8 +1319,8 @@ annotation:
Aloop_annot (loc $sloc, l) }
| FOR ne_behavior_name_list COLON contract_or_code_annotation
{ $4 $2 }
-| pragma_or_code_annotation { Acode_annot (loc $sloc,$1) }
-| pragma_or_code_annotation beg_pragma_or_code_annotation
+| code_annotation { Acode_annot (loc $sloc,$1 []) }
+| code_annotation beg_code_annotation
{ raise
(Not_well_formed (loc $sloc,
"Only one code annotation is allowed per comment"))
@@ -1458,9 +1455,7 @@ loop_grammar_extension:
/*** code annotations ***/
-beg_pragma_or_code_annotation:
-| IMPACT {}
-| SLICE {}
+beg_code_annotation:
| FOR {}
| ASSERT {}
| CHECK {}
@@ -1473,12 +1468,6 @@ beg_pragma_or_code_annotation:
| EXT_CODE_ANNOT {}
;
-pragma_or_code_annotation:
-| slice_pragma { APragma (Slice_pragma $1) }
-| impact_pragma { APragma (Impact_pragma $1) }
-| code_annotation { $1 [] }
-;
-
code_annotation:
| ASSERT lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Assert $2) }
@@ -1517,25 +1506,6 @@ code_annotation:
}
;
-slice_pragma:
-| SLICE PRAGMA any_identifier lexpr SEMICOLON
- { if $3 = "expr" then SPexpr $4
- else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
-| SLICE PRAGMA any_identifier SEMICOLON
- { if $3 = "ctrl" then SPctrl
- else if $3 = "stmt" then SPstmt
- else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
-;
-
-impact_pragma:
-| IMPACT PRAGMA any_identifier lexpr SEMICOLON
- { if $3 = "expr" then IPexpr $4
- else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
-| IMPACT PRAGMA any_identifier SEMICOLON
- { if $3 = "stmt" then IPstmt
- else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
-;
-
/*** declarations and logical definitions ***/
decl_list:
@@ -1955,7 +1925,6 @@ is_acsl_decl_or_code_annot:
| CHECK { "check" }
| ADMIT { "admit" }
| GLOBAL { "global" }
-| IMPACT { "impact" }
| INDUCTIVE { "inductive" }
| INVARIANT { "invariant" }
| ADMIT_INVARIANT { "admit invariant" }
@@ -1966,9 +1935,7 @@ is_acsl_decl_or_code_annot:
| LOOP { "loop" }
| ADMIT_LOOP { "admit loop" }
| CHECK_LOOP { "check loop" }
-| PRAGMA { "pragma" }
| PREDICATE { "predicate" }
-| SLICE { "slice" }
| TYPE { "type" }
| MODEL { "model" }
| AXIOM { "axiom" }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8317846aaa3afd18818c62b2c846b9d249e2b6e8..4bc7199b1bedb2b59684124bda7553ac9e29bffc 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9823,7 +9823,6 @@ and doBody local_env (blk: Cabs.block) : chunk =
(fun x -> x.Logic_ptree.b_name)
s.Logic_ptree.spec_behavior,
true
- | CODE_ANNOT(Logic_ptree.APragma _,_) -> [], true
| CODE_ANNOT
(Logic_ptree.AExtended(_,is_loop,(name,_)),loc) ->
let source = fst loc in
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index d7c54a7de7794c97971f49d2583fb3ab05846771..6a5bb2caf6c7c787a94beeb7079e78908c65524e 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -363,7 +363,7 @@ let xform_switch_block ?(keepSwitch=false) b =
let assert_of_clause f ca =
match ca.annot_content with
| AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _ | APragma _ | AExtended _ -> Logic_const.ptrue
+ | AAssigns _ | AAllocation _ | AExtended _ -> Logic_const.ptrue
| AStmtSpec (_bhv,s) ->
let open Logic_const in
List.fold_left
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index c514e9754880be110af5a5e4faf9d1d29bad1c64..6f805da8dae22ea573d8f57a5f9c0b26090a3741 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -242,7 +242,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
let assert_of_returns ca =
match ca.annot_content with
| AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _ | APragma _ | AExtended _ -> ptrue
+ | AAssigns _ | AAllocation _ | AExtended _ -> ptrue
| AStmtSpec (_bhvs,s) ->
let res =
List.fold_left
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index d416534d0ac42e7254ced76c440c4a2831b0e976..57de8321c4952ae06bffd6e5fe65b7bca5b7f7fb 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -31,6 +31,49 @@ let not_yet_implemented = ref ""
term depends. *)
let compute_term_deps = ref (fun _stmt _expr -> None)
+
+(* Register slice ACSL extensions:Â these are directives for the slicing plugin,
+ but they are processed in this file so we also register them here. *)
+let () =
+ let typer typing_context loc args =
+ match args with
+ | [] -> Ext_terms []
+ | _ -> typing_context.Logic_typing.error loc "Invalid slice directive"
+ in
+ Acsl_extension.register_code_annot_next_stmt
+ ~plugin:"slicing" "slice_preserve_stmt" typer false;
+ Acsl_extension.register_code_annot
+ ~plugin:"slicing" "slice_preserve_ctrl" typer false;
+ let expr_typer typing_context loc args =
+ match args with
+ | [] -> typing_context.Logic_typing.error loc "Invalid slice directive"
+ | _ ->
+ let type_term =
+ let open Logic_typing in
+ typing_context.type_term typing_context typing_context.pre_state
+ in
+ Ext_terms (List.map type_term args)
+ in
+ Acsl_extension.register_code_annot
+ ~plugin:"slicing" "slice_preserve_expr" expr_typer false
+
+type slice_directive = Stmt | Ctrl | Terms of term list
+
+let slice_directive acsl_extension =
+ match acsl_extension.ext_name with
+ | "slice_preserve_stmt" -> Some Stmt
+ | "slice_preserve_ctrl" -> Some Ctrl
+ | "slice_preserve_expr" ->
+ begin
+ match acsl_extension.ext_kind with
+ | Ext_terms terms -> Some (Terms terms)
+ | _ -> assert false
+ end
+ | _ -> None
+
+let is_slice_directive acsl_ext = Option.is_some (slice_directive acsl_ext)
+
+
type ctx = {
site: ctx_site;
before: bool option;
@@ -42,7 +85,7 @@ and ctx_site =
| StatementContract of stmt
| StatementAnnotation of stmt
-type pragmas = {ctrl: Stmt.Set.t ; stmt: Stmt.Set.t}
+type slices = {ctrl: Stmt.Set.t ; stmt: Stmt.Set.t}
type t = {before:bool ; ki:stmt ; zone:Locations.Zone.t}
type zone_info = (t list) option
type decl = {var: Varinfo.Set.t ; lbl: Logic_label.Set.t}
@@ -57,18 +100,18 @@ let mk_ctx_stmt_annot kf stmt =
{ before=Some true; site=StatementAnnotation stmt; kf }
type result = {
- pragmas: pragmas;
+ slices: slices;
locals: Varinfo.Set.t;
labels: Logic_label.Set.t;
zones: (Locations.Zone.t * Locations.Zone.t) Stmt.Map.t option;
}
-let empty_pragmas =
+let empty_slices =
{ ctrl = Stmt.Set.empty;
stmt = Stmt.Set.empty }
let empty_results = {
- pragmas = empty_pragmas;
+ slices = empty_slices;
locals = Varinfo.Set.empty;
labels = Logic_label.Set.empty;
zones = Some Stmt.Map.empty;
@@ -117,7 +160,7 @@ let get_result result =
zones, {var = result.locals; lbl = result.labels}
let get_annot_result result =
- get_result result, result.pragmas
+ get_result result, result.slices
(** Logic_var utility: *)
let extract_locals logicvars =
@@ -387,14 +430,14 @@ let populate_zone ctx visit cil_node current_zones =
with NYI msg ->
add_top_zone msg (vis#get_zones)
-let update_pragmas f results =
- { results with pragmas = f results.pragmas }
+let update_slices f results =
+ { results with slices = f results.slices }
-let add_ctrl_pragma stmt =
- update_pragmas (fun x -> { x with ctrl = Stmt.Set.add stmt x.ctrl })
+let add_ctrl_slice stmt =
+ update_slices (fun x -> { x with ctrl = Stmt.Set.add stmt x.ctrl })
-let add_stmt_pragma stmt =
- update_pragmas (fun x -> { x with stmt = Stmt.Set.add stmt x.stmt })
+let add_stmt_slice stmt =
+ update_slices (fun x -> { x with stmt = Stmt.Set.add stmt x.stmt })
let add_results_from_term ctx results t =
let zones = populate_zone ctx Visitor.visitFramacTerm t results.zones in
@@ -447,23 +490,14 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
let get_zone_from_term k term results =
let ctx = mk_ctx_stmt_annot kf k in
add_results_from_term ctx results term
+ and get_zone_from_term_list k terms results =
+ let ctx = mk_ctx_stmt_annot kf k in
+ List.fold_left (add_results_from_term ctx) results terms
and get_zone_from_pred k pred results =
let ctx = mk_ctx_stmt_annot kf k in
add_results_from_pred ctx results pred
in
match a.annot_content with
- | APragma (Slice_pragma (SPexpr term) | Impact_pragma (IPexpr term)) ->
- results |>
- (* to preserve the interpretation of the pragma *)
- get_zone_from_term ki term |>
- (* to select the reachability of the pragma *)
- add_ctrl_pragma ki
- | APragma (Slice_pragma SPctrl) ->
- (* to select the reachability of the pragma *)
- add_ctrl_pragma ki results
- | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) ->
- (* to preserve the effect of the statement *)
- add_stmt_pragma ki results
| AAssert (_behav,pred) ->
(* to preserve the interpretation of the assertion *)
get_zone_from_pred ki pred.tp_statement results
@@ -500,25 +534,44 @@ 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")
+ | AExtended (_, _, acsl_extension) ->
+ begin
+ match slice_directive acsl_extension with
+ | Some Stmt ->
+ (* to preserve the effect of the statement *)
+ add_stmt_slice ki results
+ | Some Ctrl ->
+ (* to select the reachability of the slice directive *)
+ add_ctrl_slice ki results
+ | Some (Terms terms) ->
+ results |>
+ (* to preserve the interpretation of the term *)
+ get_zone_from_term_list ki terms |>
+ (* to select the reachability of the directive *)
+ add_ctrl_slice ki
+ | None ->
+ match acsl_extension.ext_kind with
+ | 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
+ | 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
+ | _ -> raise (NYI "[logic_interp] extension")
+ end
+
(* Used by annotations entry points. *)
let get_from_stmt_annots code_annot_filter ((ki, _kf) as stmt) results =
@@ -568,9 +621,8 @@ let from_func_annots iter_on_kf_stmt code_annot_filter kf =
get_annot_result !results
(** To quickly build a annotation filter *)
-let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ~others =
+let code_annot_filter annot ~threat ~user_assert ~slicing_annot ~loop_inv ~loop_var ~others =
match annot.annot_content with
- | APragma (Slice_pragma _) -> slicing_pragma
| AAssert _ ->
(match Alarms.find annot with
| None -> user_assert
@@ -580,8 +632,8 @@ let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop
| AInvariant(_,false,_) -> others
| AAllocation _ -> others
| AAssigns _ -> others
- | APragma (Impact_pragma _) -> others
- | AStmtSpec _ | AExtended _ (* TODO *) -> false
+ | AExtended (_, _, ext) when is_slice_directive ext -> slicing_annot
+ | AStmtSpec _ | AExtended _ (* TODO *) -> false
exception Prune
diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli
index d0db985efe97c93227a17e39c029cbfcf70a5eed..39710de35f18c9a8656345cdca886abd57419a06 100644
--- a/src/kernel_services/analysis/logic_deps.mli
+++ b/src/kernel_services/analysis/logic_deps.mli
@@ -24,6 +24,9 @@ open Cil_types
val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
+(** Is an ACSL extension a directive for the slicing plug-in? *)
+val is_slice_directive: acsl_extension -> bool
+
type ctx
val mk_ctx_func_contract: ?before:bool -> kernel_function -> ctx
@@ -45,9 +48,11 @@ type zone_info = (t list) option
type decl = {var: Cil_datatype.Varinfo.Set.t ; (* related to vars of the annot *)
lbl: Cil_datatype.Logic_label.Set.t} (* related to labels of the annot *)
-type pragmas =
- {ctrl: Cil_datatype.Stmt.Set.t ; (* related to //@ slice pragma ctrl/expr *)
- stmt: Cil_datatype.Stmt.Set.t}
+
+(** Related to slice directives slice_preserve_stmt and slice_preserve_ctrl *)
+type slices =
+ { ctrl: Cil_datatype.Stmt.Set.t;
+ stmt: Cil_datatype.Stmt.Set.t }
val from_term: term -> ctx -> zone_info * decl
(** Entry point to get zones needed to evaluate the [term] relative to
@@ -67,26 +72,26 @@ val from_preds: predicate list -> ctx -> zone_info * decl
val from_stmt_annot:
code_annotation -> stmt * kernel_function ->
- (zone_info * decl) * pragmas
+ (zone_info * decl) * slices
(** Entry point to get zones needed to evaluate an annotation on the
given stmt. *)
val from_stmt_annots:
(code_annotation -> bool) option ->
- stmt * kernel_function -> (zone_info * decl) * pragmas
+ stmt * kernel_function -> (zone_info * decl) * slices
(** Entry point to get zones needed to evaluate annotations of this
[stmt]. *)
val from_func_annots:
((stmt -> unit) -> kernel_function -> unit) ->
(code_annotation -> bool) option ->
- kernel_function -> (zone_info * decl) * pragmas
+ kernel_function -> (zone_info * decl) * slices
(** Entry point to get zones
needed to evaluate annotations of this [kf]. *)
val code_annot_filter:
code_annotation ->
- threat:bool -> user_assert:bool -> slicing_pragma:bool ->
+ threat:bool -> user_assert:bool -> slicing_annot:bool ->
loop_inv:bool -> loop_var:bool -> others:bool -> bool
(** To quickly build an annotation filter *)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 44e170a706037d3d1d0a4f36b195dba00521578a..db1b59e51d962777c8b56d9aee89a83b27ae068d 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1637,7 +1637,7 @@ let do_add_code_annot ~keep_empty emitter ?kf stmt ca =
Kernel.fatal
"More than one loop assigns clause for a statement. \
Annotations internal state broken.")
- | APragma _ | AExtended _ ->
+ | AExtended _ ->
fill_tables ca (Property.ip_of_code_annot kf stmt ca)
let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 185a7fa68fe5f8f67c3219062965e23866e6e546..e144f4363dab7a06b41b6e72937efaf958a754b0 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1737,21 +1737,6 @@ and behavior = {
(** extensions *)
}
-(** Pragmas for the slicing plugin of Frama-C. *)
-and slice_pragma =
- | SPexpr of term
- | SPctrl
- | SPstmt
-
-(** Pragmas for the impact plugin of Frama-C. *)
-and impact_pragma =
- | IPexpr of term
- | IPstmt
-
-(** The various kinds of pragmas. *)
-and pragma =
- | Slice_pragma of slice_pragma
- | Impact_pragma of impact_pragma
(** all annotations that can be found in the code.
This type shares the name of its constructors with
@@ -1784,7 +1769,6 @@ and code_annotation_node =
At most one clause associated to a given (statement, behavior) couple.
@since Oxygen-20120901 when [b_allocation] has been added. *)
- | APragma of pragma (** pragma. *)
| AExtended of string list * bool * acsl_extension
(** extension in a code or loop annotation.
Boolean flag is true for loop extensions and false for code extensions
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 4789db180f66dcdf1ec164bde8bea36fa34bbfa3..1e5f0f1fdd9386c51f91aed243da5b9cc0b87773 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -419,7 +419,7 @@ let get_for_behaviors = function
| AStmtSpec(bhvs,_)
| AAssigns(bhvs,_)
| AAllocation(bhvs,_) -> bhvs
- | AVariant _ | APragma _ | AExtended _ -> []
+ | AVariant _ | AExtended _ -> []
end
| IPAxiomatic _
@@ -445,7 +445,6 @@ let has_status_ca = function
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAllocation _
| AAssigns _ -> true
| AExtended(_,_,e) -> has_status_ext e
- | APragma _ -> false
let has_status_pkind = function
| PKAssumes _ -> false
@@ -804,7 +803,6 @@ module Ordered_by_function = Datatype.Make_with_collections(
| IPPredicate { ip_kind = PKEnsures _ } -> 10
| IPCodeAnnot { ica_ca = { annot_content = AAssert _ }} -> 11
| IPCodeAnnot { ica_ca = { annot_content = AInvariant _ }} -> 12
- | IPCodeAnnot { ica_ca = { annot_content = APragma _ }} -> 13
| IPAssigns _ -> 14
| IPFrom _ -> 15
| IPAllocation _ -> 16
@@ -1184,8 +1182,6 @@ struct
| IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca={annot_content=AStmtSpec _}} ->
[ K kf ; A "contract" ; S stmt ]
- | IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca={annot_content=APragma _}} ->
- [ K kf ; A "pragma" ; S stmt ]
| IPCodeAnnot {ica_kf=kf; ica_stmt=stmt;
ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
[ K kf ; A ext_name ; S stmt ]
@@ -1468,9 +1464,6 @@ let ip_of_code_annot kf stmt ca =
| AAssigns _ ->
Option.to_list (ip_assigns_of_code_annot kf ki ca)
@ ip_from_of_code_annot kf ki ca
- | APragma p when Logic_utils.is_property_pragma p ->
- [ IPCodeAnnot {ica_kf=kf; ica_stmt=stmt; ica_ca=ca} ]
- | APragma _ -> []
| AExtended(_,_,ext) ->
if ext.ext_has_status then
[IPExtended {ie_loc=ELStmt(kf,stmt); ie_ext=ext}]
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 90d5044211b9ed9383c2cc9e4f3b3b10ad8402b0..f957ff21d99f3e8d5abbc80724f86eebd5427c3e 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -47,7 +47,7 @@ type behavior_or_loop = (* private *)
based on different sets of active behaviors. *)
| Id_loop of code_annotation
-(** Only AAssert, AInvariant, or APragma. Other code annotations are
+(** Only AAssert or AInvariant. Other code annotations are
dispatched as identified_property of their own. *)
type identified_code_annotation = {
ica_kf : kernel_function;
@@ -479,7 +479,7 @@ val ip_of_code_annot:
(** Builds the IP related to the code annotation.
should be used only on code annotations returning a single ip, i.e.
- assert, invariant, variant, pragma.
+ assert, invariant, variant.
@raise Invalid_argument if the resulting code annotation has an empty set
of identified property
@since Carbon-20110201 *)
@@ -499,7 +499,7 @@ val ip_of_global_annotation_single:
val has_status: identified_property -> bool
(** Does the property has a logical status (which may be Never_tried)?
- False for pragma, assumes clauses and some ACSL extensions.
+ False for assumes clauses and some ACSL extensions.
@since 19.0-Potassium *)
val get_kinstr: identified_property -> kinstr
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 31ead251dbcb14e5a00811a67dd84fe604fadf9e..75c2da8a093025837852d9a46bbc43b64ae07202 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3180,14 +3180,6 @@ class cil_printer () = object (self)
(pp_list nl_complete self#complete_behaviors) complete
(pp_list false self#disjoint_behaviors) disjoint
- method private slice_pragma fmt = function
- |SPexpr t -> fprintf fmt "expr @[%a@]" self#term t
- | SPctrl -> Format.pp_print_string fmt "ctrl"
- | SPstmt -> Format.pp_print_string fmt "stmt"
-
- method private impact_pragma fmt = function
- | IPexpr t -> fprintf fmt "expr @[%a@]" self#term t
- | IPstmt -> Format.pp_print_string fmt "stmt"
(* TODO: add the annot ID in debug mode?*)
method code_annotation fmt ca =
@@ -3205,14 +3197,6 @@ class cil_printer () = object (self)
pp_for_behavs behav
self#pp_acsl_keyword (string_of_assert p.tp_kind)
self#predicate p.tp_statement
- | APragma (Slice_pragma sp) ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword "slice pragma"
- self#slice_pragma sp
- | APragma (Impact_pragma sp) ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword "impact pragma"
- self#impact_pragma sp
| 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 f5892672e43757632789c1ed84c89334b32060a4..12e2557c25673e2f412019ae8ad0207db1f2a6f4 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -929,21 +929,6 @@ and pp_termination_kind fmt = function
| Continues -> Format.fprintf fmt "Continues"
| Returns -> Format.fprintf fmt "Returns"
-and pp_slice_pragma fmt = function
- | SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
- | SPctrl -> Format.fprintf fmt "SPctrl"
- | SPstmt -> Format.fprintf fmt "SPstmt"
-
-and pp_impact_pragma fmt = function
- | IPexpr(term) -> Format.fprintf fmt "IPexpr(%a)" pp_term term
- | IPstmt -> Format.fprintf fmt "IPstmt"
-
-and pp_pragma fmt = function
- | Slice_pragma(term) ->
- Format.fprintf fmt "Slice_pragma(%a)" pp_slice_pragma term
- | Impact_pragma(term) ->
- Format.fprintf fmt "Impact_pragma(%a)" pp_impact_pragma term
-
and pp_code_annotation_node fmt = function
| AAssert(string_list,p) ->
Format.fprintf fmt "AAssert(%a,%a)"
@@ -962,8 +947,6 @@ and pp_code_annotation_node fmt = function
| AAllocation(string_list,allocation) ->
Format.fprintf fmt "AAllocation(%a,%a)" (pp_list pp_string) string_list
pp_allocation allocation
- | APragma(pragma) ->
- Format.fprintf fmt "APragma(%a)" pp_pragma pragma
| AExtended(string_list,is_loop,acsl_extension) ->
Format.fprintf fmt "AExtended(%a,%B,%a)"
(pp_list pp_string) string_list is_loop pp_acsl_extension acsl_extension
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index 7cc180218f31b1bd248acdd32dc140321372fea9..dea0ff2b9283d65eb132df06a7186fcf4b01f9db 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -140,12 +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_slice_pragma :
- Format.formatter -> Cil_types.slice_pragma -> unit
-val pp_impact_pragma :
- Format.formatter -> Cil_types.impact_pragma -> unit
-val pp_pragma :
- Format.formatter -> Cil_types.pragma -> unit
val pp_code_annotation_node :
Format.formatter -> Cil_types.code_annotation_node -> unit
val pp_funspec : Format.formatter -> Cil_types.funspec -> unit
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 53d007c1f2dc87132ae953d738b5068e3faa4a0d..ab7ccf849a401267dd85d551593fafb5c2775f68 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -126,7 +126,6 @@ let pp_code_annot fmt ca =
Format.fprintf fmt "invariant%a%a" pp_for bs pp_top tp
| AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
| AAllocation(bs,_) -> Format.fprintf fmt "allocates_frees%a" pp_for bs
- | APragma _ -> Format.pp_print_string fmt "pragma"
| AVariant _ -> Format.pp_print_string fmt "variant"
| AStmtSpec _ -> Format.pp_print_string fmt "block contract"
| AExtended _ -> Format.pp_print_string fmt "extension"
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 8eb0730f39d8f72b13c4bec441b2b97e141ab92c..aeba051d5cd8d428079a2888c9794c4bc94ddbf6 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -450,22 +450,6 @@ let print_spec fmt spec =
~sep:"@\n" ~suf:"@\n" (pp_list ~sep:",@ " pp_print_string))
spec.spec_disjoint_behaviors
-let print_slice_pragma fmt p =
- match p with
- | SPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
- | SPctrl -> pp_print_string fmt "ctrl"
- | SPstmt -> pp_print_string fmt "stmt"
-
-let print_impact_pragma fmt p =
- match p with
- | IPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
- | IPstmt -> pp_print_string fmt "stmt"
-
-let print_pragma fmt p =
- match p with
- | Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
- | Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
-
let print_extension fmt (name, ext) =
fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
@@ -494,7 +478,6 @@ let print_code_annot fmt ca =
fprintf fmt "%aloop@ %a" print_behaviors bhvs print_assigns a
| AAllocation (bhvs,fa) ->
fprintf fmt "%a%a" print_behaviors bhvs (print_allocation ~isloop:true) fa
- | APragma p -> print_pragma fmt p
| AExtended (bhvs, is_loop, e) ->
fprintf fmt "%a%s%a"
print_behaviors bhvs
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 7c50dafb7adbc9f6fec297c626b63d1495ef7077..dd9d31dca5152467450b0a5f4459abb2946c960b 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -74,12 +74,9 @@ let compare_annotations la1 la2 =
| AAllocation _, AAllocation _ -> total_order
| AAllocation _, _ -> -1
- | AVariant _, (APragma _ | AExtended _) -> -1
+ | AVariant _, AExtended _ -> -1
| AVariant _, AVariant _ -> total_order
| AVariant _, _ -> 1
- | APragma _, AExtended _ -> -1
- | APragma _, APragma _ -> total_order
- | APragma _, _ -> 1
| AExtended _, AExtended _ -> total_order
| AExtended _, _ -> 1
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index b849b8f00b613b59d8d9d04d9e29bbbeb10fde06..f23eb2643d9d177222152c0621f0b10dcc1f40fa 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -823,10 +823,7 @@ struct
method! code_annotation fmt ca =
match ca.annot_content with
- | APragma p when not (Logic_utils.is_property_pragma p) ->
- (* Not currently localizable. Will be linked to the next stmt *)
- super#code_annotation fmt ca
- | AAssert _ | AInvariant _ | APragma _ | AVariant _ ->
+ | AAssert _ | AInvariant _ | AVariant _ ->
let ip =
Property.ip_of_code_annot_single
(Option.get self#current_kf)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index af74c4dd1fe05e464c10874b8088be4c8f54379a..9dc42b8d8cfa752ef4fa4d1e0c7d7cc3ce097da3 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -713,25 +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_slice_pragma p p' env =
- match p, p' with
- | SPexpr t, SPexpr t' -> is_same_term t t' env
- | SPctrl, SPctrl -> true
- | SPstmt, SPstmt -> true
- | (SPexpr _ | SPctrl | SPstmt), _ -> false
-
-and is_same_impact_pragma p p' env =
- match p, p' with
- | IPexpr t, IPexpr t' -> is_same_term t t' env
- | IPstmt, IPstmt -> true
- | (IPexpr _ | IPstmt), _ -> false
-
-and is_same_pragma p p' env =
- match p,p' with
- | 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
- | (Slice_pragma _ | Impact_pragma _), _ -> false
-
and are_same_behaviors bhvs bhvs' env =
let treat_one_behavior acc b =
match List.partition (fun b' -> b.b_name = b'.b_name) acc with
@@ -769,13 +750,12 @@ and is_same_code_annotation a a' env =
is_same_behavior_set bhvs bhvs' && is_same_assigns a a' env
| AAllocation(bhvs, a), AAllocation(bhvs',a') ->
is_same_behavior_set bhvs bhvs' && is_same_allocation a a' env
- | APragma p, APragma p' -> is_same_pragma p p' env
| AExtended (bhvs, is_next, ext),
AExtended (bhvs', is_next', ext') ->
is_same_behavior_set bhvs bhvs' && is_next = is_next' &&
is_same_acsl_extension ext ext' env
| (AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAssigns _
- | AAllocation _ | APragma _ | AExtended _), _ -> false
+ | AAllocation _ | AExtended _), _ -> false
and is_same_logic_type t t' env =
match t,t' with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a35aaa54e6cddf0b9a3bf8cbeea3abfc0a423efe..1b3ace6387f1f46102ea851ef3dc07653c483e40 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -874,9 +874,6 @@ class type cilVisitor = object
method vallocation:
allocation -> allocation visitAction
- method vslice_pragma: slice_pragma -> slice_pragma visitAction
- method vimpact_pragma: impact_pragma -> impact_pragma visitAction
-
method vdeps:
deps -> deps visitAction
@@ -1009,9 +1006,6 @@ class internal_genericCilVisitor current_func behavior queue: cilVisitor =
method vallocates _s = DoChildren
method vallocation _s = DoChildren
- method vslice_pragma _ = DoChildren
- method vimpact_pragma _ = DoChildren
-
method vdeps _ = DoChildren
method vfrom _ = DoChildren
@@ -1088,7 +1082,7 @@ let flatten_transient_sub_blocks b =
| None -> false
| Some {
skind =
- Instr (Code_annot ({ annot_content = AStmtSpec _ | APragma _}, _))}
+ Instr (Code_annot ({ annot_content = AStmtSpec _ }, _))}
-> true
| Some _ -> false
in
@@ -1835,22 +1829,6 @@ and childrenSpec vis s =
*)
s
-and visitCilSlicePragma vis p =
- doVisitCil vis id vis#vslice_pragma childrenSlicePragma p
-
-and childrenSlicePragma vis p =
- match p with
- | SPexpr t ->
- let t' = visitCilTerm vis t in if t' != t then SPexpr t' else p
- | SPctrl | SPstmt -> p
-
-and visitCilImpactPragma vis p =
- doVisitCil vis id vis#vimpact_pragma childrenImpactPragma p
-
-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 childrenModelInfo vis m =
let field_type = visitCilLogicType vis m.mi_field_type in
let base_type = visitCilType vis m.mi_base_type in
@@ -1963,12 +1941,6 @@ and childrenCodeAnnot vis ca =
let p' = vPred p in if p' != p then
change_content (AAssert (behav,p'))
else ca
- | APragma (Impact_pragma t) ->
- let t' = visitCilImpactPragma vis t in
- if t' != t then change_content (APragma (Impact_pragma t')) else ca
- | APragma (Slice_pragma t) ->
- let t' = visitCilSlicePragma vis t in
- if t' != t then change_content (APragma (Slice_pragma t')) 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 a7a2f7f0eaa4b1a98be5b6701bfba2583e1da453..11091f7b46289dc1da5ae667de797d0c4c54d2ac 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1918,9 +1918,6 @@ class type cilVisitor = object
method vallocation: allocation -> allocation visitAction
(** @since Oxygen-20120901 *)
- method vslice_pragma: slice_pragma -> slice_pragma visitAction
- method vimpact_pragma: impact_pragma -> impact_pragma visitAction
-
method vdeps: deps -> deps visitAction
method vfrom: from -> from visitAction
method vcode_annot: code_annotation -> code_annotation visitAction
@@ -2043,11 +2040,11 @@ val visitCilBlock: cilVisitor -> block -> block
(** Mark the given block as candidate to be flattened into its parent block,
after returning from its visit. This is not systematic, as the environment
might prevent it (e.g. if the preceding statement is a statement contract
- or a slicing/pragma annotation, or if there are labels involved). Use
- that whenever you're creating a block in order to hold multiple statements
- as a result of visiting a single statement. If the block contains local
- variables, it will not be marked as transient, since removing it will
- change the scope of those variables.
+ or if there are labels involved).
+ Use that whenever you're creating a block in order to hold multiple
+ statements as a result of visiting a single statement. If the block
+ contains local variables, it will not be marked as transient, since
+ removing it will change the scope of those variables.
@raise Fatal error if the given block attempts to declare local variables
and contain definitions of local variables that are not part of the block.
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 799e52d1780be8acb3b81c5e2cea92f2c4bf2abe..f11de6f809ec1404417c390aa3bfab294568466b 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2471,7 +2471,7 @@ module Code_annotation = struct
| AAssert(_,{ tp_statement = {pred_loc=loc}})
| AInvariant(_,_,{tp_statement = {pred_loc=loc}})
| AVariant({term_loc=loc},_) -> Some loc
- | AAssigns _ | AAllocation _ | APragma _ | AExtended _
+ | AAssigns _ | AAllocation _ | AExtended _
| AStmtSpec _ -> None
end
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 0c6abfa91eee04c1aebe5455b06b9903ffebdca2..855cce6149e5c8ddf39243b88212fb84162cc3d9 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -651,7 +651,7 @@ module Base_checker = struct
"%s is not a code annotation extension" ext_name);
my_labels)
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _ | APragma _ -> my_labels
+ | AAssigns _ | AAllocation _ -> my_labels
in
logic_labels <- my_labels @ logic_labels;
(* on non-normalized code, we can't really check the scope of behavior
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index a537c6ab681949f36b0ae11f1cef72af5892d371..5b66f11b696ed3809673e9bd66235797a7df8f05 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -106,7 +106,7 @@ let refresh_spec s =
let refresh_code_annotation annot =
let content =
match annot.annot_content with
- | AAssert _ | AInvariant _ | AAllocation _ | AVariant _ | APragma _
+ | AAssert _ | AInvariant _ | AAllocation _ | AVariant _
| AExtended _ as c -> c
| AStmtSpec(l,spec) -> AStmtSpec(l, refresh_spec spec)
| AAssigns(l,a) -> AAssigns(l, refresh_assigns a)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 7fbbc120b5405515bcdc851714bce589bc832134..2d75c19ccdfa05074319c0587459e1b23cdb4f82 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3834,15 +3834,6 @@ struct
List.fold_left add_formal env formals
in type_spec old_behaviors vi.vdecl false log_return_typ env s
- let slice_pragma env = function
- SPexpr t -> Cil_types.SPexpr (term env t)
- | SPctrl -> Cil_types.SPctrl
- | SPstmt -> Cil_types.SPstmt
-
- let impact_pragma env = function
- IPexpr t -> Cil_types.IPexpr (term env t)
- | IPstmt -> Cil_types.IPstmt
-
let code_annot_env () =
let env = append_here_label (append_pre_label (append_init_label
(Lenv.empty()))) in
@@ -3860,12 +3851,6 @@ struct
let p = predicate (code_annot_env()) p in
let p = Logic_const.toplevel_predicate ~kind p in
Cil_types.AAssert(behav,p)
- | APragma (Impact_pragma sp) ->
- Cil_types.APragma
- (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
- | APragma (Slice_pragma sp) ->
- Cil_types.APragma
- (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
| 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 690e9c8def3c19e111e4d27f3a62ec67a2cf9760..4fbd3210b4737feca4e9ad1d7cfe8046d17a4fc4 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -714,7 +714,7 @@ let is_trivially_true p =
let is_annot_next_stmt c =
match c.annot_content with
- | AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) -> true
+ | AStmtSpec _ -> true
| AExtended(_,is_loop,{ext_name}) ->
let warn_not_a_code_annot () =
Kernel.(
@@ -728,10 +728,7 @@ let is_annot_next_stmt c =
| Ext_code_annot Ext_next_both-> not is_loop
| Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
| AAssert _ | AInvariant _ | AVariant _
- | AAssigns _ | AAllocation _
- | APragma (Slice_pragma (SPctrl | SPexpr _))
- | APragma (Impact_pragma (IPexpr _))
- -> false
+ | AAssigns _ | AAllocation _ -> false
let rec add_attribute_glob_annot a g =
match g with
@@ -1176,24 +1173,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_slice_pragma p1 p2 =
- match p1,p2 with
- SPexpr t1, SPexpr t2 -> is_same_term t1 t2
- | SPctrl, SPctrl | SPstmt, SPstmt -> true
- | (SPexpr _ | SPctrl | SPstmt), _ -> false
-
-let is_same_impact_pragma p1 p2 =
- match p1,p2 with
- | IPexpr t1, IPexpr t2 -> is_same_term t1 t2
- | IPstmt, IPstmt -> true
- | (IPexpr _ | IPstmt), _ -> false
-
-let is_same_pragma p1 p2 =
- match p1,p2 with
- | Slice_pragma p1, Slice_pragma p2 -> is_same_slice_pragma p1 p2
- | Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
- | (Slice_pragma _ | Impact_pragma _), _ -> false
-
let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
(x1.ext_has_status = x2.ext_has_status) &&
@@ -1221,11 +1200,10 @@ let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
| AAllocation(l1,fa1), AAllocation(l2,fa2) ->
is_same_list (=) l1 l2 &&
is_same_allocation fa1 fa2
- | APragma p1, APragma p2 -> is_same_pragma p1 p2
| AExtended (l1,b1,e1), AExtended(l2,b2,e2) ->
is_same_list (=) l1 l2 && ((b1:bool) = b2) && is_same_extension e1 e2
| (AAssert _ | AStmtSpec _ | AInvariant _ | AExtended _
- | AVariant _ | AAssigns _ | AAllocation _ | APragma _ ), _ -> false
+ | AVariant _ | AAssigns _ | AAllocation _), _ -> false
let is_same_model_info mi1 mi2 =
mi1.mi_name = mi2.mi_name &&
@@ -2267,15 +2245,6 @@ let is_allocation ca =
let is_assigns ca =
match ca.annot_content with AAssigns _ -> true | _ -> false
-let is_pragma ca =
- match ca.annot_content with APragma _ -> true | _ -> false
-
-let is_slice_pragma ca =
- match ca.annot_content with APragma (Slice_pragma _) -> true | _ -> false
-
-let is_impact_pragma ca =
- match ca.annot_content with APragma (Impact_pragma _) -> true | _ -> false
-
let is_loop_extension ca =
match ca.annot_content with AExtended (_,is_loop,_) -> is_loop | _ -> false
@@ -2286,16 +2255,10 @@ let is_loop_annot s =
let is_trivial_annotation a =
match a.annot_content with
| AAssert (_,a) -> is_trivially_true a.tp_statement
- | APragma _ | AStmtSpec _ | AInvariant _ | AVariant _
+ | AStmtSpec _ | AInvariant _ | AVariant _
| AAssigns _| AAllocation _ | AExtended _
-> false
-let is_property_pragma = function
- | 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_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 62ace3c9ccfc6dec17e9c6f08ae0ae48a63a2e8f..9ef563d8833f901ce18594e055e4804f26f8a9ab 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -373,9 +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_slice_pragma : slice_pragma -> slice_pragma -> bool
-val is_same_impact_pragma : impact_pragma -> impact_pragma -> bool
-val is_same_pragma : pragma -> pragma -> bool
val is_same_code_annotation : code_annotation -> code_annotation -> bool
val is_same_global_annotation : global_annotation -> global_annotation -> bool
val is_same_axiomatic :
@@ -458,16 +455,10 @@ val is_invariant : code_annotation -> bool
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_slice_pragma : code_annotation -> bool
-val is_impact_pragma : code_annotation -> bool
val is_loop_annot : code_annotation -> bool
val is_trivial_annotation : code_annotation -> bool
-val is_property_pragma : pragma -> bool
-(** Should this pragma be proved by plugins *)
-
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 aeb6da19615b9c4372765f8f6c82c4f47339f420..79b07e9374dd3a3be35a5aebec6f5efd0c58be1b 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -319,23 +319,6 @@ type spec = {
It is possible to have more than one set of disjoint behaviors *)
}
-(** Pragmas for the value analysis plugin of Frama-C. *)
-
-and slice_pragma =
- | SPexpr of lexpr
- | SPctrl
- | SPstmt
-
-(** Pragmas for the impact plugin of Frama-C. *)
-and impact_pragma =
- | IPexpr of lexpr
- | IPstmt
-
-(** The various kinds of pragmas. *)
-and pragma =
- | Slice_pragma of slice_pragma
- | Impact_pragma of impact_pragma
-
(** all annotations that can be found in the code. This type shares the name of
its constructors with {!Cil_types.code_annotation_node}. *)
type code_annot =
@@ -366,7 +349,6 @@ type code_annot =
At most one clause associated to a given (statement, behavior) couple.
@since Oxygen-20120901 when [b_allocation] has been added. *)
- | APragma of pragma (** pragma. *)
| AExtended of string list * bool * extension
(** extension in a code or loop (when boolean flag is true) annotation.
@since Silicon-20161101
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
index 8674b84187cc5d586773767364663c238334b52a..343634fd4b6c6b6b8dcf53940a22de1b89ba2108 100644
--- a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
@@ -520,7 +520,6 @@ class visitor cat
~not_yet:"allocates"
~f:self#visit_allocates
allocates
- | APragma _ -> ()
| AExtended _ -> ()
)
stmt;
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index 439c2dba354e069fc2c3b7dff100d048f7fee5c0..3f484c98307adf09c9b9432267a43fbe7166b3d6 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -131,7 +131,6 @@ let pre_code_annotation kf stmt env annot =
then Env.not_yet env "allocation")
ppts;
env
- | APragma _ -> Env.not_yet env "pragma"
| AExtended _ -> env (* never translate extensions. *)
in
Env.handle_error convert env
@@ -150,7 +149,6 @@ let post_code_annotation kf stmt env annot =
| AVariant _
| AAssigns _
| AAllocation _
- | APragma _
| AExtended _ -> env
in
Env.handle_error convert env
diff --git a/src/plugins/eva/engine/transfer_logic.ml b/src/plugins/eva/engine/transfer_logic.ml
index 41aa1bc0dcc998b4bc84eaf8866910479fe1784f..94a4ff04fdfe2b3cd26bcc6019db097056f0d09e 100644
--- a/src/plugins/eva/engine/transfer_logic.ml
+++ b/src/plugins/eva/engine/transfer_logic.ml
@@ -162,7 +162,7 @@ let pp_code_annot fmt ca =
Format.fprintf fmt "loop invariant%a" Description.pp_named tp_statement
| AExtended (_, _, extension) ->
Format.fprintf fmt "%s annotation" extension.ext_name;
- | APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _ ->
+ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _ ->
assert false (* currently not treated by Eva *)
(* location of the given code annotation. If unknown, use the location of the
@@ -690,7 +690,6 @@ module Make
let record = record && p.tp_kind <> Admit in
let reduce = p.tp_kind <> Check in
aux ~record ~reduce code_annot behav p.tp_statement
- | APragma _
| AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _
| AStmtSpec _ (*TODO*) -> states
diff --git a/src/plugins/eva/legacy/eval_annots.ml b/src/plugins/eva/legacy/eval_annots.ml
index beff72440d8f151342f6500feb010aec0b244fea..e82b85b231c25a2deaac5c861805bbfe24b9efcf 100644
--- a/src/plugins/eva/legacy/eval_annots.ml
+++ b/src/plugins/eva/legacy/eval_annots.ml
@@ -32,7 +32,7 @@ let code_annotation_text ca =
match ca.annot_content with
| AAssert (_, {tp_kind}) -> Cil_printer.name_of_assert tp_kind
| AInvariant _ -> "loop invariant"
- | APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
+ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
assert false (* currently not treated by Value *)
@@ -210,7 +210,7 @@ let mark_green_and_red () =
| Eval_terms.Unknown -> ()
end
| AInvariant (_, false, _) | AStmtSpec _ | AVariant _ | AAssigns _
- | AAllocation _ | APragma _ | AExtended _ -> ()
+ | AAllocation _ | AExtended _ -> ()
in
Annotations.iter_all_code_annot do_code_annot
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 1381ced216afa36c447485daceaa6e24e8c3af73..5592bd188cd1a9245116289196699706a367acfe 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -654,8 +654,6 @@ let make_panel (main_ui:main_window_extension_points) =
end
| IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
- | IPCodeAnnot {ica_ca={annot_content = APragma p}} ->
- Logic_utils.is_property_pragma p (* currently always false. *)
| IPCodeAnnot _ -> false (* status of inner nodes *)
| IPAllocation {ial_kinstr=Kglobal} -> allocations.get ()
| IPAllocation {ial_kinstr=Kstmt _;ial_bhv=Id_loop _} ->
diff --git a/src/plugins/impact/options.ml b/src/plugins/impact/options.ml
index 8a089142eacd52f3e7379a24076a5541d0caa22c..634fed1d126dd0afef5f5b69a1e4f42004fd6aae 100644
--- a/src/plugins/impact/options.ml
+++ b/src/plugins/impact/options.ml
@@ -27,13 +27,14 @@ include Plugin.Register
let help = "impact analysis"
end)
-module Pragma =
+module Annot =
Kernel_function_set
(struct
- let option_name = "-impact-pragma"
+ let option_name = "-impact-annot"
let arg_name = "f1, ..., fn"
- let help = "use the impact pragmas in the code of functions f1,...,fn"
+ let help = "use the impact annotations in the code of functions f1,...,fn"
end)
+let () = Annot.add_aliases ~visible:false ~deprecated:true ["-impact-pragma"]
module Print =
False
@@ -73,7 +74,7 @@ module Upward =
let help = "compute compute impact in callers as well as in callees"
end)
-let is_on () = not (Pragma.is_empty ())
+let is_on () = not (Annot.is_empty ())
(*
Local Variables:
diff --git a/src/plugins/impact/options.mli b/src/plugins/impact/options.mli
index faebc35aff1a9f310d38823113c0ed597ed7f600..8a56c3113119bb704a84227c913ea47eb4e4fd1d 100644
--- a/src/plugins/impact/options.mli
+++ b/src/plugins/impact/options.mli
@@ -22,8 +22,8 @@
include Plugin.S
-module Pragma: Parameter_sig.Kernel_function_set
-(** Use pragmas of given function. *)
+module Annot: Parameter_sig.Kernel_function_set
+(** Use impact annotations of given function. *)
module Print: Parameter_sig.Bool
(** Print the impacted stmt on stdout. *)
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 817fae52b385f7c97a31f9f8db5874cfd4fc72b2..6de2b10f0879ba8b99dba966df5702e25e854ce8 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -98,52 +98,44 @@ let slice (stmts:stmt list) =
Options.feedback ~level:2 "slicing done";
extracted_prj
-let all_pragmas_kf l =
- List.fold_left
- (fun acc (s, a) ->
- match a.annot_content with
- | APragma (Impact_pragma IPstmt) -> s :: acc
- | APragma (Impact_pragma (IPexpr _)) ->
- Options.not_yet_implemented "impact pragmas: expr"
- | _ -> assert false)
- [] l
-
-let compute_pragmas () =
- Ast.compute ();
- let pragmas = ref [] in
- let visitor = object
- inherit Visitor.frama_c_inplace as super
-
- method! vfunc f =
- pragmas := [];
- super#vfunc f
-
- method! vstmt_aux s =
- pragmas :=
- List.map
- (fun a -> s, a)
- (Annotations.code_annot ~filter:Logic_utils.is_impact_pragma s)
- @ !pragmas;
- Cil.DoChildren
- end
+
+(* Register impact ACSL extension. *)
+let () =
+ let typer typing_context loc args =
+ match args with
+ | [] -> Ext_terms []
+ | _ -> typing_context.Logic_typing.error loc "Invalid impact directive"
in
- (* fill [pragmas] with all the pragmas of all the selected functions *)
- let pragmas =
- Options.Pragma.fold
- (fun kf acc ->
- (* Pragma option only accept defined functions. *)
- let f = Kernel_function.get_definition kf in
- ignore (Visitor.visitFramacFunction visitor f);
- if !pragmas != [] then (kf, !pragmas) :: acc else acc)
- []
+ Acsl_extension.register_code_annot_next_both
+ ~plugin:"impact" "impact_stmt" typer false
+
+let is_impact_annot code_annot =
+ match code_annot.annot_content with
+ | AExtended (_, _, { ext_name = "impact_stmt"; }) -> true
+ | _ -> false
+
+let compute_annots () =
+ Ast.compute ();
+ (* Returns the list of statements of function [kf] that have an impact
+ annotation. *)
+ let compute_impact_stmts kf acc =
+ (* Annot option only accept defined functions. *)
+ let fundec = Kernel_function.get_definition kf in
+ let has_impact_annot stmt =
+ let impact_annots = Annotations.code_annot ~filter:is_impact_annot stmt in
+ not (impact_annots = [])
+ in
+ let impact_stmts = List.filter has_impact_annot fundec.sallstmts in
+ if impact_stmts = [] then acc
+ else (kf, impact_stmts) :: acc
in
+ let impact_stmts = Options.Annot.fold compute_impact_stmts [] in
let skip = Compute_impact.skip () in
(* compute impact analyses on each kf *)
let nodes = List.fold_left
- (fun nodes (kf, pragmas) ->
- let pragmas_stmts = all_pragmas_kf pragmas in
- Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf pragmas_stmts)
- ) Pdg_aux.NS.empty pragmas
+ (fun nodes (kf, stmts) ->
+ Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf stmts))
+ Pdg_aux.NS.empty impact_stmts
in
let stmts = Compute_impact.nodes_to_stmts nodes in
if Options.Slicing.get () then ignore (slice stmts);
@@ -157,8 +149,8 @@ let from_nodes = compute_from_nodes
let main () =
if Options.is_on () then begin
Options.feedback "beginning analysis";
- assert (not (Options.Pragma.is_empty ()));
- ignore (compute_pragmas ());
+ assert (not (Options.Annot.is_empty ()));
+ ignore (compute_annots ());
Options.feedback "analysis done"
end
let () = Boot.Main.extend main
diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli
index 35e476eb808dbb9e39c63d5a75ca885ab8057e1d..7a5f7aa71d11719fc2f9f310cf200a193f72987e 100644
--- a/src/plugins/impact/register.mli
+++ b/src/plugins/impact/register.mli
@@ -24,8 +24,8 @@ open Cil_types
open Pdg_types
-val compute_pragmas: (unit -> stmt list)
-(** Compute the impact analysis from the impact pragma in the program.
+val compute_annots: (unit -> stmt list)
+(** Compute the impact analysis from the impact annotations in the program.
Print and slice the results according to the parameters -impact-print
and -impact-slice.
@return the impacted statements *)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index cd3bd66a369de8bca84eb87d54445bd10f180511..073fdad49b4425f2b10f5e98b44014da074d1f01 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -249,7 +249,7 @@ let add_code_annot_stats stmt _ ca =
List.iter
(function (_,FromAny) -> () | (_,From _) -> incr_all incr_loop_froms) l
| AAllocation _ -> () (* TODO *)
- | APragma _ | AExtended _ -> ()
+ | AExtended _ -> ()
let compute () =
if not (Computed.get()) then begin
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index ad4dd73a4323a618db05592d560f038ce6552947..11e68d855c32d780f93e60a3b152a23569527608 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -91,7 +91,6 @@ let node_of_code_annotation_node = function
| AVariant _ -> "variant"
| AAssigns _ -> "assigns"
| AAllocation _ -> "allocation"
- | APragma _ -> "ca_pragma"
| AExtended _ -> "extended"
let node_of_global_annotation = function
@@ -390,8 +389,6 @@ class full_visitor = object(self)
method! vfrees _ = Cil.DoChildren
method! vallocates _ = Cil.DoChildren
method! vallocation _ = Cil.DoChildren
- method! vslice_pragma _ = Cil.DoChildren
- method! vimpact_pragma _ = Cil.DoChildren
method! vdeps _ = Cil.DoChildren
method! vfrom _ = Cil.DoChildren
method! vcode_annot _ =
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index 41f406d05057c3d1d9c85fc89b1aa2dd156873fb..14478583f6d102aced6e6b76f0cb087503345b2d 100644
--- a/src/plugins/pdg/annot.ml
+++ b/src/plugins/pdg/annot.ml
@@ -108,7 +108,7 @@ let find_code_annot_nodes pdg stmt annot =
if Eva.Results.is_reachable stmt then
begin
let kf = PdgTypes.Pdg.get_kf pdg in
- let (data_info, decl_label_info), pragmas =
+ let (data_info, decl_label_info), slices =
Logic_deps.from_stmt_annot annot (stmt, kf)
in
let data_dpds = zone_info_nodes pdg data_info in
@@ -125,10 +125,10 @@ let find_code_annot_nodes pdg stmt annot =
try Sets.find_stmt_and_blocks_nodes pdg s @ acc
with Not_found -> acc
in
- (* can safely ignore pragmas.ctrl
+ (* can safely ignore slices.ctrl
* because we already have the ctrl dpds from the stmt node. *)
- let stmt_pragmas = pragmas.Logic_deps.stmt in
- let ctrl_dpds = Stmt.Set.fold add_stmt_nodes stmt_pragmas ctrl_dpds in
+ let stmt_slices = slices.Logic_deps.stmt in
+ let ctrl_dpds = Stmt.Set.fold add_stmt_nodes stmt_slices ctrl_dpds in
let add_label_nodes l acc = match l with
| StmtLabel stmt ->
(* TODO: we could be more precise here if we knew which label
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 98cf1b9b3514e00447f62d03052cdd8d4ced82ac..5ff525c353c9baabd13989e9543ddd309b50fbb1 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -421,7 +421,6 @@ let rec monitored_property ip =
| IPFrom _-> true
| IPDecrease _ -> true
| IPCodeAnnot {ica_ca = { annot_content = AStmtSpec _ }} -> false
- | IPCodeAnnot {ica_ca = { annot_content = APragma _ }} -> false
| IPCodeAnnot {ica_ca = { annot_content = AExtended _ }} -> true
| IPCodeAnnot {ica_ca = { annot_content = AAssert _ }} -> true
| IPCodeAnnot {ica_ca = { annot_content = AInvariant _ }} -> true
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 74349068d997ef140efa8e179dca5482a075810a..d78507281249ac7b058d68a30e9d969c4042e929 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -70,7 +70,6 @@ let search_security_requirements () =
| AStmtSpec { spec_requires = l } ->
List.exists
(is_security_predicate $ Logic_const.pred_of_id_pred) l
- | APragma _
| AInvariant _ (* | ALoopBehavior _ *)
(* [JS 2008/02/26] may contain a security predicate *)
| AVariant _ | AAssigns _
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 8d84bb2874a334504e69b69415ce4f252d27f479..c80c97892fae77886d3fa6410c586ee651e25b4c 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -70,7 +70,6 @@ struct
let t_loop_assigns = t_loop "assigns"
let t_loop_variant = t_loop "variant"
let t_loop_allocates = t_loop "allocates"
- 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 +118,6 @@ struct
| AVariant _ -> t_loop_variant
| AAssigns _ -> t_loop_assigns
| AAllocation _ -> t_loop_allocates
- | APragma _ -> t_pragma
| AExtended(_,_,{ext_name=_}) -> t_ext
end
| IPAllocation _ -> t_allocates
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index 6caebd7a71ce6bd8bce2257d35acd94d4fd074d0..5bee5b3ad24e0911ed512029825bf7128c98266c 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -253,7 +253,7 @@ module Select : sig
spare:bool ->
threat:bool ->
user_assert:bool ->
- slicing_pragma:bool ->
+ slicing_annot:bool ->
loop_inv:bool ->
loop_var:bool -> Cil_datatype.Stmt.t -> Cil_types.kernel_function -> set
@@ -301,7 +301,7 @@ module Select : sig
(** To select the annotations related to a function. *)
val select_func_annots :
set -> Mark.t -> spare:bool -> threat:bool -> user_assert:bool ->
- slicing_pragma:bool -> loop_inv:bool -> loop_var:bool ->
+ slicing_annot:bool -> loop_inv:bool -> loop_var:bool ->
Cil_types.kernel_function -> set
(** {3 Pdg selectors.} *)
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index cfde40037732f72791c945dcd45f57623a1e9a74..0387d27af71d22d097f40860e7cb525e51759e3b 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -432,17 +432,17 @@ let select_decl_var set mark vi kf =
let selection = SlicingSelect.select_decl_var kf vi mark in
add_to_selection set selection
-let select_ZoneAnnot_pragmas set ~spare pragmas kf =
+let select_ZoneAnnot_slices set ~spare slices kf =
let set =
Cil_datatype.Stmt.Set.fold
- (* selection related to statement assign and //@ slice pragma stmt *)
+ (* selection related to statement assign and //@ slice directive stmt *)
(fun ki' acc -> select_stmt acc ~spare ki' kf)
- pragmas.Logic_deps.stmt set
+ slices.Logic_deps.stmt set
in
Cil_datatype.Stmt.Set.fold
- (* selection related to //@ slice pragma ctrl/expr *)
+ (* selection related to //@ slice directive ctrl/expr *)
(fun ki' acc -> select_stmt_ctrl acc ~spare ki' kf)
- pragmas.Logic_deps.ctrl
+ slices.Logic_deps.ctrl
set
let select_ZoneAnnot_zones_decl_vars set mark (zones,decl_vars) kf =
@@ -499,36 +499,36 @@ let select_stmt_term set mark term ki kf =
Add selection of the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_annot set mark ~spare annot ki kf =
- let zones_decl_vars,pragmas =
+ let zones_decl_vars, slices =
Logic_deps.from_stmt_annot annot (ki, kf)
- in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
+ in let set = select_ZoneAnnot_slices set ~spare slices kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
Add selection of the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
-let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ki kf =
- let zones_decl_vars,pragmas =
+let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_annot ~loop_inv ~loop_var ki kf =
+ let zones_decl_vars, slices =
Logic_deps.from_stmt_annots
(Some (Logic_deps.code_annot_filter
- ~threat ~user_assert ~slicing_pragma
+ ~threat ~user_assert ~slicing_annot
~loop_inv ~loop_var ~others:false))
(ki, kf)
- in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
+ in let set = select_ZoneAnnot_slices set ~spare slices kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
Add a selection of the annotations related to a function. *)
-let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var kf =
+let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_annot ~loop_inv ~loop_var kf =
try
- let zones_decl_vars,pragmas =
+ let zones_decl_vars, slices =
Logic_deps.from_func_annots Kinstr.iter_from_func
(Some
(Logic_deps.code_annot_filter
- ~threat ~user_assert ~slicing_pragma ~loop_inv
+ ~threat ~user_assert ~slicing_annot ~loop_inv
~loop_var ~others:false))
kf
- in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
+ in let set = select_ZoneAnnot_slices set ~spare slices kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
with Kernel_function.No_Definition ->
SlicingParameters.warning ~wkey:SlicingParameters.wkey_cmdline
@@ -634,29 +634,29 @@ let add_persistent_cmdline () =
SlicingParameters.Select.Calls.get
select_func_calls_to;
add_selection
- SlicingParameters.Select.Pragma.get
+ SlicingParameters.Select.SliceAnnot.get
(fun s -> select_func_annots s top_mark
- ~threat:false ~user_assert:false ~slicing_pragma:true
+ ~threat:false ~user_assert:false ~slicing_annot:true
~loop_inv:false ~loop_var:false);
add_selection
SlicingParameters.Select.Threat.get
(fun s -> select_func_annots s top_mark
- ~threat:true ~user_assert:false ~slicing_pragma:false
+ ~threat:true ~user_assert:false ~slicing_annot:false
~loop_inv:false ~loop_var:false);
add_selection
SlicingParameters.Select.Assert.get
(fun s -> select_func_annots s top_mark
- ~threat:false ~user_assert:true ~slicing_pragma:false
+ ~threat:false ~user_assert:true ~slicing_annot:false
~loop_inv:false ~loop_var:false);
add_selection
SlicingParameters.Select.LoopInv.get
(fun s -> select_func_annots s top_mark
- ~threat:false ~user_assert:false ~slicing_pragma:false
+ ~threat:false ~user_assert:false ~slicing_annot:false
~loop_inv:true ~loop_var:false);
add_selection
SlicingParameters.Select.LoopVar.get
(fun s -> select_func_annots s top_mark
- ~threat:false ~user_assert:false ~slicing_pragma:false
+ ~threat:false ~user_assert:false ~slicing_annot:false
~loop_inv:false ~loop_var:true);
);
if not (Datatype.String.Set.is_empty
diff --git a/src/plugins/slicing/slicingCmds.mli b/src/plugins/slicing/slicingCmds.mli
index f14ca457d1feb2ab16b056431080bf25f12280b0..12336ddc7e1211f55105db73ec8e77b7882f8a01 100644
--- a/src/plugins/slicing/slicingCmds.mli
+++ b/src/plugins/slicing/slicingCmds.mli
@@ -143,7 +143,7 @@ val select_stmt_annots :
spare:bool ->
threat:bool ->
user_assert:bool ->
- slicing_pragma:bool ->
+ slicing_annot:bool ->
loop_inv:bool ->
loop_var:bool ->
stmt ->
@@ -156,7 +156,7 @@ val select_func_annots :
spare:bool ->
threat:bool ->
user_assert:bool ->
- slicing_pragma:bool ->
+ slicing_annot:bool ->
loop_inv:bool ->
loop_var:bool ->
kernel_function ->
diff --git a/src/plugins/slicing/slicingParameters.ml b/src/plugins/slicing/slicingParameters.ml
index 99606df8d84f6eb1b4b4c2514f70be21f6ecbc05..527c6993b5cd6ced8dd591bdf0322efe3c4f6d66 100644
--- a/src/plugins/slicing/slicingParameters.ml
+++ b/src/plugins/slicing/slicingParameters.ml
@@ -86,19 +86,21 @@ module Select = struct
let help = "select the loop variants of functions f1,...,fn"
end)
- module Pragma =
+ module SliceAnnot =
Kernel_function_set
(struct
- let option_name = "-slice-pragma"
+ let option_name = "-slice-annot"
let arg_name = "f1, ..., fn"
let help =
"use the slicing pragmas in the code of functions f1,...,fn as \
slicing criteria:\n\
- //@ slice pragma ctrl; to reach this control-flow point\n\
- //@ slice pragma expr <expr_desc;> to preserve the value of an expression at \
+ //@ slice_preserve_ctrl; to reach this control-flow point\n\
+ //@ slice_preserve_expr <expr>; to preserve the value of an expression at \
this control-flow point\n\
- //@ slice pragma stmt; to preserve the effect of the next statement"
+ //@ slice_preserve_stmt; to preserve the effect of the next statement"
end)
+ let () =
+ SliceAnnot.add_aliases ~visible:false ~deprecated:true ["-slice-pragma"]
module RdAccess =
String_set
@@ -222,7 +224,7 @@ let () =
Select.Assert.self;
Select.LoopInv.self;
Select.LoopVar.self;
- Select.Pragma.self;
+ Select.SliceAnnot.self;
Select.RdAccess.self;
Select.WrAccess.self;
Select.Value.self;
@@ -240,7 +242,7 @@ let is_on () =
&& Select.Assert.is_empty ()
&& Select.LoopInv.is_empty ()
&& Select.LoopVar.is_empty ()
- && Select.Pragma.is_empty ()
+ && Select.SliceAnnot.is_empty ()
&& Select.RdAccess.is_empty ()
&& Select.WrAccess.is_empty ()
&& Select.Value.is_empty ()))
@@ -259,7 +261,7 @@ let clear () =
Select.Assert.clear () ;
Select.LoopInv.clear () ;
Select.LoopVar.clear () ;
- Select.Pragma.clear () ;
+ Select.SliceAnnot.clear () ;
Select.RdAccess.clear () ;
Select.WrAccess.clear () ;
Select.Value.clear () ;
diff --git a/src/plugins/slicing/slicingParameters.mli b/src/plugins/slicing/slicingParameters.mli
index fb6007173eacc8dff52ccc1a64693b1b5e7500ce..ecf1d7864c3491b027787c995f62ba72f248ef68 100644
--- a/src/plugins/slicing/slicingParameters.mli
+++ b/src/plugins/slicing/slicingParameters.mli
@@ -30,7 +30,7 @@ module Select : sig
module Return: Parameter_sig.Kernel_function_set
module Threat: Parameter_sig.Kernel_function_set
module Assert: Parameter_sig.Kernel_function_set
- module Pragma: Parameter_sig.Kernel_function_set
+ module SliceAnnot: Parameter_sig.Kernel_function_set
module LoopInv: Parameter_sig.Kernel_function_set
module LoopVar: Parameter_sig.Kernel_function_set
module RdAccess: Parameter_sig.String_set
diff --git a/src/plugins/sparecode/Sparecode.mli b/src/plugins/sparecode/Sparecode.mli
index 6ed9b48f3a7f2551af06e4516b868a983256f165..e98a84689e1f0c7b7a91a21beed636c60e005832 100644
--- a/src/plugins/sparecode/Sparecode.mli
+++ b/src/plugins/sparecode/Sparecode.mli
@@ -24,10 +24,10 @@
(** Interface for the unused code detection. *)
module Register: sig
- val get: select_annot:bool -> select_slice_pragma:bool -> Project.t
+ val get: select_annot:bool -> select_slice_annot:bool -> Project.t
(** Remove in each function what isn't used to compute its outputs,
or its annotations when [select_annot] is true,
- or its slicing pragmas when [select_slice_pragmas] is true.
+ or its slicing annotations when [select_slice_annot] is true.
@return a new project where the sparecode has been removed.
*)
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index 77ca976d5c5e8429da5eb7c37eb6d33ff5551f70..06889bca2e6f2c7444b5cbbbe58336e8c7b2bd48 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -60,13 +60,13 @@ let rm_unused_globals ?new_proj_name ?(project=Project.current ()) () =
P.result "removed unused global declarations in new project '%s'" new_proj_name;
Project.on project Globs.rm_unused_decl new_proj_name
-let run select_annot select_slice_pragma =
+let run select_annot select_slice_annot =
P.feedback "remove unused code...";
(*let initial_file = Ast.get () in*)
let kf_entry, _library = Globals.entry_point () in
let proj =
Spare_marks.select_useful_things
- ~select_annot ~select_slice_pragma kf_entry
+ ~select_annot ~select_slice_annot kf_entry
in
let old_proj_name = Project.get_name (Project.current ()) in
let new_proj_name = (old_proj_name^" without sparecode") in
@@ -81,16 +81,16 @@ let run select_annot select_slice_pragma =
Project.copy ~selection:ctx new_prj;
new_prj
-let get ~select_annot ~select_slice_pragma =
+let get ~select_annot ~select_slice_annot =
Result.memo
- (fun _ -> run select_annot select_slice_pragma)
- (select_annot, select_slice_pragma)
+ (fun _ -> run select_annot select_slice_annot)
+ (select_annot, select_slice_annot)
let main () =
if Sparecode_params.Analysis.get () then begin
let select_annot = Sparecode_params.Annot.get () in
- let select_slice_pragma = true in
- let new_proj = get ~select_annot ~select_slice_pragma in
+ let select_slice_annot = true in
+ let new_proj = get ~select_annot ~select_slice_annot in
File.pretty_ast ~prj:new_proj ()
end
else if Sparecode_params.GlobDecl.get () then begin
diff --git a/src/plugins/sparecode/register.mli b/src/plugins/sparecode/register.mli
index 40470cd52d97cffa2356d577d95f5081657e96da..df9ac76e7f58a22574361ab4602ef55c4a3ec99e 100644
--- a/src/plugins/sparecode/register.mli
+++ b/src/plugins/sparecode/register.mli
@@ -20,10 +20,10 @@
(* *)
(**************************************************************************)
-val get: select_annot:bool -> select_slice_pragma:bool -> Project.t
+val get: select_annot:bool -> select_slice_annot:bool -> Project.t
(** Remove in each function what isn't used to compute its outputs,
or its annotations when [select_annot] is true,
- or its slicing pragmas when [select_slice_pragmas] is true.
+ or its slicing annotations when [select_slice_annot] is true.
@return a new project where the sparecode has been removed. *)
val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> Project.t
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index b1a786c3f0752b3415c6fb912ea6f4fe31c341e2..e6a15b273f8e288acab540d032b856233f023f74 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -321,7 +321,7 @@ class annot_visitor ~filter pdg = object (self)
in Cil.SkipChildren
end
-let select_annotations ~select_annot ~select_slice_pragma proj =
+let select_annotations ~select_annot ~select_slice_annot proj =
let visit_fun kf =
debug 1 "look for annotations in function %a@." Kernel_function.pretty kf;
let pdg = Pdg.Api.get kf in
@@ -329,12 +329,14 @@ let select_annotations ~select_annot ~select_slice_pragma proj =
else if PdgTypes.Pdg.is_bottom pdg
then debug 1 "pdg bottom: skip annotations"
else begin
- let filter annot = match annot.Cil_types.annot_content with
- | Cil_types.APragma (Cil_types.Slice_pragma _) -> select_slice_pragma
+ let filter annot =
+ match annot.Cil_types.annot_content with
| Cil_types.AAssert _-> (* Never select alarms, they are not useful *)
(match Alarms.find annot with
| None -> select_annot
| Some _ -> false)
+ | AExtended (_, _, ext) when Logic_deps.is_slice_directive ext ->
+ select_slice_annot
| _ -> select_annot
in
try
@@ -354,7 +356,7 @@ let finalize proj =
process_call_inputs proj;
assert (!call_in_to_check = [])
-let select_useful_things ~select_annot ~select_slice_pragma kf_entry =
+let select_useful_things ~select_annot ~select_slice_annot kf_entry =
let proj = new_project () in
assert (!call_in_to_check = []);
debug 1 "selecting function %a outputs and entry point@."
@@ -367,8 +369,8 @@ let select_useful_things ~select_annot ~select_slice_pragma kf_entry =
else begin
select_entry_point proj kf_entry pdg;
select_all_outputs proj kf_entry pdg;
- if (select_annot || select_slice_pragma) then
- select_annotations ~select_annot ~select_slice_pragma proj;
+ if (select_annot || select_slice_annot) then
+ select_annotations ~select_annot ~select_slice_annot proj;
finalize proj
end;
proj
diff --git a/src/plugins/sparecode/spare_marks.mli b/src/plugins/sparecode/spare_marks.mli
index e0e594a8d220546a93e1596cab1c32897569b38c..c75749b2736dea0e46aeaaf88db0f403c180a2b8 100644
--- a/src/plugins/sparecode/spare_marks.mli
+++ b/src/plugins/sparecode/spare_marks.mli
@@ -27,7 +27,7 @@ type proj
type fct
val select_useful_things :
- select_annot:bool -> select_slice_pragma:bool -> kernel_function -> proj
+ select_annot:bool -> select_slice_annot:bool -> kernel_function -> proj
val get_marks : proj -> kernel_function -> fct option
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index e063a84fe1583955ab8919ef691f2be0bbdc2f2a..ec6b9b0cf758c9241e9564daf8d9588654bcf6e3 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -76,7 +76,7 @@ let is_selected_ca (m: mode) ~goal (ca: code_annotation) =
| AInvariant(forb,_,_)
-> is_selected_for m ~goal forb
| AVariant _ -> is_default_bhv m
- | AExtended _ | AStmtSpec _ | APragma _ ->
+ | AExtended _ | AStmtSpec _ ->
assert false (* n/a *)
let is_active_mode ~mode ~goal (p: Property.t) =
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index bf683b0c97377bf8b756add8cfb2ea6fb62b72b1..f9c0980cbdcfa8621efb2a6a624a2d575c48d36a 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -163,7 +163,7 @@ let rec strategy_ip model pool target =
-> add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
| IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
begin match ca.annot_content with
- | AExtended _ | APragma _ -> ()
+ | AExtended _ -> ()
| AStmtSpec(fors,_) ->
(*TODO*) notyet target ;
add_fun_task model pool ~kf ~bhvs:(select kf fors) ()
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index e9a8931cb1a8a0383c4b994156c16b8b2e40a8e3..0d00f2dc2ef00c1d74def350ac92407f724c98a1 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -644,7 +644,7 @@ let annot_hints hs = function
List.iter (add_hint hs) bs ;
assigns_hints hs froms
| AAllocation _ | AAssigns(_,WritesAny) | AStmtSpec _
- | AVariant _ | APragma _ | AExtended _ -> ()
+ | AVariant _ | AExtended _ -> ()
let property_hints hs =
let open Property in function
diff --git a/tests/impact/alias.i b/tests/impact/alias.i
index 1b4edfb05d19133efb9ed8b7154bdd0dce8041cd..593bd42ea9b419bed2083b157dd5ece618610efd 100644
--- a/tests/impact/alias.i
+++ b/tests/impact/alias.i
@@ -1,12 +1,12 @@
/* run.config
- STDOPT: +"-impact-pragma f" +"-lib-entry" +"-main f" +"-eva-remove-redundant-alarms"
+ STDOPT: +"-impact-annot f" +"-lib-entry" +"-main f" +"-eva-remove-redundant-alarms"
*/
int P,c;
/*@ requires \valid(x); */
int f(int *x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int *y = x+1;
*y = 4;
int a = *(x+1) + 2;
diff --git a/tests/impact/call.i b/tests/impact/call.i
index c2c1e339205a9dc98fc5aa8120c824daafb2d343..65a046489c1fedd09ad8f9488da1f8a52c2622ae 100644
--- a/tests/impact/call.i
+++ b/tests/impact/call.i
@@ -1,8 +1,8 @@
/* run.config
-
- STDOPT: +"-impact-pragma main"
- STDOPT: +"-impact-pragma main2" +"-main main2"
- STDOPT: +"-impact-pragma main3" +"-main main3"
+
+ STDOPT: +"-impact-annot main"
+ STDOPT: +"-impact-annot main2" +"-main main2"
+ STDOPT: +"-impact-annot main3" +"-main main3"
*/
/*@ ghost int G; */
@@ -19,7 +19,7 @@ void test (void) {
/* ************************************************************************* */
void main (int x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
X = x;
test ();
}
@@ -31,7 +31,7 @@ void call_test (void) {
}
void main2(int x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
X = x;
call_test ();
}
@@ -50,7 +50,7 @@ void call_test3 (void) {
}
void main3(int x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
X = x;
call_test3 ();
}
diff --git a/tests/impact/called.i b/tests/impact/called.i
index 5971b9e56ba56310f16a6a87d08ab44032efa9a0..4c7aa54538bf67cb8e76d82c485201126e1de763 100644
--- a/tests/impact/called.i
+++ b/tests/impact/called.i
@@ -1,6 +1,6 @@
/* run.config
- STDOPT: +"-impact-pragma g" +"-lib-entry" +"-main g"
- STDOPT: +"-impact-pragma h" +"-lib-entry" +"-main h"
+ STDOPT: +"-impact-annot g" +"-lib-entry" +"-main g"
+ STDOPT: +"-impact-annot h" +"-lib-entry" +"-main h"
*/
int X;
@@ -10,7 +10,7 @@ int f(int x, int y) { X = x; return y; }
void g() {
int a, b, c, d;
b = 0;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
a = 0;
c = f(a,b);
d = X;
@@ -19,7 +19,7 @@ void g() {
void h() {
int a, b, c, d;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
b = 0;
a = 0;
c = f(a,b);
diff --git a/tests/impact/depend1.i b/tests/impact/depend1.i
index 6b3b3c0e81f98b48e957d7c91a12c261f46a2ae4..2a484acf5706576da9505cb8ced960ea6b872a3a 100644
--- a/tests/impact/depend1.i
+++ b/tests/impact/depend1.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-impact-pragma main"
+ STDOPT: +"-impact-annot main"
*/
@@ -8,7 +8,7 @@ int find(int x) { return x; }
int main()
{
int a = find(1);
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int b = find(2);
int c = find(b);
int d = find(3);
diff --git a/tests/impact/depend2.i b/tests/impact/depend2.i
index dbc0a3ccc29e05e26dfcd560b3b9e550b90ce9b6..902b09701d80a6c2a61c4c7f5c9b0ded626a3bdf 100644
--- a/tests/impact/depend2.i
+++ b/tests/impact/depend2.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-impact-pragma main"
+ STDOPT: +"-impact-annot main"
*/
int find(int x) { return x; }
@@ -9,7 +9,7 @@ int apply(int x,int y) { return find(x)+y; }
int main()
{
int a = apply(1,100);
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int b = apply(2,200);
return a+b ;
}
diff --git a/tests/impact/depend3.c b/tests/impact/depend3.c
index 4f08af95fee341ba73e23a0ea9d8b9678c9f5ee0..2f30a06de0ea70c8572f161ec9369c0fc4cae936 100644
--- a/tests/impact/depend3.c
+++ b/tests/impact/depend3.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-impact-pragma main"
+ STDOPT: +"-impact-annot main"
*/
#define N 32
@@ -20,7 +20,7 @@ int apply(int x,int y) { return find(x); }
int main()
{
int a = apply( 1 , 100 );
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int b = apply( 2 , 200 );
return a+b ;
}
diff --git a/tests/impact/depend4.i b/tests/impact/depend4.i
index 3eefa9de01d483accb100ccfaba0368a98222b88..24d60d11a44358bb6cf68c9f7140c4bea10a5214 100644
--- a/tests/impact/depend4.i
+++ b/tests/impact/depend4.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-calldeps -then -impact-pragma main"
+ STDOPT: +"-calldeps -then -impact-annot main"
*/
int a, r1, r2;
@@ -25,7 +25,7 @@ void g2() {
void main () {
g1();
- //@ impact pragma stmt;
+ //@ impact_stmt;
f();
g2();
}
diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i
index 52b560fbce0feb000e1bab6d409c7d022216c822..6b8869df18a95ad2619f92a2e980552030989ac1 100644
--- a/tests/impact/depend5.i
+++ b/tests/impact/depend5.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-pragma g"
+ STDOPT: #"@EVA_OPTIONS@ -calldeps -then -impact-annot g"
*/
int a, b, c, d, e;
@@ -12,7 +12,7 @@ void f() {
}
void g() {
- //@ impact pragma stmt;
+ //@ impact_stmt;
d = 2;
e = d;
f();
@@ -24,4 +24,3 @@ void main () {
a = 0;
g();
}
-
diff --git a/tests/impact/first.i b/tests/impact/first.i
index a210dbb40e83facee6309db9453cb18b6a4d027f..74e173934580efd26130ecd8eefb37939733d018 100644
--- a/tests/impact/first.i
+++ b/tests/impact/first.i
@@ -1,12 +1,12 @@
/* run.config
-
- STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact"
+
+ STDOPT: +"-impact-annot impact" +"-lib-entry" +"-main impact"
*/
int a, b, c, e, x, y, z, f, w;
void impact() {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
b = a;
if (c) {
x = b + c;
diff --git a/tests/impact/initial.i b/tests/impact/initial.i
index 9c20d16edba7b176b6bd7a52742417b85e833623..a64c51e4b9a545330f596a98bc0a2b688fd59374 100644
--- a/tests/impact/initial.i
+++ b/tests/impact/initial.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: also tests the parsing of cmdline options of type string_set
- STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'"
+ STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-annot g1" +"-then -main main2 -impact-annot='-@all,+g2'" +"-then -main main3 -impact-annot='-g2,+g3'"
*/
int x1, x2, y2, z2, x3;
@@ -15,7 +15,7 @@ void f1() {
void g1() {
if (c) {
- //@ impact pragma stmt;
+ //@ impact_stmt;
f1();
}
}
@@ -42,7 +42,7 @@ void aux2() {
void g2() {
if (c) {
- //@ impact pragma stmt;
+ //@ impact_stmt;
f2();
if (c) aux2();
}
@@ -65,7 +65,7 @@ void f3() {
void g3() {
- //@ impact pragma stmt;
+ //@ impact_stmt;
f3();
if (c) {
x3 = x3;
diff --git a/tests/impact/loop.i b/tests/impact/loop.i
index 0f8960d4aeefb17c00ffcee651ac700622ea31b8..6099bb2803a198777894139e2063a9b8bb89b684 100644
--- a/tests/impact/loop.i
+++ b/tests/impact/loop.i
@@ -1,6 +1,6 @@
/* run.config
-
- STDOPT: +"-impact-pragma loop" +"-lib-entry" +"-main loop"
+
+ STDOPT: +"-impact-annot loop" +"-lib-entry" +"-main loop"
*/
int c,x,y,z,w;
@@ -9,7 +9,7 @@ void loop () {
while (c) {
z = w + 1;
z = y + 1;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
x = x + 1;
y = x + 1;
}
diff --git a/tests/impact/loop2.i b/tests/impact/loop2.i
index 431ef94ee5b3e1f69e09f043b2ee85358b776721..efe9f7fac61cc78c35b173d9431de16b46dc890e 100644
--- a/tests/impact/loop2.i
+++ b/tests/impact/loop2.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: #"-impact-pragma main -lib-entry -calldeps" +"-then -ulevel 10"
+ STDOPT: #"-impact-annot main -lib-entry -calldeps" +"-then -ulevel 10"
*/
@@ -20,7 +20,7 @@ void f(int i) {
}
void main() {
- //@ impact pragma stmt;
+ //@ impact_stmt;
init ();
for (int i=0; i<10; i++) {
if (t[i]) // should not be selected
diff --git a/tests/impact/oracle/slicing.res.oracle b/tests/impact/oracle/slicing.res.oracle
index bcb4ba87e43c34bcdbab5decd6b82cb2d02298e8..07899df4b03d9d26c87033c1466749b33053b954 100644
--- a/tests/impact/oracle/slicing.res.oracle
+++ b/tests/impact/oracle/slicing.res.oracle
@@ -54,7 +54,7 @@ int w;
void impact(void)
{
if (c) a = 18;
- /*@ impact pragma stmt; */
+ /*@ \impact::impact_stmt ; */
b = a;
if (c) {
x = b + c;
diff --git a/tests/impact/slicing.i b/tests/impact/slicing.i
index 93e008b356443eaed302408ad44e8789970de6c6..57d3eb073a39d75999b560ea1c5e5efaad7239ba 100644
--- a/tests/impact/slicing.i
+++ b/tests/impact/slicing.i
@@ -1,13 +1,13 @@
/* run.config
-
- STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact" +"-impact-slicing" +"-then-on 'impact slicing'" +"-print"
+
+ STDOPT: +"-impact-annot impact" +"-lib-entry" +"-main impact" +"-impact-slicing" +"-then-on 'impact slicing'" +"-print"
*/
int a, b, c, e, x, y, z, f, w;
void impact() {
if (c) a = 18; else x = 5;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
b = a;
if (c) {
x = b + c;
diff --git a/tests/impact/topbot.c b/tests/impact/topbot.c
index 55d424eb28a3ab688027e09b4e9929c13a8ec411..a86a7b4717fc559c9a9f7e15121fa0f0d7b5f743 100644
--- a/tests/impact/topbot.c
+++ b/tests/impact/topbot.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-impact-pragma main -pdg -pdg-print"
+ STDOPT: +"-impact-annot main -pdg -pdg-print"
*/
//@ requires \false;
@@ -7,7 +7,7 @@ void f() { // Bottom PDG
}
void main(int c) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int x = 1;
int y, z;
if (c) {
diff --git a/tests/impact/undef_function.i b/tests/impact/undef_function.i
index 4c7dc4550ca84486e515423bcfd3501c0efc22c8..cb30fa6bf5895fbc54c5b7b78f43de09848fb72b 100644
--- a/tests/impact/undef_function.i
+++ b/tests/impact/undef_function.i
@@ -1,11 +1,11 @@
/* run.config
- STDOPT: +"-impact-pragma main"
+ STDOPT: +"-impact-annot main"
*/
int y;
void g(int);
int main() {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
y=2;
g(y);
return y;
diff --git a/tests/impact/variadic.i b/tests/impact/variadic.i
index c08694d9de5f9448e7bd399f39ae6a6ad93bfa93..3e0998336c2b6e191f1bcc02bf446551884bb1dd 100644
--- a/tests/impact/variadic.i
+++ b/tests/impact/variadic.i
@@ -1,13 +1,13 @@
/* run.config
COMMENT: also tests the parsing of cmdline options of type string_set
- STDOPT: +"-impact-pragma main" +"-then -main main1 -impact-pragma='-main,+main1'" +"-then -main main2 -impact-pragma='-@all,+main2'" +"-then -main main3 -impact-pragma='+aux3,-main2'" +"-then -main main4 -impact-pragma='-aux3,+aux4'"
+ STDOPT: +"-impact-annot main" +"-then -main main1 -impact-annot='-main,+main1'" +"-then -main main2 -impact-annot='-@all,+main2'" +"-then -main main3 -impact-annot='+aux3,-main2'" +"-then -main main4 -impact-annot='-aux3,+aux4'"
*/
int f(int, ...);
int main () {
int i=0;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
i++;
f(i);
}
@@ -25,7 +25,7 @@ void g2(int x, ...);
int main1() {
int x = 3;
- //@ impact pragma stmt;
+ //@ impact_stmt;
g1(1, 2, 3);
g1(1, 2);
return y;
@@ -33,7 +33,7 @@ int main1() {
int main2() {
int x = 3;
- //@ impact pragma stmt;
+ //@ impact_stmt;
g2(1, 2, 3);
g2(1, 2);
return y;
@@ -47,7 +47,7 @@ void g3(int , ...);
int aux3(int x, ...) {
int t = 3;
- //@ impact pragma stmt;
+ //@ impact_stmt;
g1(t);
g1(t);
return y;
@@ -60,7 +60,7 @@ int main3() {
}
void aux4(int x) {
- //@ impact pragma stmt;
+ //@ impact_stmt;
y = x;
}
diff --git a/tests/pdg/inter_alias2.c b/tests/pdg/inter_alias2.c
index 554c37e06f910669e9fd58512cca8316a6674f6c..3258a4dd8f02155c94933803031bfcc42405a6ec 100644
--- a/tests/pdg/inter_alias2.c
+++ b/tests/pdg/inter_alias2.c
@@ -22,6 +22,6 @@ int f2 (int b) {
int main (int i1, int i2) {
int v1 = f1 (i1);
int v2 = f2 (i2);
- /*@ slice pragma expr v1; */
+ /*@ slice_preserve_expr v1; */
return v1 + v2;
}
diff --git a/tests/saveload/load_one.ml b/tests/saveload/load_one.ml
index 02186193baa7df0b46834af0aeb7af26164b4939..c631c11a18957d8ea323ec0db94fb38a05324273 100644
--- a/tests/saveload/load_one.ml
+++ b/tests/saveload/load_one.ml
@@ -4,7 +4,7 @@ let () = at_exit (fun _ -> Sys.remove sav_file)
let main () =
let sparecode () =
- Sparecode.Register.get ~select_annot:false ~select_slice_pragma:false
+ Sparecode.Register.get ~select_annot:false ~select_slice_annot:false
in
let fp = Filepath.Normalized.of_string sav_file in
let p = sparecode () in
diff --git a/tests/slicing/bts0184.i b/tests/slicing/bts0184.i
index f23723e131cfb220da8ed61348a64de1ffb15f2b..b3f47ced58b63ff11bacad6ba5ce7e5c6e988c58 100644
--- a/tests/slicing/bts0184.i
+++ b/tests/slicing/bts0184.i
@@ -1,9 +1,9 @@
/* run.config
- STDOPT: +"-slice-pragma x -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
+ STDOPT: +"-slice-annot x -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
**/
int x(int y, int z)
{
-/*@ slice pragma expr y == 1; */
+/*@ slice_preserve_expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return y;
diff --git a/tests/slicing/bts0190.i b/tests/slicing/bts0190.i
index fc71f6c18ec146a7675765580da285dbbfbee734..22c45313d8827b3591ee39ddd48dc6354e9f2ca3 100644
--- a/tests/slicing/bts0190.i
+++ b/tests/slicing/bts0190.i
@@ -4,7 +4,7 @@ STDOPT: +"-slicing-warn-key cmdline=active -slice-rd y -then-on 'Slicing export'
int z1(void);
int x(int y, int z){
-/*@ slice pragma expr y == 1; */
+/*@ slice_preserve_expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
diff --git a/tests/slicing/bts1768.i b/tests/slicing/bts1768.i
index 4f4be2f640c0794aa40e8c4277c8301aa7e3e808..ae0fe88eff336ec2a7c9b814d0bfc1b6f73016e4 100644
--- a/tests/slicing/bts1768.i
+++ b/tests/slicing/bts1768.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-main main -slice-pragma main -ulevel 10 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
+ STDOPT: +"-main main -slice-annot main -ulevel 10 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
*/
int choix ;
int state = 1;
@@ -45,7 +45,7 @@ int main() {
lecture() ;
fsm_transition() ;
if (state == 3) {
- /*@ slice pragma ctrl ;*/
+ /*@ slice_preserve_ctrl ;*/
break ;
}
step ++ ;
diff --git a/tests/slicing/bts179.i b/tests/slicing/bts179.i
index c6268e81497ba85ee26d425ecb9b5f649c8e879b..fd223df1e26b203e1e45c41df85cc539134f8164 100644
--- a/tests/slicing/bts179.i
+++ b/tests/slicing/bts179.i
@@ -1,6 +1,6 @@
/* run.config
STDOPT: +"-slice-return main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
- STDOPT: +"-slice-pragma main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
+ STDOPT: +"-slice-annot main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
STDOPT: +"-sparecode-analysis"
*/
@@ -14,7 +14,7 @@ void g (void) {
}
int main (void) {
g();
- //@ slice pragma expr S.b;
+ //@ slice_preserve_expr S.b;
S.ab = 1; /* so that S.ab is sparecode in g() */
return S.a ;
}
diff --git a/tests/slicing/bts335.i b/tests/slicing/bts335.i
index 942dde3dcff1816e29b6e7af1dd44dd02c80bcfd..16c1ac98346088236e7f3c9d1bb48dcbf94bfbf0 100644
--- a/tests/slicing/bts335.i
+++ b/tests/slicing/bts335.i
@@ -1,12 +1,12 @@
/* run.config
- STDOPT: +"-slice-pragma g -calldeps -slicing-level 3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
+ STDOPT: +"-slice-annot g -calldeps -slicing-level 3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps"
*/
/*
-bin/toplevel.opt -slice-pragma g -calldeps -slicing-level 3 %{dep:./bts335.c} -debug 2
+bin/toplevel.opt -slice-annot g -calldeps -slicing-level 3 %{dep:./bts335.c} -debug 2
bin/toplevel.opt -pdg-debug -pdg -pdg-debug "-pdg-pot bts335" %{dep:./bts335.c}
*/
int T[2] = {0, 0};
void f (int i) { T[i]++; }
-void g (void) { f(0); /*@ slice pragma expr T[0]; */ }
+void g (void) { f(0); /*@ slice_preserve_expr T[0]; */ }
void main (int c) { if (c) g(); else f(1); }
diff --git a/tests/slicing/bts709.c b/tests/slicing/bts709.c
index 1ce3b2f276af490de9a545f1843b3192dfd5db92..4b5a219e340d4f08f3b2e47a65155065a8950ee0 100644
--- a/tests/slicing/bts709.c
+++ b/tests/slicing/bts709.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-slice-pragma func -no-unicode -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-slice-annot func -no-unicode -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
*/
#include <assert.h>
@@ -34,7 +34,7 @@ void func( void )
}
}
- //@slice pragma stmt;
+ //@slice_preserve_stmt;
65 != var2 ? assert ( 5 != var1):1;
}
diff --git a/tests/slicing/combine.ml b/tests/slicing/combine.ml
index 363a52744674203eb654ba925d0ddcd543241187..eeda7fecc26202c1bb606c158a35821d6715c02a 100644
--- a/tests/slicing/combine.ml
+++ b/tests/slicing/combine.ml
@@ -62,7 +62,7 @@ let main _ =
Format.printf "After Constant propagation :@.";
File.pretty_ast ~prj:proj3 ();
- let proj4 = Sparecode.Register.get ~select_annot:true ~select_slice_pragma:true in
+ let proj4 = Sparecode.Register.get ~select_annot:true ~select_slice_annot:true in
Format.printf "After Sparecode :@.";
File.pretty_ast ~prj:proj4 ();;
diff --git a/tests/slicing/function_lvar.i b/tests/slicing/function_lvar.i
index 05cc5c69a2033223a3a35a16e22ba0b9b2558b4f..75c022e7e60f6f7ae1c6de9f3b11e42a672cdf6c 100644
--- a/tests/slicing/function_lvar.i
+++ b/tests/slicing/function_lvar.i
@@ -1,10 +1,10 @@
/* run.config*
-OPT: -slice-pragma main -then-last -print
+OPT: -slice-annot main -then-last -print
*/
int g(int x) { return x; }
int main() {
/*@ assert &g == &g; */
- /*@ slice pragma stmt; */
+ /*@ slice_preserve_stmt; */
g(0);
}
diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i
index 41d6cb160f0b8386aa41c5e86b1e15bbe232d639..8b6b98a7c3725d0b12dc8cee469198f2ce42a2a8 100644
--- a/tests/slicing/horwitz.i
+++ b/tests/slicing/horwitz.i
@@ -17,7 +17,7 @@ void incr (char * pi) {
int A (int x, char * py) {
x = add (x, *py);
incr (py);
- /*@ slice pragma expr x;*/
+ /*@ slice_preserve_expr x;*/
return x;
}
int main (void) {
diff --git a/tests/slicing/keep_annot.i b/tests/slicing/keep_annot.i
index 3862ae38f9b5cf41da825e25319d90bb74e0c101..dfd32eac3e6827b36b35b2540bc150f51a9bc9c7 100644
--- a/tests/slicing/keep_annot.i
+++ b/tests/slicing/keep_annot.i
@@ -1,8 +1,8 @@
/* run.config
STDOPT: +"-eva-context-valid-pointers -lib-entry -main f -slice-assert f -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-eva-context-valid-pointers -lib-entry -main f -slice-assert f -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-eva-context-valid-pointers -lib-entry -main L -slice-pragma L -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-eva-context-valid-pointers -lib-entry -main L -slice-pragma L -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-eva-context-valid-pointers -lib-entry -main L -slice-annot L -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-eva-context-valid-pointers -lib-entry -main L -slice-annot L -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-slice-return bts1110 -main bts1110 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
@@ -41,7 +41,7 @@ void L (float u,int nn, float dabs[], float *y) {
*y = u - dabs[ii+1] * 2.0;
//@ assert (\forall integer k; u<=dabs[k]);
}
- //@slice pragma expr *y;
+ //@slice_preserve_expr *y;
}
int bts1110(int x) {
diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i
index bd7f5dc7b9a1dfab04bd50d4462e762751469cf9..7adcc828daba8e1cbfbe2791ccfbf025460e2b7e 100644
--- a/tests/slicing/loops.i
+++ b/tests/slicing/loops.i
@@ -1,22 +1,22 @@
/* run.config
- STDOPT: +"-deps -lib-entry -main f1 -slice-pragma f1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-deps -lib-entry -main f1 -slice-annot f1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -lib-entry -main f1 -slice-assert f1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-deps -lib-entry -main f2 -slice-pragma f2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-deps -lib-entry -main f2 -slice-annot f2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -lib-entry -main f2 -slice-assert f2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main test_infinite_loop_3 -slice-value G -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main test_infinite_loop_4 -slice-value G -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main test_infinite_loop_5 -slice-value G -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main loop -slice-value Z -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -slice-calls loop -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-deps -slice-pragma loop -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-deps -slice-annot loop -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -slice-assert loop -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main loop -slice-rd Y -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main loop -slice-rd Z -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main loop -slice-wr Y -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -main loop -slice-wr Z -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-deps -lib-entry -main stop_f1 -slice-pragma stop_f1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-deps -lib-entry -main stop_f1 -slice-annot stop_f1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -lib-entry -main stop_f1 -slice-assert stop_f1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
- STDOPT: +"-deps -lib-entry -main stop_f2 -slice-pragma stop_f2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-deps -lib-entry -main stop_f2 -slice-annot stop_f2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -lib-entry -main stop_f2 -slice-assert stop_f2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -slice-value Z -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
STDOPT: +"-deps -slice-rd Y -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
@@ -39,7 +39,7 @@ int f1 (int c) {
}
else
x = 1;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x ++;
return x;
}
@@ -52,7 +52,7 @@ void f2 (int c) {
x1++;
else
x2++;
- //@slice pragma expr x1;
+ //@slice_preserve_expr x1;
//@ assert x2 > 0 ;
}
}
@@ -71,7 +71,7 @@ int stop_f1 (int c) {
}
else
x = 1;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x ++;
return x;
}
@@ -84,7 +84,7 @@ void stop_f2 (int c) {
x1++;
else
x2++;
- //@slice pragma expr x1;
+ //@slice_preserve_expr x1;
//@ assert x2 > 0 ;
stop () ; /* never loops nor returns */
x1++; /* dead code */
@@ -174,7 +174,7 @@ void loop (int cond) {
if (cond) {
int c = 0 ;
while (1) {
- //@ slice pragma ctrl ;
+ //@ slice_preserve_ctrl ;
if (c) {
X++;
Y = Z ;
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 5b0f79536b0e31e7e140417b4a7f0d9fc16631d2..6af07bc4453f80234d48517a5b94cc498a89e27e 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -231,7 +231,7 @@ void main(void)
lecture_slice_1();
fsm_transition_slice_1();
if (state == 3) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
break;
}
step ++;
diff --git a/tests/slicing/oracle/bts179.1.res.oracle b/tests/slicing/oracle/bts179.1.res.oracle
index 2e4016d0a892b4ab989732bf1112a87de344fc72..9468617167a0663976ccf0631fb1d57685bcca52 100644
--- a/tests/slicing/oracle/bts179.1.res.oracle
+++ b/tests/slicing/oracle/bts179.1.res.oracle
@@ -49,7 +49,7 @@ void g_slice_1(void)
void main(void)
{
g_slice_1();
- /*@ slice pragma expr S.b; */ ;
+ /*@ \slicing::slice_preserve_expr S.b; */ ;
return;
}
diff --git a/tests/slicing/oracle/bts179.2.res.oracle b/tests/slicing/oracle/bts179.2.res.oracle
index ae246ea3100bf5c87632e42d4f62815627570f91..cecae1830a2612504e44128f4edb0ed64941542b 100644
--- a/tests/slicing/oracle/bts179.2.res.oracle
+++ b/tests/slicing/oracle/bts179.2.res.oracle
@@ -42,7 +42,7 @@ int main(void)
{
int __retres;
g();
- /*@ slice pragma expr S.b; */ ;
+ /*@ \slicing::slice_preserve_expr S.b; */ ;
S.ab = 1;
__retres = S.a;
return __retres;
diff --git a/tests/slicing/oracle/bts335.res.oracle b/tests/slicing/oracle/bts335.res.oracle
index 0a1d26a41156efea8686d1507fc4fbbf9a79bb6c..c5de1bb3ad6b2c2ae059cfa8219e179fb5825cfb 100644
--- a/tests/slicing/oracle/bts335.res.oracle
+++ b/tests/slicing/oracle/bts335.res.oracle
@@ -67,7 +67,7 @@ void f_slice_1(int i)
void g_slice_1(void)
{
f_slice_1(0);
- /*@ slice pragma expr T[0]; */ ;
+ /*@ \slicing::slice_preserve_expr T[0]; */ ;
return;
}
diff --git a/tests/slicing/oracle/bts709.res.oracle b/tests/slicing/oracle/bts709.res.oracle
index cad1b0604013ea4845ec40726675fb0f82bbe53d..1607e1cc847e653267cc150a5348beda19626f37 100644
--- a/tests/slicing/oracle/bts709.res.oracle
+++ b/tests/slicing/oracle/bts709.res.oracle
@@ -87,7 +87,7 @@ void func_slice_1(void)
var1 = 3;
var2 = 3;
}
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
if (65 != var2) __FC_assert((5 != var1) != 0,"bts709.c",38,"5 != var1");
return;
}
diff --git a/tests/slicing/oracle/function_lvar.res.oracle b/tests/slicing/oracle/function_lvar.res.oracle
index f5f4aae840e4b4e94778c844818bedff5f58f7d8..6eb30484b2cd0c13b75ce608cdd296a111f10084 100644
--- a/tests/slicing/oracle/function_lvar.res.oracle
+++ b/tests/slicing/oracle/function_lvar.res.oracle
@@ -46,7 +46,7 @@ void g_slice_1(void)
void main(void)
{
/*@ assert &g ≡ &g; */ ;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
g_slice_1();
return;
}
diff --git a/tests/slicing/oracle/horwitz.res.oracle b/tests/slicing/oracle/horwitz.res.oracle
index aedcf8a1bb453499d9c7b46872b3642eed9f628f..82663aa59e4ca74da1e0ce020c5e22b2e85eda95 100644
--- a/tests/slicing/oracle/horwitz.res.oracle
+++ b/tests/slicing/oracle/horwitz.res.oracle
@@ -121,7 +121,7 @@
[pdg] computing for function main
[pdg] done for function main
Slicing project worklist [default] =
-[main_slice_1 = change_call for call 23 -> A_slice_1][A_slice_1 = change_call for call 10 -> incr_slice_1]
+[main_slice_1 = change_call for call 22 -> A_slice_1][A_slice_1 = change_call for call 10 -> incr_slice_1]
[slicing] exporting project to 'Sliced code'...
[slicing] applying all slicing requests...
diff --git a/tests/slicing/oracle/keep_annot.2.res.oracle b/tests/slicing/oracle/keep_annot.2.res.oracle
index 1388652d1300aa322300d746ea02aaaee07275a7..6c1d4f17a1512a4ce58593bb9ef43682ee455074 100644
--- a/tests/slicing/oracle/keep_annot.2.res.oracle
+++ b/tests/slicing/oracle/keep_annot.2.res.oracle
@@ -44,7 +44,7 @@ void L(float u, int nn, float *dabs, float *y)
/*@ assert ∀ ℤ k; u ≤ *(dabs + k); */ ;
ii --;
}
- /*@ slice pragma expr *y; */ ;
+ /*@ \slicing::slice_preserve_expr *y; */ ;
return;
}
diff --git a/tests/slicing/oracle/keep_annot.3.res.oracle b/tests/slicing/oracle/keep_annot.3.res.oracle
index 02c0f75804a3d67baba9ab00de6b80a39d9737da..1875337f9d9b3fbcea79c12907e964c6e680108d 100644
--- a/tests/slicing/oracle/keep_annot.3.res.oracle
+++ b/tests/slicing/oracle/keep_annot.3.res.oracle
@@ -42,7 +42,7 @@ void L(float u, int nn, float *dabs, float *y)
*y = (float)((double)u - (double)*(dabs + (ii + 1)) * 2.0);
ii --;
}
- /*@ slice pragma expr *y; */ ;
+ /*@ \slicing::slice_preserve_expr *y; */ ;
return;
}
diff --git a/tests/slicing/oracle/loops.0.res.oracle b/tests/slicing/oracle/loops.0.res.oracle
index 55beef2931ddd3127c22774ea2f577ed447557ec..195fb9c2e96c8456f15003c9e6cb5f432692faae 100644
--- a/tests/slicing/oracle/loops.0.res.oracle
+++ b/tests/slicing/oracle/loops.0.res.oracle
@@ -41,7 +41,7 @@ void f1(void)
{
int x;
x = 1;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x ++;
return;
}
diff --git a/tests/slicing/oracle/loops.10.res.oracle b/tests/slicing/oracle/loops.10.res.oracle
index 45eccd8972e154ec7617ee9096d5175e2fc93cac..ad29d5d345d6cdfb451177128ad492f76e582290 100644
--- a/tests/slicing/oracle/loops.10.res.oracle
+++ b/tests/slicing/oracle/loops.10.res.oracle
@@ -67,7 +67,7 @@ void loop_slice_1(void)
{
int c;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
c = 1;
/*@ assert c ≡ 1; */ ;
}
diff --git a/tests/slicing/oracle/loops.12.res.oracle b/tests/slicing/oracle/loops.12.res.oracle
index c37d8ec3ed854e405b20549e5ffa1785801170e4..5b464448a4e655892f150d74bf75bd39bc918e61 100644
--- a/tests/slicing/oracle/loops.12.res.oracle
+++ b/tests/slicing/oracle/loops.12.res.oracle
@@ -44,7 +44,7 @@ void loop(int cond)
if (cond) {
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.13.res.oracle b/tests/slicing/oracle/loops.13.res.oracle
index 19f0f0820f6248d904aa53a0a04e82b6bada7235..989df21adb3e464f0ea941efed4593e888962e54 100644
--- a/tests/slicing/oracle/loops.13.res.oracle
+++ b/tests/slicing/oracle/loops.13.res.oracle
@@ -44,7 +44,7 @@ void loop(int cond)
if (cond) {
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.15.res.oracle b/tests/slicing/oracle/loops.15.res.oracle
index 726662f7e0d78991f8844cfe11f1397ebcf12813..75786cb22209a05b389a47ced5a2d9962108c915 100644
--- a/tests/slicing/oracle/loops.15.res.oracle
+++ b/tests/slicing/oracle/loops.15.res.oracle
@@ -51,7 +51,7 @@ void stop_f1(void)
{
int x;
x = 1;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x ++;
return;
}
diff --git a/tests/slicing/oracle/loops.17.res.oracle b/tests/slicing/oracle/loops.17.res.oracle
index 04a864ff382a7e169421e1efe1e4401581e57c13..0bf093eafe58bdd65b4e42a882559c7dac652f74 100644
--- a/tests/slicing/oracle/loops.17.res.oracle
+++ b/tests/slicing/oracle/loops.17.res.oracle
@@ -53,7 +53,7 @@ void stop_f2(int c)
int x2 = 0;
if (! (x1 + x2 < c + 10)) goto break_cont_1;
if (c) x1 ++;
- /*@ slice pragma expr x1; */ ;
+ /*@ \slicing::slice_preserve_expr x1; */ ;
break_cont_1: return;
}
diff --git a/tests/slicing/oracle/loops.2.res.oracle b/tests/slicing/oracle/loops.2.res.oracle
index 8f09cbb270ad520494649abdd757d02b44b15857..94dc22805ddea1052a9acfcf2635bc5c9fca0f77 100644
--- a/tests/slicing/oracle/loops.2.res.oracle
+++ b/tests/slicing/oracle/loops.2.res.oracle
@@ -45,7 +45,7 @@ void f2(int c)
int x1 = 0;
while (1) {
if (c) x1 ++;
- /*@ slice pragma expr x1; */ ;
+ /*@ \slicing::slice_preserve_expr x1; */ ;
}
return;
}
diff --git a/tests/slicing/oracle/loops.21.res.oracle b/tests/slicing/oracle/loops.21.res.oracle
index 060ea45f1d6604803fb3050b1fa840d9ee578064..198ab85fd7052d832b28ad3086ba799a20c0a70d 100644
--- a/tests/slicing/oracle/loops.21.res.oracle
+++ b/tests/slicing/oracle/loops.21.res.oracle
@@ -73,7 +73,7 @@ void loop_slice_1(void)
{
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.22.res.oracle b/tests/slicing/oracle/loops.22.res.oracle
index 9b53131b45d7694bd90cdce58f315e9bba6405cb..f3b6ac451e581cef7cea08755adc97fd14d61819 100644
--- a/tests/slicing/oracle/loops.22.res.oracle
+++ b/tests/slicing/oracle/loops.22.res.oracle
@@ -73,7 +73,7 @@ void loop_slice_1(void)
{
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.9.res.oracle b/tests/slicing/oracle/loops.9.res.oracle
index b5fcf07545c01ddca66358df26b66993a5833357..6710802f89bf6f9b341dafd9282b5297f1fd57cb 100644
--- a/tests/slicing/oracle/loops.9.res.oracle
+++ b/tests/slicing/oracle/loops.9.res.oracle
@@ -65,7 +65,7 @@
void loop_slice_1(void)
{
while (1)
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
return;
}
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index 87f3dae909c810ed7d3196bc2c408d991520897d..8198fa3a63315ade2aa6eb185474d71fed838277 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -265,8 +265,8 @@ Print slice = f_slice_1: (InCtrl: <[--d], [ S ]>)
(In4: <[--d], [ S ]>) */
/* <[--d], [ S ]> */
/* <[---], [---]> */ int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ /* <[---], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr z; */ /* <[---], [---]> */
+ ;
/* invisible call */ /* <[---], [---]> */
send(z);
/* <[---], [---]> */
@@ -416,8 +416,8 @@ Print slice = f_slice_1: (InCtrl: <[--d], [ S ]>)
(In4: <[--d], [ S ]>) */
/* <[--d], [ S ]> */
/* <[---], [---]> */ int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ /* <[---], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr z; */ /* <[---], [---]> */
+ ;
/* invisible call */ /* <[---], [---]> */
send(z);
/* <[---], [---]> */
@@ -555,8 +555,8 @@ Print slice = f_slice_1: (InCtrl: <[acd], [---]>)
/* call to k_slice_1: */
/* <[acd], [---]> */
/* <[---], [---]> */ int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ /* <[---], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr z; */ /* <[---], [---]> */
+ ;
/* invisible call */ /* <[---], [---]> */
send(z);
/* <[---], [---]> */
diff --git a/tests/slicing/oracle/select_by_annot.0.res.oracle b/tests/slicing/oracle/select_by_annot.0.res.oracle
index e5de9941760551310d3e1f26e7eaa08f9c620de0..a0b02825e2f205b1a3bb1e725771d9ba06f7c7e7 100644
--- a/tests/slicing/oracle/select_by_annot.0.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.0.res.oracle
@@ -186,149 +186,149 @@ RESULT for main:
-[--d]-> 8
-[--d]-> 11
-[--d]-> 57
- {n14}: Call113-InCtrl : modifS(a,b);
+ {n14}: Call111-InCtrl : modifS(a,b);
-[-c-]-> 1
- {n15}: Call113-In1 : modifS(a,b);
+ {n15}: Call111-In1 : modifS(a,b);
-[-c-]-> 1
-[--d]-> 2
-[--d]-> 6
-[--d]-> 11
-[-c-]-> 14
- {n16}: Call113-In2 : modifS(a,b);
+ {n16}: Call111-In2 : modifS(a,b);
-[-c-]-> 1
-[--d]-> 3
-[--d]-> 7
-[-c-]-> 14
- {n17}: Call113-Out(S.a) : modifS(a,b);
+ {n17}: Call111-Out(S.a) : modifS(a,b);
-[-c-]-> 1
-[-c-]-> 14
-[--d]-> 15
-[--d]-> 56
- {n18}: Call113-Out(S.b) : modifS(a,b);
+ {n18}: Call111-Out(S.b) : modifS(a,b);
-[-c-]-> 1
-[-c-]-> 14
-[--d]-> 16
-[--d]-> 55
- {n19}: Call114-InCtrl : d = new_int();
+ {n19}: Call112-InCtrl : d = new_int();
-[-c-]-> 1
- {n20}: Call114-OutRet : d = new_int();
+ {n20}: Call112-OutRet : d = new_int();
-[-c-]-> 1
-[-c-]-> 19
- {n21}: Call115-InCtrl : f1(d);
+ {n21}: Call113-InCtrl : f1(d);
-[-c-]-> 1
- {n22}: Call115-In1 : f1(d);
+ {n22}: Call113-In1 : f1(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 21
- {n23}: Call115-Out(Sa) : f1(d);
+ {n23}: Call113-Out(Sa) : f1(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 21
-[--d]-> 22
- {n24}: Call116-InCtrl : f2(d);
+ {n24}: Call114-InCtrl : f2(d);
-[-c-]-> 1
- {n25}: Call116-In1 : f2(d);
+ {n25}: Call114-In1 : f2(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 24
- {n26}: Call116-Out(Sa) : f2(d);
+ {n26}: Call114-Out(Sa) : f2(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 24
-[--d]-> 25
- {n27}: Call117-InCtrl : f3(d);
+ {n27}: Call115-InCtrl : f3(d);
-[-c-]-> 1
- {n28}: Call117-In1 : f3(d);
+ {n28}: Call115-In1 : f3(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 27
- {n29}: Call117-Out(Sa) : f3(d);
+ {n29}: Call115-Out(Sa) : f3(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 27
-[--d]-> 28
- {n30}: Call118-InCtrl : f4(d);
+ {n30}: Call116-InCtrl : f4(d);
-[-c-]-> 1
- {n31}: Call118-In1 : f4(d);
+ {n31}: Call116-In1 : f4(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 30
- {n32}: Call118-Out(Sa) : f4(d);
+ {n32}: Call116-Out(Sa) : f4(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 30
-[--d]-> 31
- {n33}: Call119-InCtrl : f5(d);
+ {n33}: Call117-InCtrl : f5(d);
-[-c-]-> 1
- {n34}: Call119-In1 : f5(d);
+ {n34}: Call117-In1 : f5(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 33
- {n35}: Call119-Out(Sa) : f5(d);
+ {n35}: Call117-Out(Sa) : f5(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 33
-[--d]-> 34
- {n36}: Call120-InCtrl : f6(d);
+ {n36}: Call118-InCtrl : f6(d);
-[-c-]-> 1
- {n37}: Call120-In1 : f6(d);
+ {n37}: Call118-In1 : f6(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 36
- {n38}: Call120-Out(Sa) : f6(d);
+ {n38}: Call118-Out(Sa) : f6(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 36
-[--d]-> 37
- {n39}: Call121-InCtrl : f7(d);
+ {n39}: Call119-InCtrl : f7(d);
-[-c-]-> 1
- {n40}: Call121-In1 : f7(d);
+ {n40}: Call119-In1 : f7(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 39
- {n41}: Call121-Out(Sa) : f7(d);
+ {n41}: Call119-Out(Sa) : f7(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 39
-[--d]-> 40
- {n42}: Call122-InCtrl : f8(d);
+ {n42}: Call120-InCtrl : f8(d);
-[-c-]-> 1
- {n43}: Call122-In1 : f8(d);
+ {n43}: Call120-In1 : f8(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 42
- {n44}: Call122-Out(S.a) : f8(d);
+ {n44}: Call120-Out(S.a) : f8(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 42
-[--d]-> 43
- {n45}: Call122-Out(Sa) : f8(d);
+ {n45}: Call120-Out(Sa) : f8(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 42
-[--d]-> 43
- {n46}: Call123-InCtrl : f9(d,a);
+ {n46}: Call121-InCtrl : f9(d,a);
-[-c-]-> 1
- {n47}: Call123-In1 : f9(d,a);
+ {n47}: Call121-In1 : f9(d,a);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 46
- {n48}: Call123-In2 : f9(d,a);
+ {n48}: Call121-In2 : f9(d,a);
-[-c-]-> 1
-[--d]-> 2
-[--d]-> 6
-[--d]-> 11
-[-c-]-> 46
- {n49}: Call123-Out(X9) : f9(d,a);
+ {n49}: Call121-Out(X9) : f9(d,a);
-[-c-]-> 1
-[-c-]-> 46
-[--d]-> 47
-[--d]-> 48
- {n50}: Call123-Out(Y9) : f9(d,a);
+ {n50}: Call121-Out(Y9) : f9(d,a);
-[-c-]-> 1
-[-c-]-> 46
-[--d]-> 54
- {n51}: Call123-Out(Z9) : f9(d,a);
+ {n51}: Call121-Out(Z9) : f9(d,a);
-[-c-]-> 1
-[-c-]-> 46
-[--d]-> 48
@@ -403,8 +403,8 @@ modifS_slice_1:
S.a += a;
/* <[---], [---]> */
S.b -= b;
- /*@ slice pragma expr S.a; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr S.a; */ /* <[ S ], [---]> */
+ ;
/* <[---], [---]> */
return;
}
@@ -435,8 +435,8 @@ main_slice_1:
/* <[--d], [---]> */
a = 1;
}
- /*@ slice pragma expr a + b; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr a + b; */ /* <[ S ], [---]> */
+ ;
/*@ assert
Eva: signed_overflow: (int)((int)(a + b) + c) + d ≤ 2147483647;
*/
@@ -491,7 +491,7 @@ struct Tstr S;
void modifS_slice_1(int a)
{
S.a += a;
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
@@ -504,7 +504,7 @@ void main(void)
/*@ assert b ≡ 0; */ ;
a = 1;
}
- /*@ slice pragma expr a + b; */ ;
+ /*@ \slicing::slice_preserve_expr a + b; */ ;
modifS_slice_1(a);
return;
}
@@ -535,8 +535,8 @@ modifS_slice_1:
S.a += a;
/* <[---], [---]> */
S.b -= b;
- /*@ slice pragma expr S.a; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr S.a; */ /* <[ S ], [---]> */
+ ;
/* <[---], [---]> */
return;
}
@@ -567,8 +567,8 @@ main_slice_1:
/* <[--d], [---]> */
a = 1;
}
- /*@ slice pragma expr a + b; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr a + b; */ /* <[ S ], [---]> */
+ ;
/*@ assert
Eva: signed_overflow: (int)((int)(a + b) + c) + d ≤ 2147483647;
*/
@@ -623,7 +623,7 @@ struct Tstr S;
void modifS_slice_1(int a)
{
S.a += a;
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
@@ -636,7 +636,7 @@ void main(void)
/*@ assert b ≡ 0; */ ;
a = 1;
}
- /*@ slice pragma expr a + b; */ ;
+ /*@ \slicing::slice_preserve_expr a + b; */ ;
modifS_slice_1(a);
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index 9b4b2a0f20bc28ddc7bd898f667559691ded6fe4..ce346dce5ae6fe4a2d3c725c3457e21a147f2742 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -168,7 +168,7 @@ void main(void)
/*@ assert b ≡ 0; */ ;
a = 1;
}
- /*@ slice pragma expr a + b; */ ;
+ /*@ \slicing::slice_preserve_expr a + b; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index 178bb3278c02a3efd47381de335569cabf167d45..4f464e044202f7031397bf447362b6aad5a5466f 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -169,7 +169,7 @@ void f7_slice_1(int cond)
{
int *p = & S.a;
if (cond) {
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
Sa = *p;
Sa ++;
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index f466ab7ac093c409ed262244406e15fcaf842df4..d5e63cd87e8a5e280c9e024ccdc80646c74ccb73 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -170,7 +170,7 @@ void f8_slice_1(int cond)
loop variant cond; */
while (cond) {
/*@ assert cond ≤ \at(cond,Pre); */ ;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
(S.a) ++;
cond --;
}
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index 1f98d6f3ef1062090ecc386a21c7e46ef9898341..72b084e92b0b701372568fded11b061d1de93232 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -164,7 +164,7 @@ void f9_slice_1(int c1, int c2)
{
if (c1 > c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: X9 = c1;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index 988211d29e3251d1434e265cc473a9b7a675e687..ab17e6f203af46bb7b00a62a6c0a63fb66a09ce8 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -167,7 +167,7 @@ struct Tstr S;
void modifS_slice_1(int a)
{
S.a += a;
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 769500d84d8314be9f397932a125b0d26fd6adf5..97c299468f5abcf87d97afb829b24f4c6a4dd82a 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -167,7 +167,7 @@ struct Tstr S;
void f1_slice_1(void)
{
int *p = & S.a;
- /*@ slice pragma expr *p; */ ;
+ /*@ \slicing::slice_preserve_expr *p; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index feed01b3a62a32da6addde70735ad325af67505c..bbab225646d614c4271c13fd4ddbbfd7e7d0216d 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -166,7 +166,7 @@ struct Tstr {
struct Tstr S;
void f2_slice_1(void)
{
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index 75357eb578c2958a0b6622c63eb334667610ce94..f94ad6d8fa10b2604bccd46e7041788e0ad08d3f 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -162,7 +162,7 @@
void f3_slice_1(int cond)
{
if (cond)
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index 1c1c5920893b474fb648f90eb55916b0c4a134da..62aa2725a1c203cdf5af59f4483f16637d32f433 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -169,7 +169,7 @@ void f4_slice_1(int cond)
{
int *p = & S.a;
if (cond)
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
Sa = *p;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index 2cf898dc5445295a4764781ccfcf2930d69ad397..368824e1e2fe61b7407066379eb528c4d004f4f6 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -162,7 +162,7 @@
void f5_slice_1(int cond)
{
if (cond)
- /*@ slice pragma expr 1; */ ;
+ /*@ \slicing::slice_preserve_expr 1; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index 9bab22454a4ca0a5c5d1eb898c853b19ee727335..4e7a90020e4d950435e49ddcb77cc18fb2157770 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -168,7 +168,7 @@ int Sa;
void f6_slice_1(int cond)
{
int *p = & S.a;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
if (cond) {
Sa = *p;
Sa ++;
diff --git a/tests/slicing/oracle/select_return.0.res.oracle b/tests/slicing/oracle/select_return.0.res.oracle
index e7783ec0de811be1c04a2ee8eebde4910c4d27f6..68854c2431078593718da8f9ad59b0ec3e2d2d78 100644
--- a/tests/slicing/oracle/select_return.0.res.oracle
+++ b/tests/slicing/oracle/select_return.0.res.oracle
@@ -118,7 +118,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.1.res.oracle b/tests/slicing/oracle/select_return.1.res.oracle
index 333c77abdecacf5ac181f11235928ed98ab43e6a..c4363591c65eca9e164596d5a4322c8f9d047263 100644
--- a/tests/slicing/oracle/select_return.1.res.oracle
+++ b/tests/slicing/oracle/select_return.1.res.oracle
@@ -113,7 +113,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.10.res.oracle b/tests/slicing/oracle/select_return.10.res.oracle
index 35cd5e8e21eb83704a80a654c59603fbf3c1e96d..a46a3eaf86cbc050fa3129ea63318a75d146cb65 100644
--- a/tests/slicing/oracle/select_return.10.res.oracle
+++ b/tests/slicing/oracle/select_return.10.res.oracle
@@ -138,7 +138,7 @@ void f_slice_1(int y)
k_slice_2(0,0);
k_slice_2(y,0);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.11.res.oracle b/tests/slicing/oracle/select_return.11.res.oracle
index 25abd7c442aa93c7ad063c8e3989c3dc0674b07e..3f364eca0dd3a36dfee64e02da055caec52fb3c8 100644
--- a/tests/slicing/oracle/select_return.11.res.oracle
+++ b/tests/slicing/oracle/select_return.11.res.oracle
@@ -115,7 +115,7 @@ int f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.12.res.oracle b/tests/slicing/oracle/select_return.12.res.oracle
index 71a60f4e33e15d0d464f1d2f159717960f91d55d..af8de07737b508dc896ab7e07ef81cdb68af6a42 100644
--- a/tests/slicing/oracle/select_return.12.res.oracle
+++ b/tests/slicing/oracle/select_return.12.res.oracle
@@ -110,7 +110,7 @@ int f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.13.res.oracle b/tests/slicing/oracle/select_return.13.res.oracle
index 374b5e578764b4891273f5c1627004a2bfa24f5f..cc454f2d4888f0c3f759925547f310391b993e7b 100644
--- a/tests/slicing/oracle/select_return.13.res.oracle
+++ b/tests/slicing/oracle/select_return.13.res.oracle
@@ -108,7 +108,7 @@ int f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.14.res.oracle b/tests/slicing/oracle/select_return.14.res.oracle
index 490fec9745427b9e85e9e5085cf96bb2da4654d0..32cb1466401e39a4844894bad302957c92f2f68b 100644
--- a/tests/slicing/oracle/select_return.14.res.oracle
+++ b/tests/slicing/oracle/select_return.14.res.oracle
@@ -113,7 +113,7 @@ int f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.15.res.oracle b/tests/slicing/oracle/select_return.15.res.oracle
index 133365cf41b2999b102ee518bc1bdeda74a6a391..b433fce8b712b2d081946d2d056f11e81c71f241 100644
--- a/tests/slicing/oracle/select_return.15.res.oracle
+++ b/tests/slicing/oracle/select_return.15.res.oracle
@@ -115,7 +115,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.16.res.oracle b/tests/slicing/oracle/select_return.16.res.oracle
index 22f1c275ac6b52a593a0c791694839a8cde3e40c..10680ce7ad94e9381ad5b808744513782c7a3f1c 100644
--- a/tests/slicing/oracle/select_return.16.res.oracle
+++ b/tests/slicing/oracle/select_return.16.res.oracle
@@ -110,7 +110,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.17.res.oracle b/tests/slicing/oracle/select_return.17.res.oracle
index c2e59c2a9427289d81812b4d653f651f21ed1a8a..3f154a6cc2979bdd45c471677b6aebbc8bfb0eec 100644
--- a/tests/slicing/oracle/select_return.17.res.oracle
+++ b/tests/slicing/oracle/select_return.17.res.oracle
@@ -108,7 +108,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.18.res.oracle b/tests/slicing/oracle/select_return.18.res.oracle
index 76d57c2c3535dd9adb61d6a4f2b87df92fa4dba7..b157018c027d3fe1b91edf3fb1cb2c34c58ec915 100644
--- a/tests/slicing/oracle/select_return.18.res.oracle
+++ b/tests/slicing/oracle/select_return.18.res.oracle
@@ -113,7 +113,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.2.res.oracle b/tests/slicing/oracle/select_return.2.res.oracle
index 30dee131fa871ac96f413368a1dfedf93387e935..30fb6b087fb844be4c60ed54967ba5696f6cbae3 100644
--- a/tests/slicing/oracle/select_return.2.res.oracle
+++ b/tests/slicing/oracle/select_return.2.res.oracle
@@ -111,7 +111,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.3.res.oracle b/tests/slicing/oracle/select_return.3.res.oracle
index 512580d248886fb56b1842c5db96c01a31b74a47..9f2fc687b002d0cb22ff66e206bb5bcf9adc37f5 100644
--- a/tests/slicing/oracle/select_return.3.res.oracle
+++ b/tests/slicing/oracle/select_return.3.res.oracle
@@ -116,7 +116,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.4.res.oracle b/tests/slicing/oracle/select_return.4.res.oracle
index 0bdd4613f7806fd5e1e2fdca4118bcc864b80afa..f4286572299790bf787d334ccefd04602b218e6a 100644
--- a/tests/slicing/oracle/select_return.4.res.oracle
+++ b/tests/slicing/oracle/select_return.4.res.oracle
@@ -119,7 +119,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.5.res.oracle b/tests/slicing/oracle/select_return.5.res.oracle
index b9b128bad9c1cbda8f696b28830c677e356c37e0..e0cdb0818c90f88a1a94fed71aaf7051efd5cb80 100644
--- a/tests/slicing/oracle/select_return.5.res.oracle
+++ b/tests/slicing/oracle/select_return.5.res.oracle
@@ -119,7 +119,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.6.res.oracle b/tests/slicing/oracle/select_return.6.res.oracle
index 2a25d0ccc9411c94fdac081176c72eec32317b15..e7b866efb2b71b50f58083c1499056f0c28c273a 100644
--- a/tests/slicing/oracle/select_return.6.res.oracle
+++ b/tests/slicing/oracle/select_return.6.res.oracle
@@ -119,7 +119,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.7.res.oracle b/tests/slicing/oracle/select_return.7.res.oracle
index 4f6a431dcc0bbeebf9682b6d4a9328ea1100950b..87b0ed4ce0c766e56e667743c17f96da284d7963 100644
--- a/tests/slicing/oracle/select_return.7.res.oracle
+++ b/tests/slicing/oracle/select_return.7.res.oracle
@@ -126,7 +126,7 @@ void f_slice_1(int y)
{
k_slice_2(y,0);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.8.res.oracle b/tests/slicing/oracle/select_return.8.res.oracle
index 24560b33d23b5d67824a153a3a76014d300dc0c2..4fcef2ec75b51f344c35da3343cbed40ff93fa3f 100644
--- a/tests/slicing/oracle/select_return.8.res.oracle
+++ b/tests/slicing/oracle/select_return.8.res.oracle
@@ -131,7 +131,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0);
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.9.res.oracle b/tests/slicing/oracle/select_return.9.res.oracle
index 1aff238e6d11794e8df6f5bb26a74905e86e1015..4cfbd57f9e989de8675cfb5434e6cd22f1b9f0a2 100644
--- a/tests/slicing/oracle/select_return.9.res.oracle
+++ b/tests/slicing/oracle/select_return.9.res.oracle
@@ -131,7 +131,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0);
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.0.res.oracle b/tests/slicing/oracle/select_return_bis.0.res.oracle
index 1986a1f5e3acae8a42ccbfff0539ce6e58d672af..b8ab1bf32e1abdea372fe78c12dc4bf254fd6b25 100644
--- a/tests/slicing/oracle/select_return_bis.0.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.0.res.oracle
@@ -130,7 +130,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.1.res.oracle b/tests/slicing/oracle/select_return_bis.1.res.oracle
index 0b66bb17ec39fc3aef7101f8b3216057365a516f..45323336f203a43c7e061ff81e5e85ca00b81310 100644
--- a/tests/slicing/oracle/select_return_bis.1.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.1.res.oracle
@@ -127,7 +127,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.10.res.oracle b/tests/slicing/oracle/select_return_bis.10.res.oracle
index 0a9c10c832f9694dc26c279a627e8db65ecfa4de..216426c6034d0b31fea09c5f271a7d1c86eadd9a 100644
--- a/tests/slicing/oracle/select_return_bis.10.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.10.res.oracle
@@ -152,7 +152,7 @@ void f_slice_1(int y)
k_slice_2(0,0);
k_slice_2(y,0);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.2.res.oracle b/tests/slicing/oracle/select_return_bis.2.res.oracle
index 77cabccd7a93c56b2af0ebead53f5ae64093c6b4..6c06347fafaa0a45054170c2f89add6393ceb7c1 100644
--- a/tests/slicing/oracle/select_return_bis.2.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.2.res.oracle
@@ -117,7 +117,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.3.res.oracle b/tests/slicing/oracle/select_return_bis.3.res.oracle
index 66d2c8939ba6cc1a5e72a993939498f530b7922c..ef2f302ebff8e4a404db69d688b28c65c648893a 100644
--- a/tests/slicing/oracle/select_return_bis.3.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.3.res.oracle
@@ -122,7 +122,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.4.res.oracle b/tests/slicing/oracle/select_return_bis.4.res.oracle
index 5b6b79c6c3273b7b0181ba75668b10a753852bd7..e31eb88952ae539002f9efb588f7690d251ce445 100644
--- a/tests/slicing/oracle/select_return_bis.4.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.4.res.oracle
@@ -139,7 +139,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.5.res.oracle b/tests/slicing/oracle/select_return_bis.5.res.oracle
index fb4196860a838d812844a6f7f39e0e4689f8dd63..db7f16507247f9a9d6bc88e360343a6a53a6cae3 100644
--- a/tests/slicing/oracle/select_return_bis.5.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.5.res.oracle
@@ -135,7 +135,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0,0);
int z = k_slice_1(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.6.res.oracle b/tests/slicing/oracle/select_return_bis.6.res.oracle
index f2a805d61ebcab10eb8ffed699629f3d5d4db38a..4555fb17d62009d1365db1ad818d4bab44edbeaf 100644
--- a/tests/slicing/oracle/select_return_bis.6.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.6.res.oracle
@@ -129,7 +129,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.7.res.oracle b/tests/slicing/oracle/select_return_bis.7.res.oracle
index 8543cd69f0576d2e3509e25d28eeead1781fc0d6..647cd4f4d18d584249b13baceae87a643060a967 100644
--- a/tests/slicing/oracle/select_return_bis.7.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.7.res.oracle
@@ -134,7 +134,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.8.res.oracle b/tests/slicing/oracle/select_return_bis.8.res.oracle
index bfe24c784f68a522a6c45c3eeb6d8f346f579a0e..a4d0ecff5967d41b188c4141249502c6e2e30359 100644
--- a/tests/slicing/oracle/select_return_bis.8.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.8.res.oracle
@@ -147,7 +147,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0,0);
k_slice_1(0,y,0,0);
int z = k_slice_1(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.9.res.oracle b/tests/slicing/oracle/select_return_bis.9.res.oracle
index e0d303d726da106b32b701381aaf68fd1b1eeb53..365ba603f24721e43c1b30b0f08695ea2a8b50a5 100644
--- a/tests/slicing/oracle/select_return_bis.9.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.9.res.oracle
@@ -145,7 +145,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0);
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/sizeof.0.res.oracle b/tests/slicing/oracle/sizeof.0.res.oracle
index eb48d65bde802474978ecbde23d96c0103d8b6ea..aefc9b579795bab56f8a987586727b51054040a5 100644
--- a/tests/slicing/oracle/sizeof.0.res.oracle
+++ b/tests/slicing/oracle/sizeof.0.res.oracle
@@ -253,7 +253,7 @@ int main(void)
r = (int)((unsigned int)r + tmp_7);
tmp_8 = SizeOfE_tab_acces_1_slice_1();
r = (int)((unsigned int)r + tmp_8);
- /*@ slice pragma expr r; */ ;
+ /*@ \slicing::slice_preserve_expr r; */ ;
return r;
}
diff --git a/tests/slicing/oracle/sizeof.11.res.oracle b/tests/slicing/oracle/sizeof.11.res.oracle
index 993cbeede01ed8cbefe2be4f5c2ae1c6e5b8e4ec..6b86b676d5758c4fa1b8aae3e7fd67b1bc5539c5 100644
--- a/tests/slicing/oracle/sizeof.11.res.oracle
+++ b/tests/slicing/oracle/sizeof.11.res.oracle
@@ -253,7 +253,7 @@ void main(void)
r = (int)((unsigned int)r + tmp_7);
tmp_8 = SizeOfE_tab_acces_1_slice_1();
r = (int)((unsigned int)r + tmp_8);
- /*@ slice pragma expr r; */ ;
+ /*@ \slicing::slice_preserve_expr r; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle
index 9b3495ef6c9ef1724c8224f4ba96b72c9c7453bc..7e656c68dc30053efe91b321b18501881678ab95 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle
@@ -4,28 +4,28 @@ int x;
int y;
void nop1(int c1, int c2)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
x = 1;
return;
}
void nop2(int c1, int c2)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
x = 1;
return;
}
void nop3(int c1, int c2)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
x = 1;
return;
}
void nop4(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
if (c1) ;
x = 1;
return;
@@ -34,7 +34,7 @@ void nop4(int c1, int c2)
void nop5(int c1, int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -42,7 +42,7 @@ void nop5(int c1, int c2)
void nop6(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -50,7 +50,7 @@ void nop6(int c1, int c2)
void nop7(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -58,7 +58,7 @@ void nop7(int c1, int c2)
void nop8(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -67,7 +67,7 @@ void nop8(int c1, int c2)
void double_effect1(int c1, int c2)
{
int tmp;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{ /* sequence */
tmp = y;
y ++;
@@ -78,7 +78,7 @@ void double_effect1(int c1, int c2)
void double_effect2(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
@@ -92,7 +92,7 @@ void double_effect3(int c1, int c2)
{
int tmp;
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = y;
@@ -106,7 +106,7 @@ void double_effect3(int c1, int c2)
void double_effect4(int c1, int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = y;
@@ -119,7 +119,7 @@ void double_effect4(int c1, int c2)
void double_effect5(int c1, int c2)
{
if (c2) {
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
@@ -133,7 +133,7 @@ void double_effect5(int c1, int c2)
void test1(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
@@ -141,7 +141,7 @@ void test1(int c1, int c2)
void test2(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
y = c2;
return;
@@ -150,7 +150,7 @@ void test2(int c1, int c2)
void test3(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
y = c2;
return;
@@ -159,7 +159,7 @@ void test3(int c1, int c2)
void test4(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
c2 ++;
@@ -172,7 +172,7 @@ void test5(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: x = c1;
y = c2;
return;
@@ -183,7 +183,7 @@ void test6(int c1, int c2)
int tmp;
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = c1;
@@ -199,7 +199,7 @@ void test7(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = c1;
@@ -215,7 +215,7 @@ void test8(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
L: { /* sequence */
@@ -233,7 +233,7 @@ void test9(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
L: c2 ++;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle
index 859cd05b5688d53d5681c11de05eeae99ac16f5d..c979fdd001bcbc8018c8f3b425af8f9a34938ce9 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop1(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle
index 92eeefa69ef9cb603ce67ef380407814b6294b83..14b61ee3dcc7e73f15af82a6a7ed21f03eae5699 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle
@@ -27,7 +27,7 @@ int x;
int y;
void double_effect2(void)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle
index 63d1a4c4296abcaa44618e751c8a4eac0e387f50..e13aebf25deff57a848f0f4e673154e8dc49197e 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle
@@ -29,7 +29,7 @@ void double_effect3(int c2)
{
int tmp;
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle
index b1a9cfead96966941da689a1f14c135260b822b4..6c3b3d034806e876f045a8fb2fcdcc9c2f4f77fa 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle
@@ -28,7 +28,7 @@ int y;
void double_effect4(int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle
index 3edd5eafad82085b60e4d91d2cc3878833a01158..3e6d00b4dec5233223404acbe7d7abc103d67e26 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle
@@ -28,7 +28,7 @@ int y;
void double_effect5(int c2)
{
if (c2) {
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle
index 2d6f39e3c2e2c4795e19e4c45ab657cb533b06a7..f25ae94dfe85a50983acd0acc521aed88b764e20 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle
@@ -27,7 +27,7 @@ int x;
void test1(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle
index 65b54f2a14d11fa76cf080103c85aed1ce2efe97..f6bfddc915e55d20f4279799b4081430499fbc33 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle
@@ -27,7 +27,7 @@ int x;
void test2(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle
index b2eb3519c6d47f3694e29bd0def49ecb39cd29e4..6ec20f98b6a273aa5af64ceb4950b6f39e8a51e6 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle
@@ -27,7 +27,7 @@ int x;
void test3(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle
index 386930d4c0100597dc1a05e19c9cbeaee3855563..ef0047584b267004aa24f93a6ddc7a96fb38bfaa 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle
@@ -29,7 +29,7 @@ int x;
void test4(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
c2 ++;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle
index d94b37154c3df4b0c3eddb8d027a4e16fd8b8548..673df80b192604b8ef5aaa4a6c5b7ca1b9f46238 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle
@@ -28,7 +28,7 @@ void test5(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle
index 3d79ea122f971d4d20b994600eafb8ffde8fe190..8be84e74f183ca9ea4bf9537df7cdcca163f5bba 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle
@@ -31,7 +31,7 @@ void test6(int c1, int c2)
int tmp;
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = c1;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle
index 74d42f097f7f7d359f19324ec0e8033091eacfea..fcc089b3aa74ea1f91a9d3ac890be2eab684ac6a 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop2(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle
index a7c38f2a592460b3b5eca23476bcf21c0780c3b7..e4a3d78ec103e2d1767f665cccb6c562dafb4428 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle
@@ -32,7 +32,7 @@ void test7(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = c1;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle
index 1aa161a7d0d04e612b0f3934872f6226401bef61..0de42a9fd053b8b6396d6fad70641da57e04edfa 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle
@@ -32,7 +32,7 @@ void test8(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
L: { /* sequence */
diff --git a/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle
index fb2cb101e4fce13e8dcba9540a6e402d5255c926..f2077fefebaf0300befec52eccfe722c6c62d728 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle
@@ -30,7 +30,7 @@ void test9(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
L: c2 ++;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle
index a71cca332e6200d919bf10ce99a6db6d323d40fd..2b78c10a6f9813ed95707f34965b42db8c103ee1 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop3(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle
index 2e6f13235085dbfb374f5a89ecc90644fa411685..93e66e70653670fa82f1ca8049cc997a05c9bd6d 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop4(int c1)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle
index 7b1fcef7bf0754c9900fb0a2b1de3f72f2c8a9b8..88f6ac72b01deb4344939068879b8ecc567afdc2 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle
@@ -26,7 +26,7 @@
void nop5(int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle
index 1b860b680b7edf5ba0de8cf98e1247ed62c75d12..5db91ace7d6c5146b0898d0e3a9542d67fa67f44 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop6(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle
index 323a531dca380282259d8dcb897bf912a9f2c493..a2bf24f8357f10ea8a6b5ba43ca6b39f24aadc5b 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop7(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle
index 7b2eada566370551036007bd99ab5c316b4d276b..dccbd2bc7bf3fa5e9d7c1bfc5cce09c8eee7fd8a 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop8(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle
index 9c1d0e59fbd93134cccc8da841258bcab379b46e..bc5d84abefa78bb526b7e80e04846b584142633e 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle
@@ -28,7 +28,7 @@ int y;
void double_effect1(void)
{
int tmp;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{ /* sequence */
tmp = y;
y ++;
diff --git a/tests/slicing/oracle/top2.0.res.oracle b/tests/slicing/oracle/top2.0.res.oracle
index 0ad4cb5d98374fa376c64d4c17137f1e14045711..3f0215a705829394589268da952f124da122274d 100644
--- a/tests/slicing/oracle/top2.0.res.oracle
+++ b/tests/slicing/oracle/top2.0.res.oracle
@@ -48,7 +48,7 @@ void main(void)
{
f_slice_1();
G ++;
- /*@ slice pragma expr G; */ ;
+ /*@ \slicing::slice_preserve_expr G; */ ;
return;
}
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index 751793b0c27928cacc419ad6151f64eba1379f59..5b6e82f7184b65cb389494885d39366c365daf3b 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -4,20 +4,20 @@
OPT: @EVA_OPTIONS@ -deps -lib-entry -main main
MODULE:
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-assert main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot modifS -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f4 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f5 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f6 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f7 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
- OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
+ OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -slice-annot f9 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps
*/
struct Tstr { int a; int b; } S;
@@ -29,7 +29,7 @@ int f1(int cond) {
//@ assert (cond != 0);
Sa = *p ;
}
- //@slice pragma expr *p;
+ //@slice_preserve_expr *p;
return Sa ;
}
@@ -38,14 +38,14 @@ int f2(int cond) {
if (cond)
//@ assert (cond != 0);
Sa = *p ;
- //@slice pragma expr S.a;
+ //@slice_preserve_expr S.a;
return Sa ;
}
int f3(int cond) {
int * p = &S.a ;
if (cond) {
- //@ slice pragma ctrl;
+ //@ slice_preserve_ctrl;
Sa = *p ;
}
return Sa ;
@@ -54,7 +54,7 @@ int f3(int cond) {
int f4(int cond) {
int * p = &S.a ;
if (cond) {
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
Sa = *p ;
}
return Sa ;
@@ -63,7 +63,7 @@ int f4(int cond) {
int f5(int cond) {
int * p = &S.a ;
if (cond) {
- //@ slice pragma expr 1;
+ //@ slice_preserve_expr 1;
Sa = *p ;
}
return Sa ;
@@ -71,7 +71,7 @@ int f5(int cond) {
int f6(int cond) {
int * p = &S.a ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
if (cond) {
Sa = *p ;
Sa ++ ;
@@ -82,7 +82,7 @@ int f6(int cond) {
int f7(int cond) {
int * p = &S.a ;
if (cond)
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{
Sa = *p ;
Sa ++ ;
@@ -100,7 +100,7 @@ int f8(int cond) {
{ //@ assert cond <= \at(cond,Pre) ;
// assert S.a + cond == \at(S.a + cond,Pre) ;
Sa = *p ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
S.a ++ ;
cond--;
}
@@ -112,7 +112,7 @@ void f9(int c1, int c2) {
if (c1 > c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{L: X9 = c1 ;}
Y9 = Z9 ;
Z9 = c2 ;
@@ -121,7 +121,7 @@ void f9(int c1, int c2) {
void modifS (int a, int b) {
S.a += a;
S.b -= b;
- //@slice pragma expr S.a;
+ //@slice_preserve_expr S.a;
}
int new_int (void);
int d;
@@ -133,7 +133,7 @@ int main (void) {
//@ assert (b == 0);
a = 1;
}
- //@ slice pragma expr a+b;
+ //@ slice_preserve_expr a+b;
int x = a+b+c+d;
modifS (a, b);
// assert (d>0 => a == 1) && (!(d>0) => a==0);
diff --git a/tests/slicing/select_by_annot.ml b/tests/slicing/select_by_annot.ml
index f6c24675639034770580bd80540ddadde8624ba1..639bb3996f745d1777ee80a8860d78bded7fd8eb 100644
--- a/tests/slicing/select_by_annot.ml
+++ b/tests/slicing/select_by_annot.ml
@@ -12,7 +12,7 @@ let main _ =
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let select = Slicing.Api.Select.empty_selects in
let select = Slicing.Api.Select.select_func_annots select mark
- ~spare:true ~threat:false ~user_assert:false ~slicing_pragma:true
+ ~spare:true ~threat:false ~user_assert:false ~slicing_annot:true
~loop_inv:true ~loop_var:true kf
in
Slicing.Api.Request.add_persistent_selection select
diff --git a/tests/slicing/select_return.i b/tests/slicing/select_return.i
index 2baa8046238f8a3e7b725b3f99df95394392d58c..2477051d26b33e0554a7d4fd406acd0159402814 100644
--- a/tests/slicing/select_return.i
+++ b/tests/slicing/select_return.i
@@ -14,10 +14,10 @@
STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
- STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 0 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
- STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
- STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
- STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
+ STDOPT: +"-slice-annot f -lib-entry -main g -slicing-level 0 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
+ STDOPT: +"-slice-annot f -lib-entry -main g -slicing-level 1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
+ STDOPT: +"-slice-annot f -lib-entry -main g -slicing-level 2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
+ STDOPT: +"-slice-annot f -lib-entry -main g -slicing-level 3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 3 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
@@ -49,7 +49,7 @@ int f(int y) {
k(0,0,0,0);
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- //@ slice pragma expr z;
+ //@ slice_preserve_expr z;
send (z);
return z;
}
diff --git a/tests/slicing/select_return_bis.i b/tests/slicing/select_return_bis.i
index da2dbbb7fd89e2320c7293016707ce0d1457cad7..c437d7d3ad18eea9055c530bf1ece94014ff054f 100644
--- a/tests/slicing/select_return_bis.i
+++ b/tests/slicing/select_return_bis.i
@@ -40,7 +40,7 @@ int f(int y) {
k(0,0,0,0);
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- //@ slice pragma expr z;
+ //@ slice_preserve_expr z;
send (z);
return z;
}
diff --git a/tests/slicing/sizeof.i b/tests/slicing/sizeof.i
index c89dd0ba1f46018d88d2ba6253746f2860c32185..431868da1318e23800145764042159e421cab681 100644
--- a/tests/slicing/sizeof.i
+++ b/tests/slicing/sizeof.i
@@ -10,7 +10,7 @@
STDOPT: +"-deps -slice-return SizeOfE_pt_tab_1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
STDOPT: +"-deps -slice-return SizeOfE_pt_tab_2 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
STDOPT: +"-deps -slice-return SizeOfE_tab_acces_1 -no-slice-callers -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
- STDOPT: +"-deps -slice-pragma main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
+ STDOPT: +"-deps -slice-annot main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
STDOPT: +"-deps -slice-assert main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps"
*/
struct St { int i, *p, tab[5] ; } st ;
@@ -101,6 +101,6 @@ int main (void) {
r += SizeOfE_pt_tab_1 ();
r += SizeOfE_pt_tab_2 ();
r += SizeOfE_tab_acces_1 ();
- //@ slice pragma expr r;
+ //@ slice_preserve_expr r;
return r;
}
diff --git a/tests/slicing/slice_pragma_stmt.i b/tests/slicing/slice_pragma_stmt.i
index d72c6f2ba13a607ced0a0e7f8e396bba12780e9c..ea554d5dc11678fecc8537bb2253994d4fd25d4f 100644
--- a/tests/slicing/slice_pragma_stmt.i
+++ b/tests/slicing/slice_pragma_stmt.i
@@ -1,122 +1,122 @@
/* run.config
STDOPT: +"-print "
- STDOPT: +"-main nop1 -slice-pragma nop1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop2 -slice-pragma nop2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop3 -slice-pragma nop3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop4 -slice-pragma nop4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop5 -slice-pragma nop5 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop6 -slice-pragma nop6 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop7 -slice-pragma nop7 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main nop8 -slice-pragma nop8 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main double_effect1 -slice-pragma double_effect1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main double_effect2 -slice-pragma double_effect2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main double_effect3 -slice-pragma double_effect3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main double_effect4 -slice-pragma double_effect4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main double_effect5 -slice-pragma double_effect5 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test1 -slice-pragma test1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test2 -slice-pragma test2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test3 -slice-pragma test3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test4 -slice-pragma test4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test5 -slice-pragma test5 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test6 -slice-pragma test6 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test7 -slice-pragma test7 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test8 -slice-pragma test8 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
- STDOPT: +"-main test9 -slice-pragma test9 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop1 -slice-annot nop1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop2 -slice-annot nop2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop3 -slice-annot nop3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop4 -slice-annot nop4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop5 -slice-annot nop5 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop6 -slice-annot nop6 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop7 -slice-annot nop7 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main nop8 -slice-annot nop8 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main double_effect1 -slice-annot double_effect1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main double_effect2 -slice-annot double_effect2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main double_effect3 -slice-annot double_effect3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main double_effect4 -slice-annot double_effect4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main double_effect5 -slice-annot double_effect5 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test1 -slice-annot test1 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test2 -slice-annot test2 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test3 -slice-annot test3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test4 -slice-annot test4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test5 -slice-annot test5 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test6 -slice-annot test6 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test7 -slice-annot test7 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test8 -slice-annot test8 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-main test9 -slice-annot test9 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
*/
typedef int stmt, expr, slice;
int x, y ;
//-------------------
void nop1(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the effect...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the effect...
; // <----- ...is missing with -print option
x = 1 ;
}
void nop2(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the effect...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the effect...
{;} // <----- ...is missing with -print option
x = 1 ;
}
void nop3(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the effect...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the effect...
{;{;;};} // <----- ...is missing with -print option
x = 1 ;
}
void nop4(int c1, int c2) {
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
if (c1) {;{;;};}
x = 1 ;
}
void nop5(int c1, int c2) {
if (c2) goto L ;
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
L:;
x = 1 ;
}
void nop6(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
L:;
x = 1 ;
}
void nop7(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
L:{;}
x = 1 ;
}
void nop8(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
{L:{;}}
x = 1 ;
}
//-------------------
void double_effect1(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
x += y++ ; // <----- ...effect is lost with -print option
}
void double_effect2(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{ x += y++ ; } // <----- ...effect is lost with -print option
}
void double_effect3(int c1, int c2) {
if (c2) goto L ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: x += y++ ; // <----- ...effect is lost with -print option
}
void double_effect4(int c1, int c2) {
if (c2) goto L ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: {x += y++ ; } // <----- ...effect is lost with -print option
}
void double_effect5(int c1, int c2) {
if (c2)
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{x += y++ ; }
}
//-------------------
void test1(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x = c1 ;
}
void test2(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x = c1 ;
y = c2 ;
}
void test3(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{x = c1 ;}
y = c2 ;
}
void test4(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{x = c1 ; c2 ++ ;} // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -124,7 +124,7 @@ void test5(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: x = c1 ; // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -132,7 +132,7 @@ void test6(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: x = c1++ ; // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -140,7 +140,7 @@ void test7(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: {x = c1++ ; c2 ++ ;} // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -148,7 +148,7 @@ void test8(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{ L: x = c1++ ; c2 ++ ;} // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -156,7 +156,7 @@ void test9(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{ x = c1 ; L: c2 = c2 + 1 ;} // <----- ...effect is lost with -print option
y = c2 ;
}
diff --git a/tests/slicing/top2.i b/tests/slicing/top2.i
index 8644cd9cd33e762cb2863ac4bb00181909e20f94..611a988af6215472fe95988c66ce0b15bde39097 100644
--- a/tests/slicing/top2.i
+++ b/tests/slicing/top2.i
@@ -1,5 +1,5 @@
/* run.config
-* STDOPT: +"-slicing-level 2 -slice-pragma main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
+* STDOPT: +"-slicing-level 2 -slice-annot main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
* STDOPT: +"-slicing-level 2 -slice-return main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check "
*/
@@ -23,6 +23,6 @@ int f(void) {
int main(void) {
int x = f();
G += 1 ;
- //@ slice pragma expr G ;
+ //@ slice_preserve_expr G ;
return x;
}
diff --git a/tests/slicing/unitialized.c b/tests/slicing/unitialized.c
index e1767ca3f34d0961e6cce3f35e2c04983c7aa8f1..4abfabec1c8e8016fc2a8caf41c4da98da272673 100644
--- a/tests/slicing/unitialized.c
+++ b/tests/slicing/unitialized.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"-slice-pragma g -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
+ STDOPT: +"-slice-annot g -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
STDOPT: +"-slice-assert g -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
STDOPT: +"-slice-assert main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
STDOPT: +"-slice-return g -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ./ocode_@PTEST_NUMBER@_@PTEST_NAME@.i "
@@ -28,7 +28,7 @@ int g() {
/* Note: y is not initialised by g. */
/* Note: GCC without optimization gives X1 == y. */
printf ("%d\n", y);
- //@slice pragma expr y ;
+ //@slice_preserve_expr y ;
//@assert X1 == y ;
return y;
}
diff --git a/tests/sparecode/bts324.i b/tests/sparecode/bts324.i
index c2cf07e2d27dc64416c108f0ed252bd255801ca0..b41f4dc2c193f58846ef9acfcd0632223f73e6c4 100644
--- a/tests/sparecode/bts324.i
+++ b/tests/sparecode/bts324.i
@@ -27,7 +27,7 @@ void main_bis (void) {
if (is_ko)
while (1) {
loop_body () ;
- /*@ slice pragma expr o0 ;*/
+ /*@ slice_preserve_expr o0 ;*/
}
}
@@ -35,7 +35,7 @@ void main_ter () {
init (&is_ko);
if (is_ko)
while (1) {
- /*@ slice pragma stmt ;*/
+ /*@ slice_preserve_stmt ;*/
loop_body () ;
}
}
diff --git a/tests/sparecode/bts324_bis.i b/tests/sparecode/bts324_bis.i
index 67093ede54f3d0ec6d263cc05b069d02cb9eaa54..ad6183b42440433a0e4a1a613f177abb309c614f 100644
--- a/tests/sparecode/bts324_bis.i
+++ b/tests/sparecode/bts324_bis.i
@@ -40,8 +40,7 @@ void main (int c) {
loop_body () ;
// note: sparecode conserve les pragmas de slicing et par conséquent ce
// qui calcule "s0", l'option -sparecode-no-annot ni change rien
- //@ impact pragma expr s0;
- //@ slice pragma expr s1;
+ //@ slice_preserve_expr s1;
}
}
diff --git a/tests/sparecode/bts334.i b/tests/sparecode/bts334.i
index f05a44ace82ecd919b5168fe6f219d4116ad420c..fb9c66fafd75d3352216f905d25a67bcd78f2b6d 100644
--- a/tests/sparecode/bts334.i
+++ b/tests/sparecode/bts334.i
@@ -1,8 +1,8 @@
/*run.config
STDOPT: +"-sparecode-debug 0 -main main_init -sparecode-analysis -sparecode-no-annot "
PLUGIN: @PTEST_PLUGIN@ slicing
- STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -then-on 'Slicing export' -print"
- STDOPT: +"-sparecode-debug 0 -main main_init -slice-pragma loop_body -calldeps -then-on 'Slicing export' -print"
+ STDOPT: +"-sparecode-debug 0 -main main_init -slice-annot loop_body -then-on 'Slicing export' -print"
+ STDOPT: +"-sparecode-debug 0 -main main_init -slice-annot loop_body -calldeps -then-on 'Slicing export' -print"
*/
int kf ;
int k[2] ;
@@ -27,7 +27,7 @@ void loop_body(void)
int val0 ;
int val1 ;
- {/*@ slice pragma expr s0;
+ {/*@ slice_preserve_expr s0;
*/
;
diff --git a/tests/sparecode/glob_decls.i b/tests/sparecode/glob_decls.i
index eb211f029f70d1e7a2720fe26d44691f7472aeaf..f5f3b98a8f6938479024fc62113329117dd078c7 100644
--- a/tests/sparecode/glob_decls.i
+++ b/tests/sparecode/glob_decls.i
@@ -1,7 +1,7 @@
/* run.config
STDOPT: +"-lib-entry -sparecode-analysis "
PLUGIN: @PTEST_PLUGIN@ slicing
- STDOPT: +"-lib-entry -slice-pragma main -slice-return main -then-on 'Slicing export' -print"
+ STDOPT: +"-lib-entry -slice-annot main -slice-return main -then-on 'Slicing export' -print"
STDOPT: +"-sparecode-rm-unused-globals"
*/
@@ -41,7 +41,7 @@ int * PX;
/*@ requires S2.a > S2.b ; */
int main (int x, Ts s) {
- //@ slice pragma expr S2 ;
+ //@ slice_preserve_expr S2 ;
int y = 3;
y += Y;
y += *PX;
diff --git a/tests/sparecode/intra.i b/tests/sparecode/intra.i
index 21f41c1d712ad71bb0ec0e4718acf2c335e91df0..07490070e5fd51c55260a069cbb4296b72850872 100644
--- a/tests/sparecode/intra.i
+++ b/tests/sparecode/intra.i
@@ -102,10 +102,10 @@ int main (int noreturn, int halt) {
struct { struct { int x; int y; } a; int b; } X10;
int Y10;
int f10 (int x) {
- //@ slice pragma expr X10;
- //@ slice pragma expr X10.a;
- //@ slice pragma expr X10.a.x;
- //@ slice pragma expr Y10;
+ //@ slice_preserve_expr X10;
+ //@ slice_preserve_expr X10.a;
+ //@ slice_preserve_expr X10.a.x;
+ //@ slice_preserve_expr Y10;
//@ assert X10.a.x >= 0;
return x;
}
diff --git a/tests/sparecode/oracle/bts324.1.res.oracle b/tests/sparecode/oracle/bts324.1.res.oracle
index 3a9715cf467150cd0976415797ce7175c97e9630..777e5eff8ed7b940466e54e6d754cbfe5eca9f3a 100644
--- a/tests/sparecode/oracle/bts324.1.res.oracle
+++ b/tests/sparecode/oracle/bts324.1.res.oracle
@@ -45,7 +45,7 @@
[pdg] Bottom for function main
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function main_bis
-[sparecode] selecting annotation : slice pragma expr o0;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr o0;
[sparecode] add selection in function 'main_bis'
[sparecode] look for annotations in function main_ter
[pdg] computing for function main_ter
@@ -72,7 +72,7 @@ void main_bis(void)
if (is_ko)
while (1) {
loop_body();
- /*@ slice pragma expr o0; */ ;
+ /*@ \slicing::slice_preserve_expr o0; */ ;
}
return;
}
diff --git a/tests/sparecode/oracle/bts324.2.res.oracle b/tests/sparecode/oracle/bts324.2.res.oracle
index 2a7fc2a7b54abd30abeae7aef88eae11895cb608..38d7bf094e6a21b22c00dedeb4a696ba4c30ba7b 100644
--- a/tests/sparecode/oracle/bts324.2.res.oracle
+++ b/tests/sparecode/oracle/bts324.2.res.oracle
@@ -50,7 +50,7 @@
[pdg] Bottom for function main_bis
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function main_ter
-[sparecode] selecting annotation : slice pragma stmt;
+[sparecode] selecting annotation : \slicing::slice_preserve_stmt ;
[sparecode] add selection in function 'main_ter'
[sparecode] finalize call input propagation
[sparecode] add selection in function 'main_ter'
@@ -71,7 +71,7 @@ void main_ter(void)
init(& is_ko);
if (is_ko)
while (1)
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
loop_body();
return;
}
diff --git a/tests/sparecode/oracle/bts324_bis.0.res.oracle b/tests/sparecode/oracle/bts324_bis.0.res.oracle
index b2f6ccff02c10e1b1dd1a0686acfadd335a33b1e..963ffef256f113f018d6065d9a99bb8e43372599 100644
--- a/tests/sparecode/oracle/bts324_bis.0.res.oracle
+++ b/tests/sparecode/oracle/bts324_bis.0.res.oracle
@@ -80,7 +80,7 @@
[from] Computing for function f <-loop_body
[from] Done for function f
[from] Done for function loop_body
-[pdg] bts324_bis.i:47: Warning: no final state. Probably unreachable...
+[pdg] bts324_bis.i:46: Warning: no final state. Probably unreachable...
[pdg] done for function main
[sparecode] add selection in function 'main'
[sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1]
@@ -94,12 +94,11 @@
[pdg] computing for function loop_body
[pdg] done for function loop_body
[sparecode] look for annotations in function main
-[sparecode] selecting annotation : impact pragma expr s0;
-[sparecode] selecting annotation : slice pragma expr s1;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr s1;
[sparecode] add selection in function 'main'
[sparecode] look for annotations in function main_bis
[pdg] computing for function main_bis
-[pdg] Warning: unreachable entry point (sid:32, function main_bis)
+[pdg] Warning: unreachable entry point (sid:31, function main_bis)
[pdg] Bottom for function main_bis
[sparecode] pdg bottom: skip annotations
[sparecode] finalize call input propagation
@@ -124,15 +123,13 @@ int f(int vi, int i)
int volatile e0;
int volatile e1;
-int s0;
int s1;
void loop_body(void)
{
int acq0 = e0;
int acq1 = e1;
- int val0 = f(acq0,0);
+ f(acq0,0);
int val1 = f(acq1,1);
- s0 = val0;
s1 = val1;
return;
}
@@ -150,8 +147,7 @@ void main(void)
init();
while (1) {
loop_body();
- /*@ impact pragma expr s0; */ ;
- /*@ slice pragma expr s1; */ ;
+ /*@ \slicing::slice_preserve_expr s1; */ ;
}
return;
}
diff --git a/tests/sparecode/oracle/bts324_bis.1.res.oracle b/tests/sparecode/oracle/bts324_bis.1.res.oracle
index 39a4a0c7230facac4fc5f9d54410e45b35175ba7..ac38ed261635f02cc1749ea5f96e410dc2d1e8cf 100644
--- a/tests/sparecode/oracle/bts324_bis.1.res.oracle
+++ b/tests/sparecode/oracle/bts324_bis.1.res.oracle
@@ -15,11 +15,11 @@
f_si[0..1] ∈ {0}
f_so[0..1] ∈ {0}
[eva] computing for function init <- main_bis.
- Called from bts324_bis.i:51.
+ Called from bts324_bis.i:50.
[eva] Recording results for init
[eva] Done for function init
[eva] computing for function loop_body <- main_bis.
- Called from bts324_bis.i:54.
+ Called from bts324_bis.i:53.
[eva] computing for function f <- loop_body <- main_bis.
Called from bts324_bis.i:22.
[eva:alarm] bts324_bis.i:10: Warning:
@@ -34,9 +34,9 @@
[eva] Done for function f
[eva] Recording results for loop_body
[eva] Done for function loop_body
-[eva] bts324_bis.i:53: starting to merge loop iterations
+[eva] bts324_bis.i:52: starting to merge loop iterations
[eva] computing for function loop_body <- main_bis.
- Called from bts324_bis.i:54.
+ Called from bts324_bis.i:53.
[eva] computing for function f <- loop_body <- main_bis.
Called from bts324_bis.i:22.
[eva:alarm] bts324_bis.i:10: Warning:
@@ -60,7 +60,7 @@
[eva] Recording results for loop_body
[eva] Done for function loop_body
[eva] computing for function loop_body <- main_bis.
- Called from bts324_bis.i:54.
+ Called from bts324_bis.i:53.
[eva] computing for function f <- loop_body <- main_bis.
Called from bts324_bis.i:22.
[eva] Recording results for f
@@ -80,7 +80,7 @@
[from] Computing for function f <-loop_body
[from] Done for function f
[from] Done for function loop_body
-[pdg] bts324_bis.i:57: Warning: no final state. Probably unreachable...
+[pdg] bts324_bis.i:56: Warning: no final state. Probably unreachable...
[pdg] done for function main_bis
[sparecode] add selection in function 'main_bis'
[sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1]
diff --git a/tests/sparecode/oracle/bts324_bis.2.res.oracle b/tests/sparecode/oracle/bts324_bis.2.res.oracle
index d1cd2c2d2a5f58500fa0fab5f14a20f27ed4c304..963ffef256f113f018d6065d9a99bb8e43372599 100644
--- a/tests/sparecode/oracle/bts324_bis.2.res.oracle
+++ b/tests/sparecode/oracle/bts324_bis.2.res.oracle
@@ -80,7 +80,7 @@
[from] Computing for function f <-loop_body
[from] Done for function f
[from] Done for function loop_body
-[pdg] bts324_bis.i:47: Warning: no final state. Probably unreachable...
+[pdg] bts324_bis.i:46: Warning: no final state. Probably unreachable...
[pdg] done for function main
[sparecode] add selection in function 'main'
[sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1]
@@ -94,11 +94,11 @@
[pdg] computing for function loop_body
[pdg] done for function loop_body
[sparecode] look for annotations in function main
-[sparecode] selecting annotation : slice pragma expr s1;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr s1;
[sparecode] add selection in function 'main'
[sparecode] look for annotations in function main_bis
[pdg] computing for function main_bis
-[pdg] Warning: unreachable entry point (sid:32, function main_bis)
+[pdg] Warning: unreachable entry point (sid:31, function main_bis)
[pdg] Bottom for function main_bis
[sparecode] pdg bottom: skip annotations
[sparecode] finalize call input propagation
@@ -123,7 +123,6 @@ int f(int vi, int i)
int volatile e0;
int volatile e1;
-int s0;
int s1;
void loop_body(void)
{
@@ -148,8 +147,7 @@ void main(void)
init();
while (1) {
loop_body();
- /*@ impact pragma expr s0; */ ;
- /*@ slice pragma expr s1; */ ;
+ /*@ \slicing::slice_preserve_expr s1; */ ;
}
return;
}
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index 046c3ca1741d5bc1d9dcbcc01efa4b654984b5ef..e977ab534d0373b45026dd6611f09a45c128ca81 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -130,7 +130,7 @@ void loop_body(void)
int acq0;
int acq1;
int val0;
- /*@ slice pragma expr s0; */ ;
+ /*@ \slicing::slice_preserve_expr s0; */ ;
acq0 = e0;
acq1 = e1;
val0 = f(acq0,0);
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 2f9cd06339971284b46828e43f46b1e27d071083..2b3b9e693429816b08d6eb31de5f168d17784f65 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -138,7 +138,7 @@ void loop_body_slice_1(void)
int acq0;
int acq1;
int val0;
- /*@ slice pragma expr s0; */ ;
+ /*@ \slicing::slice_preserve_expr s0; */ ;
acq0 = e0;
acq1 = e1;
val0 = f_slice_1(acq0,0);
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index d88f06cdf7383cf35330ccce0e3350561587299f..51b356f150a2b2bb88c4fab44d81f06357a47beb 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -173,7 +173,7 @@ void loop_body_slice_1(void)
{
int acq0;
int val0;
- /*@ slice pragma expr s0; */ ;
+ /*@ \slicing::slice_preserve_expr s0; */ ;
acq0 = e0;
val0 = f_slice_1(acq0,0);
s0 = val0;
diff --git a/tests/sparecode/oracle/glob_decls.0.res.oracle b/tests/sparecode/oracle/glob_decls.0.res.oracle
index 9476cb2c39dc8f13726a1ba21db7210682597fc2..18e1a78534b9206214d484b52332fe8a941048c4 100644
--- a/tests/sparecode/oracle/glob_decls.0.res.oracle
+++ b/tests/sparecode/oracle/glob_decls.0.res.oracle
@@ -47,7 +47,7 @@
[pdg] Bottom for function f
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function main
-[sparecode] selecting annotation : slice pragma expr S2;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr S2;
[sparecode] selecting annotation : assert X > 0;
[sparecode] add selection in function 'main'
[sparecode] finalize call input propagation
@@ -67,7 +67,7 @@ Tx X = (Tx)sizeof(Size);
int main(int x)
{
int __retres;
- /*@ slice pragma expr S2; */ ;
+ /*@ \slicing::slice_preserve_expr S2; */ ;
/*@ assert X > 0; */ ;
__retres = X + x;
return __retres;
diff --git a/tests/sparecode/oracle/glob_decls.1.res.oracle b/tests/sparecode/oracle/glob_decls.1.res.oracle
index 2c50d5d6f851d97d14e1b9101c462e59a63fcaae..86a14a5c596dcc72a35d21255588f23dcf3d8ffb 100644
--- a/tests/sparecode/oracle/glob_decls.1.res.oracle
+++ b/tests/sparecode/oracle/glob_decls.1.res.oracle
@@ -64,7 +64,7 @@ Tx X = (Tx)sizeof(Size);
int main(int x)
{
int __retres;
- /*@ slice pragma expr S2; */ ;
+ /*@ \slicing::slice_preserve_expr S2; */ ;
/*@ assert X > 0; */ ;
__retres = X + x;
return __retres;
diff --git a/tests/sparecode/oracle/glob_decls.2.res.oracle b/tests/sparecode/oracle/glob_decls.2.res.oracle
index d5e83032365641dee2547f0d97a2e9db75692e1f..fab24ebf4872afdfa05822ce68206b59a5d73762 100644
--- a/tests/sparecode/oracle/glob_decls.2.res.oracle
+++ b/tests/sparecode/oracle/glob_decls.2.res.oracle
@@ -38,7 +38,7 @@ int *PX;
int main(int x, Ts s)
{
int __retres;
- /*@ slice pragma expr S2; */ ;
+ /*@ \slicing::slice_preserve_expr S2; */ ;
int y = 3;
y += Y;
y += *PX;
diff --git a/tests/sparecode/oracle/intra.2.res.oracle b/tests/sparecode/oracle/intra.2.res.oracle
index 93f6885a56ad9fcc44ba15452f34b35cfa3c2b0a..78dd1dafaf6b822d2ea827e7d7e279045e4435ea 100644
--- a/tests/sparecode/oracle/intra.2.res.oracle
+++ b/tests/sparecode/oracle/intra.2.res.oracle
@@ -66,10 +66,10 @@ struct __anonstruct_X10_1 X10;
int Y10;
int f10(int x)
{
- /*@ slice pragma expr X10; */ ;
- /*@ slice pragma expr X10.a; */ ;
- /*@ slice pragma expr X10.a.x; */ ;
- /*@ slice pragma expr Y10; */ ;
+ /*@ \slicing::slice_preserve_expr X10; */ ;
+ /*@ \slicing::slice_preserve_expr X10.a; */ ;
+ /*@ \slicing::slice_preserve_expr X10.a.x; */ ;
+ /*@ \slicing::slice_preserve_expr Y10; */ ;
/*@ assert X10.a.x ≥ 0; */ ;
return x;
}
diff --git a/tests/sparecode/oracle/intra.4.res.oracle b/tests/sparecode/oracle/intra.4.res.oracle
index 2e4d4c9e1b1e948bf8fa50c76dc4db4dacb5ab9b..267ec32ba44cb7a2aab8d836c2ba19509ed436c8 100644
--- a/tests/sparecode/oracle/intra.4.res.oracle
+++ b/tests/sparecode/oracle/intra.4.res.oracle
@@ -45,7 +45,7 @@ struct __anonstruct_X10_1 {
struct __anonstruct_X10_1 X10;
int f10_slice_1(int x)
{
- /*@ slice pragma expr X10.a.x; */ ;
+ /*@ \slicing::slice_preserve_expr X10.a.x; */ ;
/*@ assert X10.a.x ≥ 0; */ ;
return x;
}
diff --git a/tests/value/dead_code.i b/tests/value/dead_code.i
index e0c5d2be9567894ed345ac2b6424a88f11591737..42e5d138ea89d9b291d1b7fc57e968aa3f2e11c5 100644
--- a/tests/value/dead_code.i
+++ b/tests/value/dead_code.i
@@ -1,8 +1,8 @@
void main(int in) {
int i,j=6,k,l;
-
+
i=10;
- //@ impact pragma stmt;
+
i=1;
L: if (i) {l= 17 ; goto OUT;}
// i--;