Skip to content

GitLab

why3
why3
Commit e4b9cb9c authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

test on using new bitvector module in Jessie3

parent 18811244
Hide whitespace changes
Inline Side-by-side
Showing with 295 additions and 221 deletions
modules/mach/bv.mlw
View file @ e4b9cb9c
......@@ -16,6 +16,12 @@ module BVCheck_Gen
function udiv t t : t
function urem t t : t
predicate eq t t
predicate ule t t
predicate ult t t
predicate uge t t
predicate ugt t t
val int_check (a:int) : t
requires { 0 <= a < two_power_size }
ensures { to_uint result = a }
......@@ -48,6 +54,66 @@ module BVCheck_Gen
ensures { to_uint result = mod (to_uint a) (to_uint b) }
ensures { result = urem a b }
val eq_check (a b:t) : bool
ensures { match result with
| True -> to_uint a = to_uint b
| False -> to_uint a <> to_uint b
end }
ensures { match result with
| True -> eq a b
| False -> not (eq a b)
end }
val ne_check (a b:t) : bool
ensures { match result with
| True -> to_uint a <> to_uint b
| False -> to_uint a = to_uint b
end }
ensures { match result with
| True -> not (eq a b)
| False -> eq a b
end }
val le_check (a b:t) : bool
ensures { match result with
| True -> to_uint a <= to_uint b
| False -> to_uint a > to_uint b
end }
ensures { match result with
| True -> ule a b
| False -> not (ule a b)
end }
val lt_check (a b:t) : bool
ensures { match result with
| True -> to_uint a < to_uint b
| False -> to_uint a >= to_uint b
end }
ensures { match result with
| True -> ult a b
| False -> not (ult a b)
end }
val ge_check (a b:t) : bool
ensures { match result with
| True -> to_uint a >= to_uint b
| False -> to_uint a < to_uint b
end }
ensures { match result with
| True -> uge a b
| False -> not (uge a b)
end }
val gt_check (a b:t) : bool
ensures { match result with
| True -> to_uint a > to_uint b
| False -> to_uint a <= to_uint b
end }
ensures { match result with
| True -> ugt a b
| False -> not (ugt a b)
end }
end
module BVCheck8
......@@ -63,7 +129,12 @@ module BVCheck8
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem
function urem = urem,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt
end
module BVCheck16
......@@ -79,7 +150,12 @@ module BVCheck16
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem
function urem = urem,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt
end
module BVCheck32
......@@ -95,7 +171,12 @@ module BVCheck32
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem
function urem = urem,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt
end
module BVCheck64
......@@ -111,5 +192,10 @@ module BVCheck64
function sub = sub,
function mul = mul,
function udiv = udiv,
function urem = urem
function urem = urem,
predicate eq = eq,
predicate ule = ule,
predicate ult = ult,
predicate uge = uge,
predicate ugt = ugt
end
src/jessie/ACSLtoWhy3.ml
View file @ e4b9cb9c
......@@ -174,35 +174,40 @@ let int32_module : Mlw_module.modul =
Self.fatal "Module mach.int.Int32 not found"
*)
let int32_module =
Mlw_module.read_module env ["mach";"int"] "Int32"
let uint32_module =
try
Mlw_module.read_module env ["mach";"bv"] "BVCheck32"
with e ->
Self.fatal "Exception raised while loading ref module:@ %a"
Exn_printer.exn_printer e
let int32_type : Why3.Ty.tysymbol =
Mlw_module.ns_find_ts int32_module.Mlw_module.mod_export ["int32"]
let uint32_type : Why3.Ty.tysymbol =
Mlw_module.ns_find_ts uint32_module.Mlw_module.mod_export ["t"]
let int32_to_int : Term.lsymbol = find_ls int32_module "to_int"
let uint32_to_int : Term.lsymbol = find_ls uint32_module "to_uint"
let add32_fun : Mlw_expr.psymbol = find_ps int32_module "infix +"
let uadd32_fun : Mlw_expr.psymbol = find_ps uint32_module "add_check"
let sub32_fun : Mlw_expr.psymbol = find_ps int32_module "infix -"
let usub32_fun : Mlw_expr.psymbol = find_ps uint32_module "sub_check"
let mul32_fun : Mlw_expr.psymbol = find_ps int32_module "infix *"
let umul32_fun : Mlw_expr.psymbol = find_ps uint32_module "mul_check"
let neg32_fun : Mlw_expr.psymbol = find_ps int32_module "prefix -"
(*let neg32_fun : Mlw_expr.psymbol = find_ps uint32_module "prefix -"
*)
let eq32_fun : Mlw_expr.psymbol = find_ps int32_module "eq"
let ueq32_fun : Mlw_expr.psymbol = find_ps uint32_module "eq_check"
let ne32_fun : Mlw_expr.psymbol = find_ps int32_module "ne"
let une32_fun : Mlw_expr.psymbol = find_ps uint32_module "ne_check"
let le32_fun : Mlw_expr.psymbol = find_ps int32_module "infix <="
let ule32_fun : Mlw_expr.psymbol = find_ps uint32_module "le_check"
let lt32_fun : Mlw_expr.psymbol = find_ps int32_module "infix <"
let ult32_fun : Mlw_expr.psymbol = find_ps uint32_module "lt_check"
let ge32_fun : Mlw_expr.psymbol = find_ps int32_module "infix >="
let uge32_fun : Mlw_expr.psymbol = find_ps uint32_module "ge_check"
let gt32_fun : Mlw_expr.psymbol = find_ps int32_module "infix >"
let ugt32_fun : Mlw_expr.psymbol = find_ps uint32_module "gt_check"
let int32ofint_fun : Mlw_expr.psymbol = find_ps int32_module "of_int"
let uint32ofint_fun : Mlw_expr.psymbol = find_ps uint32_module "int_check"
(* mach_int.Int64 module *)
......@@ -259,7 +264,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_uint32_type = Mlw_ty.ity_pur uint32_type []
let mlw_int64_type = Mlw_ty.ity_pur int64_type []
let rec ctype_and_default ty =
......@@ -267,9 +272,9 @@ let rec ctype_and_default ty =
| TVoid _attr -> Mlw_ty.ity_unit, Mlw_expr.e_void
| TInt (IInt, _attr) ->
let n = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
mlw_int32_type,
mlw_uint32_type,
Mlw_expr.e_app
(Mlw_expr.e_arrow int32ofint_fun [mlw_int_type] mlw_int32_type) [n]
(Mlw_expr.e_arrow uint32ofint_fun [mlw_int_type] mlw_uint32_type) [n]
| TInt (ILong, _attr) ->
let n = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
mlw_int64_type,
......@@ -512,7 +517,7 @@ let is_real_type t =
let coerce_to_int ty t =
match ty with
| Linteger -> t
| Ctype(TInt(IInt,_attr)) -> t_app int32_to_int [t]
| Ctype(TInt(IInt,_attr)) -> t_app uint32_to_int [t]
| Ctype(TInt(ILong,_attr)) -> t_app int64_to_int [t]
| _ -> Self.not_yet_implemented "coerce_to_int"
......@@ -561,7 +566,7 @@ let rec term_node ~label t =
begin
match ty, t.term_type with
| Linteger, Ctype(TInt(IInt,_attr)) ->
t_app int32_to_int [t']
t_app uint32_to_int [t']
| Linteger, Ctype(TInt(ILong,_attr)) ->
t_app int64_to_int [t']
| _ ->
......@@ -719,6 +724,7 @@ let rec predicate ~label p =
Self.not_yet_implemented "predicate Pnot"
| Pat (_, _) ->
Self.not_yet_implemented "predicate Pat"
| Pdangling _
| Pseparated _
| Por (_, _)
| Pxor (_, _)
......@@ -920,15 +926,15 @@ let loop_annot a =
let binop op e1 e2 =
let ls,ty,ty' =
match op with
| PlusA -> add32_fun, mlw_int32_type, mlw_int32_type
| MinusA -> sub32_fun, mlw_int32_type, mlw_int32_type
| 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 -> 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
| PlusA -> uadd32_fun, mlw_uint32_type, mlw_uint32_type
| MinusA -> usub32_fun, mlw_uint32_type, mlw_uint32_type
| Mult -> umul32_fun, mlw_uint32_type, mlw_uint32_type
| Lt -> ult32_fun, mlw_uint32_type, Mlw_ty.ity_bool
| Le -> ule32_fun, mlw_uint32_type, Mlw_ty.ity_bool
| Gt -> ugt32_fun, mlw_uint32_type, Mlw_ty.ity_bool
| Ge -> uge32_fun, mlw_uint32_type, Mlw_ty.ity_bool
| Eq -> ueq32_fun, mlw_uint32_type, Mlw_ty.ity_bool
| Ne -> une32_fun, mlw_uint32_type, Mlw_ty.ity_bool
| PlusPI|IndexPI|MinusPI|MinusPP ->
Self.not_yet_implemented "binop plus/minus"
| Div|Mod ->
......@@ -944,7 +950,8 @@ let unop op e =
let ls,ty,ty' =
match op with
| Neg -> (** Unary minus *)
neg32_fun, mlw_int32_type, mlw_int32_type
Self.not_yet_implemented "unop Neg"
(* neg32_fun, mlw_int32_type, mlw_int32_type*)
| BNot -> (** Bitwise complement (~) *)
Self.not_yet_implemented "unop BNot"
| LNot -> (** Logical Not (!) *)
......@@ -962,7 +969,7 @@ let constant c =
in
let n = Mlw_expr.e_const (Number.ConstInt (Literals.integer s)) in
Mlw_expr.e_app
(Mlw_expr.e_arrow int32ofint_fun [mlw_int_type] mlw_int32_type) [n]
(Mlw_expr.e_arrow uint32ofint_fun [mlw_int_type] mlw_uint32_type) [n]
| CInt64(_t,_ikind, _) ->
Self.not_yet_implemented "CInt64"
| CStr _
......@@ -988,7 +995,7 @@ let rec expr e =
Mlw_expr.e_app
(Mlw_expr.e_arrow int64ofint_fun
[mlw_int_type] mlw_int64_type)
[Mlw_expr.e_lapp int32_to_int [e'] mlw_int_type]
[Mlw_expr.e_lapp uint32_to_int [e'] mlw_int_type]
| _ ->
Self.not_yet_implemented "expr CastE"
end
......@@ -1028,7 +1035,7 @@ and lval (host,offset) =
| _ -> assert false
in
let i = expr i in
let i = Mlw_expr.e_lapp int32_to_int [i] mlw_int_type in
let i = Mlw_expr.e_lapp uint32_to_int [i] mlw_int_type in
Mlw_expr.e_lapp map_get [e;i] ity
| Mem _, _ ->
Self.not_yet_implemented "lval Mem"
......@@ -1132,6 +1139,10 @@ let rec stmt s =
[exc_break,v,Mlw_expr.e_void]
| UnspecifiedSequence _ ->
Self.not_yet_implemented "stmt UnspecifiedSequence"
| Throw (_, _) ->
Self.not_yet_implemented "stmt Throw"
| TryCatch (_, _, _) ->
Self.not_yet_implemented "stmt TryCatch"
| TryFinally (_, _, _) ->
Self.not_yet_implemented "stmt TryFinally"
| TryExcept (_, _, _, _) ->
......@@ -1364,7 +1375,7 @@ let prog p =
let m = use m map_theory in
let m = List.fold_left use m theories in
let m = use_module m ref_module in
let m = use_module m int32_module in
let m = use_module m uint32_module in
let m = List.fold_left add_pdecl m (List.rev functions) in
Self.result "made %d function(s)" (List.length functions);
let m = Mlw_module.close_module m in
......
src/jessie/register.ml
View file @ e4b9cb9c
......@@ -69,11 +69,11 @@ let process () =
List.fold_left
(get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
[]
[ "Z431", "Z3,4.3.1";
[ "Z432", "Z3,4.3.2";
"Z32 ", "Z3,3.2";
"C241", "CVC3,2.4.1";
"C414", "CVC4,1.4";
"A952", "Alt-Ergo,0.95.2,";
"A991", "Alt-Ergo,0.99.1,";
]
with e ->
ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a"
......
src/jessie/tests/basic/oracle/app.res.oracle
View file @ e4b9cb9c
......@@ -25,7 +25,7 @@
function f (x:int) : int = x + 1
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn.BuiltIn *)
......@@ -46,9 +46,9 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
goal WP_parameter_g : true
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (WP_parameter g): Valid, Valid, Valid, Valid, Valid
src/jessie/tests/basic/oracle/axiomatic.res.oracle
View file @ e4b9cb9c
......@@ -28,7 +28,7 @@
lemma l1 : forall x:int. f1 x >= 1
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (l1): Valid, Unknown, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory BagInt
......@@ -64,7 +64,7 @@
lemma l2 : f1 1 = 2
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (l2): Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations1
......@@ -80,7 +80,7 @@
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (union_comm): Unknown, Unknown, Unknown, Timeout, Timeout
[jessie3] running theory 1:
[jessie3] theory C_Functions
......@@ -102,6 +102,6 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
src/jessie/tests/basic/oracle/constants.res.oracle
View file @ e4b9cb9c
......@@ -30,7 +30,7 @@
lemma test4 : 0x1.1p4 = 17.0
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (test_ofl): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3 (test2): Valid, Valid, Valid, Valid, Valid
......@@ -56,6 +56,6 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
src/jessie/tests/basic/oracle/forty-two.res.oracle
View file @ e4b9cb9c
......@@ -32,26 +32,23 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
goal WP_parameter_f : (6 * 7) = 42
goal WP_parameter_g :
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
in_bounds 7 &&
(forall o1:int32.
to_int o1 = 7 ->
in_bounds 6 &&
(forall o2:int32.
to_int o2 = 6 ->
in_bounds (to_int o2 * to_int o1) &&
(forall o3:int32.
to_int o3 = (to_int o2 * to_int o1) ->
(forall us_retres:int32.
us_retres = o3 -> to_int us_retres = 42)))))
(0 <= 0 /\ 0 < two_power_size) &&
(to_uint (of_int 0) = 0 ->
(0 <= 7 /\ 7 < two_power_size) && (let o = of_int 7 in
to_uint o = 7 ->
(0 <= 6 /\ 6 < two_power_size) && (let o1 = of_int 6 in
to_uint o1 = 6 ->
(0 <= (to_uint o1 * to_uint o) /\
(to_uint o1 * to_uint o) < two_power_size) &&
(let o2 = mul o1 o in
to_uint o2 = (to_uint o1 * to_uint o) ->
(forall us_retres:t. us_retres = o2 -> to_uint us_retres = 42)))))
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid, Timeout, Valid, Timeout, Timeout
[jessie3] Task 2 (WP_parameter g): Valid, Valid, Valid, Valid, Timeout
src/jessie/tests/basic/oracle/generic.res.oracle
View file @ e4b9cb9c
......@@ -31,7 +31,7 @@
function bag_union (bag 'x) (bag 'x) : bag 'x
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn.BuiltIn *)
......@@ -52,6 +52,6 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
src/jessie/tests/basic/oracle/incr.res.oracle
View file @ e4b9cb9c
......@@ -32,33 +32,32 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
goal WP_parameter_f :
forall x:int32.
to_int x <= 1000000 ->
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
in_bounds 1 &&
(forall o1:int32.
to_int o1 = 1 ->
in_bounds (to_int x + to_int o1) &&
(forall o2:int32.
to_int o2 = (to_int x + to_int o1) ->
(forall us_retres:int32.
us_retres = o2 -> to_int us_retres = (to_int x + 1)))))
forall x:t.
to_uint x <= 1000000 ->
(0 <= 0 /\ 0 < two_power_size) &&
(to_uint (of_int 0) = 0 ->
(0 <= 1 /\ 1 < two_power_size) && (let o = of_int 1 in
to_uint o = 1 ->
(0 <= (to_uint x + to_uint o) /\
(to_uint x + to_uint o) < two_power_size) &&
(let o1 = add x o in
to_uint o1 = (to_uint x + to_uint o) ->
(forall us_retres:t.
us_retres = o1 -> to_uint us_retres = (to_uint x + 1)))))
goal WP_parameter_h :
forall x:int32.
forall g:int32.
(0 <= to_int x /\ to_int x <= 1000000) /\
0 <= to_int g /\ to_int g <= 1000000 ->
in_bounds (to_int g + to_int x) &&
(forall o:int32.
to_int o = (to_int g + to_int x) ->
(forall g1:int32. g1 = o -> to_int g1 = (to_int g + to_int x)))
forall x:t.
forall g:t.
(0 <= to_uint x /\ to_uint x <= 1000000) /\
0 <= to_uint g /\ to_uint g <= 1000000 ->
(0 <= (to_uint g + to_uint x) /\
(to_uint g + to_uint x) < two_power_size) && (let o = add g x in
to_uint o = (to_uint g + to_uint x) ->
(forall g1:t. g1 = o -> to_uint g1 = (to_uint g + to_uint x)))
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter h): Valid, Valid, Valid, Timeout, Timeout
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (WP_parameter f): Valid, Timeout, Valid, Timeout, Timeout
[jessie3] Task 2 (WP_parameter h): Valid, Timeout, Valid, Timeout, Valid
src/jessie/tests/basic/oracle/lemma.res.oracle
View file @ e4b9cb9c
......@@ -34,7 +34,7 @@
lemma test4r : forall x:real, y:real. (x - y) = (- (y - x))
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (test2): Valid, Unknown, Valid, Valid, Valid
[jessie3] Task 3 (test2r): Valid, Unknown, Unknown, Valid, Valid
......@@ -62,6 +62,6 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.99.1, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.2
src/jessie/tests/demo/f91.c
View file @ e4b9cb9c
......@@ -50,8 +50,6 @@ int f91(int n) {
/*
Local Variables:
compile-command: "make rec.why3ide"
compile-command: "frama-c -load-module ../../Jessie3.cmxs -jessie3 f91.c"
End:
*/
src/jessie/tests/demo/oracle/array_max.res.oracle
View file @ e4b9cb9c
......@@ -30,125 +30,108 @@
(* use ref.Ref *)
(* use mach.int.Int32 *)
(* use mach.bv.BVCheck32 *)
goal WP_parameter_max :
forall a:map int int32, len:int32.
to_int len > 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 x:int32.
x = o2 ->
in_bounds 1 &&
(forall o3:int32.
to_int o3 = 1 ->
in_bounds (to_int len - to_int o3) &&
(forall o4:int32.
to_int o4 = (to_int len - to_int o3) ->
(forall y:int32.
y = o4 ->
((0 <= to_int x /\ to_int x <= to_int y) /\
to_int y < to_int len) /\
(forall y1:int32, x1:int32.
(0 <= to_int x1 /\ to_int x1 <= to_int y1) /\
to_int y1 < to_int len ->
(forall result:bool.
(result = True <->
not to_int x1 = to_int y1) ->
(if result = True then forall result1:
bool.
(result1 =
True <->
to_int
(get a
(
to_int x1)) <=
to_int
(get a
(to_int
y1))) ->
(if result1 =
True then
in_bounds 1 &&
(forall o5:
int32.
to_int o5 =
1 ->
in_bounds
(to_int
x1 +
to_int o5) &&
(forall o6:
int32.
to_int o6 =
(to_int
x1 +
to_int o5) ->
(forall x2:
int32.
x2 = o6 ->
((0 <=
to_int x2 /\
to_int x2 <=
to_int y1) /\
to_int y1 <
to_int
forall a:map int t, len:t.
to_uint len > 0 ->
(0 <= 0 /\ 0 < two_power_size) &&
(to_uint (of_int 0) = 0 ->
(0 <= 0 /\ 0 < two_power_size) &&
(to_uint (of_int 0) = 0 ->
(0 <= 0 /\ 0 < two_power_size) && (let o = of_int 0 in
to_uint o = 0 ->
(forall x:t.
x = o ->
(0 <= 1 /\ 1 < two_power_size) && (let o1 = of_int 1 in
to_uint o1 = 1 ->
(0 <= (to_uint len - to_uint o1) /\
(to_uint len - to_uint o1) < two_power_size) &&
(let o2 = sub len o1 in
to_uint o2 = (to_uint len - to_uint o1) ->
(forall y:t.
y = o2 ->
((0 <= to_uint x /\ to_uint