Skip to content
Snippets Groups Projects
Commit fd1eb2c7 authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[wp] unit test for checks

parent da2e73df
No related branches found
No related tags found
No related merge requests found
/* run.config_qualif
OPT: -wp-timeout 1
*/
/*@
axiomatic Th {
predicate P(integer p);
predicate Q(integer q);
predicate R(integer r);
axiom A: \forall integer x; P(x) ==> Q(x);
check lemma C: ko: \forall integer x; Q(x) ==> R(x);
lemma L: ko: \forall integer x; P(x) ==> R(x); // C is not used
}
*/
/*@
axiomatic Cfg {
logic integer F(integer x);
predicate A(integer x);
predicate B(integer x);
predicate CA1(integer x);
predicate CA2(integer x);
predicate CB1(integer x);
predicate CB2(integer x);
axiom AFB: \forall integer x; A(x) ==> B(F(x));
axiom ACB1: \forall integer x; A(x) ==> CB1(F(x));
axiom CA1B2: \forall integer x; CA1(x) ==> CB2(F(x));
}
*/
/*@
ensures \result == F(x);
assigns \nothing;
*/
int f(int x);
/*@
requires A: A(x);
check requires CA1: CA1(x);
check requires CA2: ko: CA2(x);
ensures B: B(\result);
check ensures CB1: CB1(\result);
check ensures CB2: ko: CB2(\result); // CA1 is not used
assigns \nothing;
*/
int job(int x) {
return f(x);
}
/*@
requires A(x);
requires CA1(x);
ensures R: B(\result);
ensures R1: ko: CB1(\result); // CB1 is not used from job
ensures R2: ko: CA2(x); // CA2 is not used from job
assigns \nothing;
*/
int caller(int x)
{
return job(x); // CA2 is not proved
}
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Axiomatic 'Th'
------------------------------------------------------------
Lemma C:
Assume: 'A'
Prove: (P_Q x_0) -> (P_R x_0)
------------------------------------------------------------
Lemma L:
Assume: 'A'
Prove: (P_P x_0) -> (P_R x_0)
------------------------------------------------------------
------------------------------------------------------------
Function caller
------------------------------------------------------------
Goal Post-condition 'R' in 'caller':
Prove: true.
------------------------------------------------------------
Goal Post-condition 'R1,ko' in 'caller':
Assume {
Type: is_sint32(caller_0) /\ is_sint32(x).
(* Pre-condition *)
Have: P_A(x) /\ P_CA1(x).
(* Call 'job' *)
Have: P_B(caller_0).
}
Prove: P_CB1(caller_0).
------------------------------------------------------------
Goal Post-condition 'R2,ko' in 'caller':
Assume {
Type: is_sint32(caller_0) /\ is_sint32(x).
(* Pre-condition *)
Have: P_A(x) /\ P_CA1(x).
(* Call 'job' *)
Have: P_B(caller_0).
}
Prove: P_CA2(x).
------------------------------------------------------------
Goal Assigns nothing in 'caller':
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'caller' (1/2):
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'caller' (2/2):
Call Result at line 65
Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition 'A' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
:
Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition 'CA1' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
:
Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition 'CA2,ko' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
:
Assume { Type: is_sint32(x). (* Pre-condition *) Have: P_A(x) /\ P_CA1(x). }
Prove: P_CA2(x).
------------------------------------------------------------
------------------------------------------------------------
Function job
------------------------------------------------------------
Goal Post-condition 'B' in 'job':
Let x_1 = L_F(x).
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *)
Have: P_A(x).
}
Prove: P_B(x_1).
------------------------------------------------------------
Goal Post-condition 'CB1' in 'job':
Let x_1 = L_F(x).
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *)
Have: P_A(x).
}
Prove: P_CB1(x_1).
------------------------------------------------------------
Goal Post-condition 'CB2,ko' in 'job':
Let x_1 = L_F(x).
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
(* Pre-condition *)
Have: P_A(x).
}
Prove: P_CB2(x_1).
------------------------------------------------------------
Goal Assigns nothing in 'job':
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'job' (1/2):
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'job' (2/2):
Call Result at line 52
Prove: true.
------------------------------------------------------------
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_C_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess
[wp] [Qed] Goal typed_caller_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller_ensures_R1_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_caller_ensures_R2_ko : Unsuccess
[wp] [Qed] Goal typed_caller_assigns_exit : Valid
[wp] [Qed] Goal typed_caller_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_caller_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
[wp] [Qed] Goal typed_caller_call_job_requires_CA1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_requires_CA2_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid
[wp] [Alt-Ergo] Goal typed_job_ensures_CB1 : Valid
[wp] [Alt-Ergo] Goal typed_job_ensures_CB2_ko : Unsuccess
[wp] [Qed] Goal typed_job_assigns_exit : Valid
[wp] [Qed] Goal typed_job_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_job_assigns_normal_part2 : Valid
[wp] Proved goals: 11 / 17
Qed: 9
Alt-Ergo: 2 (unsuccess: 6)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic Th - - 2 0.0%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 3 2 6 83.3%
caller 6 - 9 66.7%
------------------------------------------------------------
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment