From be34f0591944039e53fdf5d55a08cebf08c18d10 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 1 Apr 2020 14:38:32 +0200
Subject: [PATCH] [wp] Adds a test for Memvar initialized and fixes bugs with
ranges
---
src/plugins/wp/MemVar.ml | 58 ++--
src/plugins/wp/ProverWhy3.ml | 7 +-
.../wp/tests/wp_acsl/initialized_memvar.i | 109 +++++++
.../oracle/initialized_memvar.res.oracle | 292 ++++++++++++++++++
.../initialized_memvar.res.oracle | 68 ++++
5 files changed, 502 insertions(+), 32 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/initialized_memvar.i
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 176e1e8eb7c..34f1609ad93 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -726,20 +726,20 @@ struct
(* --- Memory Store --- *)
(* -------------------------------------------------------------------------- *)
- let rec initialization_value value obj =
+ let rec init_value value obj =
match obj with
| C_int _ | C_float _ | C_pointer _ -> value
| C_comp ci ->
let make_term f =
- Cfield (f, KInit), initialization_value value (object_of f.ftype)
+ Cfield (f, KInit), init_value value (object_of f.ftype)
in
Lang.F.e_record (List.map make_term ci.cfields)
| C_array _ as arr ->
Lang.F.e_const Lang.t_int
- (initialization_value value (object_of_array_elem arr))
+ (init_value value (object_of_array_elem arr))
- let initialized_obj = initialization_value e_true
- let uninitialized_obj = initialization_value e_false
+ let initialized_obj = init_value e_true
+ let uninitialized_obj = init_value e_false
let stored seq obj l v = match l with
| Ref x -> noref ~op:"write to" x
@@ -1030,7 +1030,7 @@ struct
let rec initialized_loc sigma obj x ofs =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- e_eq e_true (access_init (get_init_term sigma x) ofs)
+ p_bool (access_init (get_init_term sigma x) ofs)
| C_array { arr_flat=flat } ->
let size = match flat with
| None -> unsized_array ()
@@ -1043,30 +1043,27 @@ struct
let ofs = ofs @ [Field f] in
initialized_loc sigma obj x ofs
in
- Lang.F.e_and (List.map mk_pred ci.cfields)
+ Lang.F.p_conj (List.map mk_pred ci.cfields)
and initialized_range sigma obj x ofs low up =
match obj with
| C_array { arr_element=t } ->
let v = Lang.freshvar ~basename:"i" Lang.t_int in
- let hyp = p_bool (e_and [ (e_leq low (e_var v)) ;
- (e_leq (e_var v) up) ])
- in
+ let hyp = p_and (p_leq low (e_var v)) (p_leq (e_var v) up) in
let obj = Ctypes.object_of t in
let ofs = ofs @ [ Shift(obj, e_var v) ] in
- let sub = p_bool (initialized_loc sigma obj x ofs) in
- e_prop (p_forall [v] (p_imply hyp sub))
- | _ -> raise ShiftMismatch
-
- let insert_in_array_bounds obj low up p =
- match obj with
- | C_array { arr_flat = Some { arr_size } } ->
- let hyp =
- e_and [ (e_leq (e_int 0) low) ;
- (e_leq up (e_int (arr_size - 1))) ]
- in p_imply (p_bool hyp) p
- | C_array { arr_flat = None } ->
- unsized_array ()
- | _ -> raise ShiftMismatch
+ let sub = initialized_loc sigma obj x ofs in
+ Lang.F.p_forall [v] (p_imply hyp sub)
+ | C_comp _ ->
+ let leaf = match Extlib.last ofs with
+ | Field f -> Ctypes.object_of f.ftype
+ | Shift(obj, _) -> obj
+ in
+ begin match leaf with
+ | C_array _ -> initialized_range sigma leaf x ofs low up
+ | _ -> raise ShiftMismatch
+ end
+ | _ ->
+ raise ShiftMismatch
let initialized sigma l =
match l with
@@ -1076,11 +1073,12 @@ struct
| Loc l -> M.initialized sigma.mem (Rloc(obj,l))
| Val(m,x,p) ->
if (x.vformal || x.vglob) then
- p_true
+ try valid_offset RW (vobject m x) p
+ with ShiftMismatch -> shift_mismatch l
else if is_heap_allocated m then
M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
else
- p_bool (initialized_loc sigma obj x p)
+ initialized_loc sigma obj x p
end
| Rrange(l,elt, Some a, Some b) ->
begin match l with
@@ -1088,12 +1086,12 @@ struct
| Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
| Val(m,x,p) ->
try
- let guard = insert_in_array_bounds (vobject m x) a b in
- let p =
+ let in_array = valid_range RW (vobject m x) p (elt, a, b) in
+ let initialized =
if x.vformal || x.vglob then p_true
- else p_bool (initialized_range sigma (vobject m x) x p a b)
+ else initialized_range sigma (vobject m x) x p a b
in
- F.p_imply (F.p_leq a b) (guard p)
+ F.p_imply (F.p_leq a b) (p_and in_array initialized)
with ShiftMismatch ->
if is_heap_allocated m then
let l = mloc_of_loc l in
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 2ce0d949afd..b0fbcf69d08 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -574,9 +574,12 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| ls -> Why3.Term.t_app ls [of_term' cnv a] (of_tau cnv expected)
| exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
end
- | Rdef(l), Data(Comp (c, _),_) , _ -> begin
+ | Rdef(l), Data(Comp (c, k),_) , _ -> begin
(* l is already sorted by field *)
- let s = Lang.comp_id c in
+ let s = match k with
+ | KValue -> Lang.comp_id c
+ | KInit -> Lang.comp_init_id c
+ in
match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) with
| ls ->
let l = List.map (fun (_,t) -> of_term' cnv t) l in
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/initialized_memvar.i
new file mode 100644
index 00000000000..a5b3f6a265e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memvar.i
@@ -0,0 +1,109 @@
+struct S {
+ int x ;
+ int y ;
+} ;
+struct C {
+ int x ;
+ struct S s ;
+ int a[10] ;
+} ;
+
+int x ;
+int a[10] ;
+
+struct C c ;
+struct C ac [10];
+
+void globals(void){
+ // Simple type
+ //@ check qed_ok: \initialized(&x) ;
+
+ // Array type
+ //@ check qed_ok: \initialized(&a) ;
+
+ //@ check qed_ok: \initialized(&a[4]) ;
+ //@ check qed_ko: \initialized(&a[10]) ;
+
+ //@ check qed_ok: \initialized(&a[0 .. 9]) ;
+ //@ check qed_ko: \initialized(&a[0 .. 10]) ;
+
+ // Nested struct type
+ //@ check qed_ok: \initialized(&c) ;
+ //@ check qed_ok: \initialized(&c.s) ;
+ //@ check qed_ok: \initialized(&c.s.y) ;
+
+ //@ check qed_ok: \initialized(&c.a) ;
+ //@ check qed_ok: \initialized(&c.a[4]) ;
+ //@ check qed_ko: \initialized(&c.a[10]) ;
+ //@ check qed_ok: \initialized(&c.a[0 .. 9]) ;
+ //@ check qed_ko: \initialized(&c.a[0 .. 10]) ;
+
+ // Complex accesses
+ // OK
+ //@ check qed_ok: \initialized(&ac[0]);
+ //@ check qed_ok: \initialized(&ac[1].s);
+ //@ check qed_ok: \initialized(&ac[2].s.y);
+ //@ check qed_ok: \initialized(&ac[3].a);
+ //@ check qed_ok: \initialized(&ac[4].a[5]);
+ //@ check qed_ok: \initialized(&ac[1 .. 2]);
+ //@ check provable: \initialized(&ac[2 .. 4].s);
+ //@ check provable: \initialized(&ac[2 .. 6].s.y);
+ //@ check provable: \initialized(&ac[3 .. 7].a);
+ //@ check provable: \initialized(&ac[2 .. 9].a[5 .. 8]);
+
+ // KO
+ //@ check qed_ko: \initialized(&ac[10]);
+ //@ check qed_ko: \initialized(&ac[10].a);
+ //@ check qed_ko: \initialized(&ac[4].a[12]);
+ //@ check qed_ko: \initialized(&ac[0 .. 10]);
+ //@ check not_provable: \initialized(&ac[0 .. 10].s);
+ //@ check not_provable: \initialized(&ac[0 .. 10].a);
+ //@ check not_provable: \initialized(&ac[0 .. 9].a[0 .. 10]);
+}
+
+void locals(void){
+ int x ;
+ int a[2] ;
+
+ struct C c ;
+
+ //@ check qed_ok: !\initialized(&x);
+ //@ check qed_ok: !\initialized(&a);
+ //@ check qed_ok: !\initialized(&c);
+
+ x = 1 ;
+ //@ check qed_ok: \initialized(&x);
+
+ a[0] = 1 ;
+ //@ check qed_ok: \initialized(&a[0]);
+ //@ check qed_ok: !\initialized(&a[1]);
+ //@ check qed_ok: !\initialized(&a);
+
+ a[1] = 2 ;
+ //@ check qed_ok: \initialized(&a[0]);
+ //@ check qed_ok: \initialized(&a[1]);
+ //@ check provable: \initialized(&a);
+
+ c.x = 1 ;
+ //@ check qed_ok: \initialized(&c.x);
+ //@ check qed_ok: !\initialized(&c.s);
+ //@ check qed_ok: !\initialized(&c.a);
+ //@ check qed_ok: !\initialized(&c);
+
+ c.s.x = 1;
+ //@ check qed_ok: \initialized(&c.s.x);
+ //@ check qed_ok: !\initialized(&c.s.y);
+ //@ check qed_ok: !\initialized(&c.s);
+ //@ check qed_ok: !\initialized(&c);
+
+ c.s.y = 1 ;
+ //@ check qed_ok: \initialized(&c.s);
+ //@ check qed_ok: !\initialized(&c);
+
+ c.a[0] = c.a[1] = c.a[2] = c.a[3] = c.a[4] = c.a[5] = c.a[6] = c.a[7] = c.a[8] = 1;
+ //@ check provable: \initialized(&c.a[0..8]) ;
+ //@ check qed_ok: !\initialized(&c);
+
+ c.a[9] = 1 ;
+ //@ check qed_ok: \initialized(&c);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
new file mode 100644
index 00000000000..a243863d16a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
@@ -0,0 +1,292 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_memvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function globals
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 19):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 25):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 27):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 28):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 31):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 32):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 33):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 35):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 36):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 37):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 39):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 43):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 45):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 46):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 47):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 48):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 49):
+Assume { (* Goal *) When: (2 <= i) /\ (i <= 4). }
+Prove: (0 <= i) /\ (i <= 9).
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 50):
+Assume { (* Goal *) When: (2 <= i) /\ (i <= 6). }
+Prove: (0 <= i) /\ (i <= 9).
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 51):
+Assume { (* Goal *) When: (3 <= i) /\ (i <= 7). }
+Prove: (0 <= i) /\ (i <= 9).
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 52):
+Assume { (* Goal *) When: (2 <= i) /\ (5 <= i_1) /\ (i_1 <= 8) /\ (i <= 9). }
+Prove: (0 <= i) /\ (0 <= i_1) /\ (i_1 <= 9).
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 55):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 56):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 57):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 58):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'not_provable' (file tests/wp_acsl/initialized_memvar.i, line 59):
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 10). }
+Prove: i <= 9.
+
+------------------------------------------------------------
+
+Goal Check 'not_provable' (file tests/wp_acsl/initialized_memvar.i, line 60):
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 10). }
+Prove: i <= 9.
+
+------------------------------------------------------------
+
+Goal Check 'not_provable' (file tests/wp_acsl/initialized_memvar.i, line 61):
+Assume { (* Goal *) When: (0 <= i_1) /\ (0 <= i) /\ (i_1 <= 9) /\ (i <= 10).
+}
+Prove: i <= 9.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function locals
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 70):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 71):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 72):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 75):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 78):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 79):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 80):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 83):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 84):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 85):
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 1). }
+Prove: (([false..])[0 <- true][1 <- true][i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 88):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 89):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 90):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 91):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 94):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 95):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 96):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 97):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 100):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 101):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 104):
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 8). }
+Prove: (([false..])[8 <- true][7 <- true][6 <- true][5 <- true][4 <- true][3
+ <- true][2 <- true][1 <- true][0 <- true][i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 105):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 108):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
new file mode 100644
index 00000000000..ea40fb15e88
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -0,0 +1,68 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_memvar.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 54 goals scheduled
+[wp] [Qed] Goal typed_globals_check_qed_ok : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_2 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_3 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko : Unsuccess
+[wp] [Qed] Goal typed_globals_check_qed_ok_4 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_2 : Unsuccess
+[wp] [Qed] Goal typed_globals_check_qed_ok_5 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_6 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_7 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_8 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_9 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_3 : Unsuccess
+[wp] [Qed] Goal typed_globals_check_qed_ok_10 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_4 : Unsuccess
+[wp] [Qed] Goal typed_globals_check_qed_ok_11 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_12 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_13 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_14 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_15 : Valid
+[wp] [Qed] Goal typed_globals_check_qed_ok_16 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_2 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_3 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_4 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_5 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_6 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_7 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_8 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_not_provable : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_not_provable_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_not_provable_3 : Unsuccess
+[wp] [Qed] Goal typed_locals_check_qed_ok : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_2 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_3 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_4 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_5 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_6 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_7 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_8 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_9 : Valid
+[wp] [Alt-Ergo] Goal typed_locals_check_provable : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_10 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_11 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_12 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_13 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_14 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_15 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_16 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_17 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_18 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_19 : Valid
+[wp] [Alt-Ergo] Goal typed_locals_check_provable_2 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_20 : Valid
+[wp] [Qed] Goal typed_locals_check_qed_ok_21 : Valid
+[wp] Proved goals: 43 / 54
+ Qed: 37
+ Alt-Ergo: 6 (unsuccess: 11)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ globals 16 4 31 64.5%
+ locals 21 2 23 100%
+------------------------------------------------------------
--
GitLab