Commit 8c54a72d authored by Julien Signoles's avatar Julien Signoles
Browse files

fix bugs introduced when rebasing the branch

parent 735ff34c
......@@ -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
| _ ->
......
......@@ -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 _ ->
......
......@@ -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;
}
......@@ -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;
}
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment