Commit d73368e3 authored by MARCHE Claude's avatar MARCHE Claude

Jessie3 : new examples

parent 66958c36
......@@ -44,9 +44,9 @@ use import int.ComputerDivision
val div (a:t) (b:t) : t
requires { "expl:division by zero" to_int b <> 0 }
requires { "expl:integer overflow"
requires { "expl:integer overflow"
in_bounds (ComputerDivision.div (to_int a) (to_int b)) }
ensures {
ensures {
to_int result = ComputerDivision.div (to_int a) (to_int b) }
end
......@@ -62,8 +62,8 @@ constant min_int32 : int = - 0x80000000
constant max_int32 : int = 0x7fffffff
clone export Bounded_int with
type t = int32,
clone export Bounded_int with
type t = int32,
constant min = min_int32,
constant max = max_int32
......@@ -77,10 +77,30 @@ constant min_uint32 : int = 0x00000000
constant max_uint32 : int = 0xffffffff
clone export Bounded_int with
type t = uint32,
clone export Bounded_int with
type t = uint32,
constant min = min_uint32,
constant max = max_uint32
end
module Int64
use import int.Int
type int64
constant min_int64 : int = - 0x8000000000000000
constant max_int64 : int = 0x7fffffffffffffff
clone export Bounded_int with
type t = int64,
constant min = min_int64,
constant max = max_int64
end
......@@ -119,7 +119,7 @@ let set_fun : Mlw_expr.psymbol =
(* mach_int.Int32 module *)
let mach_int_modules, mach_int_theories =
let mach_int_modules, _mach_int_theories =
Env.read_lib_file (Mlw_main.library_of_env env) ["mach_int"]
let int32_module : Mlw_module.modul = Stdlib.Mstr.find "Int32" mach_int_modules
......@@ -148,6 +148,37 @@ let lt32_fun : Mlw_expr.psymbol =
let int32ofint_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["of_int"]
(* mach_int.Int64 module *)
let mach_int_modules, mach_int_theories =
Env.read_lib_file (Mlw_main.library_of_env env) ["mach_int"]
let int64_module : Mlw_module.modul = Stdlib.Mstr.find "Int64" mach_int_modules
let int64_type : Why3.Ty.tysymbol =
Mlw_module.ns_find_ts int64_module.Mlw_module.mod_export ["int64"]
let int64_to_int : Term.lsymbol =
find int64_module.Mlw_module.mod_theory "to_int"
let add64_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["add"]
let sub64_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["sub"]
let mul64_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["mul"]
let le64_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["le"]
let lt64_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["lt"]
let int64ofint_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int64_module.Mlw_module.mod_export ["of_int"]
(* array.Array module *)
(*
......@@ -174,6 +205,7 @@ let array_type : Mlw_ty.T.itysymbol =
let unit_type = Ty.ty_tuple []
let mlw_int_type = Mlw_ty.ity_pur Ty.ts_int []
let mlw_int32_type = Mlw_ty.ity_pur int32_type []
let mlw_int64_type = Mlw_ty.ity_pur int64_type []
let ctype_and_default ty =
match ty with
......@@ -183,6 +215,11 @@ let ctype_and_default ty =
mlw_int32_type,
Mlw_expr.e_app
(Mlw_expr.e_arrow int32ofint_fun [mlw_int_type] mlw_int32_type) [n]
| TInt (ILong, _attr) ->
let n = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
mlw_int64_type,
Mlw_expr.e_app
(Mlw_expr.e_arrow int64ofint_fun [mlw_int_type] mlw_int64_type) [n]
| TInt (_, _) ->
Self.not_yet_implemented "ctype TInt"
| TFloat (_, _) ->
......
/* run.config
OPT: -journal-disable -jessie3
*/
//@ logic integer sum_upto(integer n) = n*(n+1) / 2;
/*@ lemma sum_rec: \forall integer n; n >=0 ==>
@ sum_upto(n+1) == sum_upto(n)+n+1;
@*/
/*@ requires 0 <= x <= 60000;
@ decreases x;
@ ensures \result == sum_upto(x+0);
@*/
long sum(int x) {
if (x == 0) return 0;
else return x + sum (x-1);
}
/*@ ensures \result == 36;
@*/
long main () {
long i = sum(8);
return i;
}
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 rec.c"
End:
*/
/* run.config
OPT: -journal-disable -jessie3
*/
/* Dijkstra's dutch flag */
typedef enum Color {BLUE = 1, WHITE = 2, RED = 3 } color;
/*@ predicate is_color(color c) =
@ c == BLUE || c == WHITE || c == RED ;
@*/
/*@ predicate is_color_array{L}(color *t, integer l) =
@ \valid(t+(0..(l-1))) &&
@ \forall integer i; 0 <= i < l ==> is_color(t[i]) ;
@*/
/*@ predicate is_monochrome{L}(color *t,integer i, integer j, color c) =
@ \forall integer k; i <= k < j ==> t[k] == c ;
@*/
/*@ requires \valid(t+(i..j));
@ behavior decides_monochromatic:
@ ensures \result <==> is_monochrome(t,i,j,c);
@*/
int isMonochrome(color t[], int i, int j, color c) {
/*@ loop invariant i <= k &&
@ \forall integer l; i <= l < k ==> t[l] == c;
@ loop variant j - k;
@*/
for (int k = i; k < j; k++) if (t[k] != c) return 0;
return 1;
}
/*@ requires \valid(t+i);
@ requires \valid(t+j);
@ behavior i_j_swapped:
@ assigns t[i],t[j];
@ ensures t[i] == \old(t[j]) && t[j] == \old(t[i]);
@*/
void swap(color t[], int i, int j) {
color z = t[i];
t[i] = t[j];
t[j] = z;
}
/*@ requires l >= 0 && is_color_array(t, l);
@ behavior sorts:
@ ensures
@ (\exists integer b,r;
@ is_monochrome(t,0,b,BLUE) &&
@ is_monochrome(t,b,r,WHITE) &&
@ is_monochrome(t,r,l,RED));
@*/
void flag(color t[], int l) {
int b = 0;
int i = 0;
int r = l;
/*@ loop invariant
@ is_color_array(t,l) &&
@ 0 <= b <= i <= r <= l &&
@ is_monochrome(t,0,b,BLUE) &&
@ is_monochrome(t,b,i,WHITE) &&
@ is_monochrome(t,r,l,RED);
@ loop variant r - i;
@*/
while (i < r) {
switch (t[i]) {
case BLUE:
swap(t,b++, i++);
break;
case WHITE:
i++;
break;
case RED:
swap(t,--r, i);
break;
}
}
}
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 flag.c"
End:
*/
......@@ -12,7 +12,7 @@
int isqrt(int x) {
int count = 0, sum = 1;
/*@ loop invariant count >= 0 && x >= sqr(count+0) && sum == sqr(count+1);
@ loop variant x - count;
@ loop variant x - count;
@*/
while (sum <= x) { ++count; sum += 2 * count + 1; }
return count;
......
/* run.config
OPT: -journal-disable -jessie3
*/
/*@ decreases 101-n ;
@ behavior less_than_101:
@ assumes n <= 100;
@ ensures \result == 91;
@ behavior greater_than_100:
@ assumes n >= 101;
@ ensures \result == n - 10;
@*/
int f91(int n) {
if (n <= 100) {
return f91(f91(n + 11));
}
else
return n - 10;
}
/*
Local Variables:
compile-command: "frama-c -add-path ../.. -jessie3 mccarthy.c"
End:
*/
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