Skip to content
Snippets Groups Projects
Commit ce91403b authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] test for logical patterns

parent 0b07515d
No related branches found
No related tags found
No related merge requests found
/* run.config
DONTRUN:
*/
/* run.config_qualif
OPT: -wp-status -wp-prover tip -wp-script dry
*/
/*@
axiomatic Observers {
predicate P(integer x);
}
*/
/*@
requires (x < 1000 && y < 1000 || z < 1000 && t < 1000);
ensures post: P(\result);
assigns \nothing;
*/
int target(unsigned x, unsigned y, unsigned z, unsigned t)
{
return x+y+z+t;
}
/*@
strategy Split: \tactic("Wp.split", \pattern( (A && B) || (C && D) ));
proof Split: post;
*/
# frama-c -wp [...]
[kernel] Parsing logical.i (no preprocessing)
[wp] Running WP plugin...
[wp] [Valid] Goal target_exits (Cfg) (Unreachable)
[wp] [Valid] Goal target_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_target_assigns (Qed)
[wp] [Unsuccess] typed_target_ensures_post (Tactic) (Qed)
[wp] Proved goals: 3 / 4
Terminating: 1
Unreachable: 1
Qed: 1
Unsuccess: 1
------------------------------------------------------------
Function target
------------------------------------------------------------
Goal Post-condition 'post' in 'target':
Assume {
Type: is_uint32(t) /\ is_uint32(x) /\ is_uint32(y) /\ is_uint32(z).
(* Pre-condition *)
Have: ((t <= 999) /\ (z <= 999)) \/ ((x <= 999) /\ (y <= 999)).
}
Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
Prover Script returns Unsuccess
------------------------------------------------------------
Subgoal 1/2:
- Post-condition 'post'
- Split (Case 1/2)
Goal Wp.Tactical.typed_target_ensures_post-0 (generated):
Assume {
Type: is_uint32(t) /\ is_uint32(x) /\ is_uint32(y) /\ is_uint32(z).
(* Case 1/2 *)
When: (t <= 999) /\ (z <= 999).
}
Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
------------------------------------------------------------
Subgoal 2/2:
- Post-condition 'post'
- Split (Case 2/2)
Goal Wp.Tactical.typed_target_ensures_post-1 (generated):
Assume {
Type: is_uint32(t) /\ is_uint32(x) /\ is_uint32(y) /\ is_uint32(z).
(* Case 2/2 *)
When: (x <= 999) /\ (y <= 999).
}
Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
------------------------------------------------------------
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
target 1 - 2 50.0%
------------------------------------------------------------
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