Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
aa73ade5
Commit
aa73ade5
authored
Sep 16, 2020
by
Loïc Correnson
Browse files
[wp] cleaning goal iterations
parent
23d62745
Changes
97
Hide whitespace changes
Inline
Side-by-side
src/plugins/wp/ProverScript.ml
View file @
aa73ade5
...
...
@@ -394,7 +394,8 @@ let task
begin
fun
()
->
Prover
.
simplify
~
start
~
result
wpo
>>=
fun
succeed
->
if
succeed
then
Task
.
return
()
then
(
success
wpo
(
Some
VCS
.
Qed
)
;
Task
.
return
()
)
else
let
json
=
ProofSession
.
load
wpo
in
let
script
=
Priority
.
sort
(
ProofScript
.
decode
json
)
in
...
...
src/plugins/wp/VC.ml
View file @
aa73ade5
...
...
@@ -97,6 +97,6 @@ let spawn = Prover.spawn ~delayed:true
let
server
=
ProverTask
.
server
let
command
?
provers
?
tip
vcs
=
Register
.
do_wp_proofs
_iter
?
provers
?
tip
(
fun
f
->
Bag
.
iter
f
vcs
)
Register
.
do_wp_proofs
?
provers
?
tip
vcs
(* -------------------------------------------------------------------------- *)
src/plugins/wp/register.ml
View file @
aa73ade5
...
...
@@ -220,11 +220,6 @@ let exercised = ref 0
let
session
=
ref
GOALS
.
empty
let
provers
=
ref
PM
.
empty
let
begin_session
()
=
session
:=
GOALS
.
empty
let
clear_session
()
=
session
:=
GOALS
.
empty
let
end_session
()
=
session
:=
GOALS
.
empty
let
iter_session
f
=
GOALS
.
iter
f
!
session
let
clear_scheduled
()
=
begin
scheduled
:=
0
;
...
...
@@ -260,14 +255,15 @@ let add_time s t =
if
t
>
s
.
u_time
then
s
.
u_time
<-
t
;
end
let
do_list_scheduled
iter_on_
goals
=
let
do_list_scheduled
goals
=
clear_scheduled
()
;
iter
_on_goals
Bag
.
iter
(
fun
goal
->
begin
incr
scheduled
;
session
:=
GOALS
.
add
goal
!
session
;
end
)
;
end
)
goals
;
match
!
scheduled
with
|
0
->
Wp_parameters
.
warning
~
current
:
false
"No goal generated"
|
1
->
Wp_parameters
.
feedback
"1 goal scheduled"
...
...
@@ -544,12 +540,12 @@ type mode = {
mutable
provers
:
(
VCS
.
mode
*
VCS
.
prover
)
list
;
}
let
spawn_wp_proofs
_iter
~
mode
iter_on_
goals
=
let
spawn_wp_proofs
~
mode
goals
=
if
mode
.
tactical
||
mode
.
provers
<>
[]
then
begin
let
server
=
ProverTask
.
server
()
in
ignore
(
Wp_parameters
.
Share
.
get_dir
"."
);
(* To prevent further errors *)
iter
_on_goals
Bag
.
iter
(
fun
goal
->
if
mode
.
tactical
&&
not
(
Wpo
.
is_trivial
goal
)
...
...
@@ -575,7 +571,7 @@ let spawn_wp_proofs_iter ~mode iter_on_goals =
~
result
:
do_wpo_result
~
success
:
do_wpo_success
mode
.
provers
)
;
)
goals
;
Task
.
on_server_wait
server
do_wpo_wait
;
Task
.
launch
server
end
...
...
@@ -642,13 +638,13 @@ let compute_auto ~mode =
if
mode
.
auto
<>
[]
then
mode
.
tactical
<-
true
;
end
let
do_update_session
mode
iter
=
let
do_update_session
mode
goals
=
if
mode
.
update
then
begin
let
removed
=
ref
0
in
let
updated
=
ref
0
in
let
invalid
=
ref
0
in
iter
Bag
.
iter
begin
fun
goal
->
let
results
=
Wpo
.
get_results
goal
in
let
autoproof
(
p
,
r
)
=
...
...
@@ -679,7 +675,7 @@ let do_update_session mode iter =
ProofSession
.
save
goal
(
ProofScript
.
encode
scripts
)
end
end
end
;
end
goals
;
let
r
=
!
removed
in
let
u
=
!
updated
in
let
f
=
!
invalid
in
...
...
@@ -696,7 +692,7 @@ let do_update_session mode iter =
Wp_parameters
.
result
"Updated session with %d new script%s to complete."
f
s
);
end
let
do_wp_proofs
_iter
?
provers
?
tip
iter
=
let
do_wp_proofs
?
provers
?
tip
(
goals
:
Wpo
.
t
Bag
.
t
)
=
let
mode
=
default_mode
()
in
compute_provers
~
mode
;
compute_auto
~
mode
;
...
...
@@ -709,21 +705,17 @@ let do_wp_proofs_iter ?provers ?tip iter =
end
;
let
spawned
=
mode
.
tactical
||
mode
.
provers
<>
[]
in
begin
if
spawned
then
do_list_scheduled
iter
;
spawn_wp_proofs
_iter
~
mode
iter
;
if
spawned
then
do_list_scheduled
goals
;
spawn_wp_proofs
~
mode
goals
;
if
spawned
then
begin
do_list_scheduled_result
()
;
do_update_session
mode
iter
;
do_update_session
mode
goals
;
end
else
if
not
(
Wp_parameters
.
Print
.
get
()
)
then
iter
do_wpo_display
Bag
.
iter
do_wpo_display
goals
end
let
do_wp_proofs
()
=
do_wp_proofs_iter
(
fun
f
->
Wpo
.
iter
~
on_goal
:
f
()
)
let
do_wp_proofs_for
goals
=
do_wp_proofs_iter
(
fun
f
->
Bag
.
iter
f
goals
)
(* registered at frama-c (normal) exit *)
let
do_cache_cleanup
()
=
begin
...
...
@@ -735,38 +727,6 @@ let do_cache_cleanup () =
Wp_parameters
.
result
"[Cache] removed:%d"
removed
end
(* ------------------------------------------------------------------------ *)
(* --- Secondary Entry Points --- *)
(* ------------------------------------------------------------------------ *)
(* Deprecated entry point in Dynamic. *)
let
deprecated_wp_compute
kf
bhv
ipopt
=
let
model
=
computer
()
in
let
goals
=
match
ipopt
with
|
None
->
Generator
.
compute_kf
model
?
kf
~
bhv
()
|
Some
ip
->
Generator
.
compute_ip
model
ip
in
do_wp_proofs_for
goals
let
deprecated_wp_compute_kf
kf
bhv
prop
=
let
model
=
computer
()
in
do_wp_proofs_for
(
Generator
.
compute_kf
model
?
kf
~
bhv
~
prop
()
)
let
deprecated_wp_compute_ip
ip
=
Wp_parameters
.
warning
~
once
:
true
"Dynamic 'wp_compute_ip' is now deprecated."
;
let
model
=
computer
()
in
do_wp_proofs_for
(
Generator
.
compute_ip
model
ip
)
let
deprecated_wp_compute_call
stmt
=
Wp_parameters
.
warning
~
once
:
true
"Dynamic 'wp_compute_ip' is now deprecated."
;
do_wp_proofs_for
(
Generator
.
compute_call
(
computer
()
)
stmt
)
let
deprecated_wp_clear
()
=
Wp_parameters
.
warning
~
once
:
true
"Dynamic 'wp_compute_ip' is now deprecated."
;
Wpo
.
clear
()
(* ------------------------------------------------------------------------ *)
(* --- Command-line Entry Points --- *)
(* ------------------------------------------------------------------------ *)
...
...
@@ -804,22 +764,18 @@ let cmdline_run () =
if
Wp_parameters
.
CachePrint
.
get
()
then
Kernel
.
feedback
"Cache directory: %s"
(
Cache
.
get_dir
()
)
;
let
fct
=
Wp_parameters
.
get_wp
()
in
match
fct
with
|
Wp_parameters
.
Fct_none
->
()
|
Wp_parameters
.
Fct_all
->
begin
ignore
(
wp_main
fct
);
do_wp_proofs
()
;
do_wp_print
()
;
do_wp_report
()
;
end
|
_
->
if
fct
<>
Wp_parameters
.
Fct_none
then
begin
let
goals
=
wp_main
fct
in
do_wp_proofs
goals
;
begin
let
goals
=
wp_main
fct
in
do_wp_proofs_for
goals
;
do_wp_print_for
goals
;
do_wp_report
()
;
end
if
fct
<>
Wp_parameters
.
Fct_all
then
do_wp_print_for
goals
else
do_wp_print
()
;
end
;
do_wp_report
()
;
end
(* ------------------------------------------------------------------------ *)
(* --- Register external functions --- *)
...
...
@@ -836,56 +792,6 @@ let register name ty code =
(
fun
x
->
deprecated
name
;
code
x
)
in
()
(* DEPRECATED *)
let
()
=
let
module
OLS
=
Datatype
.
List
(
Datatype
.
String
)
in
let
module
OKF
=
Datatype
.
Option
(
Kernel_function
)
in
let
module
OP
=
Datatype
.
Option
(
Property
)
in
register
"wp_compute"
(
Datatype
.
func3
OKF
.
ty
OLS
.
ty
OP
.
ty
Datatype
.
unit
)
deprecated_wp_compute
let
()
=
let
module
OKF
=
Datatype
.
Option
(
Kernel_function
)
in
let
module
OLS
=
Datatype
.
List
(
Datatype
.
String
)
in
register
"wp_compute_kf"
(
Datatype
.
func3
OKF
.
ty
OLS
.
ty
OLS
.
ty
Datatype
.
unit
)
deprecated_wp_compute_kf
let
()
=
register
"wp_compute_ip"
(
Datatype
.
func
Property
.
ty
Datatype
.
unit
)
deprecated_wp_compute_ip
let
()
=
register
"wp_compute_call"
(
Datatype
.
func
Cil_datatype
.
Stmt
.
ty
Datatype
.
unit
)
deprecated_wp_compute_call
let
()
=
register
"wp_clear"
(
Datatype
.
func
Datatype
.
unit
Datatype
.
unit
)
deprecated_wp_clear
let
run
=
Dynamic
.
register
~
plugin
:
"Wp"
"run"
(
Datatype
.
func
Datatype
.
unit
Datatype
.
unit
)
~
journalize
:
true
cmdline_run
let
()
=
let
open
Datatype
in
begin
let
t_job
=
func
Unit
.
ty
Unit
.
ty
in
let
t_iter
=
func
(
func
Wpo
.
S
.
ty
Unit
.
ty
)
Unit
.
ty
in
let
register
name
ty
f
=
ignore
(
Dynamic
.
register
name
ty
~
plugin
:
"Wp"
~
journalize
:
false
f
)
in
register
"wp_begin_session"
t_job
begin_session
;
register
"wp_end_session"
t_job
end_session
;
register
"wp_clear_session"
t_job
clear_session
;
register
"wp_iter_session"
t_iter
iter_session
;
end
(* ------------------------------------------------------------------------ *)
(* --- Tracing WP Invocation --- *)
(* ------------------------------------------------------------------------ *)
...
...
src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle
View file @
aa73ade5
...
...
@@ -4,9 +4,6 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_loop_continue_loop_invariant_established : Valid
[wp] [Qed] Goal typed_loop_continue_loop_assigns : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part1 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part2 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_invariant_preserved_part3 : Valid
...
...
@@ -19,6 +16,9 @@
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_loop_switch_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_loop_continue_loop_invariant_established : Valid
[wp] [Qed] Goal typed_loop_continue_loop_assigns : Valid
[wp] Proved goals: 15 / 15
Qed: 15
------------------------------------------------------------
...
...
src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
View file @
aa73ade5
...
...
@@ -10,26 +10,17 @@
[wp] tests/wp/stmtcompiler_test.i:81: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 27 goals scheduled
[wp] [Qed] Goal typed_behavior2_assert : Valid
[wp] [Qed] Goal typed_behavior3_assert : Valid
[wp] [Qed] Goal typed_behavior4_assert : Valid
[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unsuccess
[wp] [Qed] Goal typed_compare_assert : Valid
[wp] [Qed] Goal typed_empty_assert : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unsuccess
[wp] [Qed] Goal typed_if_assert_assert_3 : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unsuccess
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Qed] Goal typed_main_assigns_global_assert : Valid
[wp] [Qed] Goal typed_main_assigns_global_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unsuccess
[wp] [Qed] Goal typed_main_ensures_result_assert : Valid
[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unsuccess
[wp] [Qed] Goal typed_one_assign_assert : Valid
[wp] [Qed] Goal typed_one_if_assert : Valid
[wp] [Qed] Goal typed_some_seq_assert : Valid
[wp] [Qed] Goal typed_some_seq_assert_2 : Valid
[wp] [Qed] Goal typed_main_ensures_result_assert : Valid
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unsuccess
[wp] [Qed] Goal typed_main_assigns_global_assert : Valid
[wp] [Qed] Goal typed_main_assigns_global_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unsuccess
[wp] [Qed] Goal typed_zloop_ensures : Valid
[wp] [Alt-Ergo] Goal typed_zloop_loop_invariant_preserved : Unsuccess
[wp] [Qed] Goal typed_zloop_loop_invariant_established : Valid
...
...
@@ -37,6 +28,15 @@
[wp] [Qed] Goal typed_zloop_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_zloop_assert_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_zloop_assert_bad : Unsuccess
[wp] [Qed] Goal typed_behavior2_assert : Valid
[wp] [Qed] Goal typed_behavior3_assert : Valid
[wp] [Qed] Goal typed_behavior4_assert : Valid
[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unsuccess
[wp] [Alt-Ergo] Goal typed_if_assert_assert : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unsuccess
[wp] [Qed] Goal typed_if_assert_assert_3 : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unsuccess
[wp] [Qed] Goal typed_compare_assert : Valid
[wp] Proved goals: 19 / 27
Qed: 18
Alt-Ergo: 1 (unsuccess: 8)
...
...
src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
View file @
aa73ade5
...
...
@@ -14,44 +14,44 @@
[wp] tests/wp/wp_behav.c:176: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 38 goals scheduled
[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unsuccess
[wp] [Qed] Goal typed_assert_needed_assert_qed_ok_ok_with_hyp : Valid
[wp] [Alt-Ergo] Goal typed_bhv_complete_pos_neg : Valid
[wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unsuccess
[wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_x1_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_assert_qed_ok : Valid
[wp] [Qed] Goal typed_f_x2_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_assert_qed_ok_2 : Valid
[wp] [Qed] Goal typed_local_named_behavior_xpos_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_local_named_behavior_xpos_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal typed_min_complete_bx_by : Valid
[wp] [Qed] Goal typed_min_disjoint_bx_by : Valid
[wp] [Qed] Goal typed_min_bx_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_min_by_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_more_stmt_assigns_ensures_qed_ok_ok_with_hoare : Valid
[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part1 : Valid
[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part2 : Valid
[wp] [Qed] Goal typed_part_stmt_bhv_b1_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unsuccess
[wp] [Alt-Ergo] Goal typed_razT_loop_invariant_qed_ok_preserved : Valid
[wp] [Qed] Goal typed_razT_loop_invariant_qed_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unsuccess
[wp] [Qed] Goal typed_stmt_assigns_ensures : Valid
[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unsuccess
[wp] [Alt-Ergo] Goal typed_bhv_complete_pos_neg : Valid
[wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_requires_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_ok_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal typed_stmt_contract_assigns_requires_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_assigns_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_assigns_assigns : Valid
[wp] [Qed] Goal typed_stmt_contract_assigns_ok_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_assigns_ok_asgn_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_local_named_behavior_xpos_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_local_named_behavior_xpos_ensures_qed_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unsuccess
[wp] [Qed] Goal typed_assert_needed_assert_qed_ok_ok_with_hyp : Valid
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unsuccess
[wp] [Qed] Goal typed_stmt_assigns_ensures : Valid
[wp] [Alt-Ergo] Goal typed_razT_loop_invariant_qed_ok_preserved : Valid
[wp] [Qed] Goal typed_razT_loop_invariant_qed_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unsuccess
[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part1 : Valid
[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part2 : Valid
[wp] [Qed] Goal typed_more_stmt_assigns_ensures_qed_ok_ok_with_hoare : Valid
[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unsuccess
[wp] [Qed] Goal typed_part_stmt_bhv_b1_ensures_qed_ok : Valid
[wp] Proved goals: 32 / 38
Qed: 30
Alt-Ergo: 2 (unsuccess: 6)
...
...
src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
View file @
aa73ade5
...
...
@@ -8,16 +8,16 @@
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_call_g_call_g_requires_qed_ok_Rga : Valid
[wp] [Qed] Goal typed_call_g_call_g_requires_Rgb : Valid
[wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
[wp] [Alt-Ergo] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
[wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_stmt_pre_requires_qed_ok_Rstmt : Valid
[wp] [Qed] Goal typed_call_g_call_g_requires_qed_ok_Rga : Valid
[wp] [Qed] Goal typed_call_g_call_g_requires_Rgb : Valid
[wp] Proved goals: 10 / 10
Qed: 9
Alt-Ergo: 1
...
...
src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
View file @
aa73ade5
...
...
@@ -15,27 +15,27 @@
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_bis_assert_qed_ko_ko1 : Unsuccess
[wp] [Qed] Goal hoare_bts0513_bis_assert_qed_ok_ok : Valid
[wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok_2 : Valid
[wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok_stmt_p : Valid
[wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok : Valid
[wp] [Alt-Ergo] Goal hoare_default_behaviors_assert_rte_signed_overflow : Unsuccess
[wp] [Qed] Goal hoare_default_behaviors_assigns : Valid
[wp] [Qed] Goal hoare_dpd1_assert_qed_ok_A : Valid
[wp] [Alt-Ergo] Goal hoare_dpd1_ensures_qed_ko_Eko : Unsuccess
[wp] [Qed] Goal hoare_dpd1_assigns : Valid
[wp] [Qed] Goal hoare_dpd2_assert_qed_ok_A : Valid
[wp] [Alt-Ergo] Goal hoare_dpd2_ensures_qed_ko_Eko : Unsuccess
[wp] [Qed] Goal hoare_dpd2_assigns : Valid
[wp] [Qed] Goal hoare_
spec_if_ensures
_qed_ok_
2
: Valid
[wp] [Qed] Goal hoare_
dpd2_assert
_qed_ok_
A
: Valid
[wp] [Qed] Goal hoare_spec_if_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_spec_if_assigns : Valid
[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow : Unsuccess
[wp] [Qed] Goal hoare_spec_if_assigns_2 : Valid
[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow_2 : Unsuccess
[wp] [Qed] Goal hoare_spec_if_assigns_3 : Valid
[wp] [Qed] Goal hoare_spec_if_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal hoare_spec_if_cond_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_spec_if_not_cond_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok_stmt_p : Valid
[wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok : Valid
[wp] [Alt-Ergo] Goal hoare_default_behaviors_assert_rte_signed_overflow : Unsuccess
[wp] [Qed] Goal hoare_default_behaviors_assigns : Valid
[wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok_2 : Valid
[wp] Proved goals: 17 / 25
Qed: 17
Alt-Ergo: 0 (unsuccess: 8)
...
...
src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
View file @
aa73ade5
...
...
@@ -36,8 +36,8 @@
goal wp_goal :
forall f:t.
let r = of_f32
(to_f32 (of_f64 f))
in
eq_f
64
f (0x1.
9999999
99999Ap-4:t) -> of_f64 (to_f64 r) = r
let r = of_f32
f
in
eq_f
32
f (0x1.99999Ap-4:t) ->
of_f32 (to_f32 (
of_f64 (to_f64 r)
))
= r
end
[wp:print-generated]
theory WP1
...
...
@@ -67,8 +67,8 @@
goal wp_goal :
forall f:t.
eq_f
64
f (0x1.
9999999
99999Ap-4:t) ->
not of_f
64
f = (
13421773.0 / 13421772
8.0)
eq_f
32
f (0x1.99999Ap-4:t) ->
not of_f
32
f = (
3602879701896397.0 / 3602879701896396
8.0)
end
[wp:print-generated]
theory WP2
...
...
@@ -98,8 +98,7 @@
goal wp_goal :
forall f:t.
eq_f64 f (0x1.999999999999Ap-4:t) ->
of_f64 f = (3602879701896397.0 / 36028797018963968.0)
eq_f32 f (0x1.99999Ap-4:t) -> of_f32 f = (13421773.0 / 134217728.0)
end
[wp:print-generated]
theory WP3
...
...
@@ -128,8 +127,7 @@
(* use frama_c_wp.cfloat.Cfloat *)
goal wp_goal :
forall f:t.
eq_f64 f (0x1.999999999999Ap-4:t) -> not of_f64 f = (1.0 / 10.0)
forall f:t. eq_f32 f (0x1.99999Ap-4:t) -> not of_f32 f = (1.0 / 10.0)
end
[wp:print-generated]
theory WP4
...
...
@@ -159,9 +157,8 @@
goal wp_goal :
forall f:t1.
let r = of_f321 f in
eq_f32 f (0x1.99999Ap-4:t1) ->
of_f321 (to_f321 (of_f641 (to_f641 r))) = r
let r = of_f321 (to_f321 (of_f641 f)) in
eq_f64 f (0x1.999999999999Ap-4:t1) -> of_f641 (to_f641 r) = r
end
[wp:print-generated]
theory WP5
...
...
@@ -191,8 +188,8 @@
goal wp_goal :
forall f:t1.
eq_f
32
f (0x1.99999Ap-4:t1) ->
not of_f
32
1 f = (
3602879701896397.0 /' 3602879701896396
8.0)
eq_f
64
f (0x1.
9999999
99999Ap-4:t1) ->
not of_f
64
1 f = (
13421773.0 /' 13421772
8.0)
end
[wp:print-generated]
theory WP6
...
...
@@ -222,7 +219,8 @@
goal wp_goal :
forall f:t1.
eq_f32 f (0x1.99999Ap-4:t1) -> of_f321 f = (13421773.0 /' 134217728.0)
eq_f64 f (0x1.999999999999Ap-4:t1) ->
of_f641 f = (3602879701896397.0 /' 36028797018963968.0)
end
[wp:print-generated]
theory WP7
...
...
@@ -251,7 +249,8 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
goal wp_goal :
forall f:t1. eq_f32 f (0x1.99999Ap-4:t1) -> not of_f321 f = (1.0 /' 10.0)
forall f:t1.
eq_f64 f (0x1.999999999999Ap-4:t1) -> not of_f641 f = (1.0 /' 10.0)
end
[wp] 8 goals generated
------------------------------------------------------------
...
...
src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
View file @
aa73ade5
...
...
@@ -4,10 +4,37 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 42 goals scheduled
[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
[wp] [Qed] Goal typed_field_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_field_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_comp_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_check_CHECK : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_invariant_CHECK_established : Valid
...
...
@@ -19,33 +46,6 @@
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part1 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part2 : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_loop_assigns_2_part3 : Valid
[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_comp_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
[wp] [Qed] Goal typed_field_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_field_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_initialize_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part3 : Valid
[wp] Proved goals: 42 / 42
Qed: 27
Alt-Ergo: 15
...
...
src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
View file @
aa73ade5
...
...
@@ -4,28 +4,28 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled