diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index bdd66e6ceacff29e6a49b27351ea8d2c1e790b3d..f5f780dd7d02bf57a3c44434d4fb7f2e60cd61f2 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -27,6 +27,8 @@ Plugin E-ACSL <next-release>
-* E-ACSL [2024-09-16] fix logic variable escaping its scope
-* E-ACSL [2024-09-03] handle negative integers generated by RTE
+- E-ACSL [2024-09-03] add support for labelled logic functions in case
+ they are called only with the Here label.
-* E-ACSL [2024-08-30] fix typing exception occurring for applications
of axiomatically defined premises and logic functions
-* E-ACSL [2024-08-22] fix arity confusion of generated functions.
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index a6fd74c101fa752d845c2383249fb3fa07a01e4e..9d89e6d9279e643fb7460d8af131b8241e83df9a 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -21,13 +21,14 @@
(**************************************************************************)
open Cil_types
+open Cil_datatype
let dkey = Options.Dkey.logic_normalizer
module Id_predicate =
Datatype.Make_with_collections
(struct
- include Cil_datatype.Predicate
+ include Predicate
let name = "E_ACSL.Id_predicate"
(* The function compare should never be used since we only use this
datatype for hashtables *)
@@ -82,8 +83,180 @@ end
module Predicates = Memo (Id_predicate.Hashtbl)
module Terms = Memo (Misc.Id_term.Hashtbl)
+module Here_specialized = Memo (Logic_info.Hashtbl)
+
+let pp_logic_info fmt li =
+ Printer.pp_global_annotation fmt (Dfun_or_pred (li, Location.unknown))
+
+module Logic_infos : sig
+ val origin_of_lv : logic_var -> logic_var
+ val generated_of : logic_info -> logic_info list
+end = struct
+ let original_of_lv lv =
+ Here_specialized.original_opt
+ {l_var_info = lv;
+ l_labels = [];
+ l_tparams = [];
+ l_type = None;
+ l_profile = [];
+ l_body = LBnone}
+
+ let rec origin_of_lv lv =
+ match original_of_lv lv with
+ | None -> lv
+ | Some origin -> origin_of_lv origin.l_var_info
+
+ let generated_of li = Option.to_list @@ Here_specialized.normalized_opt li
+end
+
+(** E-ACSL currently is not in general capable of translationg predicates and
+ logic functions with labels. However often such functions are used
+ while supplying the Here label.
+ In this case we can specialize the logic function, such that it has no
+ labels, substituting all occurrences of the original labels by the Here
+ label. Then the specialized function can be used instead of the original
+ one whenever all labels are Here. *)
+module Here_inliner : sig
+ val preprocess_pred : predicate -> predicate option
+ val preprocess_term : term -> term option
+
+ (** apply a preprocessor to the result of another *)
+ val bind : ('a -> 'a option) -> 'a -> 'a option -> 'a option
+end = struct
+
+ let here = BuiltinLabel Here
+ let is_here = (=) here
+ let are_all_here labels = List.length labels > 0 && List.for_all is_here labels
+
+ (** substitute occurrences of li_old by li_new; also substitute occurrences
+ of li_old's formal parameters by li_new's parameters; li_new does not
+ have any labels so substitute occurrences of li_old's labels by Here *)
+ let substitute li_old li_new =
+ let formal_substitutions =
+ Logic_var.Map.of_seq
+ (List.to_seq @@ List.combine li_old.l_profile li_new.l_profile)
+ in
+ let is_obsolete_label =
+ let obsolete_labels =
+ Logic_label.Set.of_seq @@ List.to_seq @@ here :: li_old.l_labels
+ in
+ fun l -> Logic_label.Set.mem l obsolete_labels
+ in
+ object
+ inherit Visitor.frama_c_inplace
+
+ method! vlogic_var_use lv =
+ match Logic_var.Map.find_opt lv formal_substitutions with
+ | None -> DoChildren
+ | Some lv' -> ChangeTo lv'
+
+ method !vpredicate p =
+ match p.pred_content with
+ | Papp (li, labels, args) when
+ Logic_info.equal li li_old && List.for_all is_obsolete_label labels ->
+ let p = {p with pred_content = Papp (li_new, [], args)} in
+ ChangeDoChildrenPost (p, fun x -> x)
+ | _ -> DoChildren
+
+ method !vterm t =
+ match t.term_node with
+ | Tat (body, label) when is_obsolete_label label ->
+ ChangeDoChildrenPost (body, fun x -> x)
+ | Tapp (li, labels, args) when
+ Logic_info.equal li li_old && List.for_all is_obsolete_label labels ->
+ let t = {t with term_node = Tapp (li_new, [], args)} in
+ ChangeDoChildrenPost (t, fun x -> x)
+ | _ -> DoChildren
+
+ method !vlogic_info_use l =
+ if Logic_info.equal l li_old
+ then ChangeTo li_new
+ else DoChildren
+
+ method !vlogic_label l =
+ if is_obsolete_label l then ChangeTo here else DoChildren
+ end
+
+ let specialize li =
+ let f li =
+ let lv_name = Functions.RTL.mk_gen_name (li.l_var_info.lv_name ^ "_here") in
+ let vi = {li.l_var_info with lv_name; lv_id = Cil_const.new_raw_id ()} in
+ let li' = {
+ li with
+ l_var_info = vi;
+ l_labels = [];
+ l_profile =
+ List.map (fun lv -> {lv with lv_id = Cil_const.new_raw_id ()}) li.l_profile
+ } in
+ let li' = Visitor.visitFramacLogicInfo (substitute li li') li' in
+ let pred_or_term =
+ match li.l_type with None -> "predicate" | Some _ -> "logic function"
+ in
+ Options.feedback ~dkey ~level:2
+ "specializing %s %a for use cases using the Here label"
+ pred_or_term
+ Printer.pp_logic_info li;
+ Options.feedback ~dkey ~level:3
+ "specialized version of %s %a:@ @[%a@]"
+ pred_or_term
+ Printer.pp_logic_info li
+ pp_logic_info li';
+ Some li'
+ in
+ Option.get @@ Here_specialized.memoize f li
+
+ let inliner = object (self)
+ inherit Visitor.frama_c_inplace
+
+ method !vpredicate p =
+ match p.pred_content with
+ | Papp (li, labels, args) when are_all_here labels ->
+ Options.feedback ~dkey ~level:3
+ "inlining Here labels for predicate: @[%a@]"
+ Printer.pp_predicate p;
+ let li = specialize li in
+ (* The Cil visitor does not descend into [logic_info] definitions. *)
+ let li = Visitor.visitFramacLogicInfo self li in
+ let p = {p with pred_content = Papp(li, [], args)} in
+ ChangeDoChildrenPost (p, fun x -> x)
+ | _ -> DoChildren
+
+ method !vterm t =
+ match t.term_node with
+ | Tapp(li, labels, args) when are_all_here labels ->
+ Options.feedback ~dkey ~level:3
+ "inlining Here labels for term: %a"
+ Printer.pp_term t;
+ let li = specialize li in
+ (* The Cil visitor does not descend into [logic_info] definitions. *)
+ let li = Visitor.visitFramacLogicInfo self li in
+ let t = {t with term_node = Tapp(li, [], args)} in
+ ChangeDoChildrenPost (t, fun x -> x)
+ | _ -> DoChildren
+ end
+
+ let preprocess_pred p =
+ match p.pred_content with
+ | Papp(_li, labels, _args) when are_all_here labels ->
+ Some (Visitor.visitFramacPredicate inliner p)
+ | _ -> None
+
+ let preprocess_term t =
+ match t.term_node with
+ | Tapp(_li, labels, _args) when are_all_here labels ->
+ Some (Visitor.visitFramacTerm inliner t)
+ | _ -> None
+
+ (* apply to the result of a first preprocessor a second one *)
+ let bind f orig = function
+ | None -> f orig (* first preprocessor yields nothing, use original value *)
+ | Some p -> match f p with
+ | None -> Some p (* second preprocessor yields nothing *)
+ | Some p -> Some p
+end
let preprocess_pred ~loc p =
+ Here_inliner.(bind preprocess_pred) p @@
match p.pred_content with
| Pvalid_read(BuiltinLabel Here as llabel, t)
| Pvalid(BuiltinLabel Here as llabel, t) -> begin
@@ -108,6 +281,7 @@ let preprocess_pred ~loc p =
| _ -> None
let preprocess_term ~loc t =
+ Here_inliner.(bind preprocess_term) 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" ->
@@ -163,4 +337,5 @@ let get_orig_term = Terms.original
let clear () =
Terms.clear ();
- Predicates.clear ()
+ Predicates.clear ();
+ Here_specialized.clear ()
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
index e081f4da94962c7aa74f83db97b788a95b7f1aad..f44075f1407cdc02e2ee07b3bb17508f96039d76 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
@@ -41,6 +41,22 @@ val preprocess_annot : code_annotation -> unit
val preprocess_predicate : predicate -> unit
(** Preprocess a predicate and its children and store the results *)
+(** The analyses in [Logic_normalizer] may:
+ - create new auxiliary predicates and logic functions
+ - transform inductively and axiomatically defined logic functions and
+ predicates into recursively defined ones
+ This module provides functions to inquire about their status. *)
+module Logic_infos : sig
+ val generated_of : logic_info -> logic_info list
+ (** auxiliary [logic_info]s generated from the given [logic_info]. *)
+
+ val origin_of_lv : logic_var -> logic_var
+ (** Identify the [logic_info] from which the [logic_info] identified by the
+ given argument stems from. This is required in order to create meaningful
+ feedback messages for the user who should not be confronted with the
+ names of generated logic functions. *)
+end
+
val get_pred : predicate -> predicate
(** Retrieve the preprocessed form of a predicate *)
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
index f33b65bf6e1f4a50acd12245e858f5356b07c3f6..22bc5c1b8565be6684a590add64198b882c5a794 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.ml
+++ b/src/plugins/e-acsl/src/code_generator/assigns.ml
@@ -75,7 +75,8 @@ let rec get_assigns_from ~loc env lprofile lv =
Options.warning ~current:true "no assigns clause generated for \
function %a because pointers as arguments \
is not yet supported"
- Printer.pp_logic_var lv;
+ Printer.pp_logic_var
+ (Logic_normalizer.Logic_infos.origin_of_lv lv);
raise NoAssigns
end
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 289cc2bb6f4e7fddee0a8e05350577e88c39165a..8a004c3669c2c09f0f7119020ae2a9145889b872 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -374,10 +374,16 @@ end
let reset () = Gen_functions.clear ()
let add_generated_functions_to_file file =
+ let rec decls_of_li ?(loc = Location.unknown) li =
+ let dependencies =
+ List.concat_map (decls_of_li ~loc)
+ (Logic_normalizer.Logic_infos.generated_of li)
+ in
+ let kfs = Gen_functions.kernel_functions_of_logic_info li in
+ dependencies @ List.map (fun kf -> GFunDecl (Cil.empty_funspec (), kf, loc)) kfs
+ in
let generated_decls_of_global = function
- | GAnnot(Dfun_or_pred(li, loc), _) ->
- let kfs = Gen_functions.kernel_functions_of_logic_info li in
- List.map (fun kf -> GFunDecl (Cil.empty_funspec (), kf, loc)) kfs
+ | GAnnot(Dfun_or_pred(li, loc), _) -> decls_of_li ~loc li
| _ -> []
in
(* add declarations of generated functions just below the logic
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index c1e35f6afa59bc1aedf39e16abebe356cb49344f..6bf27aa86ccbd5e29bca87ef93b766e1005fd29b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -85,11 +85,11 @@ double __gen_e_acsl_f2(double x);
/*@ predicate p_here{L}(integer x) = x > 0;
*/
-int __gen_e_acsl_p_here(int x);
+int __gen_e_acsl_p_here_here(int x);
/*@ logic integer f_here{L}(integer x) = x;
*/
-int __gen_e_acsl_f_here(int x);
+int __gen_e_acsl_f_here_here(int x);
/*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
*/
@@ -113,7 +113,7 @@ int z = 8;
/*@ logic integer f3{L}(integer y) = \at(z + y,L);
*/
-long __gen_e_acsl_f3(int y);
+long __gen_e_acsl_f3_here(int y);
int main(void)
{
@@ -454,54 +454,58 @@ int main(void)
}
/*@ assert over(1., 2.) == 0.5; */ ;
{
- int __gen_e_acsl_p_here_2;
+ int __gen_e_acsl_p_here_here_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_16 =
{.values = (void *)0};
- __gen_e_acsl_p_here_2 = __gen_e_acsl_p_here(27);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"p_here(27)",
- 0,__gen_e_acsl_p_here_2);
+ __gen_e_acsl_p_here_here_2 = __gen_e_acsl_p_here_here(27);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,
+ "__gen_e_acsl_p_here_here(27)",0,
+ __gen_e_acsl_p_here_here_2);
__gen_e_acsl_assert_data_16.blocking = 1;
__gen_e_acsl_assert_data_16.kind = "Assertion";
__gen_e_acsl_assert_data_16.pred_txt = "p_here(27)";
__gen_e_acsl_assert_data_16.file = "functions.c";
__gen_e_acsl_assert_data_16.fct = "main";
__gen_e_acsl_assert_data_16.line = 93;
- __e_acsl_assert(__gen_e_acsl_p_here_2,& __gen_e_acsl_assert_data_16);
+ __e_acsl_assert(__gen_e_acsl_p_here_here_2,& __gen_e_acsl_assert_data_16);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
}
/*@ assert p_here(27); */ ;
{
- int __gen_e_acsl_f_here_2;
+ int __gen_e_acsl_f_here_here_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_17 =
{.values = (void *)0};
- __gen_e_acsl_f_here_2 = __gen_e_acsl_f_here(27);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,"f_here(27)",
- 0,__gen_e_acsl_f_here_2);
+ __gen_e_acsl_f_here_here_2 = __gen_e_acsl_f_here_here(27);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,
+ "__gen_e_acsl_f_here_here(27)",0,
+ __gen_e_acsl_f_here_here_2);
__gen_e_acsl_assert_data_17.blocking = 1;
__gen_e_acsl_assert_data_17.kind = "Assertion";
__gen_e_acsl_assert_data_17.pred_txt = "f_here(27) == 27";
__gen_e_acsl_assert_data_17.file = "functions.c";
__gen_e_acsl_assert_data_17.fct = "main";
__gen_e_acsl_assert_data_17.line = 94;
- __e_acsl_assert(__gen_e_acsl_f_here_2 == 27,
+ __e_acsl_assert(__gen_e_acsl_f_here_here_2 == 27,
& __gen_e_acsl_assert_data_17);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_17);
}
/*@ assert f_here(27) == 27; */ ;
{
- long __gen_e_acsl_f3_2;
+ long __gen_e_acsl_f3_here_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_18 =
{.values = (void *)0};
- __gen_e_acsl_f3_2 = __gen_e_acsl_f3(5);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,"f3(5)",0,
- __gen_e_acsl_f3_2);
+ __gen_e_acsl_f3_here_2 = __gen_e_acsl_f3_here(5);
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,
+ "__gen_e_acsl_f3_here(5)",0,
+ __gen_e_acsl_f3_here_2);
__gen_e_acsl_assert_data_18.blocking = 1;
__gen_e_acsl_assert_data_18.kind = "Assertion";
__gen_e_acsl_assert_data_18.pred_txt = "f3(5) == 13";
__gen_e_acsl_assert_data_18.file = "functions.c";
__gen_e_acsl_assert_data_18.fct = "main";
__gen_e_acsl_assert_data_18.line = 96;
- __e_acsl_assert(__gen_e_acsl_f3_2 == 13L,& __gen_e_acsl_assert_data_18);
+ __e_acsl_assert(__gen_e_acsl_f3_here_2 == 13L,
+ & __gen_e_acsl_assert_data_18);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_18);
}
/*@ assert f3(5) == 13; */ ;
@@ -805,21 +809,6 @@ double __gen_e_acsl_f2(double x)
return __gen_e_acsl__8;
}
-/*@ assigns \result;
- assigns \result \from x; */
-int __gen_e_acsl_p_here(int x)
-{
- int __retres = x > 0;
- return __retres;
-}
-
-/*@ assigns \result;
- assigns \result \from x; */
-int __gen_e_acsl_f_here(int x)
-{
- return x;
-}
-
/*@ assigns \result;
assigns \result \from x; */
int __gen_e_acsl_f_sum(int x)
@@ -926,14 +915,6 @@ int __gen_e_acsl_signum_3(__e_acsl_mpq_t x)
return __gen_e_acsl_if_4;
}
-/*@ assigns \result;
- assigns \result \from y; */
-long __gen_e_acsl_f3(int y)
-{
- long __retres = z + (long)y;
- return __retres;
-}
-
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)x); */
int __gen_e_acsl_f4(__e_acsl_mpz_struct * x)
@@ -1105,4 +1086,27 @@ void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x)
return;
}
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_p_here_here(int x)
+{
+ int __retres = x > 0;
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_f_here_here(int x)
+{
+ return x;
+}
+
+/*@ assigns \result;
+ assigns \result \from y; */
+long __gen_e_acsl_f3_here(int y)
+{
+ long __retres = z + (long)y;
+ return __retres;
+}
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index 1397e624078c0700e7bf18faf078bdeb20a83da9..af0ce5a8cf2ea6d83c5d80046abcf396c8134b22 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,8 +1,11 @@
[e-acsl] beginning translation.
[e-acsl] FRAMAC_SHARE/libc/string.h:431: Warning:
no assigns clause generated for function valid_read_nstring because pointers as arguments is not yet supported
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:280: Warning:
- E-ACSL construct `labeled \valid_read' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
+ no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:277: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 8be695d45b22f463ff59f911800447ce33636a1e..e6397626eec5ed493b37b2127175735ac0c77c8c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -54,66 +54,68 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
+ char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
{
__e_acsl_mpz_t __gen_e_acsl_n;
- unsigned long __gen_e_acsl_size;
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl_sub_2;
- __e_acsl_mpz_t __gen_e_acsl_add;
- unsigned long __gen_e_acsl__3;
- unsigned long __gen_e_acsl_if;
- int __gen_e_acsl_valid;
- unsigned long __gen_e_acsl_size_2;
- unsigned long __gen_e_acsl__4;
- unsigned long __gen_e_acsl_if_2;
- int __gen_e_acsl_valid_read;
unsigned long __gen_e_acsl_size_3;
- unsigned long __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl_sub_6;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ unsigned long __gen_e_acsl__9;
unsigned long __gen_e_acsl_if_3;
- int __gen_e_acsl_valid_read_2;
+ int __gen_e_acsl_valid;
unsigned long __gen_e_acsl_size_4;
- unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl__10;
unsigned long __gen_e_acsl_if_4;
+ int __gen_e_acsl_valid_read_2;
unsigned long __gen_e_acsl_size_5;
- unsigned long __gen_e_acsl__7;
+ unsigned long __gen_e_acsl__11;
unsigned long __gen_e_acsl_if_5;
+ int __gen_e_acsl_valid_read_3;
+ unsigned long __gen_e_acsl_size_6;
+ unsigned long __gen_e_acsl__12;
+ unsigned long __gen_e_acsl_if_6;
+ unsigned long __gen_e_acsl_size_7;
+ unsigned long __gen_e_acsl__13;
+ unsigned long __gen_e_acsl_if_7;
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
+ __gen_e_acsl_at_2 = src;
__gmpz_init_set_ui(__gen_e_acsl_n,n);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
- __gmpz_init_set_si(__gen_e_acsl_,1L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init(__gen_e_acsl_sub_2);
- __gmpz_sub(__gen_e_acsl_sub_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
- if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
- else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gmpz_init_set_ui(__gen_e_acsl_n_4,n);
+ __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gmpz_init(__gen_e_acsl_sub_6);
+ __gmpz_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gen_e_acsl__9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__9;
+ if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
__gen_e_acsl_valid = __e_acsl_valid((void *)(dest + 1 * 0),
- __gen_e_acsl_if,(void *)dest,
+ __gen_e_acsl_if_3,(void *)dest,
(void *)(& dest));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"dest",
(void *)dest);
@@ -123,9 +125,9 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"n",0,n);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"size",0,
- __gen_e_acsl_size);
+ __gen_e_acsl_size_3);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"size",0,
- __gen_e_acsl_size);
+ __gen_e_acsl_size_3);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
"room_nstring: \\valid(dest + (0 .. n - 1))",
0,__gen_e_acsl_valid);
@@ -142,14 +144,14 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
{.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
- if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
- else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(dest + 1 * 0),
- __gen_e_acsl_if_2,
- (void *)dest,
- (void *)(& dest));
+ __gen_e_acsl__10 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__10;
+ if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(dest + 1 * 0),
+ __gen_e_acsl_if_4,
+ (void *)dest,
+ (void *)(& dest));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"dest",
(void *)dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
@@ -158,9 +160,9 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"n",0,n);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
- __gen_e_acsl_size_2);
+ __gen_e_acsl_size_4);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
- __gen_e_acsl_size_2);
+ __gen_e_acsl_size_4);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
__gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(dest + (0 .. n - 1))";
@@ -168,16 +170,16 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_4.fct = "strncpy";
__gen_e_acsl_assert_data_4.line = 434;
__gen_e_acsl_assert_data_4.name = "separated_guard";
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
- if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
- else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(src + 1 * 0),
- __gen_e_acsl_if_3,
+ __gen_e_acsl__11 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gen_e_acsl_size_5 = 1UL * __gen_e_acsl__11;
+ if (__gen_e_acsl_size_5 <= 0UL) __gen_e_acsl_if_5 = 0UL;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(src + 1 * 0),
+ __gen_e_acsl_if_5,
(void *)src,
(void *)(& src));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"src",
@@ -188,9 +190,9 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
"sizeof(char const)",0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"n",0,n);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"size",0,
- __gen_e_acsl_size_3);
+ __gen_e_acsl_size_5);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"size",0,
- __gen_e_acsl_size_3);
+ __gen_e_acsl_size_5);
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "RTE";
__gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(src + (0 .. n - 1))";
@@ -198,20 +200,20 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_5.fct = "strncpy";
__gen_e_acsl_assert_data_5.line = 434;
__gen_e_acsl_assert_data_5.name = "separated_guard";
- __e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
- if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
- else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
- __gen_e_acsl__7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_5 = 1UL * __gen_e_acsl__7;
- if (__gen_e_acsl_size_5 <= 0UL) __gen_e_acsl_if_5 = 0UL;
- else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl__12 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gen_e_acsl_size_6 = 1UL * __gen_e_acsl__12;
+ if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_6 = 0UL;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl__13 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gen_e_acsl_size_7 = 1UL * __gen_e_acsl__13;
+ if (__gen_e_acsl_size_7 <= 0UL) __gen_e_acsl_if_7 = 0UL;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
__gen_e_acsl_separated = __e_acsl_separated(2UL,dest + 1 * 0,
- __gen_e_acsl_if_4,
+ __gen_e_acsl_if_6,
src + 1 * 0,
- __gen_e_acsl_if_5);
+ __gen_e_acsl_if_7);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"dest",
(void *)dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(char)",
@@ -220,9 +222,9 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"n",0,n);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_4);
+ __gen_e_acsl_size_6);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_4);
+ __gen_e_acsl_size_6);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
@@ -231,9 +233,9 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
"sizeof(char const)",0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"n",0,n);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_5);
+ __gen_e_acsl_size_7);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_5);
+ __gen_e_acsl_size_7);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"separation: \\separated(dest + (0 .. n - 1), src + (0 .. n - 1))",
0,__gen_e_acsl_separated);
@@ -247,25 +249,25 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert(__gen_e_acsl_separated,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl_sub_2);
- __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl_sub_6);
+ __gmpz_clear(__gen_e_acsl_add_3);
}
__retres = strncpy(dest,src,n);
__e_acsl_initialize((void *)dest,n);
{
- unsigned long __gen_e_acsl_size_6;
- __e_acsl_mpz_t __gen_e_acsl__8;
- __e_acsl_mpz_t __gen_e_acsl_sub_3;
- __e_acsl_mpz_t __gen_e_acsl__9;
- __e_acsl_mpz_t __gen_e_acsl_sub_4;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- unsigned long __gen_e_acsl__10;
- unsigned long __gen_e_acsl_if_6;
- int __gen_e_acsl_initialized;
+ unsigned long __gen_e_acsl_size_8;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ __e_acsl_mpz_t __gen_e_acsl_sub_7;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_sub_8;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ unsigned long __gen_e_acsl__16;
+ unsigned long __gen_e_acsl_if_8;
+ int __gen_e_acsl_initialized_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result",
@@ -283,27 +285,27 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
- __gmpz_init_set_si(__gen_e_acsl__8,1L);
- __gmpz_init(__gen_e_acsl_sub_3);
- __gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_init_set_si(__gen_e_acsl__9,0L);
- __gmpz_init(__gen_e_acsl_sub_4);
- __gmpz_sub(__gen_e_acsl_sub_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gen_e_acsl__10 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gen_e_acsl_size_6 = 1UL * __gen_e_acsl__10;
- if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_6 = 0UL;
- else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at +
- 1 * 0),
- __gen_e_acsl_if_6);
+ __gmpz_init_set_si(__gen_e_acsl__14,1L);
+ __gmpz_init(__gen_e_acsl_sub_7);
+ __gmpz_sub(__gen_e_acsl_sub_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __gmpz_init_set_si(__gen_e_acsl__15,0L);
+ __gmpz_init(__gen_e_acsl_sub_8);
+ __gmpz_sub(__gen_e_acsl_sub_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __gen_e_acsl__16 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gen_e_acsl_size_8 = 1UL * __gen_e_acsl__16;
+ if (__gen_e_acsl_size_8 <= 0UL) __gen_e_acsl_if_8 = 0UL;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(__gen_e_acsl_at +
+ 1 * 0),
+ __gen_e_acsl_if_8);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
(void *)__gen_e_acsl_at);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
@@ -311,14 +313,14 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"\\old(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
- __gen_e_acsl_size_6);
+ __gen_e_acsl_size_8);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
- __gen_e_acsl_size_6);
+ __gen_e_acsl_size_8);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
"initialization: \\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
- 0,__gen_e_acsl_initialized);
+ 0,__gen_e_acsl_initialized_2);
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "Postcondition";
__gen_e_acsl_assert_data_7.pred_txt = "\\initialized(\\old(dest) + (0 .. \\old(n) - 1))";
@@ -326,17 +328,17 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_7.fct = "strncpy";
__gen_e_acsl_assert_data_7.line = 438;
__gen_e_acsl_assert_data_7.name = "initialization";
- __e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert(__gen_e_acsl_initialized_2,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__e_acsl_contract_clean(__gen_e_acsl_contract);
__e_acsl_delete_block((void *)(& src));
__e_acsl_delete_block((void *)(& dest));
- __gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_sub_3);
- __gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_sub_4);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl_sub_7);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_sub_8);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl_at_3);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 22861bb8b860502478a963a058939debbb3fe233..22c523cc0e400b2f2d32a346ef8fafb958ff87f6 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -158,7 +158,9 @@ __inline static void fail_ncomp(int cond, char *fmt, int l, int r)
char *__gen_e_acsl_strdup(char const *s)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char const *__gen_e_acsl_at;
char *__retres;
+ __gen_e_acsl_at = s;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__retres = strdup(s);
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 9c38744e026b52389077dae64f7fe875e17a8dd0..08a859cae3870b75595d0c5de2dc1ed0efd8a12f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -571,7 +571,9 @@ void test_memory_tracking(void)
char *__gen_e_acsl_strdup(char const *s)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char const *__gen_e_acsl_at;
char *__retres;
+ __gen_e_acsl_at = s;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__retres = strdup(s);
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index fbde72d4e6bb3694690b2025904cbcf9a5e49a5f..72856675c7256d5ff38179c189fcb2ddcbc1675e 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -132,7 +132,9 @@ char *__gen_e_acsl_strdup(char const *s);
char *__gen_e_acsl_strdup(char const *s)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
+ char const *__gen_e_acsl_at;
char *__retres;
+ __gen_e_acsl_at = s;
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__retres = strdup(s);
{
diff --git a/src/plugins/e-acsl/tests/examples/functions_contiki.c b/src/plugins/e-acsl/tests/examples/functions_contiki.c
index 2ff9daebd5d78c03b9fa541bf0fc71461d27285b..45ff25a313aaf719bd2f8d529571f18707ada62e 100644
--- a/src/plugins/e-acsl/tests/examples/functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/functions_contiki.c
@@ -1,4 +1,5 @@
/* run.config
+ STDOPT: +"-eva-unroll-recursive-calls 5"
COMMENT: functions used in Contiki
*/
diff --git a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
index 7becfbbc7834eb8af9c7dc3946ae0b88d8d1a0b0..df1002f83e4a186ee2c81c4bec178b2b1663353b 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
+++ b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
@@ -1,8 +1,8 @@
[e-acsl] beginning translation.
-[e-acsl] functions_contiki.c:27: Warning:
+[e-acsl] functions_contiki.c:28: Warning:
no assigns clause generated for function length because pointers as arguments is not yet supported
-[e-acsl] functions_contiki.c:27: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
+[e-acsl] functions_contiki.c:28: Warning:
+ no assigns clause generated for function length_aux because pointers as arguments is not yet supported
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions_contiki.c:27: Warning: assertion got status unknown.
+[eva:alarm] functions_contiki.c:18: Warning:
+ accessing uninitialized left-value. assert \initialized(&l->next);
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
index 0c529b0a24a4ede16794536a1fce067e84579189..e7954636ad487616bd571772f858217ff2a5769e 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
@@ -20,9 +20,13 @@ logic integer length_aux{L}(struct list *l, integer n) =
(n < 2147483647? length_aux(l->next, n + 1): -1)),
L);
*/
+long __gen_e_acsl_length_aux_here(struct list *l, unsigned int n);
+
/*@ logic integer length{L}(struct list *l) = \at(length_aux(l, 0),L);
*/
+long __gen_e_acsl_length_here(struct list *l);
+
int main(void)
{
int __retres;
@@ -40,6 +44,24 @@ int main(void)
struct list *l = & node1;
__e_acsl_store_block((void *)(& l),8UL);
__e_acsl_full_init((void *)(& l));
+ {
+ long __gen_e_acsl_length_here_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_length_here_2 = __gen_e_acsl_length_here(l);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"l",(void *)l);
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,
+ "__gen_e_acsl_length_here(l)",0,
+ __gen_e_acsl_length_here_2);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "length(l) == 3";
+ __gen_e_acsl_assert_data.file = "functions_contiki.c";
+ __gen_e_acsl_assert_data.fct = "main";
+ __gen_e_acsl_assert_data.line = 28;
+ __e_acsl_assert(__gen_e_acsl_length_here_2 == 3L,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ }
/*@ assert length(l) == 3; */ ;
__retres = 0;
__e_acsl_delete_block((void *)(& l));
@@ -50,4 +72,35 @@ int main(void)
return __retres;
}
+long __gen_e_acsl_length_here(struct list *l)
+{
+ long __gen_e_acsl_length_aux_here_4;
+ __gen_e_acsl_length_aux_here_4 = __gen_e_acsl_length_aux_here(l,0U);
+ return __gen_e_acsl_length_aux_here_4;
+}
+
+long __gen_e_acsl_length_aux_here(struct list *l, unsigned int n)
+{
+ long __gen_e_acsl_if_3;
+ if (n < 0U) __gen_e_acsl_if_3 = -1;
+ else {
+ long __gen_e_acsl_if_2;
+ if (l == (struct list *)0) __gen_e_acsl_if_2 = n;
+ else {
+ long __gen_e_acsl_if;
+ if (n < 2147483647U) {
+ long __gen_e_acsl_length_aux_here_3;
+ /*@ assert Eva: initialization: \initialized(&l->next); */
+ __gen_e_acsl_length_aux_here_3 = __gen_e_acsl_length_aux_here
+ (l->next,n + 1U);
+ __gen_e_acsl_if = __gen_e_acsl_length_aux_here_3;
+ }
+ else __gen_e_acsl_if = -1;
+ __gen_e_acsl_if_2 = __gen_e_acsl_if;
+ }
+ __gen_e_acsl_if_3 = __gen_e_acsl_if_2;
+ }
+ return __gen_e_acsl_if_3;
+}
+
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 0fd82086aff53183bb5c5a2f320a2fb4a147469d..498e8881d33844d2151eea6f3457761ecf70eb49 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -736,11 +736,13 @@ void test_specifier_application(char const *allowed, char const *fmt,
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
unsigned long __gen_e_acsl_strcpy_src_size;
+ char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
+ __gen_e_acsl_at_2 = src;
__gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
@@ -945,8 +947,10 @@ char *__gen_e_acsl_strchr(char const *s, int c)
*/
size_t __gen_e_acsl_strlen(char const *s)
{
+ char const *__gen_e_acsl_at;
size_t __retres;
__e_acsl_store_block((void *)(& s),8UL);
+ __gen_e_acsl_at = s;
__retres = strlen(s);
__e_acsl_delete_block((void *)(& s));
return __retres;
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
index 32abf0b9b66fd9826f2f2341ac33d477707ef7e4..483dbf2f421fe71d14ed5a5f7d81ad1ce620b7d0 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -9,6 +9,12 @@
#include "time.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+int ( __gen_e_acsl_empty_block_here)(void *s);
+
+int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n);
+
+int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
@@ -398,10 +404,35 @@ int main(void)
*/
void *__gen_e_acsl_memset(void *s, int c, size_t n)
{
+ size_t __gen_e_acsl_at_3;
+ int __gen_e_acsl_at_2;
void *__gen_e_acsl_at;
void *__retres;
- __e_acsl_store_block((void *)(& s),8UL);
- __gen_e_acsl_at = s;
+ {
+ int __gen_e_acsl_valid_or_empty_here_2;
+ __e_acsl_store_block((void *)(& s),8UL);
+ __gen_e_acsl_at = s;
+ __gen_e_acsl_at_2 = c;
+ __gen_e_acsl_at_3 = n;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_valid_or_empty_here_2 = __gen_e_acsl_valid_or_empty_here
+ (s,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"s",s);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "valid_s: __gen_e_acsl_valid_or_empty_here(s, n)",
+ 0,__gen_e_acsl_valid_or_empty_here_2);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "valid_or_empty(s, n)";
+ __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data.fct = "memset";
+ __gen_e_acsl_assert_data.line = 148;
+ __gen_e_acsl_assert_data.name = "valid_s";
+ __e_acsl_assert(__gen_e_acsl_valid_or_empty_here_2,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ }
__retres = memset(s,c,n);
__e_acsl_initialize(s,n);
{
@@ -441,27 +472,69 @@ void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n)
{
void *__gen_e_acsl_at;
void *__retres;
- __e_acsl_store_block((void *)(& src),8UL);
- __e_acsl_store_block((void *)(& dest),8UL);
- __gen_e_acsl_at = dest;
+ {
+ int __gen_e_acsl_valid_or_empty_here_3;
+ int __gen_e_acsl_valid_read_or_empty_here_2;
+ __e_acsl_store_block((void *)(& src),8UL);
+ __e_acsl_store_block((void *)(& dest),8UL);
+ __gen_e_acsl_at = dest;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_valid_or_empty_here_3 = __gen_e_acsl_valid_or_empty_here
+ (dest,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
+ 0,__gen_e_acsl_valid_or_empty_here_3);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
+ __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data.fct = "memmove";
+ __gen_e_acsl_assert_data.line = 137;
+ __gen_e_acsl_assert_data.name = "valid_dest";
+ __e_acsl_assert(__gen_e_acsl_valid_or_empty_here_3,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __gen_e_acsl_valid_read_or_empty_here_2 = __gen_e_acsl_valid_read_or_empty_here
+ ((void *)src,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
+ (void *)src);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
+ 0,__gen_e_acsl_valid_read_or_empty_here_2);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Precondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
+ __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_2.fct = "memmove";
+ __gen_e_acsl_assert_data_2.line = 138;
+ __gen_e_acsl_assert_data_2.name = "valid_src";
+ __e_acsl_assert(__gen_e_acsl_valid_read_or_empty_here_2,
+ & __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ }
__retres = memmove(dest,src,n);
__e_acsl_initialize(dest,n);
{
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"\\result",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"\\result",
__retres);
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"\\old(dest)",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"\\old(dest)",
__gen_e_acsl_at);
- __gen_e_acsl_assert_data_4.blocking = 1;
- __gen_e_acsl_assert_data_4.kind = "Postcondition";
- __gen_e_acsl_assert_data_4.pred_txt = "\\result == \\old(dest)";
- __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/string.h";
- __gen_e_acsl_assert_data_4.fct = "memmove";
- __gen_e_acsl_assert_data_4.line = 142;
- __gen_e_acsl_assert_data_4.name = "result_ptr";
- __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_4);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
+ __gen_e_acsl_assert_data_5.blocking = 1;
+ __gen_e_acsl_assert_data_5.kind = "Postcondition";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\result == \\old(dest)";
+ __gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_5.fct = "memmove";
+ __gen_e_acsl_assert_data_5.line = 142;
+ __gen_e_acsl_assert_data_5.name = "result_ptr";
+ __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
__e_acsl_delete_block((void *)(& src));
__e_acsl_delete_block((void *)(& dest));
return __retres;
@@ -489,6 +562,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
void *__gen_e_acsl_at;
void *__retres;
{
+ int __gen_e_acsl_valid_or_empty_here_4;
+ int __gen_e_acsl_valid_read_or_empty_here_3;
unsigned long __gen_e_acsl_size;
__e_acsl_mpz_t __gen_e_acsl_n;
__e_acsl_mpz_t __gen_e_acsl_;
@@ -513,6 +588,44 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_valid_or_empty_here_4 = __gen_e_acsl_valid_or_empty_here
+ (dest,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
+ 0,__gen_e_acsl_valid_or_empty_here_4);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
+ __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data.fct = "memcpy";
+ __gen_e_acsl_assert_data.line = 112;
+ __gen_e_acsl_assert_data.name = "valid_dest";
+ __e_acsl_assert(__gen_e_acsl_valid_or_empty_here_4,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __gen_e_acsl_valid_read_or_empty_here_3 = __gen_e_acsl_valid_read_or_empty_here
+ ((void *)src,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
+ (void *)src);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
+ 0,__gen_e_acsl_valid_read_or_empty_here_3);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Precondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
+ __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_2.fct = "memcpy";
+ __gen_e_acsl_assert_data_2.line = 113;
+ __gen_e_acsl_assert_data_2.name = "valid_src";
+ __e_acsl_assert(__gen_e_acsl_valid_read_or_empty_here_3,
+ & __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
@@ -666,4 +779,176 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
}
}
+int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n)
+{
+ int __gen_e_acsl_empty_block_here_2;
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_empty_block_here_2 = __gen_e_acsl_empty_block_here(s);
+ if (__gen_e_acsl_empty_block_here_2) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read(s,sizeof(char),s,
+ (void *)(& s));
+ __gen_e_acsl_or = __gen_e_acsl_valid_read;
+ }
+ if (__gen_e_acsl_or) {
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl_if;
+ int __gen_e_acsl_valid;
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
+ if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)s + 1 * 0),
+ __gen_e_acsl_if,s,(void *)(& s));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid;
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ else __gen_e_acsl_and_2 = 0;
+ return __gen_e_acsl_and_2;
+}
+
+int ( __gen_e_acsl_empty_block_here)(void *s)
+{
+ unsigned long __gen_e_acsl_block_length;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_block_length = __e_acsl_block_length(s);
+ if (__gen_e_acsl_block_length == 0UL) {
+ unsigned long __gen_e_acsl_offset;
+ __gen_e_acsl_offset = __e_acsl_offset(s);
+ __gen_e_acsl_and = __gen_e_acsl_offset == 0UL;
+ }
+ else __gen_e_acsl_and = 0;
+ return __gen_e_acsl_and;
+}
+
+int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n)
+{
+ int __gen_e_acsl_empty_block_here_3;
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_empty_block_here_3 = __gen_e_acsl_empty_block_here(s);
+ if (__gen_e_acsl_empty_block_here_3) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read(s,sizeof(char),s,
+ (void *)(& s));
+ __gen_e_acsl_or = __gen_e_acsl_valid_read;
+ }
+ if (__gen_e_acsl_or) {
+ __e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_le;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le_2;
+ unsigned long __gen_e_acsl_size_2;
+ int __gen_e_acsl_valid_read_2;
+ __gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_init_set(__gen_e_acsl_size,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ else __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+ {.values = (void *)0};
+ __gmpz_init_set_ui(__gen_e_acsl__4,18446744073709551615UL);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,
+ "__gen_e_acsl_if",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_assert_data_3.blocking = 1;
+ __gen_e_acsl_assert_data_3.kind = "RTE";
+ __gen_e_acsl_assert_data_3.pred_txt = "(\\let size = sizeof(char) * (((n - 1) - 1) + 1); size <= 0? 0: size) <=\n18446744073709551615";
+ __gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_3.fct = "valid_read_or_empty_here";
+ __gen_e_acsl_assert_data_3.line = 52;
+ __gen_e_acsl_assert_data_3.name = "offset_lesser_or_eq_than_SIZE_MAX";
+ __e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __gen_e_acsl_size_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)s +
+ 1 * 1),
+ __gen_e_acsl_size_2,s,
+ (void *)(& s));
+ __gen_e_acsl_and = __gen_e_acsl_valid_read_2;
+ __gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_if);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ else __gen_e_acsl_and = 0;
+ return __gen_e_acsl_and;
+}
+
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
index 3489f579ec4b0249d9064a074072cae93e37035c..2c95285a9e9a2b94308334229801130e12d514ce 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -182,30 +182,30 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
{
__e_acsl_mpz_t __gen_e_acsl_strcat_src_size_2;
__e_acsl_mpz_t __gen_e_acsl_strcat_dest_size_2;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl__8;
int __gen_e_acsl_le;
- unsigned long __gen_e_acsl_size_2;
+ unsigned long __gen_e_acsl_size_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
__gmpz_init_set_ui(__gen_e_acsl_strcat_src_size_2,
__gen_e_acsl_strcat_src_size);
__gmpz_init_set_ui(__gen_e_acsl_strcat_dest_size_2,
__gen_e_acsl_strcat_dest_size);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_strcat_src_size_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_strcat_dest_size_2));
- __gmpz_init_set_si(__gen_e_acsl_,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_init_set_ui(__gen_e_acsl__8,18446744073709551615UL);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_8,
"__gen_e_acsl_strcat_src_size",0,
__gen_e_acsl_strcat_src_size);
@@ -221,14 +221,14 @@ char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
__gen_e_acsl_assert_data_8.name = "size_lesser_or_eq_than_SIZE_MAX";
__e_acsl_assert(__gen_e_acsl_le <= 0,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
- __gen_e_acsl_size_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __e_acsl_initialize((void *)dest,__gen_e_acsl_size_2);
+ __gen_e_acsl_size_4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __e_acsl_initialize((void *)dest,__gen_e_acsl_size_4);
__gmpz_clear(__gen_e_acsl_strcat_src_size_2);
__gmpz_clear(__gen_e_acsl_strcat_dest_size_2);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl__8);
}
{
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
@@ -386,7 +386,8 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
size_t n)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
- __e_acsl_mpz_t __gen_e_acsl_at_2;
+ __e_acsl_mpz_t __gen_e_acsl_at_3;
+ char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
{
@@ -419,8 +420,9 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
+ __gen_e_acsl_at_2 = src;
__gmpz_init_set_ui(__gen_e_acsl_n,n);
- __gmpz_init_set(__gen_e_acsl_at_2,
+ __gmpz_init_set(__gen_e_acsl_at_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gen_e_acsl_contract = __e_acsl_contract_init(2UL);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
@@ -618,7 +620,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_init_set_si(__gen_e_acsl__8,1L);
__gmpz_init(__gen_e_acsl_sub_3);
__gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__gmpz_init_set_si(__gen_e_acsl__9,0L);
__gmpz_init(__gen_e_acsl_sub_4);
@@ -643,7 +645,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,"sizeof(char)",
0,1);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"\\old(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3));
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
__gen_e_acsl_size_6);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"size",0,
@@ -668,7 +670,7 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
__gmpz_clear(__gen_e_acsl__9);
__gmpz_clear(__gen_e_acsl_sub_4);
__gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_at_2);
+ __gmpz_clear(__gen_e_acsl_at_3);
return __retres;
}
}
@@ -688,11 +690,13 @@ char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
{
unsigned long __gen_e_acsl_strcpy_src_size;
+ char const *__gen_e_acsl_at_2;
char *__gen_e_acsl_at;
char *__retres;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__gen_e_acsl_at = dest;
+ __gen_e_acsl_at_2 = src;
__gen_e_acsl_strcpy_src_size = __e_acsl_builtin_strlen(src);
__retres = strcpy(dest,src);
{
diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
index 3391277a9a4a8c700164541d29032b764d6a0904..d6ab15b134feef6c04847d8603b2d0b999f4f181 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -2,21 +2,14 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:148: Warning:
no assigns clause generated for function valid_or_empty because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/string.h:49: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
+ no assigns clause generated for function empty_block because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/string.h:148: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning:
E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:137: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:138: Warning:
no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported
-[e-acsl] FRAMAC_SHARE/libc/string.h:52: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:137: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -24,12 +17,6 @@
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -38,6 +25,14 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] FRAMAC_SHARE/libc/string.h:148: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:148: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:148: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:152: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -82,6 +77,24 @@
[eva:alarm] mem.c:19: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:112: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:112: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:112: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:52: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:115: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -119,6 +132,22 @@
[eva:alarm] mem.c:25: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:137: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:137: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:137: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:138: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:138: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:138: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:142: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
index 00c9e9bab1d0642c1b664b698c697135bcdc5456..d35a4002aa1ad8679db90991595af70652d7e4b4 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -1,8 +1,11 @@
[e-acsl] beginning translation.
[e-acsl] FRAMAC_SHARE/libc/string.h:497: Warning:
no assigns clause generated for function valid_read_nstring because pointers as arguments is not yet supported
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:280: Warning:
- E-ACSL construct `labeled \valid_read' is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
+ no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:277: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:498: Warning:
no assigns clause generated for function valid_string because pointers as arguments is not yet supported
@@ -60,8 +63,6 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:476: Warning:
- no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:277: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
@@ -93,7 +94,8 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:431: Warning:
- E-ACSL construct `labeled \valid_read' is not yet supported.
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
index 7244509fa59a1d36e166341d9f8c317efc1f5c3e..06a7c0bcdb3ba3d204cd384176359e57c23508e1 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
@@ -392,8 +392,10 @@ int main(int argc, char **argv)
*/
size_t __gen_e_acsl_strlen(char const *s)
{
+ char const *__gen_e_acsl_at;
size_t __retres;
__e_acsl_store_block((void *)(& s),8UL);
+ __gen_e_acsl_at = s;
__retres = strlen(s);
__e_acsl_delete_block((void *)(& s));
return __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index 5284f282963682e4507a2e0de7aa871255547eff..efad32ac68e962ae59e21a54dedcd551f37959b1 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -10,6 +10,12 @@
#include "time.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+int ( __gen_e_acsl_empty_block_here)(void *s);
+
+int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n);
+
+int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n);
+
/*@ requires valid_dest: valid_or_empty(dest, n);
requires valid_src: valid_read_or_empty(src, n);
requires
@@ -733,15 +739,40 @@ int main(void)
*/
void *__gen_e_acsl_memset(void *s, int c, size_t n)
{
+ size_t __gen_e_acsl_at_3;
+ int __gen_e_acsl_at_2;
void *__gen_e_acsl_at;
void *__retres;
- __e_acsl_store_block((void *)(& s),8UL);
- __e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
- __gen_e_acsl_at = s;
- __e_acsl_temporal_reset_parameters();
- __e_acsl_temporal_reset_return();
- __e_acsl_temporal_save_nreferent_parameter((void *)(& s),0U);
- __e_acsl_temporal_memset(s,c,n);
+ {
+ int __gen_e_acsl_valid_or_empty_here_2;
+ __e_acsl_store_block((void *)(& s),8UL);
+ __e_acsl_temporal_pull_parameter((void *)(& s),0U,8UL);
+ __gen_e_acsl_at = s;
+ __gen_e_acsl_at_2 = c;
+ __gen_e_acsl_at_3 = n;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_valid_or_empty_here_2 = __gen_e_acsl_valid_or_empty_here
+ (s,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"s",s);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "valid_s: __gen_e_acsl_valid_or_empty_here(s, n)",
+ 0,__gen_e_acsl_valid_or_empty_here_2);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "valid_or_empty(s, n)";
+ __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data.fct = "memset";
+ __gen_e_acsl_assert_data.line = 148;
+ __gen_e_acsl_assert_data.name = "valid_s";
+ __e_acsl_assert(__gen_e_acsl_valid_or_empty_here_2,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_temporal_reset_parameters();
+ __e_acsl_temporal_reset_return();
+ __e_acsl_temporal_save_nreferent_parameter((void *)(& s),0U);
+ __e_acsl_temporal_memset(s,c,n);
+ }
__retres = memset(s,c,n);
__e_acsl_initialize(s,n);
{
@@ -786,188 +817,400 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
void *__gen_e_acsl_at;
void *__retres;
{
- unsigned long __gen_e_acsl_size;
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl_sub_2;
- __e_acsl_mpz_t __gen_e_acsl_add;
- unsigned long __gen_e_acsl__3;
- unsigned long __gen_e_acsl_if;
- int __gen_e_acsl_valid_read;
- unsigned long __gen_e_acsl_size_2;
- unsigned long __gen_e_acsl__4;
- unsigned long __gen_e_acsl_if_2;
- int __gen_e_acsl_valid_read_2;
+ int __gen_e_acsl_valid_or_empty_here_3;
+ int __gen_e_acsl_valid_read_or_empty_here_2;
unsigned long __gen_e_acsl_size_3;
- unsigned long __gen_e_acsl__5;
- unsigned long __gen_e_acsl_if_3;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_sub_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ unsigned long __gen_e_acsl__7;
+ unsigned long __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_read_3;
unsigned long __gen_e_acsl_size_4;
- unsigned long __gen_e_acsl__6;
+ unsigned long __gen_e_acsl__8;
+ unsigned long __gen_e_acsl_if_3;
+ int __gen_e_acsl_valid_read_4;
+ unsigned long __gen_e_acsl_size_5;
+ unsigned long __gen_e_acsl__9;
unsigned long __gen_e_acsl_if_4;
+ unsigned long __gen_e_acsl_size_6;
+ unsigned long __gen_e_acsl__10;
+ unsigned long __gen_e_acsl_if_5;
int __gen_e_acsl_separated;
__e_acsl_store_block((void *)(& src),8UL);
__e_acsl_store_block((void *)(& dest),8UL);
__e_acsl_temporal_pull_parameter((void *)(& dest),0U,8UL);
__e_acsl_temporal_pull_parameter((void *)(& src),1U,8UL);
__gen_e_acsl_at = dest;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_valid_or_empty_here_3 = __gen_e_acsl_valid_or_empty_here
+ (dest,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
+ 0,__gen_e_acsl_valid_or_empty_here_3);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
+ __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data.fct = "memcpy";
+ __gen_e_acsl_assert_data.line = 112;
+ __gen_e_acsl_assert_data.name = "valid_dest";
+ __e_acsl_assert(__gen_e_acsl_valid_or_empty_here_3,
+ & __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
+ __gen_e_acsl_valid_read_or_empty_here_2 = __gen_e_acsl_valid_read_or_empty_here
+ ((void *)src,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,"n",0,n);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
+ (void *)src);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
+ 0,__gen_e_acsl_valid_read_or_empty_here_2);
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Precondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
+ __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_2.fct = "memcpy";
+ __gen_e_acsl_assert_data_2.line = 113;
+ __gen_e_acsl_assert_data_2.name = "valid_src";
+ __e_acsl_assert(__gen_e_acsl_valid_read_or_empty_here_2,
+ & __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __gmpz_init_set_ui(__gen_e_acsl_n,n);
- __gmpz_init_set_si(__gen_e_acsl_,1L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init(__gen_e_acsl_sub_2);
- __gmpz_sub(__gen_e_acsl_sub_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
- if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
- else __gen_e_acsl_if = __gen_e_acsl_size;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)dest +
- 1 * 0),
- __gen_e_acsl_if,dest,
- (void *)(& dest));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"dest",dest);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
- 0,1);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
- 0,1);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"n",0,n);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
- __gen_e_acsl_size);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
- __gen_e_acsl_size);
- __gen_e_acsl_assert_data_4.blocking = 1;
- __gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read((char *)dest + (0 .. n - 1))";
- __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/string.h";
- __gen_e_acsl_assert_data_4.fct = "memcpy";
- __gen_e_acsl_assert_data_4.line = 115;
- __gen_e_acsl_assert_data_4.name = "separated_guard";
- __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_4);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
- if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
- else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)src +
+ __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
+ __gmpz_init(__gen_e_acsl_sub_4);
+ __gmpz_sub(__gen_e_acsl_sub_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gen_e_acsl__7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__7;
+ if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_2 = 0UL;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_3;
+ __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)dest +
1 * 0),
- __gen_e_acsl_if_2,
- (void *)src,
- (void *)(& src));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"src",
- (void *)src);
+ __gen_e_acsl_if_2,dest,
+ (void *)(& dest));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_5,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"sizeof(char)",
0,1);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"sizeof(char)",
0,1);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"n",0,n);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"size",0,
- __gen_e_acsl_size_2);
+ __gen_e_acsl_size_3);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_5,"size",0,
- __gen_e_acsl_size_2);
+ __gen_e_acsl_size_3);
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "RTE";
- __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read((char *)src + (0 .. n - 1))";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read((char *)dest + (0 .. n - 1))";
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/string.h";
__gen_e_acsl_assert_data_5.fct = "memcpy";
__gen_e_acsl_assert_data_5.line = 115;
__gen_e_acsl_assert_data_5.name = "separated_guard";
- __e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert(__gen_e_acsl_valid_read_3,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
- if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
- else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
- __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
- if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
- else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
+ {.values = (void *)0};
+ __gen_e_acsl__8 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__8;
+ if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_3 = 0UL;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_4;
+ __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)((char *)src +
+ 1 * 0),
+ __gen_e_acsl_if_3,
+ (void *)src,
+ (void *)(& src));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"src",
+ (void *)src);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
+ 0,1);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"sizeof(char)",
+ 0,1);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,"n",0,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,"size",0,
+ __gen_e_acsl_size_4);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_6,"size",0,
+ __gen_e_acsl_size_4);
+ __gen_e_acsl_assert_data_6.blocking = 1;
+ __gen_e_acsl_assert_data_6.kind = "RTE";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read((char *)src + (0 .. n - 1))";
+ __gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_6.fct = "memcpy";
+ __gen_e_acsl_assert_data_6.line = 115;
+ __gen_e_acsl_assert_data_6.name = "separated_guard";
+ __e_acsl_assert(__gen_e_acsl_valid_read_4,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
+ __gen_e_acsl__9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_size_5 = 1UL * __gen_e_acsl__9;
+ if (__gen_e_acsl_size_5 <= 0UL) __gen_e_acsl_if_4 = 0UL;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_5;
+ __gen_e_acsl__10 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gen_e_acsl_size_6 = 1UL * __gen_e_acsl__10;
+ if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_5 = 0UL;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_6;
__gen_e_acsl_separated = __e_acsl_separated(2UL,(char *)dest + 1 * 0,
- __gen_e_acsl_if_3,
+ __gen_e_acsl_if_4,
(char *)src + 1 * 0,
- __gen_e_acsl_if_4);
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"dest",dest);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(char)",
+ __gen_e_acsl_if_5);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"dest",dest);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
0,1);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(char)",
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
0,1);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"n",0,n);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_3);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_3);
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"src",
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"n",0,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
+ __gen_e_acsl_size_5);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
+ __gen_e_acsl_size_5);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"src",
(void *)src);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(char)",
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
0,1);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"sizeof(char)",
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"sizeof(char)",
0,1);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"n",0,n);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_4);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,"size",0,
- __gen_e_acsl_size_4);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"n",0,n);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
+ __gen_e_acsl_size_6);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_4,"size",0,
+ __gen_e_acsl_size_6);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
"separation:\n \\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))",
0,__gen_e_acsl_separated);
- __gen_e_acsl_assert_data_3.blocking = 1;
- __gen_e_acsl_assert_data_3.kind = "Precondition";
- __gen_e_acsl_assert_data_3.pred_txt = "\\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))";
- __gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/string.h";
- __gen_e_acsl_assert_data_3.fct = "memcpy";
- __gen_e_acsl_assert_data_3.line = 115;
- __gen_e_acsl_assert_data_3.name = "separation";
- __e_acsl_assert(__gen_e_acsl_separated,& __gen_e_acsl_assert_data_3);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "Precondition";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))";
+ __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_4.fct = "memcpy";
+ __gen_e_acsl_assert_data_4.line = 115;
+ __gen_e_acsl_assert_data_4.name = "separation";
+ __e_acsl_assert(__gen_e_acsl_separated,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& dest),0U);
__e_acsl_temporal_save_nreferent_parameter((void *)(& src),1U);
__e_acsl_temporal_memcpy(dest,(void *)src,n);
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl_sub_2);
- __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_sub_4);
+ __gmpz_clear(__gen_e_acsl_add_2);
}
__retres = memcpy(dest,src,n);
__e_acsl_initialize(dest,n);
{
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\result",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,"\\result",
__retres);
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_7,"\\old(dest)",
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_8,"\\old(dest)",
__gen_e_acsl_at);
- __gen_e_acsl_assert_data_7.blocking = 1;
- __gen_e_acsl_assert_data_7.kind = "Postcondition";
- __gen_e_acsl_assert_data_7.pred_txt = "\\result == \\old(dest)";
- __gen_e_acsl_assert_data_7.file = "FRAMAC_SHARE/libc/string.h";
- __gen_e_acsl_assert_data_7.fct = "memcpy";
- __gen_e_acsl_assert_data_7.line = 119;
- __gen_e_acsl_assert_data_7.name = "result_ptr";
- __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_7);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
+ __gen_e_acsl_assert_data_8.blocking = 1;
+ __gen_e_acsl_assert_data_8.kind = "Postcondition";
+ __gen_e_acsl_assert_data_8.pred_txt = "\\result == \\old(dest)";
+ __gen_e_acsl_assert_data_8.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_8.fct = "memcpy";
+ __gen_e_acsl_assert_data_8.line = 119;
+ __gen_e_acsl_assert_data_8.name = "result_ptr";
+ __e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_8);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
__e_acsl_delete_block((void *)(& src));
__e_acsl_delete_block((void *)(& dest));
return __retres;
}
}
+int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n)
+{
+ int __gen_e_acsl_empty_block_here_2;
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_and_2;
+ __gen_e_acsl_empty_block_here_2 = __gen_e_acsl_empty_block_here(s);
+ if (__gen_e_acsl_empty_block_here_2) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read(s,sizeof(char),s,
+ (void *)(& s));
+ __gen_e_acsl_or = __gen_e_acsl_valid_read;
+ }
+ if (__gen_e_acsl_or) {
+ unsigned long __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ unsigned long __gen_e_acsl__3;
+ unsigned long __gen_e_acsl_if;
+ int __gen_e_acsl_valid;
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
+ if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)((char *)s + 1 * 0),
+ __gen_e_acsl_if,s,(void *)(& s));
+ __gen_e_acsl_and_2 = __gen_e_acsl_valid;
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ else __gen_e_acsl_and_2 = 0;
+ return __gen_e_acsl_and_2;
+}
+
+int ( __gen_e_acsl_empty_block_here)(void *s)
+{
+ unsigned long __gen_e_acsl_block_length;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_block_length = __e_acsl_block_length(s);
+ if (__gen_e_acsl_block_length == 0UL) {
+ unsigned long __gen_e_acsl_offset;
+ __gen_e_acsl_offset = __e_acsl_offset(s);
+ __gen_e_acsl_and = __gen_e_acsl_offset == 0UL;
+ }
+ else __gen_e_acsl_and = 0;
+ return __gen_e_acsl_and;
+}
+
+int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n)
+{
+ int __gen_e_acsl_empty_block_here_3;
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_empty_block_here_3 = __gen_e_acsl_empty_block_here(s);
+ if (__gen_e_acsl_empty_block_here_3) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_valid_read;
+ __gen_e_acsl_valid_read = __e_acsl_valid_read(s,sizeof(char),s,
+ (void *)(& s));
+ __gen_e_acsl_or = __gen_e_acsl_valid_read;
+ }
+ if (__gen_e_acsl_or) {
+ __e_acsl_mpz_t __gen_e_acsl_size;
+ __e_acsl_mpz_t __gen_e_acsl_sizeof;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_le;
+ __e_acsl_mpz_t __gen_e_acsl_if;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_le_2;
+ unsigned long __gen_e_acsl_size_2;
+ int __gen_e_acsl_valid_read_2;
+ __gmpz_init_set_si(__gen_e_acsl_sizeof,1L);
+ __gmpz_init_set_ui(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_sub_2);
+ __gmpz_sub(__gen_e_acsl_sub_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sizeof),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
+ __gmpz_init_set(__gen_e_acsl_size,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_size),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_le <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ else __gmpz_init_set(__gen_e_acsl_if,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_size));
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
+ {.values = (void *)0};
+ __gmpz_init_set_ui(__gen_e_acsl__4,18446744073709551615UL);
+ __gen_e_acsl_le_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_if),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,
+ "__gen_e_acsl_if",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_assert_data_3.blocking = 1;
+ __gen_e_acsl_assert_data_3.kind = "RTE";
+ __gen_e_acsl_assert_data_3.pred_txt = "(\\let size = sizeof(char) * (((n - 1) - 1) + 1); size <= 0? 0: size) <=\n18446744073709551615";
+ __gen_e_acsl_assert_data_3.file = "FRAMAC_SHARE/libc/string.h";
+ __gen_e_acsl_assert_data_3.fct = "valid_read_or_empty_here";
+ __gen_e_acsl_assert_data_3.line = 52;
+ __gen_e_acsl_assert_data_3.name = "offset_lesser_or_eq_than_SIZE_MAX";
+ __e_acsl_assert(__gen_e_acsl_le_2 <= 0,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
+ __gen_e_acsl_size_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+ __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)s +
+ 1 * 1),
+ __gen_e_acsl_size_2,s,
+ (void *)(& s));
+ __gen_e_acsl_and = __gen_e_acsl_valid_read_2;
+ __gmpz_clear(__gen_e_acsl_size);
+ __gmpz_clear(__gen_e_acsl_sizeof);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl__2);
+ __gmpz_clear(__gen_e_acsl_if);
+ __gmpz_clear(__gen_e_acsl__4);
+ }
+ else __gen_e_acsl_and = 0;
+ return __gen_e_acsl_and;
+}
+
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index d421a5613b26293031f99c2f68eb452ebc82d9f2..c9851298903b4367411d8b16bb63c8b09e3a5e65 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -2,21 +2,14 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:148: Warning:
no assigns clause generated for function valid_or_empty because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/string.h:49: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
+ no assigns clause generated for function empty_block because pointers as arguments is not yet supported
[e-acsl] FRAMAC_SHARE/libc/string.h:148: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning:
E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning:
no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported
-[e-acsl] FRAMAC_SHARE/libc/string.h:52: Warning:
- E-ACSL construct `predicates with labels' is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -49,6 +42,24 @@
[eva:alarm] t_memcpy.c:21: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:112: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:112: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:112: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:52: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:113: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:115: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
@@ -95,6 +106,14 @@
[eva:alarm] t_memcpy.c:26: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:148: Warning:
+ function __e_acsl_assert_register_ptr: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:148: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:148: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:152: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
\valid(data->values) got status unknown.