Commit d570208e authored by Julien Signoles's avatar Julien Signoles
Browse files

[Typing] always catch exceptions raised by Interval.infer

parent 7c70c155
......@@ -95,7 +95,10 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
| _ ->
Options.fatal "Unexpected comparison operator"
in
let i = Interval.infer t_size in
let i =
try Interval.infer t_size
with Interval.Not_a_number | Interval.Is_a_real -> assert false
in
(* The EXACT amount of memory that is needed can be known at runtime. This
is because the tightest bounds for the variables can be known at runtime.
Example: In the following predicate
......
......@@ -120,44 +120,46 @@ let bounds_for_small_type ~loc (t1, lv, t2) =
| Linteger ->
t1, t2, None
| Ctype ty ->
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let i =
(* Ival.join would NOT be correct here:
Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
but NOT [-3..300] *)
Ival.inject_range (Ival.min_int i1) (Ival.max_int i2)
in
let ity = Interval.interv_of_typ ty in
if Ival.is_included i ity then
(* case 1 *)
t1, t2, None
else if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then begin
(* case 2 *)
let i = Ival.meet i ity in
(* now we potentially have a better interval for [lv]
==> update the binding *)
Interval.Env.replace lv i;
(* the smaller bounds *)
let min, max = Misc.finite_min_and_max i in
let t1 = Logic_const.tint ~loc min in
let t2 = Logic_const.tint ~loc max in
let ctx = Typing.number_ty_of_typ ty in
(* we are assured that we will not have a GMP,
once again because we intersected with [ity] *)
Typing.type_term ~use_gmp_opt:false ~ctx t1;
Typing.type_term ~use_gmp_opt:false ~ctx t2;
t1, t2, None
end else
(* case 3 *)
let min, max = Misc.finite_min_and_max ity in
let guard_lower = Logic_const.tint ~loc min in
let guard_upper = Logic_const.tint ~loc max in
let lv_term = Logic_const.tvar ~loc lv in
let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
let guard_upper = Logic_const.prel ~loc (Rle, lv_term, guard_upper) in
let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
t1, t2, Some guard
(try
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let i =
(* Ival.join would NOT be correct here:
Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
but NOT [-3..300] *)
Ival.inject_range (Ival.min_int i1) (Ival.max_int i2)
in
let ity = Interval.interv_of_typ ty in
if Ival.is_included i ity then
(* case 1 *)
t1, t2, None
else if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then begin
(* case 2 *)
let i = Ival.meet i ity in
(* now we potentially have a better interval for [lv]
==> update the binding *)
Interval.Env.replace lv i;
(* the smaller bounds *)
let min, max = Misc.finite_min_and_max i in
let t1 = Logic_const.tint ~loc min in
let t2 = Logic_const.tint ~loc max in
let ctx = Typing.number_ty_of_typ ty in
(* we are assured that we will not have a GMP,
once again because we intersected with [ity] *)
Typing.type_term ~use_gmp_opt:false ~ctx t1;
Typing.type_term ~use_gmp_opt:false ~ctx t2;
t1, t2, None
end else
(* case 3 *)
let min, max = Misc.finite_min_and_max ity in
let guard_lower = Logic_const.tint ~loc min in
let guard_upper = Logic_const.tint ~loc max in
let lv_term = Logic_const.tvar ~loc lv in
let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
let guard_upper = Logic_const.prel ~loc (Rle, lv_term, guard_upper) in
let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
t1, t2, Some guard
with Interval.Not_a_number | Interval.Is_a_real -> assert false)
| Ltype _ | Lvar _ | Lreal | Larrow _ ->
Options.abort "quantification over non-integer type is not part of E-ACSL"
......
......@@ -113,21 +113,25 @@ let rec has_empty_quantif_with_false_negative = function
(* case 2 *)
false
| (t1, rel1, _, rel2, t2) :: guards ->
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let lower_bound, _ = Ival.min_and_max i1 in
let _, upper_bound = Ival.min_and_max i2 in
match lower_bound, upper_bound with
| Some lower_bound, Some upper_bound ->
let res = match rel1, rel2 with
| Rle, Rle -> lower_bound > upper_bound
| Rle, Rlt | Rlt, Rle -> lower_bound >= upper_bound
| Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
| _ -> assert false
in
res (* case 1 *) || has_empty_quantif_with_false_negative guards
| None, _ | _, None ->
has_empty_quantif_with_false_negative guards
try
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
let lower_bound, _ = Ival.min_and_max i1 in
let _, upper_bound = Ival.min_and_max i2 in
match lower_bound, upper_bound with
| Some lower_bound, Some upper_bound ->
let res = match rel1, rel2 with
| Rle, Rle -> lower_bound > upper_bound
| Rle, Rlt | Rlt, Rle -> lower_bound >= upper_bound
| Rlt, Rlt -> lower_bound >= Z.sub upper_bound Z.one
| _ -> assert false
in
res (* case 1 *) || has_empty_quantif_with_false_negative guards
| None, _ | _, None ->
has_empty_quantif_with_false_negative guards
with
| Interval.Not_a_number -> assert false
| Interval.Is_a_real -> Error.not_yet "quantification over real numbers"
let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
......
......@@ -2,27 +2,27 @@
COMMENT: logic functions without labels
*/
/* /\*@ predicate p1(int x, int y) = x + y > 0; *\/ */
/* /\*@ predicate p2(integer x, integer y) = x + y > 0; *\/ */
/*@ predicate p1(int x, int y) = x + y > 0; */
/*@ predicate p2(integer x, integer y) = x + y > 0; */
/*@ logic integer f1(integer x, integer y) = x + y; */
/* // E-ACSL integer typing: */
/* // types less than int are considered as int */
/* /\*@ logic char h_char(char c) = c; *\/ */
/* /\*@ logic short h_short(short s) = s; *\/ */
// E-ACSL integer typing:
// types less than int are considered as int
/*@ logic char h_char(char c) = c; */
/*@ logic short h_short(short s) = s; */
/* /\*@ logic int g_hidden(int x) = x; *\/ */
/* /\*@ logic int g(int x) = g_hidden(x); *\/ */
/*@ logic int g_hidden(int x) = x; */
/*@ logic int g(int x) = g_hidden(x); */
/* struct mystruct { int k, l; }; */
/* typedef struct mystruct mystruct; */
/* /\*@ logic mystruct t1(mystruct m) = m; *\/ */
/* /\*@ logic integer t2(mystruct m) = m.k + m.l; *\/ */
struct mystruct { int k, l; };
typedef struct mystruct mystruct;
/*@ logic mystruct t1(mystruct m) = m; */
/*@ logic integer t2(mystruct m) = m.k + m.l; */
/* // To test function call in other clauses than assert: */
/* /\*@ predicate k_pred(integer x) = x > 0; *\/ */
/* /\*@ requires k_pred(x); *\/ */
// To test function call in other clauses than assert:
/*@ predicate k_pred(integer x) = x > 0; */
/*@ requires k_pred(x); */
void k(int x) {}
// To test non-interference with global inits:
......@@ -39,28 +39,28 @@ int glob = 5;
int main (void) {
int x = 1, y = 2;
/* /\*@ assert p1(x, y); *\/ ; */
/* /\*@ assert p2(3, 4); *\/ ; */
/* /\*@ assert p2(5, 99999999999999999999999999999); *\/ ; */
/*@ assert p1(x, y); */ ;
/*@ assert p2(3, 4); */ ;
/*@ assert p2(5, 99999999999999999999999999999); */ ;
/* /\*@ assert f1(x, y) == 3; *\/ ; */
/* /\*@ assert p2(x, f1(3, 4)); *\/ ; */
/* /\*@ assert f1(9, 99999999999999999999999999999) > 0; *\/ ; */
/*@ assert f1(x, y) == 3; */ ;
/*@ assert p2(x, f1(3, 4)); */ ;
/*@ assert f1(9, 99999999999999999999999999999) > 0; */ ;
/*@ assert f1(99999999999999999999999999999,
99999999999999999999999999999) ==
199999999999999999999999999998; */ ;
/* /\*@ assert g(x) == x; *\/ ; */
/*@ assert g(x) == x; */ ;
/* char c = 'c'; */
/* /\*@ assert h_char(c) == c; *\/ ; */
/* short s = 1; */
/* /\*@ assert h_short(s) == s; *\/ ; */
char c = 'c';
/*@ assert h_char(c) == c; */ ;
short s = 1;
/*@ assert h_short(s) == s; */ ;
/* mystruct m; */
/* m.k = 8; */
/* m.l = 9; */
/* /\*@ assert t2(t1(m)) == 17; *\/ ; */
mystruct m;
m.k = 8;
m.l = 9;
/*@ assert t2(t1(m)) == 17; */ ;
k(9);
......
This diff is collapsed.
Markdown is supported
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