diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index 20412be44c5849c3990fca4312bc6ca45e259e49..16469811570e79da8ec474f0fa045ea990fbea91 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+type 'a formatter = Format.formatter -> 'a -> unit
+
type t = Z.t
let equal = Z.equal
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 1c341b3a7a97c7f6a8d6f91c50664d3b3f080441..5fc9867d046704fdf4effaf59e0d7af9e377994f 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -23,6 +23,8 @@
(** Extension of [Big_int] compatible with [Zarith].
@since Nitrogen-20111001 *)
+type 'a formatter = Format.formatter -> 'a -> unit
+
type t = Z.t
val equal : t -> t -> bool
@@ -212,9 +214,9 @@ val to_string : t -> string
val of_string : string -> t
(** @raise Invalid_argument when the string cannot be parsed. *)
-val pretty : ?hexa:bool -> t Pretty_utils.formatter
+val pretty : ?hexa:bool -> t formatter
-val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
+val pp_bin : ?nbits:int -> ?sep:string -> t formatter
(** Print binary format. Digits are output by blocs of 4 bits
separated by [~sep] with at least [~nbits] total bits. If [nbits] is
non positive, it will be ignored.
@@ -222,7 +224,7 @@ val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
Positive values are prefixed with ["0b"] and negative values
are printed as their 2-complement ([lnot]) with prefix ["1b"]. *)
-val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
+val pp_hex : ?nbits:int -> ?sep:string -> t formatter
(** Print hexadecimal format. Digits are output by blocs of 16 bits
(4 hex digits) separated by [~sep] with at least [~nbits] total bits.
If [nbits] is non positive, it will be ignored.
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index 49be26a813e5d081869f30134b0c70c1e8357db9..863dd66e8b1fea843a525477e234ab209ca85f3e 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -452,7 +452,7 @@ let nextafter_aux ~is_f32 fincr fdecr x y =
then y
else if isnan x || isnan y then nan
else if x = 0.0 (* or -0.0 *) then
- if x < y then min_denormal_float is_f32 else -. (min_denormal_float is_f32)
+ if x < y then min_denormal_float ~is_f32 else -. (min_denormal_float ~is_f32)
(* the following conditions might be simpler if we had unsigned ints
(uint32/uint64) *)
else if x = neg_infinity (* && y = neg_infinity *) then fdecr x
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index 576e24a014ccdece73bb21a2996dc07375123c05..5af4e5c1cc4cc3d996ec000be6b6f9a5066028de 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -162,7 +162,7 @@ exception CannotMerge of string
the same keys, or if the root JSON element is not an object.
@since 23.0-Vanadium
*)
-val merge_object : Filepath.Normalized.t -> Yojson.Basic.t -> unit
+val merge_object : Filepath.Normalized.t -> t -> unit
(**
[merge_list path json_array] merges the array [json_array] into the
@@ -173,7 +173,7 @@ val merge_object : Filepath.Normalized.t -> Yojson.Basic.t -> unit
@raise CannotMerge if the root JSON element is not an array.
@since 23.0-Vanadium
*)
-val merge_array : Filepath.Normalized.t -> Yojson.Basic.t -> unit
+val merge_array : Filepath.Normalized.t -> t -> unit
(**
[from_file path] opens [path] and stores its JSON object in
@@ -181,7 +181,7 @@ val merge_array : Filepath.Normalized.t -> Yojson.Basic.t -> unit
@raise Yojson.Json_error if [path] is a malformed JSON file.
@since 23.0-Vanadium
*)
-val from_file: Filepath.Normalized.t -> Yojson.Basic.t
+val from_file: Filepath.Normalized.t -> t
(**
Flushes the JSON objects in the cache. Returns the names of the written
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 621b258f44d25e98be761f865c2be7fd0e6dbd39..dfb8d49cd2d416643ce6cd900aabc9db78ca8bcd 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -59,7 +59,7 @@ SRC_PROJECT_INITIALIZER:=\
SRC_ANALYSES:= \
rte \
lscope \
- predicate_normalizer \
+ logic_normalizer \
bound_variables \
interval \
typing \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 9f014a0a1abe4040f1804d2d5e5caf67ca31ce72..3daf5993839c6a94719a95604afacee9328db77c 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -76,11 +76,11 @@ src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/logic_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/logic_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/predicate_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/analyses/predicate_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/memory_tracking.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/rte.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/rte.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index d598f893bafdea3b5c687ff9eaf08ae0969e2f37..9ca2a162568d089f09e9f94cbfc5eab49fd7eeaf 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -731,7 +731,7 @@ end
method !vpredicate p =
let loc = p.pred_loc in
- match Predicate_normalizer.get p with
+ match Logic_normalizer.get_pred p with
| PoT_pred p -> Error.generic_handle (process_quantif ~loc) () p;
Cil.DoChildren
| PoT_term _ -> Cil.DoChildren
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
similarity index 72%
rename from src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
rename to src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index 420768ebdf7899096001c547976dd67709818d79..46efb9de68cdb81c771a2c1b7cf55d77754be37c 100644
--- a/src/plugins/e-acsl/src/analyses/predicate_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -41,29 +41,45 @@ module Id_predicate =
(* Memoization module which retrieves the preprocessed form of predicates *)
module Memo: sig
- val memo: (predicate -> pred_or_term option) -> predicate -> unit
- val get: predicate -> pred_or_term
+ val memo_pred: (predicate -> pred_or_term option) -> predicate -> unit
+ val get_pred: predicate -> pred_or_term
+ val memo_term : (term -> term option) -> term -> unit
+ val get_term : term -> term
val clear: unit -> unit
end = struct
- let tbl = Id_predicate.Hashtbl.create 97
+ let tbl_term = Misc.Id_term.Hashtbl.create 97
+ let tbl_pred = Id_predicate.Hashtbl.create 97
- let get p =
- try Id_predicate.Hashtbl.find tbl p
+ let get_pred p =
+ try Id_predicate.Hashtbl.find tbl_pred p
with Not_found -> Lscope.PoT_pred p
- let memo process p =
- try ignore (Id_predicate.Hashtbl.find tbl p) with
+ let memo_pred process p =
+ try ignore (Id_predicate.Hashtbl.find tbl_pred p) with
| Not_found ->
match process p with
- | Some pot -> Id_predicate.Hashtbl.add tbl p (pot)
+ | Some pot -> Id_predicate.Hashtbl.add tbl_pred p pot
| None -> ()
- let clear () = Id_predicate.Hashtbl.clear tbl
+ let get_term t =
+ try Misc.Id_term.Hashtbl.find tbl_term t
+ with Not_found -> t
+
+ let memo_term process t =
+ try ignore (Misc.Id_term.Hashtbl.find tbl_term t) with
+ | Not_found ->
+ match process t with
+ | Some term -> Misc.Id_term.Hashtbl.add tbl_term t term
+ | None -> ()
+
+ let clear () =
+ Misc.Id_term.Hashtbl.clear tbl_term;
+ Id_predicate.Hashtbl.clear tbl_pred
end
-let preprocess ~loc p =
+let preprocess_pred ~loc p =
match p.pred_content with
| Pvalid_read(BuiltinLabel Here as llabel, t)
| Pvalid(BuiltinLabel Here as llabel, t) -> begin
@@ -97,6 +113,27 @@ let preprocess ~loc p =
Some (Lscope.PoT_term tapp)
| _ -> None
+let preprocess_term ~loc t =
+ match t.term_node with
+ | Tapp(li, lst, [ t1; t2; {term_node = Tlambda([ k ], predicate)}])
+ when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
+ let logic_info = Cil_const.make_logic_info "\\sum" in
+ logic_info.l_type <- li.l_type;
+ logic_info.l_tparams <- li.l_tparams;
+ logic_info.l_labels <- li.l_labels;
+ logic_info.l_profile <- li.l_profile;
+ logic_info.l_body <- li.l_body;
+ let conditional_term =
+ Logic_const.term ~loc
+ (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
+ in
+ let lambda_term =
+ Logic_const.term ~loc (Tlambda([ k ], conditional_term)) Linteger
+ in
+ Some (Logic_const.term ~loc
+ (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
+ | _ -> None
+
let preprocessor = object
inherit Visitor.frama_c_inplace
@@ -140,11 +177,15 @@ let preprocessor = object
| GText _
-> Cil.SkipChildren
- method !vpredicate p =
+ method !vpredicate p =
let loc = p.pred_loc in
- Memo.memo (preprocess ~loc) p;
+ Memo.memo_pred (preprocess_pred ~loc) p;
Cil.DoChildren
+ method !vterm t =
+ let loc = t.term_loc in
+ Memo.memo_term (preprocess_term ~loc) t;
+ Cil.DoChildren
end
let preprocess ast =
@@ -156,5 +197,6 @@ let preprocess_annot annot =
let preprocess_predicate p =
ignore (Visitor.visitFramacPredicate preprocessor p)
-let get = Memo.get
+let get_pred = Memo.get_pred
+let get_term = Memo.get_term
let clear = Memo.clear
diff --git a/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
similarity index 95%
rename from src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
rename to src/plugins/e-acsl/src/analyses/logic_normalizer.mli
index 06f9a7d199f523f4910770686c438d6e2ed3faca..49654d41d6f8e0fd786c5aef35df856b8e32252e 100644
--- a/src/plugins/e-acsl/src/analyses/predicate_normalizer.mli
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
@@ -41,7 +41,9 @@ val preprocess_annot : code_annotation -> unit
val preprocess_predicate : predicate -> unit
(** Preprocess a predicate and its children and store the results *)
-val get : predicate -> Lscope.pred_or_term
+val get_pred : predicate -> Lscope.pred_or_term
(** Retrieve the preprocessed form of a predicate *)
+val get_term : term -> term
+(** Retrieve the preprocessed form of a term *)
val clear: unit -> unit
(** clear the table of normalized predicates *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index db78316a1b6e841c86f00c68957261cd18d0b414..bbc74b118c622dbc23942b3409e8622ba3f86773 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -284,7 +284,7 @@ end
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
-let ty_of_interv ?ctx = function
+let ty_of_interv ?ctx ?(use_gmp_opt = false) = function
| Interval.Float(fk, _) -> C_float fk
| Interval.Rational -> Rational
| Interval.Real -> Real
@@ -294,8 +294,10 @@ let ty_of_interv ?ctx = function
let kind = Interval.ikind_of_ival iv in
(match ctx with
| None
- | Some (Gmpz | Nan) ->
+ | Some Nan ->
C_integer kind
+ | Some Gmpz ->
+ if use_gmp_opt then Gmpz else C_integer kind
| Some (C_integer ik as ctx) ->
(* return [ctx] type for types smaller than int to prevent superfluous
casts in the generated code *)
@@ -382,7 +384,13 @@ let type_letin li li_t =
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
iff [use_gmp_opt] is true. *)
-let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
+let rec type_term
+ ~use_gmp_opt
+ ?(under_lambda=false)
+ ?(arith_operand=false)
+ ?ctx
+ ?(lenv=[])
+ t =
let ctx = Option.map (mk_ctx ~use_gmp_opt) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
@@ -408,13 +416,16 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
| TSizeOfStr _
| TAlignOf _ ->
let i = Interval.infer t in
- let ty = ty_of_interv ?ctx i in
+ (* a constant or a left value directly under a lambda should be a gmp
+ if the infered context for the lambda is gmp *)
+ let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
dup ty
| TLval tlv ->
let i = Interval.infer t in
- let ty = ty_of_interv ?ctx i in
+ let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in
type_term_lval ~lenv tlv;
+ (* Options.feedback "Type : %a" D.pretty ty; *)
dup ty
| Toffset(_, t')
@@ -619,7 +630,8 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
ignore
(type_term
~use_gmp_opt:true ~arith_operand:true ~ctx:ty_bound ~lenv t2);
- let ty = ty_of_interv (Interval.infer t) in
+ let ty = ty_of_interv (Interval.infer t) ~use_gmp_opt:true ?ctx in
+ (* Options.feedback "type of extended quantifier: %a" D.pretty ty; *)
ignore (type_term ~use_gmp_opt:true ?ctx ~lenv lambda);
dup ty
| [ ] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ ->
@@ -654,7 +666,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
ignore (type_term ~use_gmp_opt:true ~lenv li_t);
dup (type_term ~use_gmp_opt:true ?ctx ~lenv t).ty
| Tlambda ([ _ ],lt) ->
- dup (type_term ~use_gmp_opt:true ?ctx lt).ty;
+ dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx lt).ty;
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
@@ -665,6 +677,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
| Ttype _
| Tempty_set -> dup Nan
in
+ let t = Logic_normalizer.get_term t in
Memo.memo ~lenv
(fun t ->
let ty, op = infer t in
@@ -792,9 +805,8 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
Interval.Env.add lv i;
(t1, lv, t2)
-
and type_predicate ?(lenv=[]) p =
- match Predicate_normalizer.get p with
+ match Logic_normalizer.get_pred p with
| PoT_term t -> type_term ~use_gmp_opt:true ~lenv t
| PoT_pred p ->
Cil.CurrentLoc.set p.pred_loc;
@@ -1004,12 +1016,12 @@ let type_code_annot lenv annot =
ignore (Visitor.visitFramacCodeAnnotation (typer_visitor lenv) annot)
let preprocess_predicate lenv p =
- Predicate_normalizer.preprocess_predicate p;
+ Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
ignore (Visitor.visitFramacPredicate (typer_visitor lenv) p)
let preprocess_rte ~lenv rte =
- Predicate_normalizer.preprocess_annot rte;
+ Logic_normalizer.preprocess_annot rte;
Bound_variables.preprocess_annot rte;
type_code_annot lenv rte
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 5bf1e0c93495657e607390089849b37e407c0c46..f6b783cf0cdd3798fbe76fc148235e374caccb7d 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -108,11 +108,7 @@ val type_term:
even if -e-acsl-gmp-only is set. *)
val type_named_predicate: ?lenv:Function_params_ty.t -> predicate -> unit
-(** Compute the type of each term of the given predicate.
-
- If {!must_clear} is true, the typing environment is reset before translating
- the predicate. The environment should be reset when translating a new
- assertion, and kept otherwise. *)
+(** Compute the type of each term of the given predicate. *)
val clear: unit -> unit
(** Remove all the previously computed types. *)
@@ -156,7 +152,7 @@ val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit
(** {2 Typing/types-related utils} *)
(*****************************************************************************)
-val ty_of_interv: ?ctx:number_ty -> Interval.t -> number_ty
+val ty_of_interv: ?ctx:number_ty -> ?use_gmp_opt:bool -> Interval.t -> number_ty
(* Compute the smallest type (bigger than [int]) which can contain the whole
interval. It is the \theta operator of the JFLA's paper. *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 23e1965ce624983cfe2fdabf4e2e86afc1d35587..5964cedbcf0f2e4f2bda5df6a81fad34446385c4 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -852,7 +852,7 @@ let reset_all ast =
Literal_strings.reset ();
Global_observer.reset ();
Bound_variables.clear_guards ();
- Predicate_normalizer.clear ();
+ Logic_normalizer.clear ();
Typing.clear ();
(* reset some kernel states: *)
(* reset the CFG that has been heavily modified by the code generation step *)
@@ -869,7 +869,7 @@ let inject () =
Options.feedback ~level:2
"preprocessing annotations in project %a"
Project.pretty current_project;
- Predicate_normalizer.preprocess ast;
+ Logic_normalizer.preprocess ast;
Options.feedback ~level:2
"normalizing quantifiers in project %a"
Project.pretty current_project;
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 448cba21c748a362471580206b36de98237956ab..b0c3d6a1339d342555305618a54b60683025d3f1 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -744,27 +744,9 @@ and context_insensitive_term_to_exp ~adata kf env t =
when li.l_body = LBnone && (li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product")->
extended_quantifier_to_exp ~adata ~loc kf env t t1 t2 lambda li.l_var_info
- | Tapp(li, lst, [ t1; t2; {term_node = Tlambda([ k ], predicate)}])
+ | Tapp(li, _, _)
when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
- let logic_info = Cil_const.make_logic_info "\\sum" in
- logic_info.l_type <- li.l_type;
- logic_info.l_tparams <- li.l_tparams;
- logic_info.l_labels <- li.l_labels;
- logic_info.l_profile <- li.l_profile;
- logic_info.l_body <- li.l_body;
- let numof_as_sum =
- let conditional_term =
- Logic_const.term
- (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
- in
- let lambda_term =
- Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
- in
- (Logic_const.term
- (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
- in
- Typing.type_term ~use_gmp_opt:true numof_as_sum;
- context_insensitive_term_to_exp ~adata kf env numof_as_sum
+ assert false
| Tapp(_, [], _) ->
let e, adata, env = Logic_functions.tapp_to_exp ~adata kf env t in
let adata, env = Assert.register_term ~loc kf env t e adata in
@@ -871,6 +853,7 @@ and term_to_exp ~adata kf env t =
environment '%a'"
Printer.pp_term t generate_rte Typing.Function_params_ty.pretty
(Env.Local_vars.get env);
+ let t = Logic_normalizer.get_term t in
Extlib.flatten
(Env.with_rte_and_result env false
~f:(fun env ->
@@ -1242,7 +1225,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
| Pfresh _ -> Env.not_yet env "\\fresh"
and predicate_to_exp ~adata ?name kf ?rte env p =
- match Predicate_normalizer.get p with
+ match Logic_normalizer.get_pred p with
| PoT_term t -> term_to_exp ~adata kf env t
| PoT_pred p ->
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
diff --git a/src/plugins/e-acsl/tests/arith/extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/extended_quantifiers.c
index a3abd3674abba6e1762f2018448959e837ec60c7..4ae454f31ab1d21e81689d91024553d6943524b6 100644
--- a/src/plugins/e-acsl/tests/arith/extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/extended_quantifiers.c
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: sum operations
+ COMMENT: extended quantifiers (sum, product, numof)
*/
#include <limits.h>
diff --git a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
index 3fcbe6979c0408e461a31fcabe4acf5d8d0a67f8..e8c1201d2fab96550a0a4713cbf0033d66af1405 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/extended_quantifiers.res.oracle
@@ -44,16 +44,16 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:17: Warning:
assertion got status unknown.
-[eva:alarm] :0: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:20: Warning:
signed overflow. assert __gen_e_acsl_k_8 + __gen_e_acsl_one_8 ≤ 2147483647;
-[eva:alarm] :0: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:20: Warning:
signed overflow.
assert __gen_e_acsl_accumulator_8 + __gen_e_acsl_lambda_8 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:20: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:20: Warning:
assertion got status unknown.
-[eva:alarm] :0: Warning:
+[eva:alarm] tests/arith/extended_quantifiers.c:21: Warning:
signed overflow.
assert __gen_e_acsl_accumulator_9 + __gen_e_acsl_lambda_9 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:21: Warning:
@@ -69,28 +69,28 @@
assertion got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning:
signed overflow.
- assert __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
+ assert __gen_e_acsl_k_11 + __gen_e_acsl_one_11 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:26: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
signed overflow.
- assert __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
+ assert __gen_e_acsl_k_12 + __gen_e_acsl_one_12 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:27: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
- signed overflow. assert 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+ signed overflow. assert 2 * __gen_e_acsl_k_13 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
signed overflow.
- assert __gen_e_acsl_k_15 + __gen_e_acsl_one_13 ≤ 2147483647;
+ assert __gen_e_acsl_k_13 + __gen_e_acsl_one_13 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning:
- signed overflow. assert 2 * __gen_e_acsl_k_16 ≤ 2147483647;
+ signed overflow. assert 2 * __gen_e_acsl_k_14 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:29: Warning:
signed overflow.
- assert __gen_e_acsl_k_16 + __gen_e_acsl_one_14 ≤ 2147483647;
+ assert __gen_e_acsl_k_14 + __gen_e_acsl_one_14 ≤ 2147483647;
[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/extended_quantifiers.c:28: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index 0dc365800f3a322f927c8f285959f3d817a014eb..344827cd9d9610ec5a069db4944584a4603c5db3 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -62,7 +62,7 @@ int main(void)
else {
{
__e_acsl_mpz_t __gen_e_acsl_;
- __gmpz_init_set_ui(__gen_e_acsl_,18446744073709551615UL);
+ __gmpz_init_set_str(__gen_e_acsl_,"18446744073709551615",10);
__gmpz_set(__gen_e_acsl_lambda_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gmpz_clear(__gen_e_acsl_);
@@ -376,13 +376,7 @@ int main(void)
__gen_e_acsl_cond_10 = __gen_e_acsl_k_10 > 100;
if (__gen_e_acsl_cond_10) break;
else {
- {
- __e_acsl_mpz_t __gen_e_acsl_k_11;
- __gmpz_init_set_si(__gen_e_acsl_k_11,(long)__gen_e_acsl_k_10);
- __gmpz_set(__gen_e_acsl_lambda_10,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_11));
- __gmpz_clear(__gen_e_acsl_k_11);
- }
+ __gmpz_set_si(__gen_e_acsl_lambda_10,(long)__gen_e_acsl_k_10);
__gmpz_mul(__gen_e_acsl_accumulator_10,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_10),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_10));
@@ -405,7 +399,7 @@ int main(void)
}
/*@ assert \product(1, 100, \lambda ℤ k; k) ≥ 3628800; */ ;
{
- int __gen_e_acsl_k_12;
+ int __gen_e_acsl_k_11;
int __gen_e_acsl_one_11;
int __gen_e_acsl_cond_11;
unsigned long __gen_e_acsl_lambda_11;
@@ -414,18 +408,18 @@ int main(void)
__gen_e_acsl_cond_11 = 0;
__gen_e_acsl_lambda_11 = 0;
__gen_e_acsl_accumulator_11 = 1;
- __gen_e_acsl_k_12 = 1;
+ __gen_e_acsl_k_11 = 1;
while (1) {
- __gen_e_acsl_cond_11 = __gen_e_acsl_k_12 > 10;
+ __gen_e_acsl_cond_11 = __gen_e_acsl_k_11 > 10;
if (__gen_e_acsl_cond_11) break;
else {
- __gen_e_acsl_lambda_11 = (unsigned long)__gen_e_acsl_k_12;
+ __gen_e_acsl_lambda_11 = (unsigned long)__gen_e_acsl_k_11;
__gen_e_acsl_accumulator_11 *= __gen_e_acsl_lambda_11;
/*@ assert
Eva: signed_overflow:
- __gen_e_acsl_k_12 + __gen_e_acsl_one_11 ≤ 2147483647;
+ __gen_e_acsl_k_11 + __gen_e_acsl_one_11 ≤ 2147483647;
*/
- __gen_e_acsl_k_12 += __gen_e_acsl_one_11;
+ __gen_e_acsl_k_11 += __gen_e_acsl_one_11;
}
}
__e_acsl_assert(__gen_e_acsl_accumulator_11 == 3628800UL,1,"Assertion",
@@ -435,7 +429,7 @@ int main(void)
}
/*@ assert \product(1, 10, \lambda ℤ k; k) ≡ 3628800; */ ;
{
- int __gen_e_acsl_k_13;
+ int __gen_e_acsl_k_12;
int __gen_e_acsl_one_12;
int __gen_e_acsl_cond_12;
__e_acsl_mpz_t __gen_e_acsl_lambda_12;
@@ -446,26 +440,20 @@ int main(void)
__gen_e_acsl_cond_12 = 0;
__gmpz_init_set_si(__gen_e_acsl_lambda_12,0L);
__gmpz_init_set_si(__gen_e_acsl_accumulator_12,1L);
- __gen_e_acsl_k_13 = -10;
+ __gen_e_acsl_k_12 = -10;
while (1) {
- __gen_e_acsl_cond_12 = __gen_e_acsl_k_13 > 10;
+ __gen_e_acsl_cond_12 = __gen_e_acsl_k_12 > 10;
if (__gen_e_acsl_cond_12) break;
else {
- {
- __e_acsl_mpz_t __gen_e_acsl_k_14;
- __gmpz_init_set_si(__gen_e_acsl_k_14,(long)__gen_e_acsl_k_13);
- __gmpz_set(__gen_e_acsl_lambda_12,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_14));
- __gmpz_clear(__gen_e_acsl_k_14);
- }
+ __gmpz_set_si(__gen_e_acsl_lambda_12,(long)__gen_e_acsl_k_12);
__gmpz_mul(__gen_e_acsl_accumulator_12,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_12),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_12));
/*@ assert
Eva: signed_overflow:
- __gen_e_acsl_k_13 + __gen_e_acsl_one_12 ≤ 2147483647;
+ __gen_e_acsl_k_12 + __gen_e_acsl_one_12 ≤ 2147483647;
*/
- __gen_e_acsl_k_13 += __gen_e_acsl_one_12;
+ __gen_e_acsl_k_12 += __gen_e_acsl_one_12;
}
}
__gmpz_init_set_si(__gen_e_acsl__8,0L);
@@ -480,12 +468,12 @@ int main(void)
}
/*@ assert \product(-10, 10, \lambda ℤ k; k) ≡ 0; */ ;
{
- int __gen_e_acsl_k_15;
+ int __gen_e_acsl_k_13;
int __gen_e_acsl_one_13;
int __gen_e_acsl_cond_13;
__e_acsl_mpz_t __gen_e_acsl_lambda_13;
__e_acsl_mpz_t __gen_e_acsl_accumulator_13;
- int __gen_e_acsl_k_16;
+ int __gen_e_acsl_k_14;
int __gen_e_acsl_one_14;
int __gen_e_acsl_cond_14;
__e_acsl_mpz_t __gen_e_acsl_lambda_14;
@@ -495,17 +483,17 @@ int main(void)
__gen_e_acsl_cond_13 = 0;
__gmpz_init_set_si(__gen_e_acsl_lambda_13,0L);
__gmpz_init_set_si(__gen_e_acsl_accumulator_13,1L);
- __gen_e_acsl_k_15 = -20;
+ __gen_e_acsl_k_13 = -20;
while (1) {
- __gen_e_acsl_cond_13 = __gen_e_acsl_k_15 > -1;
+ __gen_e_acsl_cond_13 = __gen_e_acsl_k_13 > -1;
if (__gen_e_acsl_cond_13) break;
else {
{
__e_acsl_mpz_t __gen_e_acsl__9;
/*@ assert
- Eva: signed_overflow: 2 * __gen_e_acsl_k_15 ≤ 2147483647;
+ Eva: signed_overflow: 2 * __gen_e_acsl_k_13 ≤ 2147483647;
*/
- __gmpz_init_set_si(__gen_e_acsl__9,(long)(2 * __gen_e_acsl_k_15));
+ __gmpz_init_set_si(__gen_e_acsl__9,(long)(2 * __gen_e_acsl_k_13));
__gmpz_set(__gen_e_acsl_lambda_13,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
__gmpz_clear(__gen_e_acsl__9);
@@ -515,26 +503,26 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_13));
/*@ assert
Eva: signed_overflow:
- __gen_e_acsl_k_15 + __gen_e_acsl_one_13 ≤ 2147483647;
+ __gen_e_acsl_k_13 + __gen_e_acsl_one_13 ≤ 2147483647;
*/
- __gen_e_acsl_k_15 += __gen_e_acsl_one_13;
+ __gen_e_acsl_k_13 += __gen_e_acsl_one_13;
}
}
__gen_e_acsl_one_14 = 1;
__gen_e_acsl_cond_14 = 0;
__gmpz_init_set_si(__gen_e_acsl_lambda_14,0L);
__gmpz_init_set_si(__gen_e_acsl_accumulator_14,1L);
- __gen_e_acsl_k_16 = 1;
+ __gen_e_acsl_k_14 = 1;
while (1) {
- __gen_e_acsl_cond_14 = __gen_e_acsl_k_16 > 20;
+ __gen_e_acsl_cond_14 = __gen_e_acsl_k_14 > 20;
if (__gen_e_acsl_cond_14) break;
else {
{
__e_acsl_mpz_t __gen_e_acsl__10;
/*@ assert
- Eva: signed_overflow: 2 * __gen_e_acsl_k_16 ≤ 2147483647;
+ Eva: signed_overflow: 2 * __gen_e_acsl_k_14 ≤ 2147483647;
*/
- __gmpz_init_set_si(__gen_e_acsl__10,(long)(2 * __gen_e_acsl_k_16));
+ __gmpz_init_set_si(__gen_e_acsl__10,(long)(2 * __gen_e_acsl_k_14));
__gmpz_set(__gen_e_acsl_lambda_14,
(__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
__gmpz_clear(__gen_e_acsl__10);
@@ -544,9 +532,9 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_14));
/*@ assert
Eva: signed_overflow:
- __gen_e_acsl_k_16 + __gen_e_acsl_one_14 ≤ 2147483647;
+ __gen_e_acsl_k_14 + __gen_e_acsl_one_14 ≤ 2147483647;
*/
- __gen_e_acsl_k_16 += __gen_e_acsl_one_14;
+ __gen_e_acsl_k_14 += __gen_e_acsl_one_14;
}
}
__gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_13),
diff --git a/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i b/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
new file mode 100644
index 0000000000000000000000000000000000000000..b8da5291288462fc754c0543b201c32a1660f66d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/extended_quantifiers.i
@@ -0,0 +1,17 @@
+/* run.config
+ COMMENT: extended quantifiers (sum, product, numof)
+*/
+
+int main(void) {
+
+ /*@ assert \sum(2, 10, \lambda integer k; 2 * k) == 108; */;
+ /*@ assert \sum(1, 10, \lambda integer k; 1) == 10; */;
+
+ /*@ assert \numof(2, 10, \lambda integer k; k - 2 >= 0) == 9; */;
+
+ /*@ assert \product(1, 10, \lambda integer k; k) == 3628800; */;
+ /*@ assert \product(-10, 10, \lambda integer k; k) == 0; */;
+ ;
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ab3eacdf01b24921195fa7a659f9cbdc142d2c1b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/extended_quantifiers.res.oracle
@@ -0,0 +1,22 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:7: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:7: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:8: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:8: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:10: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:10: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:12: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:12: Warning:
+ assertion got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:13: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/gmp-only/extended_quantifiers.i:13: Warning:
+ assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
new file mode 100644
index 0000000000000000000000000000000000000000..f20f45faae5ce42560b8d7dcfbd86be450f89730
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
@@ -0,0 +1,301 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+int main(void)
+{
+ int __retres;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_k;
+ __e_acsl_mpz_t __gen_e_acsl_one;
+ int __gen_e_acsl_cond;
+ __e_acsl_mpz_t __gen_e_acsl_lambda;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_eq;
+ __gmpz_init_set_si(__gen_e_acsl_,2L);
+ __gmpz_init_set_si(__gen_e_acsl__2,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one,1L);
+ __gen_e_acsl_cond = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator,0L);
+ __gmpz_init_set(__gen_e_acsl_k,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ while (1) {
+ __gen_e_acsl_cond = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_cond > 0) break;
+ else {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __gmpz_init_set_si(__gen_e_acsl__3,2L);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k));
+ __gmpz_set(__gen_e_acsl_lambda,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_mul);
+ }
+ __gmpz_add(__gen_e_acsl_accumulator,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda));
+ __gmpz_add(__gen_e_acsl_k,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one));
+ }
+ }
+ __gmpz_init_set_si(__gen_e_acsl__4,108L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main",
+ "\\sum(2, 10, \\lambda integer k; 2 * k) == 108",
+ "tests/gmp-only/extended_quantifiers.i",7);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_k);
+ __gmpz_clear(__gen_e_acsl_one);
+ __gmpz_clear(__gen_e_acsl_lambda);
+ __gmpz_clear(__gen_e_acsl_accumulator);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ /*@ assert \sum(2, 10, \lambda ℤ k; 2 * k) ≡ 108; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_k_2;
+ __e_acsl_mpz_t __gen_e_acsl_one_2;
+ int __gen_e_acsl_cond_2;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_2;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_2;
+ int __gen_e_acsl_eq_2;
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set_si(__gen_e_acsl__6,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one_2,1L);
+ __gen_e_acsl_cond_2 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_2,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_2,0L);
+ __gmpz_init_set(__gen_e_acsl_k_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ while (1) {
+ __gen_e_acsl_cond_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ if (__gen_e_acsl_cond_2 > 0) break;
+ else {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __gmpz_init_set_str(__gen_e_acsl__7,"1",10);
+ __gmpz_set(__gen_e_acsl_lambda_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_clear(__gen_e_acsl__7);
+ }
+ __gmpz_add(__gen_e_acsl_accumulator_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_2));
+ __gmpz_add(__gen_e_acsl_k_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_2));
+ }
+ }
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","main",
+ "\\sum(1, 10, \\lambda integer k; 1) == 10",
+ "tests/gmp-only/extended_quantifiers.i",8);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_k_2);
+ __gmpz_clear(__gen_e_acsl_one_2);
+ __gmpz_clear(__gen_e_acsl_lambda_2);
+ __gmpz_clear(__gen_e_acsl_accumulator_2);
+ }
+ /*@ assert \sum(1, 10, \lambda ℤ k; 1) ≡ 10; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_k_3;
+ __e_acsl_mpz_t __gen_e_acsl_one_3;
+ int __gen_e_acsl_cond_3;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_3;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_3;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ int __gen_e_acsl_eq_3;
+ __gmpz_init_set_si(__gen_e_acsl__8,2L);
+ __gmpz_init_set_si(__gen_e_acsl__9,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one_3,1L);
+ __gen_e_acsl_cond_3 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_3,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_3,0L);
+ __gmpz_init_set(__gen_e_acsl_k_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ while (1) {
+ __gen_e_acsl_cond_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ if (__gen_e_acsl_cond_3 > 0) break;
+ else {
+ {
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_ge;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __gmpz_init_set_si(__gen_e_acsl__10,2L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ if (__gen_e_acsl_ge >= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_clear(__gen_e_acsl__12);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ __gmpz_init_set_si(__gen_e_acsl__13,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gmpz_clear(__gen_e_acsl__13);
+ }
+ __gmpz_set(__gen_e_acsl_lambda_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_if);
+ }
+ __gmpz_add(__gen_e_acsl_accumulator_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_3));
+ __gmpz_add(__gen_e_acsl_k_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_3));
+ }
+ }
+ __gmpz_init_set_si(__gen_e_acsl__14,9L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,1,"Assertion","main",
+ "\\numof(2, 10, \\lambda integer k; k - 2 >= 0) == 9",
+ "tests/gmp-only/extended_quantifiers.i",10);
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_k_3);
+ __gmpz_clear(__gen_e_acsl_one_3);
+ __gmpz_clear(__gen_e_acsl_lambda_3);
+ __gmpz_clear(__gen_e_acsl_accumulator_3);
+ __gmpz_clear(__gen_e_acsl__14);
+ }
+ /*@ assert \numof(2, 10, \lambda ℤ k; k - 2 ≥ 0) ≡ 9; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ __e_acsl_mpz_t __gen_e_acsl_k_4;
+ __e_acsl_mpz_t __gen_e_acsl_one_4;
+ int __gen_e_acsl_cond_4;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_4;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_4;
+ __e_acsl_mpz_t __gen_e_acsl__17;
+ int __gen_e_acsl_eq_4;
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
+ __gmpz_init_set_si(__gen_e_acsl__16,10L);
+ __gmpz_init_set_si(__gen_e_acsl_one_4,1L);
+ __gen_e_acsl_cond_4 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_4,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_4,1L);
+ __gmpz_init_set(__gen_e_acsl_k_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ while (1) {
+ __gen_e_acsl_cond_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ if (__gen_e_acsl_cond_4 > 0) break;
+ else {
+ __gmpz_set(__gen_e_acsl_lambda_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4));
+ __gmpz_mul(__gen_e_acsl_accumulator_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_4));
+ __gmpz_add(__gen_e_acsl_k_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_4));
+ }
+ }
+ __gmpz_init_set_ui(__gen_e_acsl__17,3628800UL);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,1,"Assertion","main",
+ "\\product(1, 10, \\lambda integer k; k) == 3628800",
+ "tests/gmp-only/extended_quantifiers.i",12);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl__16);
+ __gmpz_clear(__gen_e_acsl_k_4);
+ __gmpz_clear(__gen_e_acsl_one_4);
+ __gmpz_clear(__gen_e_acsl_lambda_4);
+ __gmpz_clear(__gen_e_acsl_accumulator_4);
+ __gmpz_clear(__gen_e_acsl__17);
+ }
+ /*@ assert \product(1, 10, \lambda ℤ k; k) ≡ 3628800; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl__18;
+ __e_acsl_mpz_t __gen_e_acsl_neg;
+ __e_acsl_mpz_t __gen_e_acsl_k_5;
+ __e_acsl_mpz_t __gen_e_acsl_one_5;
+ int __gen_e_acsl_cond_5;
+ __e_acsl_mpz_t __gen_e_acsl_lambda_5;
+ __e_acsl_mpz_t __gen_e_acsl_accumulator_5;
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ int __gen_e_acsl_eq_5;
+ __gmpz_init_set_si(__gen_e_acsl__18,10L);
+ __gmpz_init(__gen_e_acsl_neg);
+ __gmpz_neg(__gen_e_acsl_neg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ __gmpz_init_set_si(__gen_e_acsl_one_5,1L);
+ __gen_e_acsl_cond_5 = 0;
+ __gmpz_init_set_si(__gen_e_acsl_lambda_5,0L);
+ __gmpz_init_set_si(__gen_e_acsl_accumulator_5,1L);
+ __gmpz_init_set(__gen_e_acsl_k_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
+ while (1) {
+ __gen_e_acsl_cond_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
+ if (__gen_e_acsl_cond_5 > 0) break;
+ else {
+ __gmpz_set(__gen_e_acsl_lambda_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5));
+ __gmpz_mul(__gen_e_acsl_accumulator_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_lambda_5));
+ __gmpz_add(__gen_e_acsl_k_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_k_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_one_5));
+ }
+ }
+ __gmpz_init_set_si(__gen_e_acsl__19,0L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,1,"Assertion","main",
+ "\\product(-10, 10, \\lambda integer k; k) == 0",
+ "tests/gmp-only/extended_quantifiers.i",13);
+ __gmpz_clear(__gen_e_acsl__18);
+ __gmpz_clear(__gen_e_acsl_neg);
+ __gmpz_clear(__gen_e_acsl_k_5);
+ __gmpz_clear(__gen_e_acsl_one_5);
+ __gmpz_clear(__gen_e_acsl_lambda_5);
+ __gmpz_clear(__gen_e_acsl_accumulator_5);
+ __gmpz_clear(__gen_e_acsl__19);
+ }
+ /*@ assert \product(-10, 10, \lambda ℤ k; k) ≡ 0; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_dev/extended_quantifiers.e-acsl.err.log b/src/plugins/e-acsl/tests/gmp-only/oracle_dev/extended_quantifiers.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 5f0767c667b169e7b5eff49b5007636e14a92a0b..869a3f3915845f8bf290cc1f736ed76c918ad304 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -709,15 +709,22 @@ struct
obj , domain , seq , loc
let cc_stored lv seq loc obj expr =
- if Cil.isVolatileLval lv &&
- Cvalues.volatile ~warn:"unsafe write-access to volatile l-value" ()
- then None
+ let intercept_volatile kind lv =
+ let warn = "unsafe " ^ kind ^ "-access to volatile l-value" in
+ Cil.isVolatileLval lv && Cvalues.volatile ~warn ()
+ in
+ if intercept_volatile "write" lv then None
else
let value = match expr.enode with
- | Lval lv -> M.copied seq obj loc (C.lval seq.pre lv)
- | _ -> M.stored seq obj loc (C.val_of_exp seq.pre expr)
+ | Lval lv when not @@ intercept_volatile "read" lv ->
+ M.copied seq obj loc (C.lval seq.pre lv)
+ | _ ->
+ (* Note: a volatile lval will be compiled to an unknown value *)
+ M.stored seq obj loc (C.val_of_exp seq.pre expr)
in
let init = match expr.enode with
+ | Lval lv when intercept_volatile "read" lv ->
+ M.stored_init seq obj loc (Cvalues.initialized_obj obj)
| Lval lv when Cil.(isStructOrUnionType @@ typeOfLval lv) ->
M.copied_init seq obj loc (C.lval seq.pre lv)
| _ ->
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
index 2df04eb693e0221ae001c0fbd615d432dec4cd3c..b24ccc3ce53c9991dc222d4927c9798cd922f55a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
@@ -2,11 +2,24 @@
[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function default_init
+------------------------------------------------------------
+
+Goal Check 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 46):
+Assume {
+ Type: is_sint8(ClientId_0) /\ is_sint32(R1_0).
+ (* Pre-condition *)
+ Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: R1_0 = 0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function job_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 15):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 16):
Prove: w = 0.
------------------------------------------------------------
@@ -14,7 +27,7 @@ Prove: w = 0.
Function job_read
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 21):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 22):
Assume { Type: is_sint32(x). }
Prove: x = w.
@@ -23,7 +36,7 @@ Prove: x = w.
Function job_struct
------------------------------------------------------------
-Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 29):
+Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 30):
Prove: true.
------------------------------------------------------------
@@ -31,11 +44,11 @@ Prove: true.
Function job_struct_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 36):
Prove: EqS1_st_v(w, w_1).
------------------------------------------------------------
-[wp] tests/wp_plugin/volatile.i:32: Warning:
+[wp] tests/wp_plugin/volatile.i:33: Warning:
Memory model hypotheses for function 'job_struct_assigns':
/*@ behavior wp_typed:
requires \separated(p, &sv); */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
index 63e2b65a2c49a5ca6bf4edcaf5f179a9121e0b6d..c93f2248bbf30e4332b712a26b366f59212dc1d7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
@@ -2,29 +2,54 @@
[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/volatile.i:15: Warning:
+[wp] tests/wp_plugin/volatile.i:16: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:14: Warning:
+[wp] tests/wp_plugin/volatile.i:15: Warning:
unsafe write-access to volatile l-value
-[wp] tests/wp_plugin/volatile.i:21: Warning:
+[wp] tests/wp_plugin/volatile.i:22: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:20: Warning:
+[wp] tests/wp_plugin/volatile.i:21: Warning:
unsafe read-access to volatile l-value
-[wp] tests/wp_plugin/volatile.i:35: Warning:
+[wp] tests/wp_plugin/volatile.i:36: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:35: Warning:
+[wp] tests/wp_plugin/volatile.i:36: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:34: Warning:
+[wp] tests/wp_plugin/volatile.i:35: Warning:
unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning:
+ unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:45: Warning:
+ unsafe read-access to volatile l-value
+------------------------------------------------------------
+ Function default_init
+------------------------------------------------------------
+
+Goal Check 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 46):
+tests/wp_plugin/volatile.i:45: warning from wp:
+ - Warning: ignore volatile attribute
+ Reason: unsafe read-access to volatile l-value
+Let x = GlobalConst_0[ClientId_0].
+Assume {
+ Type: is_sint8(ClientId_0) /\ is_sint32(x).
+ (* Heap *)
+ Type: IsArray_sint32(GlobalConst_0).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 15) -> (GlobalConst_0[i] = 0))).
+ (* Pre-condition *)
+ Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function job_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 15):
-tests/wp_plugin/volatile.i:14: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 16):
+tests/wp_plugin/volatile.i:15: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe write-access to volatile l-value
-tests/wp_plugin/volatile.i:15: warning from wp:
+tests/wp_plugin/volatile.i:16: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
Prove: true.
@@ -34,11 +59,11 @@ Prove: true.
Function job_read
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 21):
-tests/wp_plugin/volatile.i:20: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 22):
+tests/wp_plugin/volatile.i:21: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe read-access to volatile l-value
-tests/wp_plugin/volatile.i:21: warning from wp:
+tests/wp_plugin/volatile.i:22: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
Prove: true.
@@ -48,7 +73,7 @@ Prove: true.
Function job_struct
------------------------------------------------------------
-Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 29):
+Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 30):
Prove: true.
------------------------------------------------------------
@@ -56,20 +81,23 @@ Prove: true.
Function job_struct_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
-tests/wp_plugin/volatile.i:34: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 36):
+tests/wp_plugin/volatile.i:35: warning from wp:
- Warning: ignore volatile attribute
- Reason: unsafe write-access to volatile l-value
+ Reason: unsafe read-access to volatile l-value
tests/wp_plugin/volatile.i:35: warning from wp:
+ - Warning: ignore volatile attribute
+ Reason: unsafe write-access to volatile l-value
+tests/wp_plugin/volatile.i:36: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
-tests/wp_plugin/volatile.i:35: warning from wp:
+tests/wp_plugin/volatile.i:36: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
Prove: true.
------------------------------------------------------------
-[wp] tests/wp_plugin/volatile.i:32: Warning:
+[wp] tests/wp_plugin/volatile.i:33: Warning:
Memory model hypotheses for function 'job_struct_assigns':
/*@ behavior wp_typed:
requires \separated(p, &sv); */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..51ab2374303a31162f49c5cba1909d674157fb7a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle
@@ -0,0 +1,26 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_assigns_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_read_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Qed] Goal typed_job_struct_assert_ok_dead_code : Valid
+[wp] [Alt-Ergo] Goal typed_job_struct_assigns_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_default_init_check_KO_WHEN_VOLATILE : Unsuccess
+[wp] Proved goals: 1 / 5
+ Qed: 1
+ Alt-Ergo: 0 (unsuccess: 4)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job_assigns - - 1 0.0%
+ job_read - - 1 0.0%
+ job_struct 1 - 1 100%
+ job_struct_assigns - - 1 0.0%
+ default_init - - 1 0.0%
+------------------------------------------------------------
+[wp] tests/wp_plugin/volatile.i:33: Warning:
+ Memory model hypotheses for function 'job_struct_assigns':
+ /*@ behavior wp_typed:
+ requires \separated(p, &sv); */
+ void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bfc0ecc2ae39d06cb58566862af0fc0f9a0c2ceb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle
@@ -0,0 +1,44 @@
+# frama-c -wp -wp-no-volatile [...]
+[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/volatile.i:16: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:15: Warning:
+ unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:22: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:21: Warning:
+ unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:36: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:36: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning:
+ unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning:
+ unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:45: Warning:
+ unsafe read-access to volatile l-value
+[wp] 5 goals scheduled
+[wp] [Qed] Goal typed_job_assigns_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Qed] Goal typed_job_read_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Qed] Goal typed_job_struct_assert_ok_dead_code : Valid
+[wp] [Qed] Goal typed_job_struct_assigns_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Alt-Ergo] Goal typed_default_init_check_KO_WHEN_VOLATILE : Valid
+[wp] Proved goals: 5 / 5
+ Qed: 4
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job_assigns 1 - 1 100%
+ job_read 1 - 1 100%
+ job_struct 1 - 1 100%
+ job_struct_assigns 1 - 1 100%
+ default_init - 1 1 100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/volatile.i:33: Warning:
+ Memory model hypotheses for function 'job_struct_assigns':
+ /*@ behavior wp_typed:
+ requires \separated(p, &sv); */
+ void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/volatile.i b/src/plugins/wp/tests/wp_plugin/volatile.i
index 81be3c130b37e940d99c901af4ad44c1a8a1bd9c..49c337571ffbf7ee91e6a35cccc053fc33bce4d3 100644
--- a/src/plugins/wp/tests/wp_plugin/volatile.i
+++ b/src/plugins/wp/tests/wp_plugin/volatile.i
@@ -2,11 +2,12 @@
OPT:
OPT: -wp-no-volatile
*/
-
/* run.config_qualif
- DONTRUN:
+ OPT:
+ OPT: -wp-no-volatile
*/
+
volatile int v ;
void job_assigns(void)
@@ -34,3 +35,13 @@ void job_struct_assigns(struct st_v *p)
*p = sv;
/*@ assert KO_WHEN_VOLATILE: *p == sv ; */ ;
}
+
+int const volatile GlobalConst[16];
+
+/*@ requires 0 ≤ ClientId < 16; */
+void default_init(char const ClientId)
+{
+ int R1;
+ R1 = GlobalConst[ClientId];
+ //@ check KO_WHEN_VOLATILE: R1 == 0 ;
+}