Commit d4853948 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[logic] Don't generate spurious contracts with add_assigns ~keep_empty:true

parent 41b2699d
......@@ -184,7 +184,7 @@ class visit_assembly =
let ca =
Logic_const.new_code_annotation (AStmtSpec ([],spec))
in
Annotations.add_code_annot emitter ~kf stmt ca;
Annotations.add_code_annot ~keep_empty:false emitter ~kf stmt ca;
if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
then begin
let active = [] in
......
......@@ -1037,6 +1037,21 @@ let add_ensures e kf ?stmt ?active ?behavior l =
in
extend_behavior e kf ?stmt ?active ?behavior set_bhv
let get_full_spec kf ?stmt ?(behavior=[]) () =
match stmt with
| None ->
(try funspec ~populate:false kf with Not_found -> Cil.empty_funspec())
| Some stmt ->
let filter a =
match a.annot_content with
| AStmtSpec(bhvs,_) when is_same_behavior_set bhvs behavior -> true
| _ -> false
in
(match code_annot ~filter stmt with
| [] -> Cil.empty_funspec ()
| [ { annot_content = AStmtSpec(_,s)} ] -> s
| _ -> Kernel.fatal "More than one contract associated to a statement")
let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
let set_bhv full_bhv e_bhv =
let keep_empty = keep_empty && full_bhv.b_assigns = WritesAny in
......@@ -1059,7 +1074,20 @@ let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
(Property.ip_from_of_behavior kf ki active full_bhv);
)
in
extend_behavior e kf ?stmt ?active ?behavior set_bhv
let old_spec = get_full_spec kf ?stmt ?behavior:active () in
let bhv =
match behavior with
| None -> Cil.find_default_behavior old_spec
| Some name ->
List.find_opt (fun { b_name } -> b_name = name) old_spec.spec_behavior
in
let is_empty =
match bhv with
| None -> true
| Some b -> b.b_assigns = WritesAny
in
if not (keep_empty && is_empty) then
extend_behavior e kf ?stmt ?active ?behavior set_bhv
let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
let ki = kinstr stmt in
......@@ -1153,7 +1181,7 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
of the contract, they do not need any update here.
*)
remove_code_annot_internal emitter ~remove_statuses:false ~kf stmt ca';
fill_tables ca []
fill_tables ca' []
| _ ->
Kernel.fatal
"more than one contract attached to a given statement for \
......
......@@ -7,4 +7,6 @@ void f() {
int i = 0;
/*@ loop assigns i; */
while (i< 10) { i++; }
while (i>0) { i--; }
}
......@@ -3,7 +3,7 @@ open Cil_types
let e1 = Emitter.(create "emitter1" [ Code_annot ] [] [])
let e2 = Emitter.(create "emitter2" [ Code_annot ] [] [])
let add_assigns e kf stmt v =
let mk_assigns e v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
......@@ -11,12 +11,15 @@ let add_assigns e kf stmt v =
term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
in
let id_v = Logic_const.new_identified_term named_term_v in
Annotations.add_code_annot e ~kf stmt
Writes[id_v,FromAny]
let add_assigns ?(keep_empty=false) e kf stmt v =
Annotations.add_code_annot ~keep_empty e ~kf stmt
(Logic_const.new_code_annotation
(AAssigns ([], Writes [id_v, FromAny])));
(AAssigns ([], mk_assigns e v)));
Filecheck.check_ast ("after insertion of loop assigns " ^ v.vname)
let add_allocates e kf stmt v =
let add_allocates ?(keep_empty=false) e kf stmt v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
......@@ -24,7 +27,7 @@ let add_allocates e kf stmt v =
term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
in
let id_v = Logic_const.new_identified_term named_term_v in
Annotations.add_code_annot e ~kf stmt
Annotations.add_code_annot ~keep_empty e ~kf stmt
(Logic_const.new_code_annotation
(AAllocation([],FreeAlloc ([],[id_v]))));
Filecheck.check_ast ("after insertion of loop allocates " ^ v.vname )
......@@ -47,6 +50,12 @@ let main () =
List.find
(fun s -> match s.skind with Loop _ -> true | _ -> false) def.sallstmts
in
let s2 =
List.find
(fun s' -> s!=s' && (match s'.skind with Loop _ -> true | _ -> false))
def.sallstmts
in
let s3 = Kernel_function.find_return kf in
let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
......@@ -55,6 +64,8 @@ let main () =
add_assigns e1 kf s j;
add_assigns e2 kf s k;
add_assigns e1 kf s l;
add_assigns ~keep_empty:true e2 kf s2 j;
Annotations.add_assigns ~keep_empty:true e1 kf ~stmt:s3 (mk_assigns e1 k);
add_allocates e1 kf s p;
add_allocates e2 kf s q;
Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
......
......@@ -13,6 +13,7 @@ void f(void)
loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
*/
while (i < 10) i ++;
while (i > 0) i --;
return;
}
......
Markdown is supported
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