Commit 41ec8d66 authored by MARCHE Claude's avatar MARCHE Claude

Jessie3: more on machine integers

parent df63b22f
......@@ -36,6 +36,14 @@ val neg (a:t) : t
requires { "expl:integer overflow" in_bounds (- (to_int a)) }
ensures { to_int result = - (to_int a) }
val eq (a:t) (b:t) : bool
requires { true }
ensures { if result = True then to_int a = to_int b else to_int a <> to_int b }
val ne (a:t) (b:t) : bool
requires { true }
ensures { if result = True then to_int a <> to_int b else to_int a = to_int b }
val le (a:t) (b:t) : bool
requires { true }
ensures { if result = True then to_int a <= to_int b else to_int a > to_int b }
......@@ -44,6 +52,14 @@ val lt (a:t) (b:t) : bool
requires { true }
ensures { if result = True then to_int a < to_int b else to_int a >= to_int b }
val ge (a:t) (b:t) : bool
requires { true }
ensures { if result = True then to_int a >= to_int b else to_int a < to_int b }
val gt (a:t) (b:t) : bool
requires { true }
ensures { if result = True then to_int a > to_int b else to_int a <= to_int b }
use import int.ComputerDivision
val div (a:t) (b:t) : t
......
......@@ -144,12 +144,24 @@ let mul32_fun : Mlw_expr.psymbol =
let neg32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["neg"]
let eq32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["eq"]
let ne32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["ne"]
let le32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["le"]
let lt32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["lt"]
let ge32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["ge"]
let gt32_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["gt"]
let int32ofint_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps int32_module.Mlw_module.mod_export ["of_int"]
......@@ -402,14 +414,18 @@ let get_var v =
let program_funs = Hashtbl.create 257
let create_function v args ret_type lambda =
let create_function v args spec ret_type =
let id = Ident.id_fresh v.vname in
let aty = Mlw_ty.vty_arrow args ~spec (Mlw_ty.VTvalue ret_type) in
let ps = Mlw_expr.create_psymbol id aty in
(*
let def = Mlw_expr.create_fun_defn id lambda in
let ps = def.Mlw_expr.fun_ps in
*)
Self.result "created program function %s (%d)" v.vname v.vid;
let arg_ty = List.map (fun v -> v.Mlw_ty.pv_ity) args in
Hashtbl.add program_funs v.vid (ps,arg_ty,ret_type);
def
ps
let get_function v =
try
......@@ -871,8 +887,10 @@ let binop op e1 e2 =
| Mult -> mul32_fun, mlw_int32_type, mlw_int32_type
| Lt -> lt32_fun, mlw_int32_type, Mlw_ty.ity_bool
| Le -> le32_fun, mlw_int32_type, Mlw_ty.ity_bool
| Gt | Ge | Eq | Ne ->
Self.not_yet_implemented "binop comp"
| Gt -> gt32_fun, mlw_int32_type, Mlw_ty.ity_bool
| Ge -> ge32_fun, mlw_int32_type, Mlw_ty.ity_bool
| Eq -> eq32_fun, mlw_int32_type, Mlw_ty.ity_bool
| Ne -> ne32_fun, mlw_int32_type, Mlw_ty.ity_bool
| PlusPI|IndexPI|MinusPI|MinusPP ->
Self.not_yet_implemented "binop plus/minus"
| Div|Mod ->
......@@ -1185,6 +1203,7 @@ let fundecl fdec =
c_letrec = 0;
}
in
let ps = create_function fun_id args spec ret_type in
let body = block body in
let full_body = List.fold_right Mlw_expr.e_let locals body in
let lambda = {
......@@ -1193,8 +1212,8 @@ let fundecl fdec =
l_spec = spec;
}
in
let def = create_function fun_id args ret_type lambda in
Mlw_decl.create_rec_decl [def]
let def = Mlw_expr.create_rec_defn [ps,lambda] in
Mlw_decl.create_rec_decl def
......
......@@ -16,17 +16,18 @@ an element maximal in the array.
*/
/*@ requires len > 0 && \valid(a+(0..(len-1)));
@ ensures 0 <= \result < len &&
@ \forall integer i; 0 <= i < len ==> a[i] <= a[\result];
/*@ requires len > 0;
@ // requires \valid(a+(0..(len-1)));
@ ensures 0 <= \result < len;
@ // ensures \forall integer i; 0 <= i < len ==> a[i] <= a[\result];
@*/
int max(int *a, int len) {
int x = 0;
int y = len-1;
/*@ loop invariant 0 <= x <= y < len &&
@ \forall integer i;
@ 0 <= i < x || y < i < len ==>
@ a[i] <= \max(a[x],a[y]);
/*@ loop invariant 0 <= x <= y < len;
@ // loop invariant \forall integer i;
@ // 0 <= i < x || y < i < len ==>
@ // a[i] <= \max(a[x],a[y]);
@ loop variant y - x;
@*/
while (x != y) {
......
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