Skip to content
Snippets Groups Projects
Commit 0366fc38 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[wp] do not put check requires in environment of other PO for caller

parent 0d2b237b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/wpAnnot.ml
+ 3
− 0
View file @ 0366fc38
......@@ -373,6 +373,9 @@ let kind_to_select config kind id = match kind with
| WpStrategy.AcallPre(goal,fct) ->
let goal = goal && goal_to_select config id in
Some (WpStrategy.AcallPre(goal,fct))
| WpStrategy.AcallCheck(fct) ->
if goal_to_select config id then Some (WpStrategy.AcallCheck fct)
else None
| WpStrategy.AcallPost _ ->
if goal_to_select config id then Some kind else None
| WpStrategy.Ahyp | WpStrategy.AcallHyp _ -> Some kind
......
src/plugins/wp/wpStrategy.ml
+ 58
− 12
View file @ 0366fc38
......@@ -48,10 +48,15 @@ type annot_kind =
| AcallPre of bool * kernel_function
(* annotation is a called function precondition :
to be considered as hyp, and goal if bool=true *)
| AcallCheck of kernel_function
(* annotation is a called function check-only precondition.
to be considered as goal only. *)
| AcallPost of kernel_function
(* annotation is a called function post check :
to be considered as goal only *)
type call_pre_kind = CPhyp | CPgoal | CPboth
(* -------------------------------------------------------------------------- *)
(* --- Annotations for one program point. --- *)
(* -------------------------------------------------------------------------- *)
......@@ -68,7 +73,7 @@ type annots = {
p_both : (bool * WpPropId.pred_info) list;
p_cut : (bool * WpPropId.pred_info) list;
call_hyp : WpPropId.pred_info list ForCall.t; (* post and pre *)
call_pre : (bool * WpPropId.pred_info) list ForCall.t; (* goal only *)
call_pre : (call_pre_kind * WpPropId.pred_info) list ForCall.t;
call_post : WpPropId.pred_info list ForCall.t; (* post goals only (not hyp) *)
call_asgn : WpPropId.assigns_full_info ForCall.t;
a_goal : WpPropId.assigns_full_info;
......@@ -112,10 +117,20 @@ let add_prop acc kind id p =
| Some p -> Some(WpPropId.mk_pred_info id p) in
let add_hyp l = match get_p with None -> l | Some p -> p::l in
let add_goal l = match get_p with None -> l | Some p -> p::l in
let add_both_std goal l =
match get_p with None -> l | Some p -> (goal,p) :: l
in
let add_both goal l =
match get_p with
| None -> l
| Some p -> (goal, p)::l
| Some p ->
let kind = if goal then CPboth else CPhyp in
(kind, p)::l
in
let add_pre l =
match get_p with
| None -> l
| Some p -> (CPgoal, p) :: l
in
let add_for_call fct calls =
let l = try ForCall.find fct calls with Not_found -> [] in
......@@ -123,6 +138,10 @@ let add_prop acc kind id p =
let add_both_call fct goal calls =
let l = try ForCall.find fct calls with Not_found -> [] in
ForCall.add fct (add_both goal l) calls in
let add_pre_call fct calls =
let l = try ForCall.find fct calls with Not_found -> [] in
ForCall.add fct (add_pre l) calls
in
let info = acc.info in
let goal, info = match kind with
| Ahyp ->
......@@ -130,13 +149,15 @@ let add_prop acc kind id p =
| Agoal ->
true, { info with p_goal = add_goal info.p_goal }
| Aboth goal ->
goal, { info with p_both = add_both goal info.p_both }
goal, { info with p_both = add_both_std goal info.p_both }
| AcutB goal ->
goal, { info with p_cut = add_both goal info.p_cut }
goal, { info with p_cut = add_both_std goal info.p_cut }
| AcallHyp fct ->
false, { info with call_hyp = add_for_call fct info.call_hyp }
| AcallPre (goal,fct) ->
goal, { info with call_pre = add_both_call fct goal info.call_pre }
| AcallCheck fct ->
true, { info with call_pre = add_pre_call fct info.call_pre }
| AcallPost fct ->
true, { info with call_post = add_for_call fct info.call_post }
in let acc = { acc with info = info } in
......@@ -212,13 +233,24 @@ let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
let p = normalize id labels ?assumes p in
add_prop acc kind id p
let update_kind kind pre =
if pre.ip_content.tp_only_check then begin
match kind with
| AcallPre(false,_) -> None
| AcallPre(true, kf) -> Some (AcallCheck kf)
| _ -> Some kind
end else Some kind
let add_prop_call_pre acc kind id ~assumes pre =
let labels = NormAtLabels.labels_fct_pre in
let p = Logic_const.pred_of_id_pred pre in
(* assumes can be normalized in the same time *)
let p = Logic_const.pimplies (assumes, p) in
let p = normalize id labels p in
add_prop acc kind id p
match update_kind kind pre with
| None -> acc
| Some kind ->
let labels = NormAtLabels.labels_fct_pre in
let p = Logic_const.pred_of_id_pred pre in
(* assumes can be normalized in the same time *)
let p = Logic_const.pimplies (assumes, p) in
let p = normalize id labels p in
add_prop acc kind id p
let add_prop_call_post acc kind called_kf bhv tkind ~assumes post =
let id = WpPropId.mk_fct_post_id called_kf bhv (tkind, post) in
......@@ -444,6 +476,14 @@ let filter_both l =
p::h_acc, if goal then p::g_acc else g_acc
in List.fold_left add ([], []) l
let filter_both_call l =
let add (h_acc, g_acc) (goal, p) =
match goal with
| CPboth -> p :: h_acc, p :: g_acc
| CPhyp -> p :: h_acc, g_acc
| CPgoal -> h_acc, p :: g_acc
in List.fold_left add ([], []) l
let get_both_hyp_goals annots = filter_both annots.info.p_both
let get_call_hyp annots fct =
......@@ -451,7 +491,7 @@ let get_call_hyp annots fct =
with Not_found -> []
let get_call_pre annots fct =
try filter_both (ForCall.find fct annots.info.call_pre)
try filter_both_call (ForCall.find fct annots.info.call_pre)
with Not_found -> [],[]
let get_call_post annots fct =
......@@ -478,8 +518,14 @@ let pp_annots fmt acc =
Format.fprintf fmt "%s%s: %a@."
k (if b then "" else " (h)") WpPropId.pp_pred_of_pred_info p
in
let pp_pred_c k c p =
let kind = match c with CPboth -> "(h+g)" | CPgoal -> "g" | CPhyp -> "h" in
Format.fprintf fmt "%s%s: %a@."
k kind WpPropId.pp_pred_of_pred_info p
in
let pp_pred_list k l = List.iter (fun p -> pp_pred k true p) l in
let pp_pred_b_list k l = List.iter (fun (b, p) -> pp_pred k b p) l in
let pp_pred_c_list k l = List.iter (fun (c, p) -> pp_pred_c k c p) l in
begin
pp_pred_list "H" acc.p_hyp;
pp_pred_list "G" acc.p_goal;
......@@ -493,7 +539,7 @@ let pp_annots fmt acc =
ForCall.iter
(fun kf bhs ->
let name = "CallPre:" ^ (Kernel_function.get_name kf) in
pp_pred_b_list name bhs)
pp_pred_c_list name bhs)
acc.call_pre;
ForCall.iter
(fun kf asgn ->
......
src/plugins/wp/wpStrategy.mli
+ 3
− 0
View file @ 0366fc38
......@@ -58,6 +58,9 @@ type annot_kind =
| AcallPre of bool * kernel_function
(** annotation is a called function precondition :
to be considered as hyp, and goal if bool=true *)
| AcallCheck of kernel_function
(** annotation is check-only called function precondition.
handled internally by {!add_prop_call_pre} below. *)
| AcallPost of kernel_function
(** annotation is a called function post check :
to be considered as goal only (no hyp) *)
......
tests/spec/generalized_check.i
+ 9
− 5
View file @ 0366fc38
......@@ -3,19 +3,23 @@ OPT: -wp-fct f,main -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
*/
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
/*@ check requires \valid(x);
/*@ check requires f_valid_x: \valid(x);
assigns *x;
check ensures *x == 0;
check ensures f_init_x: *x == 0;
*/
void f(int* x) {
/*@ check \valid(x); */ // can't be proved by WP: we ignore the requires
/*@ check f_valid_ko: \valid(x); */
*x = 0;
}
int main() {
int a = 4;
f(&a);
/*@ check a == 0; */ // can't be proved by WP: we ignore the ensures
volatile int c;
int* p = (void*)0;
if (c) p = &a;
f(p);
/*@ check main_valid_ko: \valid(p); */
/*@ check main_p_content_ko: *p == 0; */
}
void loop () {
......
tests/spec/oracle/generalized_check.res.oracle
+ 66
− 19
View file @ 0366fc38
......@@ -5,15 +5,19 @@
[wp:strategy] take f_assigns *x;
[wp:strategy] [add_node_annots] on <stmt-1>
[wp:strategy] [add_node_annots] on <stmt-2>
[wp:strategy] [add_node_annots] on <stmt-30>
[wp:strategy] [add_node_annots] on <stmt-36>
[wp:strategy] 'main' is the main entry point
[wp:strategy] [add_node_annots] on <stmt-5>
[wp:strategy] [add_node_annots] on <callIn-6>
[wp:strategy] [add_node_annots] on <stmt-6>
[wp:strategy] [add_node_annots] on <testIn-8>
[wp:strategy] [add_node_annots] on <stmt-9>
[wp:strategy] [add_node_annots] on <callIn-11>
[wp:strategy] take main_assigns *x;
[wp:strategy] [add_node_annots] on <callIn-6>
[wp:strategy] [add_node_annots] on <stmt-7>
[wp:strategy] [add_node_annots] on <stmt-8>
[wp:strategy] [add_node_annots] on <stmt-32>
[wp:strategy] [add_node_annots] on <callIn-11>
[wp:strategy] [add_node_annots] on <stmt-12>
[wp:strategy] [add_node_annots] on <stmt-13>
[wp:strategy] [add_node_annots] on <stmt-14>
[wp:strategy] [add_node_annots] on <stmt-38>
[wp] Warning: Missing RTE guards
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
......@@ -88,29 +92,68 @@
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp] 6 goals scheduled
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Failed] Goal typed_f_check
[wp] [Qed] Goal typed_f_ensures : Valid
[wp] [Failed] Goal typed_f_check_f_valid_ko
[wp] [Qed] Goal typed_f_ensures_f_init_x : Valid
[wp] [Failed] Goal typed_lemma_easy_proof
[wp] [Qed] Goal typed_main_call_f_requires : Valid
[wp] [Failed] Goal typed_main_check
[wp] Proved goals: 3 / 6
Qed: 3
[wp] [Failed] Goal typed_main_call_f_requires_f_valid_x
[wp] [Failed] Goal typed_main_check_main_p_content_ko
[wp] [Failed] Goal typed_main_check_main_valid_ko
[wp] Proved goals: 2 / 7
Qed: 2
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
/* Generated by Frama-C */
/*@ check lemma easy_proof: \false;
*/
/*@ check requires \valid(x);
check ensures *\old(x) ≡ 0;
assigns *x; */
/*@ check requires f_valid_x: \valid(x);
check ensures f_init_x: *\old(x) ≡ 0;
assigns *x;
*/
void f(int *x)
{
/*@ check \valid(x); */ ;
/*@ check f_valid_ko: \valid(x); */ ;
*x = 0;
return;
}
......@@ -118,9 +161,13 @@ void f(int *x)
int main(void)
{
int __retres;
int volatile c;
int a = 4;
f(& a);
/*@ check a ≡ 0; */ ;
int *p = (int *)0;
if (c) p = & a;
f(p);
/*@ check main_valid_ko: \valid(p); */ ;
/*@ check main_p_content_ko: *p ≡ 0; */ ;
__retres = 0;
return __retres;
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment