diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index f98b3485092d29c6659b6a6a989cfe64ffb99acc..52a296b94c20e44c20b56ae1cf8e293a4ee427a3 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -90,7 +90,8 @@ let preprocess_pred ~loc p =
~loc
(llabel, Logic_utils.mk_logic_AddrOf ~loc tlv lty)
in
- (* need to store a copy, to avoid p to appear in its own preprocessed form (otherwise it loops) *)
+ (* need to store a copy, to avoid p to appear in its own preprocessed
+ form (otherwise it loops) *)
let p_copy =
match p.pred_content with
| Pvalid_read _ -> Logic_const.pvalid_read ~loc (llabel, t)
@@ -100,17 +101,6 @@ let preprocess_pred ~loc p =
Some (Lscope.PoT_pred (Logic_const.pand ~loc (init, p_copy)))
| _ -> None
end
- | Papp(li, labels, args) ->
- (* Simply use the implementation of Tapp(li, labels, args). To achieve this,
- we create a clone of [li] for which the type is transformed from [None]
- (type of predicates) to [Some boolean] (typed as a term). *)
- let prj = Project.current () in
- let o = object inherit Visitor.frama_c_copy prj end in
- let li = Visitor.visitFramacLogicInfo o li in
- let lty = Logic_const.boolean_type in
- li.l_type <- Some lty;
- let tapp = Logic_const.term ~loc (Tapp(li, labels, args)) lty in
- Some (Lscope.PoT_term tapp)
| _ -> None
let preprocess_term ~loc t =
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 3910a72214b8b54afff5763973715792e3d3e2c9..0234137c76103a4d35bc3c5a38a8d975d1b90162 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -879,7 +879,7 @@ and type_predicate ?(lenv=[]) p =
begin
let guards, goal =
Error.retrieve_preprocessing
- "quantified predicate"
+ "preprocessing of quantified predicate"
Bound_variables.get_preprocessed_quantifier
p
in
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 f81c8701aad1a93b61e4ff08f0ce7e38d9b4d10e..fe81e164e286babf865fd97aca574a98d6f576e2 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -332,8 +332,12 @@ let add_generated_functions globals =
(* Generate (and memoize) the function body and create the call to the
generated function. *)
-let function_to_exp ~loc fname env kf t li params_ty args =
- let ret_ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+let function_to_exp ~loc ?tapp fname env kf li params_ty args =
+ let ret_ty =
+ match tapp with
+ | Some tapp -> Typing.get_typ ~lenv:(Env.Local_vars.get env) tapp
+ | None -> (Cil_types.TInt (IInt, []))
+ in
let gen tbl =
let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
Typing.Function_params_ty.Hashtbl.add tbl params_ty kf;
@@ -387,11 +391,11 @@ let function_to_exp ~loc fname env kf t li params_ty args =
~name:li.l_var_info.lv_name
env
kf
- (Some t)
+ tapp
ret_ty
(fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
-let raise_errors l = function
+let raise_errors = function
| LBnone ->
Error.not_yet
"logic functions or predicates with no definition nor reads clause"
@@ -399,59 +403,51 @@ let raise_errors l = function
Error.not_yet "logic functions or predicates performing read accesses"
| LBinductive _ -> Error.not_yet "inductive logic functions"
| LBterm _
- | LBpred _ ->
- match l with
- | [] -> ()
- | _::_ -> Error.not_yet "logic functions or predicates with labels"
+ | LBpred _ -> ()
-let tapp_to_exp ~adata kf env ?eargs tapp =
- match tapp.term_node with
- | Tapp(li, l, targs) ->
- let loc = tapp.term_loc in
+let app_to_exp ~adata ~loc ?tapp kf env ?eargs
+ ((li, targs) : logic_info * term list) =
let fname = li.l_var_info.lv_name in
(* build the varinfo (as an expression) which stores the result of the
function call. *)
let _, e, adata, env =
if Builtins.mem li.l_var_info.lv_name then
- match l with
- | _::_ -> Error.not_yet "E-ACSL built-in functions with labels"
- | [] ->
- (* E-ACSL built-in function call *)
- let args, adata, env =
- match eargs with
- | None ->
- List.fold_right
- (fun targ (l, adata, env) ->
- let e, adata, env = !term_to_exp_ref ~adata kf env targ in
- e :: l, adata, env)
- targs
- ([], adata, env)
- | Some eargs ->
- if List.compare_lengths targs eargs != 0 then
- Options.fatal
- "[Tapp] unexpected number of arguments when calling %s"
- fname;
- eargs, adata, env
- in
- let vi, e, env =
- Env.new_var
- ~loc
- ~name:(fname ^ "_app")
- env
- kf
- (Some tapp)
- (Misc.cty (Option.get li.l_type))
- (fun vi _ ->
- [ Smart_stmt.rtl_call ~loc
- ~result:(Cil.var vi)
- ~prefix:""
- fname
- args ])
- in
- vi, e, adata, env
+ (* E-ACSL built-in function call *)
+ let args, adata, env =
+ match eargs with
+ | None ->
+ List.fold_right
+ (fun targ (l, adata, env) ->
+ let e, adata, env = !term_to_exp_ref ~adata kf env targ in
+ e :: l, adata, env)
+ targs
+ ([], adata, env)
+ | Some eargs ->
+ if List.compare_lengths targs eargs != 0 then
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname;
+ eargs, adata, env
+ in
+ let vi, e, env =
+ Env.new_var
+ ~loc
+ ~name:(fname ^ "_app")
+ env
+ kf
+ tapp
+ (Misc.cty (Option.get li.l_type))
+ (fun vi _ ->
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ fname
+ args ])
+ in
+ vi, e, adata, env
else
begin
- raise_errors l li.l_body;
+ raise_errors li.l_body;
(* build the arguments and compute the integer_ty of the parameters *)
let params_ty, args, adata, env =
let eargs, adata, env =
@@ -504,16 +500,123 @@ let tapp_to_exp ~adata kf env ?eargs tapp =
Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
in
let vi, e, env =
- function_to_exp ~loc gen_fname env kf tapp li params_ty args
+ function_to_exp ~loc ?tapp gen_fname env kf li params_ty args
in
vi, e, adata, env
end
in
e, adata, env
- | _ ->
- Options.fatal
- "tapp_to_exp called with '%a' instead of Tapp term"
- Printer.pp_term tapp
+
+(* let tapp_to_exp ~adata kf env ?eargs tapp = *)
+(* match tapp.term_node with *)
+(* | Tapp(li, l, targs) -> *)
+(* let loc = tapp.term_loc in *)
+(* let fname = li.l_var_info.lv_name in *)
+(* (\* build the varinfo (as an expression) which stores the result of the *)
+(* function call. *\) *)
+(* let _, e, adata, env = *)
+(* if Builtins.mem li.l_var_info.lv_name then *)
+(* match l with *)
+(* | _::_ -> Error.not_yet "E-ACSL built-in functions with labels" *)
+(* | [] -> *)
+(* (\* E-ACSL built-in function call *\) *)
+(* let args, adata, env = *)
+(* match eargs with *)
+(* | None -> *)
+(* List.fold_right *)
+(* (fun targ (l, adata, env) -> *)
+(* let e, adata, env = !term_to_exp_ref ~adata kf env targ in *)
+(* e :: l, adata, env) *)
+(* targs *)
+(* ([], adata, env) *)
+(* | Some eargs -> *)
+(* if List.compare_lengths targs eargs != 0 then *)
+(* Options.fatal *)
+(* "[Tapp] unexpected number of arguments when calling %s" *)
+(* fname; *)
+(* eargs, adata, env *)
+(* in *)
+(* let vi, e, env = *)
+(* Env.new_var *)
+(* ~loc *)
+(* ~name:(fname ^ "_app") *)
+(* env *)
+(* kf *)
+(* (Some tapp) *)
+(* (Misc.cty (Option.get li.l_type)) *)
+(* (fun vi _ -> *)
+(* [ Smart_stmt.rtl_call ~loc *)
+(* ~result:(Cil.var vi) *)
+(* ~prefix:"" *)
+(* fname *)
+(* args ]) *)
+(* in *)
+(* vi, e, adata, env *)
+(* else *)
+(* begin *)
+(* raise_errors l li.l_body; *)
+(* (\* build the arguments and compute the integer_ty of the parameters *\) *)
+(* let params_ty, args, adata, env = *)
+(* let eargs, adata, env = *)
+(* match eargs with *)
+(* | None -> *)
+(* List.fold_right *)
+(* (fun targ (eargs, adata, env) -> *)
+(* let e, adata, env = !term_to_exp_ref ~adata kf env targ in *)
+(* e :: eargs, adata, env) *)
+(* targs *)
+(* ([], adata, env) *)
+(* | Some eargs -> *)
+(* if List.compare_lengths targs eargs != 0 then *)
+(* Options.fatal *)
+(* "[Tapp] unexpected number of arguments when calling %s" *)
+(* fname; *)
+(* eargs, adata, env *)
+(* in *)
+(* try *)
+(* List.fold_right2 *)
+(* (fun targ earg (params_ty, args, adata, env) -> *)
+(* let param_ty = *)
+(* Typing.get_number_ty *)
+(* ~lenv:(Env.Local_vars.get env) *)
+(* targ *)
+(* in *)
+(* let e, env = *)
+(* try *)
+(* let ty = Typing.typ_of_number_ty param_ty in *)
+(* Typed_number.add_cast *)
+(* ~loc *)
+(* env *)
+(* kf *)
+(* (Some ty) *)
+(* Typed_number.C_number *)
+(* (Some targ) *)
+(* earg *)
+(* with Typing.Not_a_number -> *)
+(* earg, env *)
+(* in *)
+(* param_ty :: params_ty, e :: args, adata, env) *)
+(* targs eargs *)
+(* ([], [], adata ,env) *)
+(* with Invalid_argument _ -> *)
+(* Options.fatal *)
+(* "[Tapp] unexpected number of arguments when calling %s" *)
+(* fname *)
+(* in *)
+(* let gen_fname = *)
+(* Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname) *)
+(* in *)
+(* let vi, e, env = *)
+(* function_to_exp ~loc ~tapp gen_fname env kf li params_ty args *)
+(* in *)
+(* vi, e, adata, env *)
+(* end *)
+(* in *)
+(* e, adata, env *)
+(* | _ -> *)
+(* Options.fatal *)
+(* "tapp_to_exp called with '%a' instead of Tapp term" *)
+(* Printer.pp_term tapp *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.mli b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
index e5f646c360bb21f73d839f74ec629f8d1388744e..39f5e71b5740afca5268e636ec0419f210608b25 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.mli
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.mli
@@ -36,12 +36,14 @@ open Cil_types
val reset: unit -> unit
-val tapp_to_exp:
+val app_to_exp:
adata:Assert.t ->
+ loc:location ->
+ ?tapp:term ->
kernel_function ->
Env.t ->
?eargs:exp list ->
- term ->
+ logic_info * term list ->
exp * Assert.t * Env.t
(** Translate a Tapp term to an expression. If the optional argument [eargs] is
provided, then these expressions are used as arguments of the fonction. *)
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index ff6d18098da8cfc67cd21c7a7b23dbb286de01e4..28f9cc13914766a32aa85b68c6a78811ce9a9f49 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -109,12 +109,14 @@ let handle_annotations env kf stmt =
Typing.type_term ~use_gmp_opt:true tapp;
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
let e_tapp, _, env =
- Logic_functions.tapp_to_exp
+ Logic_functions.app_to_exp
~adata:Assert.no_data
+ ~loc
+ ~tapp
kf
env
~eargs:[e_old; e]
- tapp
+ (measure, [t_old; t])
in
let msg =
Format.asprintf
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index d569c5df9ee9c84e8e3a789109d9c7231926d57e..144703164492ce26c48c770b51f8150ffbcd3981 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -68,7 +68,7 @@ let convert kf env loc ~is_forall quantif =
(* guarded quantification over integers (or a subtype of integer) *)
let bound_vars, goal =
Error.retrieve_preprocessing
- "quantified predicate"
+ "preprocessing of quantified predicate"
Bound_variables.get_preprocessed_quantifier
quantif
in
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index d11f6481ab8bec7bd4cb0ccab07050fbdff2d617..2f359ead172364cac0338a8343d3666b8f251c7b 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -767,12 +767,13 @@ and context_insensitive_term_to_exp ~adata kf env t =
| Tapp(li, _, _)
when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
assert false
- | Tapp(_, [], _) ->
- let e, adata, env = Logic_functions.tapp_to_exp ~adata kf env t in
+ | Tapp(li, [], args) ->
+ let e, adata, env =
+ Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env (li, args) in
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, Typed_number.C_number, "app"
| Tapp(_, _ :: _, _) ->
- Env.not_yet env "logic functions or predicates with labels"
+ Env.not_yet env "logic functions with labels"
| Tlambda(_, lt) ->
let exp, adata, env = term_to_exp ~adata kf env lt in
exp, adata, env, Typed_number.C_number, ""
@@ -1039,7 +1040,12 @@ and predicate_content_to_exp ~adata ?name kf env p =
match p.pred_content with
| Pfalse -> Cil.zero ~loc, adata, env
| Ptrue -> Cil.one ~loc, adata, env
- | Papp _ -> Options.fatal "Reached applied predicate: %a" Printer.pp_predicate p;
+ | Papp (_, _::_,_) -> Env.not_yet env "predicates with labels"
+ | Papp (li, [], args) ->
+ let e, adata, env =
+ Logic_functions.app_to_exp ~adata ~loc kf env (li, args) in
+ let adata, env = Assert.register_pred ~loc kf env p e adata in
+ e, adata, env
| Pdangling _ -> Env.not_yet env "\\dangling"
| Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
| Pvalid_function _ -> Env.not_yet env "\\valid_function"
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 6aebd3583d94ca969621b0130e324f1f8aec2d6b..2538bb41a7aef9b61b6c37e3e05f4eaefa7d9f45 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,7 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
index 785bb4d1a1e21157ee06063aaaac742b0d19d976..878f304364d4a5a2a67a7f26c024cdfb692e14a1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
@@ -6,12 +6,10 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index 3367e2acfe62389f490071eedf4a433b181cc886..455bfd43413ff0193be76f0b37f94cdfa2afc6f3 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -19,16 +19,13 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
Some assumes clauses could not be translated.
@@ -39,8 +36,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 3e8329fdab9843ee60527c5553ba99d3fd33d7d0..247fe7037ee8d8b4c19af56b986307549d5473f8 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -14,16 +14,13 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
Some assumes clauses could not be translated.
@@ -34,8 +31,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 63fa3d663a20e3ea37390b3ff59807ccabe20f05..96325fbbbf3c10a63062b0076067e5fd1e6d8547 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -17,16 +17,13 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
Some assumes clauses could not be translated.
@@ -37,8 +34,7 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
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 ae9a44dd2551efdcf148715845d54bd6aaed774a..2327ee08af4c360fa7edbcefdb921c527b678be7 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,7 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] tests/examples/functions_contiki.c:27: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/examples/functions_contiki.c:27: Warning:
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 2b791e3541a23ef13830317b9ea07bbe17a1835d..0af10b1ad0589e04d7261412d8ef3fc45b457f14 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -21,8 +21,7 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
@@ -40,8 +39,7 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:173: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:176: Warning:
E-ACSL construct `user-defined logic type' is not yet supported.
@@ -59,9 +57,8 @@
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:180: Warning:
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:181: Warning:
E-ACSL construct
@@ -71,8 +68,7 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
index e66ace13b42b0c23943de0125ef7c106870e94e9..e927713310d2c53cf43bf6358a130d86e65b9137 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -6,12 +6,10 @@
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
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 234a0c3eb0ee7ec3bb6181e7a8d94a4d3878cbc0..2c1a720d90b85e102387507a174c1c39a27e5240 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -1,7 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -10,12 +9,10 @@
E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:121: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -25,12 +22,10 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:96: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
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 92c864736fb000c03417c43e377e3d1ef73988b7..377b65dcf61dd653c06589d75be4ffd0aab9529d 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -1,19 +1,15 @@
[e-acsl] beginning translation.
[e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
@@ -44,12 +40,10 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:424: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
@@ -71,8 +65,7 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
@@ -97,8 +90,7 @@
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
diff --git a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
index cf4f531b3ee983c209330fb353666577caa839c6..7ee1d9449abb35b1d4500ca2d6340ff7cc6f83ff 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
@@ -3,8 +3,7 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
index 362b90a9aa1066abdeab79981edb2bd136cff44a..d57b82d4e506da7776ddb3bfb43bfb7febfd40a7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -5,12 +5,10 @@
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
Some assumes clauses could not be translated.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index 7936c2eba8e8ddf4880fffdd44b734ce70929b3d..945052964a5ac5bf8ba77080f4728c7be8407b09 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -3,8 +3,7 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:485: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
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 322634c9ecbdd994890c2c5dc7be36316aa80871..c5ea5bf43129ede55019f8a712cc291af94b9239 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
@@ -1,7 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -10,12 +9,10 @@
E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:96: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
+ E-ACSL construct `predicates with labels' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.