Commit 7dfdb1a8 authored by MARCHE Claude's avatar MARCHE Claude

Jessie3: improved support for arrays

parent 0357d64c
......@@ -207,7 +207,7 @@ 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 =
let rec ctype_and_default ty =
match ty with
| TVoid _attr -> Mlw_ty.ity_unit, Mlw_expr.e_void
| TInt (IInt, _attr) ->
......@@ -224,9 +224,9 @@ let ctype_and_default ty =
Self.not_yet_implemented "ctype TInt"
| TFloat (_, _) ->
Self.not_yet_implemented "ctype TFloat"
| TPtr(TInt(_,_), _attr) ->
Self.not_yet_implemented "ctype TPtr(TInt,_)"
(* Mlw_ty.ity_pur map_ts [mlw_int_type ; mlw_int_type], *)
| TPtr(TInt _ as t, _attr) ->
let t,_ = ctype_and_default t in
Mlw_ty.ity_pur map_ts [mlw_int_type ; t], Mlw_expr.e_void
| TPtr(_ty, _attr) ->
Self.not_yet_implemented "ctype TPtr"
| TArray (_, _, _, _) ->
......@@ -693,6 +693,7 @@ let add_decls_as_theory theories id decls =
let th = Theory.create_theory id in
let th = use th int_theory in
let th = use th real_theory in
let th = use th map_theory in
let th = List.fold_left use th theories in
let th = List.fold_left add_decl th (List.rev decls) in
let th = Theory.close_theory th in
......@@ -932,19 +933,17 @@ and lval (host,offset) =
Mlw_expr.e_value v
| Var _, (Field (_, _)|Index (_, _)) ->
Self.not_yet_implemented "lval Var"
| Mem({enode = BinOp((PlusPI|IndexPI),e,i,_ty)}), NoOffset ->
(* e[i] -> Map.get !e i *)
| Mem({enode = BinOp((PlusPI|IndexPI),e,i,ty)}), NoOffset ->
(* e[i] -> Map.get e i *)
let e = expr e in
let ity = match e.Mlw_expr.e_vty with
| Mlw_ty.VTvalue ity -> ity
| Mlw_ty.VTarrow _ -> assert false
let ity =
match ty with
| TPtr(t,_) -> ctype t
| _ -> assert false
in
Mlw_expr.e_lapp map_get [e;expr i] ity
(*
let ty = ctype ty in
let t = Mlw_expr.e_app (mk_get ity ty) [e] in
t (* Mlw_expr.e_lapp map_get [t;expr i] ity *)
*)
let i = expr i in
let i = Mlw_expr.e_lapp int32_to_int [i] mlw_int_type in
Mlw_expr.e_lapp map_get [e;i] ity
| Mem _, _ ->
Self.not_yet_implemented "lval Mem"
......@@ -1274,15 +1273,11 @@ let prog p =
in
let m = use m int_theory in
let m = use m real_theory in
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 = List.fold_left
(fun m f ->
Self.result "making function";
add_pdecl m f)
m (List.rev functions)
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
List.rev (m.Mlw_module.mod_theory :: theories) ;
......
......@@ -62,9 +62,7 @@ let process () =
[ "Z431", "Z3,4.3.1";
"Z32 ", "Z3,3.2";
"C241", "CVC3,2.4.1";
"C22 ", "CVC3,2.2";
"A951", "Alt-Ergo,0.95.1,";
(* "A94", "Alt-Ergo,0.94"; *)
]
in
let theories = ACSLtoWhy3.prog prog in
......@@ -72,8 +70,8 @@ let process () =
List.iter (fun th ->
ACSLtoWhy3.Self.result "running theory 1:";
ACSLtoWhy3.Self.result "@[<hov 2>%a@]" Pretty.print_theory th;
let tasks = Task.split_theory th None None in
ACSLtoWhy3.Self.result "@[<h 0>%a@]"
let tasks = List.rev (Task.split_theory th None None) in
ACSLtoWhy3.Self.result "@[<h 0>Provers: %a@]"
(Pp.print_list Pp.comma
(fun fmt (_n,p,_d) ->
let p = p.Whyconf.prover in
......@@ -81,7 +79,8 @@ let process () =
provers;
let _ =
List.fold_left (fun n t ->
ACSLtoWhy3.Self.result "@[<h 0>Task %d: %a@]" n
let g = Task.task_goal t in
ACSLtoWhy3.Self.result "@[<h 0>Task %d (%s): %a@]" n g.Decl.pr_name.Ident.id_string
(Pp.print_list Pp.comma (fun fmt (_n,p,d) -> run_on_task fmt p d t))
provers;
n+1) 1 tasks
......
/*@ ensures \result == t[0];
/*@ ensures \result == t[0] + 0;
@*/
int f(int t[]) {
return t[0];
......
[kernel] preprocessing with "gcc -C -E -I. tests/basic/app.c"
[jessie3] creating logic symbol 739 (f)
[jessie3] processing function g
[jessie3] created program function g (740)
[jessie3] found 1 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 1 function(s)
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use why3.BuiltIn *)
(* use int.Int *)
(* use real.Real *)
(* use map.Map *)
function f (x:int) : int = x + 1
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.Bool *)
(* use why3.Unit *)
(* use why3.Prelude *)
(* use int.Int *)
(* use real.Real *)
(* use map.Map *)
(* use Global_logic_declarations *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
goal WP_parameter_g : true
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter g): Valid, Valid, Valid, Valid
......@@ -14,12 +14,14 @@
(* use real.Real *)
(* use map.Map *)
function f1 (x:int) : int = (x * x) + 1
lemma l1 : forall x:int. f1 x >= 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] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (l1): Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory BagInt
(* use why3.BuiltIn *)
......@@ -28,6 +30,8 @@
(* use real.Real *)
(* use map.Map *)
(* use Global_logic_declarations *)
type bag
......@@ -52,8 +56,8 @@
lemma l2 : f1 1 = 2
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] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (l2): Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations1
(* use why3.BuiltIn *)
......@@ -62,12 +66,14 @@
(* use real.Real *)
(* use map.Map *)
(* use BagInt *)
lemma union_comm : forall b1:bag, b2:bag. bag_union b1 b2 = bag_union b2 b1
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Unknown, Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (union_comm): Unknown, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -82,10 +88,12 @@
(* use real.Real *)
(* use map.Map *)
(* use Global_logic_declarations1 *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
......@@ -5,8 +5,6 @@
[jessie3] created program function g (743)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] making function
[jessie3] making function
[jessie3] made 2 function(s)
[jessie3] running theory 1:
[jessie3] theory C_Functions
......@@ -22,6 +20,8 @@
(* use real.Real *)
(* use map.Map *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
......@@ -43,7 +43,7 @@
goal WP_parameter_g :
forall x:int32.
0 <= to_int x /\ to_int x <= 100 ->
10 <= to_int x /\ to_int x <= 100 ->
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
......@@ -54,26 +54,10 @@
(forall o2:int32.
to_int o2 = (to_int x - to_int o1) ->
(0 <= to_int o2 /\ to_int o2 <= 1000) &&
(forall ustmp:int32.
(to_int ustmp - to_int o2) > 0 ->
(to_int o - to_int x) >= 0))))
(forall o3:int32.
(to_int o3 - to_int o2) > 0 ->
(forall y:int32. y = o3 -> (to_int y - to_int x) >= 0)))))
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] failure: Exception raised when running provers:
anomaly: Sys.Break
[kernel] Current source was: tests/basic/call.c:16
The full backtrace is:
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Plug-in jessie3 aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130501.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid, Valid, Valid, Valid
......@@ -10,6 +10,8 @@
(* use real.Real *)
(* use map.Map *)
lemma test1 : (2 + 0xa) = 0xc
lemma test_ofl : (0xffffffff + 1) = 0x100000000
......@@ -20,12 +22,12 @@
lemma test4 : 0x1.1p4 = 17.0
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 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid
[jessie3] Task 2 (test_ofl): Valid, Valid, Valid, Valid
[jessie3] Task 3 (test2): Valid, Valid, Valid, Valid
[jessie3] Task 4 (test3): Valid, Valid, Valid, Valid
[jessie3] Task 5 (test4): Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -40,10 +42,12 @@
(* use real.Real *)
(* use map.Map *)
(* use Global_logic_declarations *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[kernel] preprocessing with "gcc -C -E -I. tests/basic/forty-two.c"
[jessie3] processing function f
[jessie3] created program function f (738)
[jessie3] processing function g
[jessie3] created program function g (740)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 2 function(s)
......@@ -18,6 +20,8 @@
(* use real.Real *)
(* use map.Map *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
......@@ -40,6 +44,6 @@
(forall us_retres:int32.
us_retres = o3 -> to_int us_retres = 42)))))
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 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid, Valid, Valid, Valid
......@@ -13,6 +13,8 @@
(* use real.Real *)
(* use map.Map *)
type bag 'x
function occ 'x (bag 'x) : int
......@@ -21,7 +23,7 @@
function bag_union (bag 'x) (bag 'x) : bag 'x
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -36,10 +38,12 @@
(* use real.Real *)
(* use map.Map *)
(* use Bag *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[kernel] preprocessing with "gcc -C -E -I. tests/basic/incr.c"
[jessie3] processing function f
[jessie3] created program function f (738)
[jessie3] processing function h
[jessie3] created program function h (744)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 3 function(s)
......@@ -18,6 +20,8 @@
(* use real.Real *)
(* use map.Map *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
......@@ -47,6 +51,6 @@
to_int o = (to_int g + to_int x) ->
(forall g1:int32. g1 = o -> to_int g1 = (to_int g + to_int x)))
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 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter h): Valid, Valid, Valid, Valid
......@@ -10,6 +10,8 @@
(* use real.Real *)
(* use map.Map *)
lemma test1 : (2 + 2) = 4
lemma test2 : forall x:int. (x * x) >= 0
......@@ -24,14 +26,14 @@
lemma test4r : forall x:real, y:real. (x - y) = (- (y - x))
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 2: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5: Valid, Unknown, Unknown, Valid, Valid
[jessie3] Task 6: Valid, Valid, Valid, Valid, Valid
[jessie3] Task 7: Valid, Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid
[jessie3] Task 2 (test2): Valid, Valid, Valid, Valid
[jessie3] Task 3 (test2r): Valid, Unknown, Valid, Valid
[jessie3] Task 4 (test3): Valid, Valid, Valid, Valid
[jessie3] Task 5 (test3r): Valid, Valid, Valid, Valid
[jessie3] Task 6 (test4): Valid, Valid, Valid, Valid
[jessie3] Task 7 (test4r): Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -46,10 +48,12 @@
(* use real.Real *)
(* use map.Map *)
(* use Global_logic_declarations *)
(* use ref.Ref *)
(* use mach_int.Int32 *)
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
......@@ -18,8 +18,6 @@ int isqrt(int x) {
return count;
}
#if 0
//@ ensures \result == 4;
int main () {
int r;
......@@ -29,7 +27,6 @@ int main () {
return r;
}
#endif
/*
Local Variables:
......
[kernel] preprocessing with "gcc -C -E -I. tests/demo/isqrt.c"
[jessie3] creating logic symbol 739 (sqr)
[jessie3] processing function isqrt
[jessie3] created program function isqrt (740)
[jessie3] processing function main
[jessie3] created program function main (747)
[jessie3] found 1 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 1 function(s)
[jessie3] made 2 function(s)
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use why3.BuiltIn *)
......@@ -12,9 +15,11 @@
(* use real.Real *)
(* use map.Map *)
function sqr (x:int) : int = x * x
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
......@@ -29,6 +34,8 @@
(* use real.Real *)
(* use map.Map *)
(* use Global_logic_declarations *)
(* use ref.Ref *)
......@@ -37,7 +44,7 @@
goal WP_parameter_isqrt :
forall x:int32.
to_int x >= 0 ->
to_int x <= 1000000000 /\ to_int x >= 0 ->
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
......@@ -157,6 +164,22 @@
else (to_int count1 >= 0 /\
sqr (to_int count1 + 0) <= to_int x) /\
to_int x < sqr (to_int count1 + 1))))))))))
goal WP_parameter_main :
in_bounds 0 &&
(forall o:int32.
to_int o = 0 ->
in_bounds 17 &&
(forall o1:int32.
to_int o1 = 17 ->
(to_int o1 <= 1000000000 /\ to_int o1 >= 0) &&
(forall o2:int32.
(to_int o2 >= 0 /\ sqr (to_int o2 + 0) <= to_int o1) /\
to_int o1 < sqr (to_int o2 + 1) ->
(forall r:int32.
r = o2 ->
not to_int r < 4 && not to_int r > 4 && to_int r = 4))))
end
[jessie3] Alt-Ergo 0.95.1, CVC3 2.2, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1: Unknown, Unknown, Timeout, Timeout, Timeout
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter isqrt): Timeout, Timeout, Timeout, Timeout
[jessie3] Task 2 (WP_parameter main): Unknown, Unknown, Valid, Valid
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