diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 6a8454d1f870128ebd5abfa85b2cc9a1daefc381..49ca8b5c56c1fd21ab1c0327f93153cea87537fe 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,9 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2022-11-08] Add support for functions returning a rational
+-* E-ACSL [2022-11-08] Fix assign clause and result as extra argument for functions
+ returning a structure (frama-c/frama-c#1139)
- E-ACSL [2022-19-07] Improve typing precision of variables appearing in comparisons
-* E-ACSL [2022-09-08] Fix typing of recursive predicates (frama-c/e-acsl#198)
-* E-ACSL [2022-17-06] Fix wrong cast from pointer to integer (frama-c/frama-c#1119)
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
index eaa80b49e8f8e2682faa4c3d36b8bd9b3148d362..1febf4acf418151ba282d9fcca47fd37164559df 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.ml
+++ b/src/plugins/e-acsl/src/code_generator/assigns.ml
@@ -81,10 +81,8 @@ let rec get_assigns_from ~loc env lprofile lv =
(* Special case when the function takes an extra argument as its result:
For the argument [__e_acsl_mpz_t *__retres_arg], this function generates the
- expression [( *__retres_arg )[0]] *)
-let get_gmp_integer ~loc vi =
- Smart_exp.lval
- ~loc
- (Mem
- (Smart_exp.lval ~loc (Var vi, NoOffset)),
- (Index (Cil.zero ~loc, NoOffset)))
+ expression [( *__retres_arg )[0]]. For a struct argument, this function just
+ generates the variable corresponding to the argument. *)
+let get_assigned_var ~loc ~is_gmp vi =
+ let var = if is_gmp then Smart_exp.mem ~loc vi else Cil.evar ~loc vi
+ in Logic_utils.expr_to_term var
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.mli b/src/plugins/e-acsl/src/code_generator/assigns.mli
index c245cd4de580cb26a4dd2a241cacc02c913f2540..cf064eccd35dbb3023f8f600750e0e0e600299ce 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.mli
+++ b/src/plugins/e-acsl/src/code_generator/assigns.mli
@@ -31,7 +31,7 @@ val get_assigns_from :
(* @returns the list of expressions that are allowed to be used to assign the
the result of a logic function *)
-val get_gmp_integer :
- loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
+val get_assigned_var :
+ loc:Cil_types.location -> is_gmp:bool -> Cil_types.varinfo -> Cil_types.term
(* @returns the expression that gets assigned when the result of the function is
- a pointer on a GMP type *)
+ passed as an additional argument *)
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index efc72c375b0559a68b2db7706a817f0444aaf640..38608a2fddc9289e35c1a72413c5ddc0f3e8b591 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -106,40 +106,6 @@ let generic_affect ~loc fname lv ev e =
end else
Smart_stmt.assigns ~loc:e.eloc ~result:lv e
-let init_set ~loc lv ev e =
- let fname =
- let ty = Cil.typeOf ev in
- if Gmp_types.Z.is_t ty then
- "__gmpz_init_set"
- else if Gmp_types.Q.is_t ty then
- Options.fatal "no __gmpq_init_set: init then set separately"
- else
- ""
- in
- try generic_affect ~loc fname lv ev e
- with
- | Longlong IULongLong ->
- (match e.enode with
- | Lval elv ->
- assert (Gmp_types.Z.is_t (Cil.typeOf ev));
- let call =
- Smart_stmt.rtl_call ~loc
- ~prefix:""
- "__gmpz_import"
- [ ev;
- Cil.one ~loc;
- Cil.one ~loc;
- Cil.sizeOf ~loc (TInt(IULongLong, []));
- Cil.zero ~loc;
- Cil.zero ~loc;
- Cil.mkAddrOf ~loc elv ]
- in
- Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
- | _ ->
- Error.not_yet "unsigned long long expression requiring GMP")
- | Longlong ILongLong ->
- Error.not_yet "long long requiring GMP"
-
let affect ~loc lv ev e =
let fname =
let ty = Cil.typeOf ev in
@@ -151,6 +117,43 @@ let affect ~loc lv ev e =
with Longlong _ ->
Error.not_yet "quantification over long long and requiring GMP"
+let init_set ~loc lv ev e =
+ let mpz_init_set fname =
+ try generic_affect ~loc fname lv ev e
+ with
+ | Longlong IULongLong ->
+ (match e.enode with
+ | Lval elv ->
+ assert (Gmp_types.Z.is_t (Cil.typeOf ev));
+ let call =
+ Smart_stmt.rtl_call ~loc
+ ~prefix:""
+ "__gmpz_import"
+ [ ev;
+ Cil.one ~loc;
+ Cil.one ~loc;
+ Cil.sizeOf ~loc (TInt(IULongLong, []));
+ Cil.zero ~loc;
+ Cil.zero ~loc;
+ Cil.mkAddrOf ~loc elv ]
+ in
+ Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
+ | _ ->
+ Error.not_yet "unsigned long long expression requiring GMP")
+ | Longlong ILongLong ->
+ Error.not_yet "long long requiring GMP"
+ in
+ let ty = Cil.typeOf ev in
+ if Gmp_types.Z.is_t ty then
+ mpz_init_set "__gmpz_init_set"
+ else if Gmp_types.Q.is_t ty then
+ Smart_stmt.block_stmt
+ (Cil.mkBlock
+ [ init ~loc ev ;
+ affect ~loc lv ev e ])
+ else
+ mpz_init_set ""
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
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 331ec21a4ea44268ed23683105a300ab2c16fb96..861672fca4f8924e8b715a2947c25673ab164c1d 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -55,9 +55,14 @@ let term_to_exp_ref
(* @return true iff the result of the function is provided by reference as the
first extra argument at each call *)
-let result_as_extra_argument = Gmp_types.Z.is_t
-(* TODO: to be extended to any compound type? E.g. returning a struct is not
- good practice... *)
+let result_as_extra_argument typ =
+ let is_composite typ =
+ match Cil.unrollType typ with
+ | TComp _ | TPtr _ | TArray _ -> true
+ | TInt _ | TVoid _ | TFloat _ | TFun _ | TNamed _ | TEnum _
+ | TBuiltin_va_list _ -> false
+ in
+ Gmp_types.is_t typ || is_composite typ
(*****************************************************************************)
(****************** Generation of function bodies ****************************)
@@ -151,6 +156,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
in
(* build the varinfo storing the result *)
let res_as_extra_arg = result_as_extra_argument ret_ty in
+ let is_gmp = Gmp_types.is_t ret_ty in
let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
let vname = "__retres" in
if res_as_extra_arg then
@@ -209,7 +215,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
let assigned_var =
Logic_const.new_identified_term
(if res_as_extra_arg then
- Logic_utils.expr_to_term (Assigns.get_gmp_integer ~loc ret_vi)
+ Assigns.get_assigned_var ~loc ~is_gmp ret_vi
else
Logic_const.tresult fundec.svar.vtype)
in
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index 904f1c9fb591cb72f64869f322dd1d5f438134fd..102ac515432819a2f174fadaff5cb929c186b07a 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -412,11 +412,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let ty = Typing.get_typ ~logic_env t in
let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
let e, _, env = term_to_exp kf env t in
- let ty = Cil.typeOf e in
- let init_set =
- if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
- in
- let let_stmt = init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
+ let let_stmt = Gmp.init_set ~loc (Cil.var vi_of_lv) exp_of_lv e in
let stmts, env =
mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 4e11ce0f4e4a79c512b78f656aec5700dd1cce3a..4f385a6ff5df6ed5010a860c2cda9c12f3e08730 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -22,13 +22,6 @@
open Cil_types
-(* No init_set for GMPQ: init then set separately *)
-let init_set ~loc lval vi_e e =
- Smart_stmt.block_stmt
- (Cil.mkBlock
- [ Gmp.init ~loc vi_e ;
- Gmp.affect ~loc lval vi_e e ])
-
let create ~loc ?name e env kf t_opt =
let ty = Cil.typeOf e in
if Gmp_types.Q.is_t ty then
diff --git a/src/plugins/e-acsl/src/code_generator/rational.mli b/src/plugins/e-acsl/src/code_generator/rational.mli
index 84f197cab38f15517f4b84fb2dc11ed975dfab9d..72e4a5a2b555da0634d08adc0df440aeca31f995 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.mli
+++ b/src/plugins/e-acsl/src/code_generator/rational.mli
@@ -33,11 +33,6 @@ val create:
exp * Env.t
(** Create a real *)
-(* TODO: change the call convention *)
-val init_set: loc:location -> lval -> exp -> exp -> stmt
-(** [init_set lval lval_as_exp exp] sets [lval] to [exp] while guranteeing that
- [lval] is properly initialized wrt the underlying real library. *)
-
val normalize_str: string -> string
(** Normalize the string so that it fits the representation used by the
underlying real library. For example, "0.1" is a real number in ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
index bd7c20cc87f4316a8d3a07befb042b97ec5a31ea..3475ed66929c0271d5731943f98c76f4a6b338a5 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
@@ -71,6 +71,11 @@ let lnot ~loc e =
let null ~loc =
Cil.mkCast ~newt:(TPtr (TVoid [], [])) (Cil.zero ~loc)
+let mem ~loc vi =
+ lval
+ ~loc
+ (Cil.mkMem ~addr:(Cil.evar ~loc vi) ~off:(Index (Cil.zero ~loc, NoOffset)))
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
index a2f1dbd82002aea2d8ecbc7a4ea03cf42ec0df3a..2cffdd27908b6b7c5d8ec78a4c37ea4da8a37a2a 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
@@ -46,6 +46,8 @@ val lnot: loc:location -> exp -> exp
val null: loc:location -> exp
(** [null ~loc] creates an expression to represent the NULL pointer. *)
+val mem: loc:location -> varinfo -> exp
+(** [mem ~loc v] creates a Mem expression with an explicit index of 0 *)
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index cf14ab17aa83a48331f6ebf86548c3b230534d5f..654ff848a0f0518204f319e010983f731fda1728 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -282,10 +282,7 @@ let pretranslate_to_exp ~loc kf env pot =
t_opt
ty
(fun var_vi var_e ->
- let init_set =
- if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
- in
- [ init_set ~loc (Cil.var var_vi) var_e e ])
+ [ Gmp.init_set ~loc (Cil.var var_vi) var_e e ])
in
var_vi, env
diff --git a/src/plugins/e-acsl/src/code_generator/translate_utils.ml b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
index 5b6f157fc6c94f5b8c41fc08f5624e2c122cea64..665dd752c4410b6b117afb4504cd20b7581668f4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_utils.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_utils.ml
@@ -284,8 +284,7 @@ let env_of_li ~adata ~loc kf env li =
let stmt = match Typing.get_number_ty ~logic_env t with
| C_integer _ | C_float _ | Nan ->
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
- | Gmpz -> Gmp.init_set ~loc (Cil.var vi) vi_e e
- | Rational -> Rational.init_set ~loc (Cil.var vi) vi_e e
+ | Gmpz | Rational -> Gmp.init_set ~loc (Cil.var vi) vi_e e
| Real -> Error.not_yet "real number"
in
adata, Env.add_stmt env stmt
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index 428a12d2cb243e2d8963729e3579d9a52091f9bc..ead203551b4cf464f28044f412691cf8f18bae15 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -43,6 +43,9 @@ int glob = 5;
// Test sums inside functions
/*@ logic integer f_sum (integer x) = \sum(1,x,\lambda integer y; 1); */
+// Test functions returning a rational
+/*@ logic real over(real a, real b) = a/b; */
+
int main(void) {
int x = 1, y = 2;
/*@ assert p1(x, y); */;
@@ -67,6 +70,7 @@ int main(void) {
mystruct m;
m.k = 8;
m.l = 9;
+ /*@ assert \let r = t1(m); r.k == 8; */;
/*@ assert t2(t1(m)) == 17; */;
k(9);
@@ -74,7 +78,9 @@ int main(void) {
double d = 2.0;
/*@ assert f2(d) > 0; */;
- /*@ assert f_sum (100) == 100; */
+ /*@ assert f_sum (100) == 100; */;
+
+ /*@ assert over(1., 2.) == 0.5; */;
// not yet supported
/* /\*@ assert p_notyet(27); *\/ ; */
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
index 722a30329dc0d8844b5db2c70565c8812edee5a3..bb5a7cd1b3c49b8c32e0f0e920d1c1116b32fc3d 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,61 +1,73 @@
[e-acsl] beginning translation.
+[e-acsl] functions.c:73: Warning:
+ E-ACSL construct `function application' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions.c:48: Warning:
+[eva:alarm] functions.c:51: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:48: Warning:
+[eva:alarm] functions.c:51: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:50: Warning:
+[eva:alarm] functions.c:53: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:52: Warning:
+[eva:alarm] functions.c:55: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:52: Warning:
+[eva:alarm] functions.c:55: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:53: Warning:
+[eva:alarm] functions.c:56: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:53: Warning:
+[eva:alarm] functions.c:56: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:54: Warning:
+[eva:alarm] functions.c:57: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:55: Warning:
+[eva:alarm] functions.c:58: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:60: Warning:
+[eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:60: Warning:
+[eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:63: Warning:
+[eva:alarm] functions.c:66: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:63: Warning:
+[eva:alarm] functions.c:66: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:65: Warning:
+[eva:alarm] functions.c:68: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:65: Warning:
+[eva:alarm] functions.c:68: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:70: Warning:
+[eva:alarm] functions.c:73: Warning:
+ function __e_acsl_assert_register_struct: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] functions.c:73: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:70: Warning:
+[eva:alarm] functions.c:73: Warning: assertion got status unknown.
+[eva:alarm] functions.c:74: Warning:
+ function __e_acsl_assert_register_struct: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] functions.c:74: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:28: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:75: Warning:
+[eva:alarm] functions.c:79: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] functions.c:75: Warning:
+[eva:alarm] functions.c:79: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:75: Warning:
+[eva:alarm] functions.c:79: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] functions.c:81: Warning: assertion got status unknown.
+[eva:alarm] functions.c:83: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:77: Warning: assertion got status unknown.
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 192abded1c01d4e34b486e5e9ec1cb56a80a8f3c..ca9e702ccf90ad1eae903661f7a1d6954148d184 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -57,7 +57,7 @@ int __gen_e_acsl_g(int x);
/*@ logic mystruct t1(mystruct m) = m;
*/
-mystruct __gen_e_acsl_t1(mystruct m);
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m);
/*@ logic integer t2(mystruct m) = m.k + m.l;
*/
@@ -88,9 +88,13 @@ double __gen_e_acsl_f2(double x);
/*@ logic integer f_notyet{L}(integer x) = x;
*/
/*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
+ */
+int __gen_e_acsl_f_sum(int x);
+
+/*@ logic real over(real a, real b) = a / b;
*/
-int __gen_e_acsl_f_sum(int x);
+void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b);
int main(void)
{
@@ -112,7 +116,7 @@ int main(void)
__gen_e_acsl_assert_data.pred_txt = "p1(x, y)";
__gen_e_acsl_assert_data.file = "functions.c";
__gen_e_acsl_assert_data.fct = "main";
- __gen_e_acsl_assert_data.line = 48;
+ __gen_e_acsl_assert_data.line = 51;
__e_acsl_assert(__gen_e_acsl_p1_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -129,7 +133,7 @@ int main(void)
__gen_e_acsl_assert_data_2.pred_txt = "p2(3, 4)";
__gen_e_acsl_assert_data_2.file = "functions.c";
__gen_e_acsl_assert_data_2.fct = "main";
- __gen_e_acsl_assert_data_2.line = 49;
+ __gen_e_acsl_assert_data_2.line = 52;
__e_acsl_assert(__gen_e_acsl_p2_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
@@ -150,7 +154,7 @@ int main(void)
__gen_e_acsl_assert_data_3.pred_txt = "p2(5, 99999999999999999999999999999)";
__gen_e_acsl_assert_data_3.file = "functions.c";
__gen_e_acsl_assert_data_3.fct = "main";
- __gen_e_acsl_assert_data_3.line = 50;
+ __gen_e_acsl_assert_data_3.line = 53;
__e_acsl_assert(__gen_e_acsl_p2_4,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_);
@@ -170,7 +174,7 @@ int main(void)
__gen_e_acsl_assert_data_4.pred_txt = "f1(x, y) == 3";
__gen_e_acsl_assert_data_4.file = "functions.c";
__gen_e_acsl_assert_data_4.fct = "main";
- __gen_e_acsl_assert_data_4.line = 52;
+ __gen_e_acsl_assert_data_4.line = 55;
__e_acsl_assert(__gen_e_acsl_f1_2 == 3L,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
@@ -192,7 +196,7 @@ int main(void)
__gen_e_acsl_assert_data_5.pred_txt = "p2(x, f1(3, 4))";
__gen_e_acsl_assert_data_5.file = "functions.c";
__gen_e_acsl_assert_data_5.fct = "main";
- __gen_e_acsl_assert_data_5.line = 53;
+ __gen_e_acsl_assert_data_5.line = 56;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
}
@@ -218,7 +222,7 @@ int main(void)
__gen_e_acsl_assert_data_6.pred_txt = "f1(9, 99999999999999999999999999999) > 0";
__gen_e_acsl_assert_data_6.file = "functions.c";
__gen_e_acsl_assert_data_6.fct = "main";
- __gen_e_acsl_assert_data_6.line = 54;
+ __gen_e_acsl_assert_data_6.line = 57;
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__gmpz_clear(__gen_e_acsl__3);
@@ -249,7 +253,7 @@ int main(void)
__gen_e_acsl_assert_data_7.pred_txt = "f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998";
__gen_e_acsl_assert_data_7.file = "functions.c";
__gen_e_acsl_assert_data_7.fct = "main";
- __gen_e_acsl_assert_data_7.line = 55;
+ __gen_e_acsl_assert_data_7.line = 58;
__e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gmpz_clear(__gen_e_acsl__5);
@@ -275,7 +279,7 @@ int main(void)
__gen_e_acsl_assert_data_8.pred_txt = "g(x) == x";
__gen_e_acsl_assert_data_8.file = "functions.c";
__gen_e_acsl_assert_data_8.fct = "main";
- __gen_e_acsl_assert_data_8.line = 60;
+ __gen_e_acsl_assert_data_8.line = 63;
__e_acsl_assert(__gen_e_acsl_g_2 == x,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
}
@@ -295,7 +299,7 @@ int main(void)
__gen_e_acsl_assert_data_9.pred_txt = "h_char(c) == c";
__gen_e_acsl_assert_data_9.file = "functions.c";
__gen_e_acsl_assert_data_9.fct = "main";
- __gen_e_acsl_assert_data_9.line = 63;
+ __gen_e_acsl_assert_data_9.line = 66;
__e_acsl_assert((int)__gen_e_acsl_h_char_2 == (int)c,
& __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
@@ -316,7 +320,7 @@ int main(void)
__gen_e_acsl_assert_data_10.pred_txt = "h_short(s) == s";
__gen_e_acsl_assert_data_10.file = "functions.c";
__gen_e_acsl_assert_data_10.fct = "main";
- __gen_e_acsl_assert_data_10.line = 65;
+ __gen_e_acsl_assert_data_10.line = 68;
__e_acsl_assert((int)__gen_e_acsl_h_short_2 == (int)s,
& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
@@ -325,64 +329,111 @@ int main(void)
m.k = 8;
m.l = 9;
{
+ mystruct __gen_e_acsl_r;
mystruct __gen_e_acsl_t1_2;
- long __gen_e_acsl_t2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
- __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
- __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_2);
+ __gen_e_acsl_t1(& __gen_e_acsl_t1_2,m);
+ __gen_e_acsl_r = __gen_e_acsl_t1_2;
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,"r.k",0,
+ __gen_e_acsl_r.k);
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"m");
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_11,"t1(m)");
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_11,"t2(t1(m))",
- 0,__gen_e_acsl_t2_2);
__gen_e_acsl_assert_data_11.blocking = 1;
__gen_e_acsl_assert_data_11.kind = "Assertion";
- __gen_e_acsl_assert_data_11.pred_txt = "t2(t1(m)) == 17";
+ __gen_e_acsl_assert_data_11.pred_txt = "\\let r = t1(m); r.k == 8";
__gen_e_acsl_assert_data_11.file = "functions.c";
__gen_e_acsl_assert_data_11.fct = "main";
- __gen_e_acsl_assert_data_11.line = 70;
- __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_11);
+ __gen_e_acsl_assert_data_11.line = 73;
+ __e_acsl_assert(__gen_e_acsl_r.k == 8,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
}
- /*@ assert t2(t1(m)) == 17; */ ;
- __gen_e_acsl_k(9);
- double d = 2.0;
+ /*@ assert \let r = t1(m); r.k == 8; */ ;
{
- double __gen_e_acsl_f2_2;
+ mystruct __gen_e_acsl_t1_4;
+ long __gen_e_acsl_t2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
- __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
- __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"d",d);
- __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_12,"f2(d)",
- __gen_e_acsl_f2_2);
+ __gen_e_acsl_t1(& __gen_e_acsl_t1_4,m);
+ __gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_4);
+ __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"m");
+ __e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"t1(m)");
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_12,"t2(t1(m))",
+ 0,__gen_e_acsl_t2_2);
__gen_e_acsl_assert_data_12.blocking = 1;
__gen_e_acsl_assert_data_12.kind = "Assertion";
- __gen_e_acsl_assert_data_12.pred_txt = "f2(d) > 0";
+ __gen_e_acsl_assert_data_12.pred_txt = "t2(t1(m)) == 17";
__gen_e_acsl_assert_data_12.file = "functions.c";
__gen_e_acsl_assert_data_12.fct = "main";
- __gen_e_acsl_assert_data_12.line = 75;
- __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_12);
+ __gen_e_acsl_assert_data_12.line = 74;
+ __e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
}
- /*@ assert f2(d) > 0; */ ;
+ /*@ assert t2(t1(m)) == 17; */ ;
+ __gen_e_acsl_k(9);
+ double d = 2.0;
{
- int __gen_e_acsl_f_sum_2;
+ double __gen_e_acsl_f2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_13 =
{.values = (void *)0};
- __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_13,"f_sum(100)",
- 0,__gen_e_acsl_f_sum_2);
+ __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
+ __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_13,"d",d);
+ __e_acsl_assert_register_double(& __gen_e_acsl_assert_data_13,"f2(d)",
+ __gen_e_acsl_f2_2);
__gen_e_acsl_assert_data_13.blocking = 1;
__gen_e_acsl_assert_data_13.kind = "Assertion";
- __gen_e_acsl_assert_data_13.pred_txt = "f_sum(100) == 100";
+ __gen_e_acsl_assert_data_13.pred_txt = "f2(d) > 0";
__gen_e_acsl_assert_data_13.file = "functions.c";
__gen_e_acsl_assert_data_13.fct = "main";
- __gen_e_acsl_assert_data_13.line = 77;
- __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
- & __gen_e_acsl_assert_data_13);
+ __gen_e_acsl_assert_data_13.line = 79;
+ __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
}
+ /*@ assert f2(d) > 0; */ ;
+ {
+ int __gen_e_acsl_f_sum_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_14 =
+ {.values = (void *)0};
+ __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_14,"f_sum(100)",
+ 0,__gen_e_acsl_f_sum_2);
+ __gen_e_acsl_assert_data_14.blocking = 1;
+ __gen_e_acsl_assert_data_14.kind = "Assertion";
+ __gen_e_acsl_assert_data_14.pred_txt = "f_sum(100) == 100";
+ __gen_e_acsl_assert_data_14.file = "functions.c";
+ __gen_e_acsl_assert_data_14.fct = "main";
+ __gen_e_acsl_assert_data_14.line = 81;
+ __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
+ & __gen_e_acsl_assert_data_14);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
+ }
/*@ assert f_sum(100) == 100; */ ;
+ {
+ __e_acsl_mpq_t __gen_e_acsl_over_2;
+ __e_acsl_mpq_t __gen_e_acsl__11;
+ int __gen_e_acsl_eq_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_15 =
+ {.values = (void *)0};
+ __gen_e_acsl_over(& __gen_e_acsl_over_2,1.,2.);
+ __gmpq_init(__gen_e_acsl__11);
+ __gmpq_set_d(__gen_e_acsl__11,0.5);
+ __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
+ __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data_15,
+ "over(1., 2.)",
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2));
+ __gen_e_acsl_assert_data_15.blocking = 1;
+ __gen_e_acsl_assert_data_15.kind = "Assertion";
+ __gen_e_acsl_assert_data_15.pred_txt = "over(1., 2.) == 0.5";
+ __gen_e_acsl_assert_data_15.file = "functions.c";
+ __gen_e_acsl_assert_data_15.fct = "main";
+ __gen_e_acsl_assert_data_15.line = 83;
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_15);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
+ __gmpq_clear(__gen_e_acsl_over_2);
+ __gmpq_clear(__gen_e_acsl__11);
+ }
+ /*@ assert over(1., 2.) == 0.5; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
@@ -540,11 +591,12 @@ int __gen_e_acsl_g(int x)
return __gen_e_acsl_g_hidden_2;
}
-/*@ assigns \result;
- assigns \result \from m; */
-mystruct __gen_e_acsl_t1(mystruct m)
+/*@ assigns __retres_arg;
+ assigns __retres_arg \from m; */
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m)
{
- return m;
+ *__retres_arg = m;
+ return;
}
/*@ assigns \result;
@@ -612,4 +664,27 @@ int __gen_e_acsl_f_sum(int x)
return __gen_e_acsl_accumulator;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from a, b; */
+void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b)
+{
+ __e_acsl_mpq_t __gen_e_acsl_b;
+ __e_acsl_mpq_t __gen_e_acsl__10;
+ __e_acsl_mpq_t __gen_e_acsl_div_2;
+ __gmpq_init(__gen_e_acsl_b);
+ __gmpq_set_d(__gen_e_acsl_b,b);
+ __gmpq_init(__gen_e_acsl__10);
+ __gmpq_set_d(__gen_e_acsl__10,a);
+ __gmpq_init(__gen_e_acsl_div_2);
+ __gmpq_div(__gen_e_acsl_div_2,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
+ __gmpq_init(*__retres_arg);
+ __gmpq_set(*__retres_arg,(__e_acsl_mpq_struct const *)(__gen_e_acsl_div_2));
+ __gmpq_clear(__gen_e_acsl_b);
+ __gmpq_clear(__gen_e_acsl__10);
+ __gmpq_clear(__gen_e_acsl_div_2);
+ return;
+}
+
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index 11e868ecff42b57483b231fea8c40d5782b95b31..8dacca6e91c64b25bd74aff9816d9713734b3a5f 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -58,7 +58,7 @@ int __gen_e_acsl_g(int x);
/*@ logic mystruct t1(mystruct m) = m;
*/
-mystruct __gen_e_acsl_t1(mystruct m);
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m);
/*@ logic integer t2(mystruct m) = m.k + m.l;
*/
@@ -378,7 +378,7 @@ int main(void)
int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
- __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t1(& __gen_e_acsl_t1_2,m);
__gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
__gmpz_init_set_si(__gen_e_acsl__16,17L);
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2),
@@ -657,11 +657,12 @@ int __gen_e_acsl_g(int x)
return __gen_e_acsl_g_hidden_2;
}
-/*@ assigns \result;
- assigns \result \from m; */
-mystruct __gen_e_acsl_t1(mystruct m)
+/*@ assigns __retres_arg;
+ assigns __retres_arg \from m; */
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m)
{
- return m;
+ *__retres_arg = m;
+ return;
}
/*@ assigns (*__retres_arg)[0];