Commit ade03918 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

jessie3: workaround pb with f(int32)

parent 9682a625
......@@ -534,14 +534,29 @@ let eq op ty1 t1 ty2 t2 =
| _,_ ->
Self.not_yet_implemented "eq"
let compare op ty1 t1 ty2 t2 =
match ty1,ty2 with
| Linteger, Linteger -> t_app op [t1;t2]
| Lreal, Lreal -> assert false
| Ctype _,_ ->
Self.not_yet_implemented "compare Ctype"
| Ltype _, Ltype _ -> assert false
| Lvar _,_ ->
Self.not_yet_implemented "compare Lvar"
| Larrow _,_ ->
Self.not_yet_implemented "compare Larrow"
| _,_ ->
Self.not_yet_implemented "compare"
let rel (ty1,t1) op (ty2,t2) =
match op with
| Req -> eq Term.t_equ ty1 t1 ty2 t2
| Rneq -> eq Term.t_neq ty1 t1 ty2 t2
| Rge when is_int_type ty1 && is_int_type ty2 -> t_app ge_int [t1;t2]
| Rle when is_int_type ty1 && is_int_type ty2 -> t_app le_int [t1;t2]
| Rgt when is_int_type ty1 && is_int_type ty2 -> t_app gt_int [t1;t2]
| Rlt when is_int_type ty1 && is_int_type ty2 -> t_app lt_int [t1;t2]
| Rge when is_int_type ty1 && is_int_type ty2 -> compare ge_int ty1 t1 ty2 t2
| Rle when is_int_type ty1 && is_int_type ty2 -> compare le_int ty1 t1 ty2 t2
| Rgt when is_int_type ty1 && is_int_type ty2 -> compare gt_int ty1 t1 ty2 t2
| Rlt when is_int_type ty1 && is_int_type ty2 -> compare lt_int ty1 t1 ty2 t2
| Rge when is_real_type ty1 && is_real_type ty2 -> t_app ge_real [t1;t2]
| Rge ->
Self.not_yet_implemented "rel Rge"
......
......@@ -6,11 +6,11 @@
//@ logic integer sqr(integer x) = x * x;
/*@ requires x >= 0;
@ ensures \result >= 0 ; // && sqr(\result) <= x && x < sqr(\result + 1);
@ ensures \result >= 0 && sqr(\result+0) <= x && x < sqr(\result + 1);
@*/
int isqrt(int x) {
int count = 0, sum = 1;
/*@ loop invariant count >= 0 && x >= sqr(count) ; // && sum == sqr(count+1);
/*@ loop invariant count >= 0 && x >= sqr(count+0) && sum == sqr(count+1);
@ loop variant x - count;
@*/
while (sum <= x) { ++count; sum += 2 * count + 1; }
......
......@@ -2,4 +2,4 @@
[jessie3] processing function binary_search
[kernel] Plug-in jessie3 aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
'[Plug-in jessie3] predicate'.
'[Plug-in jessie3] ctype TPtr(TInt,_)'.
......@@ -33,25 +33,130 @@
(* use ref.Ref *)
(* use mach_int.Int32 *)
goal WP_parameter_isqrt :
forall x:int.
x >= 0 ->
(forall count:int.
count = 0 ->
(forall sum:int.
sum = 1 ->
((count >= 0 /\ x >= sqr count) /\ sum = sqr (count + 1)) /\
(forall sum1:int, count1:int.
(count1 >= 0 /\ x >= sqr count1) /\ sum1 = sqr (count1 + 1) ->
(if sum1 <= x then forall count2:int.
count2 = (count1 + 1) ->
(forall sum2:int.
sum2 = (sum1 + ((2 * count2) + 1)) ->
((count2 >= 0 /\ x >= sqr count2) /\
sum2 = sqr (count2 + 1)) /\
0 <= (x - count1) /\
(x - count2) < (x - count1))
else (count1 >= 0 /\ sqr count1 <= x) /\ x < sqr (count1 + 1)))))
forall x:int32.
to_int x >= 0 ->
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
in_bounds 0 &&
(forall o1:int32.
to_int o1 = 0 ->
in_bounds 0 &&
(forall o2:int32.
to_int o2 = 0 ->
(forall count:int32.
count = o2 ->
in_bounds 1 &&
(forall o3:int32.
to_int o3 = 1 ->
(forall sum:int32.
sum = o3 ->
((to_int count >= 0 /\
to_int x >= sqr (to_int count + 0)) /\
to_int sum = sqr (to_int count + 1)) /\
(forall sum1:int32, count1:int32.
(to_int count1 >= 0 /\
to_int x >= sqr (to_int count1 + 0)) /\
to_int sum1 = sqr (to_int count1 + 1) ->
(forall result:bool.
(if result = True then to_int sum1 <=
to_int x
else to_int sum1 > to_int x) ->
(if result = True then in_bounds 1 &&
(forall o4:int32.
to_int o4 = 1 ->
in_bounds
(to_int count1 +
to_int o4) &&
(forall o5:
int32.
to_int o5 =
(to_int
count1 +
to_int o4) ->
(forall count2:
int32.
count2 =
o5 ->
in_bounds
1 &&
(forall o6:
int32.
to_int o6 =
1 ->
in_bounds
2 &&
(forall o7:
int32.
to_int o7 =
2 ->
in_bounds
(to_int
o7 *
to_int
count2) &&
(forall o8:
int32.
to_int o8 =
(to_int
o7 *
to_int
count2) ->
in_bounds
(to_int
o8 +
to_int o6) &&
(forall o9:
int32.
to_int o9 =
(to_int
o8 +
to_int o6) ->
in_bounds
(to_int
sum1 +
to_int o9) &&
(forall o10:
int32.
to_int
o10 =
(to_int
sum1 +
to_int o9) ->
(forall sum2:
int32.
sum2 =
o10 ->
((to_int
count2 >=
0 /\
to_int x >=
sqr
(to_int
count2 +
0)) /\
to_int
sum2 =
sqr
(to_int
count2 +
1)) /\
0 <=
(to_int x -
to_int
count1) /\
(to_int x -
to_int
count2) <
(to_int x -
to_int
count1))))))))))
else (to_int count1 >= 0 /\
sqr (to_int count1 + 0) <= to_int x) /\
to_int x < sqr (to_int count1 + 1))))))))))
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 1: Unknown, Unknown, Timeout, Timeout, Timeout
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