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

[logic] fix handling of alloc clauses in the same way as assigns

parent 792aeaac
......@@ -1103,7 +1103,20 @@ let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
Extlib.may Property_status.register
(Property.ip_allocation_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_allocation = FreeAllocAny
in
if not (keep_empty && is_empty) then
extend_behavior e kf ?stmt ?active ?behavior set_bhv
let add_extended e kf ?stmt ?active ?behavior ext =
let set_bhv _ e_bhv =
......@@ -1235,54 +1248,43 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
"More than one loop assigns clause for a statement. \
Annotations internal state broken.")
| AAllocation (bhvs, alloc) ->
let filter ca =
let filter_ca ca =
match ca.annot_content with
| AAllocation(bhvs',_) -> is_same_behavior_set bhvs bhvs'
| _ -> false
in
(match code_annot ~filter stmt with
let filter e ca = Emitter.equal e emitter && filter_ca ca in
let ca_e = code_annot_emitter ~filter stmt in
let ca_total = code_annot ~filter:filter_ca stmt in
(match ca_total with
| [] when keep_empty -> ()
| [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
| l ->
let merge_alloc_ca acc alloc =
match alloc.annot_content with
| AAllocation(_,a) -> merge_allocation ~keep_empty acc a
| _ -> acc
in
let alloc' = List.fold_left merge_alloc_ca FreeAllocAny l in
let merged_a =
{ ca with annot_content = AAllocation(bhvs,alloc') }
in
let ip =
Property.(
ip_of_allocation kf (Kstmt stmt)
(Id_loop merged_a) alloc')
in
Extlib.may Property_status.remove ip;
let new_alloc = merge_allocation ~keep_empty alloc' alloc in
let new_a =
{ ca with annot_content = AAllocation(bhvs,new_alloc) }
in
let ip =
Property.(
ip_of_allocation
kf (Kstmt stmt) (Id_loop new_a) new_alloc)
in
let emit_a =
match code_annot ~emitter ~filter stmt with
| [] -> ca
| [ { annot_content = AAllocation(_,alloc') } as ca ] ->
| [{ annot_content = AAllocation(_,alloc_total)}] ->
let alloc_e =
match ca_e with
| [] -> FreeAllocAny
| [ { annot_content = AAllocation(_, alloc') } as ca,_ ] ->
remove_code_annot_internal emitter ~kf stmt ca;
{ ca with annot_content =
AAllocation(
bhvs,
merge_allocation ~keep_empty alloc' alloc) }
alloc'
| _ ->
Kernel.fatal
"More than one allocation clause for a statement. \
Annotations internal state broken"
"More than one loop assigns clause for a statement. \
Annotations internal state broken."
in
fill_tables emit_a (Extlib.list_of_opt ip))
(* we have assigns at statement level, just not from this
emitter yet, hence merge at emitter level regardless of keep_empty *)
let merged_e = merge_allocation ~keep_empty:false alloc_e alloc in
let new_a = { ca with annot_content = AAllocation(bhvs,merged_e) } in
let merged_total = merge_allocation ~keep_empty alloc_total alloc in
let ips =
Property.ip_of_code_annot kf stmt
{ ca with annot_content = AAllocation(bhvs,merged_total) }
in
fill_tables new_a ips
| _ ->
Kernel.fatal
"More than one loop assigns clause for a statement. \
Annotations internal state broken.")
| APragma _ | AExtended _ ->
fill_tables ca (Property.ip_of_code_annot kf stmt ca)
......
......@@ -19,7 +19,7 @@ let add_assigns ?(keep_empty=false) e kf stmt v =
(AAssigns ([], mk_assigns e v)));
Filecheck.check_ast ("after insertion of loop assigns " ^ v.vname)
let add_allocates ?(keep_empty=false) e kf stmt v =
let mk_allocates e v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
......@@ -27,9 +27,11 @@ let add_allocates ?(keep_empty=false) 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
FreeAlloc ([],[id_v])
let add_allocates ?(keep_empty=false) e kf stmt v =
Annotations.add_code_annot ~keep_empty e ~kf stmt
(Logic_const.new_code_annotation
(AAllocation([],FreeAlloc ([],[id_v]))));
(Logic_const.new_code_annotation (AAllocation([],mk_allocates e v)));
Filecheck.check_ast ("after insertion of loop allocates " ^ v.vname )
let check_only_one f =
......@@ -61,6 +63,7 @@ let main () =
let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
let r = Cil.makeLocalVar def ~insert:true "r" Cil.intPtrType in
add_assigns e1 kf s j;
add_assigns e2 kf s k;
add_assigns e1 kf s l;
......@@ -68,6 +71,9 @@ let main () =
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;
add_allocates e1 kf s r;
add_allocates ~keep_empty:true e2 kf s2 p;
Annotations.add_allocates ~keep_empty:true e1 kf ~stmt:s3 (mk_allocates e1 k);
Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
Annotations.iter_code_annot (check_only_one Logic_utils.is_allocation) s;
let lassigns =
......
......@@ -2,6 +2,7 @@
/* Generated by Frama-C */
void f(void)
{
int *r;
int *q;
int *p;
int l;
......@@ -10,7 +11,8 @@ void f(void)
int i = 0;
/*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter1: l),
(added_by_emitter2: k);
loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
loop allocates
(added_by_emitter1: p), (added_by_emitter1: r), (added_by_emitter2: q);
*/
while (i < 10) i ++;
while (i > 0) i --;
......
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