diff --git a/src/plugins/e-acsl/gmp.ml b/src/plugins/e-acsl/gmp.ml
index 8193c9fe30259e53afa25b39f8ab3e4f9bb3dedf..33c7013de586574a9c5631dff29d7c7d70213492 100644
--- a/src/plugins/e-acsl/gmp.ml
+++ b/src/plugins/e-acsl/gmp.ml
@@ -53,7 +53,10 @@ module Z = struct
include Make(struct end)
let t_struct_torig_ref = mk_dummy_type_info_ref ()
+ let set_t_struct ty = t_struct_torig_ref := ty
+ (* TODO: why not a pointer here (but an array of size 1 instead? *)
+ (* TODO: should be const *)
let t_ptr () =
TNamed(
{
@@ -94,6 +97,8 @@ let init_t () =
method !vglob = function
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
self#set Z.set_t info
+ | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_struct" ->
+ self#set Z.set_t_struct info
| GType({ torig_name = s } as info, _) when s = "__e_acsl_mpq_t" ->
self#set Q.set_t info
| _ ->
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index cd0ad0b5b52346982079c45a777d8ac2e1f760e8..171a654d313576cffae1a2e3d1434972c0608246 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -32,9 +32,6 @@ open Cil_types
exception Is_a_real
exception Not_a_number
-(* Not_a_number has priority over Is_a_real *)
-
-exception Not_an_integer
(* constructors *)
@@ -166,7 +163,7 @@ end = struct
(* TODO RATIONAL: what to do with is_real? *)
Env.add param larger_i;
larger_i
- with Not_an_integer ->
+ with Not_a_number ->
(* no need to add [param] to the environment *)
Ival.bottom)
li.l_profile
@@ -317,7 +314,7 @@ let rec infer_with_real t is_real =
| LBterm t' ->
let rec fixpoint i =
let is_included, new_i =
- Logic_function_env.widen ~infer_with_real t' i
+ Logic_function_env.widen ~infer_with_real t i
in
if is_included then begin
List.iter (fun lv -> Env.remove lv) li.l_profile;
@@ -389,11 +386,7 @@ and infer_term_host thost is_real =
match v.lv_type with
| Linteger ->
Ival.inject_range None None, false
- | Ctype (TFloat _) ->
- (* TODO RATIONAL: examine below. That is MR !226! *)
- (* TODO: handle in MR !226 *)
- raise Not_an_integer
- | Lreal ->
+ | Ctype (TFloat _) | Lreal ->
(* TODO RATIONAL: why bottom and not top? Why not raising Is_a_real? *)
Ival.bottom, true
| Ctype _ ->
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
index 1bf6931b3419cd8216a32e4081f39286c417a3f3..b554b4b014ce358be8f65b0350a1f1539dcd227a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -15,30 +15,30 @@ int __gen_e_acsl_p1(int x, int y);
/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
*/
+int __gen_e_acsl_p2(int x, int y);
+
int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
int __gen_e_acsl_p2_5(int x, long y);
-int __gen_e_acsl_p2(int x, int y);
-
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
- __e_acsl_mpz_struct * y);
+long __gen_e_acsl_f1(int x, int y);
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
__e_acsl_mpz_struct * y);
-long __gen_e_acsl_f1(int x, int y);
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y);
/*@ logic char h_char(char c) = c;
*/
-char __gen_e_acsl_h_char(int c);
+int __gen_e_acsl_h_char(int c);
/*@ logic short h_short(short s) = s;
*/
-short __gen_e_acsl_h_short(int s);
+int __gen_e_acsl_h_short(int s);
/*@ logic int g_hidden(int x) = x;
*/
@@ -178,19 +178,18 @@ int main(void)
char c = (char)'c';
/*@ assert h_char(c) ≡ c; */
{
- char __gen_e_acsl_h_char_2;
+ int __gen_e_acsl_h_char_2;
__gen_e_acsl_h_char_2 = __gen_e_acsl_h_char((int)c);
- __e_acsl_assert((int)__gen_e_acsl_h_char_2 == (int)c,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_h_char_2 == (int)c,(char *)"Assertion",
(char *)"main",(char *)"h_char(c) == c",56);
}
short s = (short)1;
/*@ assert h_short(s) ≡ s; */
{
- short __gen_e_acsl_h_short_2;
+ int __gen_e_acsl_h_short_2;
__gen_e_acsl_h_short_2 = __gen_e_acsl_h_short((int)s);
- __e_acsl_assert((int)__gen_e_acsl_h_short_2 == (int)s,
- (char *)"Assertion",(char *)"main",
- (char *)"h_short(s) == s",58);
+ __e_acsl_assert(__gen_e_acsl_h_short_2 == (int)s,(char *)"Assertion",
+ (char *)"main",(char *)"h_short(s) == s",58);
}
m.k = 8;
m.l = 9;
@@ -221,16 +220,9 @@ void __gen_e_acsl_k(int x)
return;
}
-char __gen_e_acsl_h_char(int c)
-{
- char __retres = (char)c;
- return __retres;
-}
-
-short __gen_e_acsl_h_short(int s)
+int __gen_e_acsl_h_short(int s)
{
- short __retres = (short)s;
- return __retres;
+ return s;
}
int __gen_e_acsl_g_hidden(int x)
@@ -252,13 +244,19 @@ mystruct __gen_e_acsl_t1(mystruct m)
int __gen_e_acsl_p1(int x, int y)
{
- int __retres = x + (long)y > 0L;
+ int __retres = x + y > 0L;
return __retres;
}
long __gen_e_acsl_t2(mystruct m)
{
- long __retres = m.k + (long)m.l;
+ long __retres = m.k + m.l;
+ return __retres;
+}
+
+int __gen_e_acsl_p2(int x, int y)
+{
+ int __retres = x + y > 0L;
return __retres;
}
@@ -306,29 +304,16 @@ int __gen_e_acsl_p2_5(int x, long y)
return __retres;
}
-int __gen_e_acsl_p2(int x, int y)
-{
- int __retres = x + (long)y > 0L;
- return __retres;
-}
-
int __gen_e_acsl_k_pred(int x)
{
int __retres = x > 0;
return __retres;
}
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
- __e_acsl_mpz_struct * y)
+long __gen_e_acsl_f1(int x, int y)
{
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
+ long __retres = x + y;
+ return __retres;
}
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
@@ -348,10 +333,22 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
return;
}
-long __gen_e_acsl_f1(int x, int y)
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
{
- long __retres = x + (long)y;
- return __retres;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
+}
+
+int __gen_e_acsl_h_char(int c)
+{
+ return c;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
index 9989adf5ca2bee1aad2ee77c8cb647276dbd3573..0feabbd93d9fca8d89aeecd37186eb085a3daec2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -15,28 +15,28 @@ int __gen_e_acsl_p1(int x, int y);
/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
*/
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
-
int __gen_e_acsl_p2(int x, int y);
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
- __e_acsl_mpz_struct * y);
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
__e_acsl_mpz_struct * y);
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y);
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y);
/*@ logic char h_char(char c) = c;
*/
-char __gen_e_acsl_h_char(int c);
+int __gen_e_acsl_h_char(int c);
/*@ logic short h_short(short s) = s;
*/
-short __gen_e_acsl_h_short(int s);
+int __gen_e_acsl_h_short(int s);
/*@ logic int g_hidden(int x) = x;
*/
@@ -199,7 +199,7 @@ int main(void)
char c = (char)'c';
/*@ assert h_char(c) ≡ c; */
{
- char __gen_e_acsl_h_char_2;
+ int __gen_e_acsl_h_char_2;
__e_acsl_mpz_t __gen_e_acsl_app_2;
__e_acsl_mpz_t __gen_e_acsl_c;
int __gen_e_acsl_eq_4;
@@ -216,7 +216,7 @@ int main(void)
short s = (short)1;
/*@ assert h_short(s) ≡ s; */
{
- short __gen_e_acsl_h_short_2;
+ int __gen_e_acsl_h_short_2;
__e_acsl_mpz_t __gen_e_acsl_app_3;
__e_acsl_mpz_t __gen_e_acsl_s;
int __gen_e_acsl_eq_5;
@@ -266,16 +266,9 @@ void __gen_e_acsl_k(int x)
return;
}
-char __gen_e_acsl_h_char(int c)
-{
- char __retres = (char)c;
- return __retres;
-}
-
-short __gen_e_acsl_h_short(int s)
+int __gen_e_acsl_h_short(int s)
{
- short __retres = (short)s;
- return __retres;
+ return s;
}
int __gen_e_acsl_g_hidden(int x)
@@ -337,27 +330,6 @@ void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
return;
}
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_3;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_gt_3;
- __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
- (__e_acsl_mpz_struct const *)(y));
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- int __retres = __gen_e_acsl_gt_3 > 0;
- __gmpz_clear(__gen_e_acsl_x_3);
- __gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl__4);
- return __retres;
-}
-
int __gen_e_acsl_p2(int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -382,6 +354,27 @@ int __gen_e_acsl_p2(int x, int y)
return __retres;
}
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_gt_3;
+ __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+ (__e_acsl_mpz_struct const *)(y));
+ __gmpz_init_set_si(__gen_e_acsl__4,0L);
+ __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+ int __retres = __gen_e_acsl_gt_3 > 0;
+ __gmpz_clear(__gen_e_acsl_x_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl__4);
+ return __retres;
+}
+
int __gen_e_acsl_k_pred(int x)
{
__e_acsl_mpz_t __gen_e_acsl_x;
@@ -397,16 +390,22 @@ int __gen_e_acsl_k_pred(int x)
return __retres;
}
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
- __e_acsl_mpz_struct * y)
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
{
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
- (__e_acsl_mpz_struct const *)(y));
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl_add_6);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ __gmpz_clear(__gen_e_acsl_x_4);
+ __gmpz_clear(__gen_e_acsl_y_3);
+ __gmpz_clear(__gen_e_acsl_add_4);
return;
}
@@ -427,23 +426,22 @@ void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
return;
}
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+ __e_acsl_mpz_struct * y)
{
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y_3;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
+ (__e_acsl_mpz_struct const *)(y));
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
- __gmpz_clear(__gen_e_acsl_x_4);
- __gmpz_clear(__gen_e_acsl_y_3);
- __gmpz_clear(__gen_e_acsl_add_4);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+ __gmpz_clear(__gen_e_acsl_add_6);
return;
}
+int __gen_e_acsl_h_char(int c)
+{
+ return c;
+}
+
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 399976653d80d69ea901530c793a2192a228f556..bb76cea30ea8b5c70da5cc060ae3a35cda0c5230 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -337,7 +337,7 @@ and context_insensitive_term_to_exp kf env t =
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
let name = Misc.name_of_binop bop in
let _, e, env =
- Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
+ Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
in
e, env, C_number, ""
else if Real.is_t ty then