Commit 0d9bf98c authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[logic] add optional keep_empty parameters to add_code_annot

similar semantics as the parameter of same name in
`add_assigns` and `add_allocates` in contracts
parent c1b88c51
......@@ -1087,7 +1087,7 @@ let add_extended e kf ?stmt ?active ?behavior ext =
(** {3 Adding code annotations} *)
let add_code_annot emitter ?kf stmt ca =
let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
(* Kernel.feedback "%a: adding code annot %a with stmt %a (%d)"
Project.pretty (Project.current ())
Code_annotation.pretty ca
......@@ -1165,7 +1165,7 @@ let add_code_annot emitter ?kf stmt ca =
| [ { annot_content = AAssigns(_, assigns') } as ca,_ ] ->
remove_code_annot_internal emitter ~kf stmt ca;
let merged =
merge_assigns ~keep_empty:false assigns' assigns
merge_assigns ~keep_empty assigns' assigns
in
{ a with annot_content = AAssigns (bhvs, merged) }
| _ ->
......@@ -1177,7 +1177,7 @@ let add_code_annot emitter ?kf stmt ca =
match ca_total with
| [] -> Property.ip_of_code_annot kf stmt a
| [ { annot_content = AAssigns (_,assigns') } ] ->
let merged = merge_assigns ~keep_empty:false assigns' assigns in
let merged = merge_assigns ~keep_empty assigns' assigns in
Property.ip_of_code_annot
kf stmt { a with annot_content = AAssigns(bhvs,merged) }
| _ ->
......@@ -1197,7 +1197,7 @@ let add_code_annot emitter ?kf stmt ca =
| l ->
let merge_alloc_ca acc alloc =
match alloc.annot_content with
| AAllocation(_,a) -> merge_allocation ~keep_empty:false acc a
| AAllocation(_,a) -> merge_allocation ~keep_empty acc a
| _ -> acc
in
let alloc' = List.fold_left merge_alloc_ca FreeAllocAny l in
......@@ -1210,7 +1210,7 @@ let add_code_annot emitter ?kf stmt ca =
(Id_loop merged_a) alloc')
in
Extlib.may Property_status.remove ip;
let new_alloc = merge_allocation ~keep_empty:false alloc' alloc in
let new_alloc = merge_allocation ~keep_empty alloc' alloc in
let new_a =
{ a with annot_content = AAllocation(bhvs,new_alloc) }
in
......@@ -1227,7 +1227,7 @@ let add_code_annot emitter ?kf stmt ca =
{ a with annot_content =
AAllocation(
bhvs,
merge_allocation ~keep_empty:false alloc' alloc) }
merge_allocation ~keep_empty alloc' alloc) }
| _ ->
Kernel.fatal
"More than one allocation clause for a statement. \
......
......@@ -261,6 +261,7 @@ val fold_decreases:
(**************************************************************************)
val add_code_annot:
?keep_empty:bool ->
Emitter.t -> ?kf:kernel_function -> stmt -> code_annotation -> unit
(** Add a new code annotation attached to the given statement. If [kf] is
provided, the function runs faster.
......@@ -270,9 +271,16 @@ val add_code_annot:
Trying to associate more than one will result in a merge of the contracts.
The same things happens with loop assigns and allocates/frees.
The [keep_empty] argument is only used for loop assigns
and loop allocates, where it is used to decide whether to add the given
code annot in case the corresponding category was empty. It defaults to
[true], which is sound wrt ACSL semantics of equating an absence of
annotation with assigns/allocates \everything.
There can be at most one loop variant registered per statement.
Attempting to register a second one will result in a fatal error.
@modify Frama-C+dev: add keep_empty argument
*)
val add_assert:
......
......@@ -701,7 +701,7 @@ let emit_all_statuses _ =
let () = Ast.apply_after_computed emit_all_statuses
let add_annotation kf st a =
Annotations.add_code_annot Emitter.end_user ~kf st a;
Annotations.add_code_annot ~keep_empty:false Emitter.end_user ~kf st a;
(* Now check if the annotation is valid by construction
(provided normalization is correct). *)
match a.annot_content with
......@@ -741,7 +741,7 @@ let synchronize_source_annot has_new_stmt kf =
st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
has_new_stmt := true;
Annotations.add_code_annot
Emitter.end_user ~kf st_ann annot;
~keep_empty:false Emitter.end_user ~kf st_ann annot;
(true, st_ann)
end else begin
add_annotation kf st annot;
......
......@@ -123,7 +123,7 @@ let inline_call loc caller callee return args =
fd.sbody.bstmts <- inits @ fd.sbody.bstmts;
end else begin
(* put a statement contract on top of the function's body,
but only after we have assigned the formals. Not that there
but only after we have assigned the formals. Note that there
is no need to rename behaviors: they will only shadow behaviors
of the caller within callee's body, just as we need.
*)
......
......@@ -124,7 +124,8 @@ object(self)
remove;
List.iter
(fun (e, a) ->
Annotations.add_code_annot e ~kf:new_kf stmt a)
Annotations.add_code_annot
~keep_empty:false e ~kf:new_kf stmt a)
add)
self#get_filling_actions
end
......
......@@ -48,7 +48,7 @@ let move kf ~old new_stmt =
List.iter
(fun (e, ca) ->
Annotations.remove_code_annot ~kf e old ca;
Annotations.add_code_annot ~kf e new_stmt ca)
Annotations.add_code_annot ~keep_empty:false ~kf e new_stmt ca)
l;
(* update the gotos of the function jumping to one of the labels *)
let f =
......
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