Commit c143bb80 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'stable/scandium'

parents 89037a03 9abcd565
Version number Date of release Notes
============== =============== =====
21.1 (Scandium) 2020, June 25 Bugs fixed
21.0 (Scandium) 2020, June 11
20.0 (Calcium) 2019, December 4
19.1 (Potassium) 2019, September 18 OCaml 4.08 compatibility
......
......@@ -30,6 +30,10 @@ Open Source Release <next-release>
- Eva [2020-05-20] Supports the ACSL mathematical operator \abs
- Kernel [2020-05-18] Support for C11's _Noreturn function specifier
###################################
Open Source Release 21.1 (Scandium)
###################################
###################################
Open Source Release 21.0 (Scandium)
###################################
......@@ -3517,11 +3521,11 @@ Open Source Release 4.1 (Beryllium-20090901)
-! Syntactic_callgraph [2009-08-27] New design of the callgraph in the GUI.
Frama-C now requires ocamlgraph 1.2.
- Logic "reads" clauses on logic functions and predicates, which
disappeared with the introduction of axiomatic blocks, have been
resurected. Beware that the semantics is slightly different
from before: see ACSL document for details. It is used to
automatically generate footprint axioms.
- Logic [2009-08-25]"reads" clauses on logic functions and predicates,
which disappeared with the introduction of axiomatic blocks,
have been ressurrected. Beware that the semantics is slightly
different from before: see ACSL document for details. It is used
to automatically generate footprint axioms.
- GUI [2009-08-18] Improved display of summary information when
selecting a file.
- Kernel [2009-08-05] New options -kernel-help, -kernel-verbose and
......@@ -3980,7 +3984,7 @@ Binary Release 1.0 (Hydrogen-20080302)
Open Source Release 1.0 (Hydrogen-20080301)
###########################################
- First release
- Kernel [2008-03-01] First release.
......
......@@ -228,6 +228,8 @@ case "${STEP}" in
run "cp Changelog $WEBSITE_DIR/src/last-release/Changelog"
run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/wpChangelog"
run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/last-release/wpChangelog"
run "cp src/plugins/e-acsl/doc/Changelog $WEBSITE_DIR/src/eacslChangelog"
run "cp src/plugins/e-acsl/doc/Changelog $WEBSITE_DIR/src/last-release/eacslChangelog"
fi
;&
3)
......
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
version: "21.0+dev"
version: "21.1+dev"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
......@@ -65,7 +65,7 @@ authors: [
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
doc: "http://frama-c.com/download/user-manual-21.0-Scandium.pdf"
doc: "http://frama-c.com/download/user-manual-21.1-Scandium.pdf"
bug-reports: "https://bts.frama-c.com/"
tags: [
"deductive"
......
......@@ -49,7 +49,6 @@ Plugin E-ACSL 21.0 (Scandium)
model analysis is running.
-* E-ACSL [2020-03-10] Fix frama-c/e-acsl#105 about misplaced
`__e_acsl_delete_block` in presence of gotos to return statements.
- E-ACSL [2020-03-09] Improve verdict messages emitted by e_acsl_assert.
-* E-ACSL [2020-03-16] Fix #?1386 and frama-c/e-acsl#91 about the tracking
of variables declared inside the body of switches.
- E-ACSL [2020-02-09] Improve verdict messages emitted by e_acsl_assert.
......@@ -157,7 +156,7 @@ Plugin E-ACSL 16.0 (Sulfur-20171101)
respective shadow spaces.
########################################
Plugin E-ACSL 15.0 (Phosphorus-20170515)
Plugin E-ACSL 15.0 (Phosphorus-20170501)
########################################
- runtime [2017-03-29] The (much more efficient) shadow memory model is
......@@ -184,9 +183,9 @@ Plugin E-ACSL 15.0 (Phosphorus-20170515)
operations in a few cases: the generated code might have
overflowed.
###########################
Plugin E-ACSL 0.8 (Silicon)
###########################
####################################
Plugin E-ACSL 0.8 (Silicon-20161101)
####################################
-* e-acsl-gcc [2016-11-07] Added --rte-select feature to e-acsl-gcc.sh.
-* e-acsl-gcc [2016-08-02] Added --rt-debug feature to e-acsl-gcc.sh.
......@@ -222,9 +221,9 @@ Plugin E-ACSL 0.8 (Silicon)
initialization of tracked memory blocks in the E-ACSL
memory model library.
#############################
Plugin E-ACSL 0.6 (Magnesium)
#############################
######################################
Plugin E-ACSL 0.6 (Magnesium_20151002)
######################################
-* e-acsl-gcc [2016-01-22] Add an e-acsl-gcc.sh option allowing to skip
compilation of original sources.
......@@ -238,9 +237,9 @@ Plugin E-ACSL 0.6 (Magnesium)
-* runtime [2015-11-06] Fix a crash occuring when using a recent libc
while GMP headers provided by E-ACSL are used.
##########################
Plugin E-ACSL 0.5 (Sodium)
##########################
###################################
Plugin E-ACSL 0.5 (Sodium_20150201)
###################################
- E-ACSL [2015-06-01] Support of \freeable. Thus illegal calls to
free (e.g. double free) are detected.
......@@ -256,9 +255,9 @@ o E-ACSL [2014-12-17] Export a minimal API for other plug-ins.
-* E-ACSL [2014-10-27] Add a missing cast when translating an integral
type used in a floating point/real context in an annotation.
##########################
Plugin E-ACSL 0.4.1 (Neon)
##########################
###################################
Plugin E-ACSL 0.4.1 (Neon_20140301)
###################################
-* E-ACSL [2014-08-05] Fix bug #1838 about memset.
-* E-ACSL [2014-08-05] Fix bug #1818 about initialization of globals.
......
......@@ -26,12 +26,19 @@ Plugin WP <next-release>
- WP [2020-06-12] Supports the \initialized ACSL predicate
#########################
Plugin WP 21.1 (Scandium)
#########################
-* WP [2020-06-23] Fixes Coq region function
-* WP [2020-06-23] Fixes MemTyped structure loader for wp-rte
#########################
Plugin WP 21.0 (Scandium)
#########################
- WP [2020-04-10] Full support for Why3 IEEE float library
- WP [2020-04-10] Removed option-wp-check
- WP [2020-04-10] Removed option -wp-check
- WP [2020-04-09] Added smoke tests for dead call (-wp-smoke-dead-call)
- WP [2020-03-23] Added smoke tests for dead code (-wp-smoke-dead-code)
- WP [2020-03-23] Added smoke tests for dead loop (-wp-smoke-dead-loop)
......@@ -41,16 +48,16 @@ Plugin WP 21.0 (Scandium)
- WP [2020-02-21] Why3 prover full-names use ':' instead of ','
- WP [2020-02-20] Fixes handling of LoopCurrent in loop invariants
- WP [2020-02-10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env)
- WP [2020-02-10] Update scripts with FRAMAC_WP_SCRIPT=update and-wp-prover script
- WP [2020-02-10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script
- WP [2020-02-10] Move frame conditions to Type section for better filtering
- WP [2020-02-10] Extended frame conditions to pointers inside compound
- WP [2020-02-10] Extended frame conditions with global C-types
- WP [2019-17-04] Control splitting with-wp-max-split <n>
- WP [2019-17-04] Control splitting with -wp-max-split <n>
- WP [2019-12-19] Fix drivers in different projects
- WP [2019-12-04] Added option-wp-run-all-provers
- WP [2019-12-04] Added option -wp-run-all-provers
- WP [2019-06-04] Checks for inconsistent requires (-wp-smoke-tests)
- WP [2019-01-29] Emit a warning when no goal is generated
- WP [2018-04-17] Limit the number of splits (see-wp-max-split)
- WP [2018-04-17] Limit the number of splits (see -wp-max-split)
- TIP [2018-04-03] Create session directory only on demand
- TIP [2018-03-19] Specification of JSON script format
- WP [2018-03-18] Additional lemma about remainder (mod)
......
......@@ -131,8 +131,8 @@ struct
begin
let prefix = Fun.debug phi in
let sigma = Sigma.create () in
List.iter
(fun chunk ->
List.iteri
(fun i chunk ->
List.iter
(fun (name,triggers,conditions,m1,m2) ->
let mem1 = assigned sigma chunk m1 chunks in
......@@ -151,8 +151,8 @@ struct
[ (Trigger.of_term value1 :: triggers );
(Trigger.of_term value2 :: triggers ) ]
in
let l_name = Pretty_utils.sfprintf "%s_%s_%a"
prefix name Chunk.pretty chunk in
let l_name = Pretty_utils.sfprintf "%s_%s_%a%d"
prefix name Chunk.pretty chunk i in
let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
Definitions.define_lemma {
l_assumed = true ;
......
......@@ -160,6 +160,9 @@ struct
let compare a b = rank a - rank b
let equal = (=)
let pretty fmt c = Format.pp_print_string fmt (name c)
let detailed_pretty fmt = function
| M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
| m -> Format.pp_print_string fmt (name m)
let val_of_chunk = function
| M_int _ | M_char -> L.Int
| M_f32 -> Cfloat.tau_of_float Ctypes.Float32
......@@ -1150,7 +1153,7 @@ and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
let mchunk c =
match c with
| T_init -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KInit)
| _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
| _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.detailed_pretty c, KValue)
let lookup s e =
try mchunk (Tmap.find e s)
......
......@@ -34,7 +34,7 @@ The recommended versions for external provers are:
\begin{tabular}{crlc}
Prover & Versions & Download &\\
\hline
\textsf{Why3} & \verb|1.2.0| &
\textsf{Why3} & \verb|1.3.1| &
\url{http://why3.lri.fr} & \cite{Why3}\\
\textsf{Alt-Ergo} & \verb|2.0.0| &
\url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\
......@@ -48,7 +48,7 @@ Other versions might be supported as well, typically, as far as we know:
\begin{itemize}
\item \textsf{Alt-Ergo} \verb+2.2.0+ and \verb+2.3.0+, although distributed under a non-commercial licence.
% \item \textsf{Coq} \verb+8.7.2+ and \verb+8.8.2+, although proof scripts compatibility can be an issue.
\item \textsf{Why3} \verb+1.0.0+ and \verb+1.1.1+, although only \verb+1.2.0+ is provided with Coq support.
\item \textsf{Why3} \verb+1.3.1+.
\end{itemize}
Other provers, like \textsf{Coq}, \textsf{Gappa}, \textsf{Z3}, \textsf{CVC3},
......
......@@ -249,7 +249,7 @@ Lemma separated_1 :
Admitted.
(* Why3 goal *)
Definition region : array Z.
Definition region : Z -> Z.
Admitted.
(* Why3 goal *)
......@@ -262,7 +262,7 @@ Admitted.
(* Why3 assumption *)
Definition framed (m: farray addr addr) : Prop :=
forall (p:addr), ((region .[ (base (m .[ p ]))] ) <= 0%Z)%Z.
forall (p:addr), ((region (base (m .[ p ])) ) <= 0%Z)%Z.
(* Why3 goal *)
Lemma separated_included :
......
# frama-c -wp -wp-rte -wp-no-let [...]
[kernel] Parsing tests/wp_acsl/struct_fields.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[rte] annotating function foo
[wp] 2 goals scheduled
---------------------------------------------
--- Context 'typed_foo' Cluster 'Chunk'
---------------------------------------------
theory Chunk
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.memory.Memory *)
(* use frama_c_wp.cint.Cint *)
predicate is_sint8_chunk (m:addr -> int) =
forall a:addr. is_sint8 (get m a)
predicate is_sint16_chunk (m:addr -> int) =
forall a:addr. is_sint16 (get m a)
predicate is_sint32_chunk (m:addr -> int) =
forall a:addr. is_sint32 (get m a)
end
---------------------------------------------
--- Context 'typed_foo' Cluster 'S1_X'
---------------------------------------------
theory S1_X
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
type S1_X =
| S1_X1 (F1_X_a:int) (F1_X_b:int) (F1_X_c:int)
(* use frama_c_wp.cint.Cint *)
predicate IsS1_X (s:S1_X) =
(is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
end
---------------------------------------------
--- Context 'typed_foo' Cluster 'Compound'
---------------------------------------------
theory Compound
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.memory.Memory *)
function shiftfield_F1_X_a (p:addr) : addr = shift p 0
function shiftfield_F1_X_b (p:addr) : addr = shift p 1
function shiftfield_F1_X_c (p:addr) : addr = shift p 2
(* use S1_X *)
function Load_S1_X (p:addr) (mchar:addr -> int) (mint:addr -> int) (mint1:
addr -> int) : S1_X =
S1_X1 (get mchar (shiftfield_F1_X_a p)) (get mint (shiftfield_F1_X_b p))
(get mint1 (shiftfield_F1_X_c p))
Q_Load_S1_X_update_Mchar0 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
separated p 3 q 1 ->
Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
Q_Load_S1_X_eqmem_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
eqmem mchar mchar1 q n].
included p 3 q n ->
eqmem mchar mchar1 q n ->
Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
Q_Load_S1_X_havoc_Mchar0 :
forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
addr -> int, n:int, p:addr, q:addr
[Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
separated p 3 q n ->
Load_S1_X p (havoc mchar1 mchar q n) mint mint1
= Load_S1_X p mchar mint mint1
Q_Load_S1_X_update_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
separated p 3 q 1 ->
Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
Q_Load_S1_X_eqmem_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
eqmem mint1 mint2 q n].
included p 3 q n ->
eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
Q_Load_S1_X_havoc_Mint1 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
[Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
separated p 3 q n ->
Load_S1_X p mchar (havoc mint2 mint1 q n) mint
= Load_S1_X p mchar mint1 mint
Q_Load_S1_X_update_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
separated p 3 q 1 ->
Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
Q_Load_S1_X_eqmem_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
eqmem mint1 mint2 q n].
included p 3 q n ->
eqmem mint1 mint2 q n ->
Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
Q_Load_S1_X_havoc_Mint2 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
-> int, n:int, p:addr, q:addr
[Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
separated p 3 q n ->
Load_S1_X p mchar mint (havoc mint2 mint1 q n)
= Load_S1_X p mchar mint mint1
end
[wp:print-generated]
theory WP
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.memory.Memory *)
(* use Chunk *)
(* use S1_X *)
(* use Compound *)
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
addr -> int, a:addr.
region (base a) <= 0 ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
is_sint8_chunk t2 ->
linked t1 ->
sconst t2 ->
cinits t ->
valid_rd t1 a 3 -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rw t1 a 3
end
[wp:print-generated]
theory WP1
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
(* use int.Int *)
(* use int.ComputerDivision *)
(* use real.RealInfix *)
(* use frama_c_wp.qed.Qed *)
(* use map.Map *)
(* use frama_c_wp.memory.Memory *)
(* use Chunk *)
(* use S1_X *)
(* use Compound *)
goal wp_goal :
forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
addr -> int, a:addr.
region (base a) <= 0 ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
is_sint8_chunk t2 ->
linked t1 ->
sconst t2 ->
cinits t -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rd t1 a 3
end
[wp] 2 goals generated
------------------------------------------------------------
Function foo
------------------------------------------------------------
Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0) /\
IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
cinits(Init_0).
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
(* Block In *)
Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
Init_r_0.
}
Prove: valid_rd(Malloc_0, p, 3).
------------------------------------------------------------
Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
Assume {
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
(* Heap *)
Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
cinits(Init_0).
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
(* Block In *)
Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
Init_r_0.
(* Assertion 'rte,mem_access' *)
Have: valid_rd(Malloc_0, p, 3).
(* Initializer *)
Init: a = r.
}
Prove: valid_rw(Malloc_0, p, 3).
------------------------------------------------------------
/* run.config
OPT:-wp-rte -wp-no-let -wp-gen -wp-prover why3 -wp-msg-key print-generated
*/
/* run.config_qualif
DONTRUN:
*/
struct X {
char a ;
short b ;
int c ;
};
void foo(struct X* p){
struct X r = *p ;
*p = r ;
}
\ No newline at end of file
......@@ -60,19 +60,19 @@ theory Compound
function Load_S2_A (p:addr) (mint:addr -> int) : S2_A =
S2_A1 (get mint (shiftfield_F2_A_dummy p))
Q_Load_S2_A_update_Mint :
Q_Load_S2_A_update_Mint0 :
forall mint:addr -> int, p:addr, q:addr, v:int
[Load_S2_A p (set mint q v)].
not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
Q_Load_S2_A_eqmem_Mint :
Q_Load_S2_A_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
eqmem mint mint1 q n].
included p 1 q n ->
eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
Q_Load_S2_A_havoc_Mint :
Q_Load_S2_A_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p (havoc mint1 mint q n)].
separated p 1 q n ->
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/region_to_coq.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 4 goals scheduled
[wp] [Coq] Goal typed_copy_loop_invariant_preserved : Saved script
[wp] [Coq (native)] Goal typed_copy_loop_invariant_preserved : Valid
[wp] [Coq] Goal typed_copy_loop_invariant_established : Saved script
[wp] [Coq (native)] Goal typed_copy_loop_invariant_established : Valid
[wp] [Qed] Goal typed_copy_loop_assigns_part1 : Valid
[wp] [Coq] Goal typed_copy_loop_assigns_part2 : Saved script
[wp] [Coq (native)] Goal typed_copy_loop_assigns_part2 : Valid
[wp] Proved goals: 4 / 4
Qed: 1
Coq (native): 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
copy 1 - 4 100%
------------------------------------------------------------