diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index dc8a7b04de93c3339b11c2a6491735cc636c6c9f..8a626416fecf5ab947f5dd52142218fb32d3b535 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -62,12 +62,18 @@ type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
exception Parse_error
+(* Where an Eva directive is applied. *)
+type kind =
+ | Here (* The directive is applied when encountered. *)
+ | Stmt (* The directive has effect on the next statement. *)
+ | Loop (* The directive concerns a loop. *)
+
module type Annotation =
sig
type t
val name : string
- val is_loop_annot : bool
+ val kind : kind
val parse : typing_context:Logic_typing.typing_context -> lexpr list -> t
val export : t -> acsl_extension_kind
val import : acsl_extension_kind -> t
@@ -87,16 +93,19 @@ struct
print fmt (import lp)
let () =
- if is_loop_annot then
- Acsl_extension.register_code_annot_next_loop name typer ~printer false
- else
- Acsl_extension.register_code_annot_next_stmt name typer ~printer false
+ let register =
+ match kind with
+ | Here -> Acsl_extension.register_code_annot
+ | Stmt -> Acsl_extension.register_code_annot_next_stmt
+ | Loop -> Acsl_extension.register_code_annot_next_loop
+ in
+ register name typer ~printer false
let get stmt =
let filter_add _emitter annot acc =
match annot.annot_content with
- | Cil_types.AExtended (_, is_loop_annot', {ext_name=name'; ext_kind})
- when name' = name && is_loop_annot' = is_loop_annot ->
+ | Cil_types.AExtended (_, is_loop_annot, {ext_name=name'; ext_kind})
+ when name' = name && is_loop_annot = (kind = Loop) ->
import ext_kind :: acc
| _ -> acc
in
@@ -106,7 +115,7 @@ struct
let loc = Cil_datatype.Stmt.loc stmt in
let param = M.export annot in
let extension = Logic_const.new_acsl_extension name loc false param in
- let annot_node = Cil_types.AExtended ([], is_loop_annot, extension) in
+ let annot_node = Cil_types.AExtended ([], kind = Loop, extension) in
let code_annotation = Logic_const.new_code_annotation annot_node in
Annotations.add_code_annot emitter stmt code_annotation
end
@@ -116,7 +125,7 @@ module Slevel = Register (struct
type t = slevel_annotation
let name = "slevel"
- let is_loop_annot = false
+ let kind = Here
let parse ~typing_context:_ = function
| [{lexpr_node = PLvar "default"}] -> SlevelDefault
@@ -161,7 +170,7 @@ module Unroll = Register (struct
type t = unroll_annotation
let name = "unroll"
- let is_loop_annot = true
+ let kind = Loop
let parse ~typing_context = function
| [] -> UnrollFull
@@ -191,6 +200,8 @@ struct
when possible, to avoid changes due to its reconversion to a C term. *)
type t = split_term * Cil_types.term option
+ let kind = Here
+
let term_to_exp = Logic_to_c.term_to_exp ?result:None
let parse ~typing_context:context = function
@@ -231,19 +242,16 @@ end
module Split = Register (struct
include SplitTermAnnotation
let name = "split"
- let is_loop_annot = false
end)
module Merge = Register (struct
include SplitTermAnnotation
let name = "merge"
- let is_loop_annot = false
end)
module DynamicSplit = Register (struct
include SplitTermAnnotation
let name = "dynamic_split"
- let is_loop_annot = false
end)
let get_slevel_annot stmt =
@@ -275,7 +283,7 @@ let add_flow_annot ~emitter stmt flow_annotation =
module Subdivision = Register (struct
type t = int
let name = "subdivide"
- let is_loop_annot = false
+ let kind = Stmt
let parse ~typing_context:_ = function
| [{lexpr_node = PLconstant (IntConstant i)}] ->
@@ -316,7 +324,7 @@ module Allocation = struct
include Register (struct
type t = allocation_kind
let name = "eva_allocate"
- let is_loop_annot = false
+ let kind = Stmt
let parse ~typing_context:_ = function
| [{lexpr_node = PLvar s}] -> Extlib.the ~exn:Parse_error (of_string s)
@@ -356,7 +364,7 @@ let get_allocation = Allocation.get
module ArraySegmentation = Register (struct
type t = Cil_types.varinfo * Cil_types.offset * Cil_types.exp list
let name = "array_partition"
- let is_loop_annot = false
+ let kind = Here
let convert = function
| {term_node = TLval (TVar {lv_origin=Some vi}, toffset)} :: tbounds ->
@@ -402,7 +410,7 @@ let read_array_segmentation ext = ArraySegmentation.import ext.ext_kind
module DomainScope = Register (struct
type t = string * Cil_types.varinfo list
let name = "eva_domain_scope"
- let is_loop_annot = false
+ let kind = Here
let parse ~typing_context:context =
let parse_domain = function
diff --git a/tests/value/oracle/local_slevel.res.oracle b/tests/value/oracle/local_slevel.res.oracle
index ed3e146882954d10d8006e8bff555354f887b127..8dfd964a3ce6047ef3a8f0a901faa3d9209f784f 100644
--- a/tests/value/oracle/local_slevel.res.oracle
+++ b/tests/value/oracle/local_slevel.res.oracle
@@ -78,7 +78,7 @@
[eva] local_slevel.i:37: Frama_C_show_each: {47}
[eva] local_slevel.i:37: Frama_C_show_each: {48}
[eva] local_slevel.i:37: Frama_C_show_each: {49}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 100 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 100 states
[eva] local_slevel.i:37: Frama_C_show_each: {50}
[eva] local_slevel.i:37: Frama_C_show_each: {51}
[eva] local_slevel.i:37: Frama_C_show_each: {52}
@@ -129,7 +129,7 @@
[eva] local_slevel.i:37: Frama_C_show_each: {97}
[eva] local_slevel.i:37: Frama_C_show_each: {98}
[eva] local_slevel.i:37: Frama_C_show_each: {99}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 200 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 200 states
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main
@@ -185,7 +185,7 @@ void main1(void)
while (i < 80) {
/*@ ensures \true;
assigns v; */
- /*@ slevel 50; */
+ /*@ slevel 50; */ ;
if (i % 2) v = 1; else v = -1;
Frama_C_show_each(v,i,r);
v *= v;
@@ -251,7 +251,7 @@ void main1(void)
while (i < 80) {
/*@ ensures \true;
assigns v; */
- /*@ slevel 50; */
+ /*@ slevel 50; */ ;
if (i % 2) v = 1; else v = -1;
Frama_C_show_each(v,i,r);
v *= v;
@@ -317,7 +317,7 @@ void main1(void)
while (i < 80) {
/*@ ensures \true;
assigns v; */
- /*@ slevel 50; */
+ /*@ slevel 50; */ ;
if (i % 2) v = 1; else v = -1;
Frama_C_show_each(v,i,r);
v *= v;
@@ -446,7 +446,7 @@ void main(void)
[eva] local_slevel.i:37: Frama_C_show_each: {47}
[eva] local_slevel.i:37: Frama_C_show_each: {48}
[eva] local_slevel.i:37: Frama_C_show_each: {49}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 100 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 100 states
[eva] local_slevel.i:37: Frama_C_show_each: {50}
[eva] local_slevel.i:37: Frama_C_show_each: {51}
[eva] local_slevel.i:37: Frama_C_show_each: {52}
@@ -497,7 +497,7 @@ void main(void)
[eva] local_slevel.i:37: Frama_C_show_each: {97}
[eva] local_slevel.i:37: Frama_C_show_each: {98}
[eva] local_slevel.i:37: Frama_C_show_each: {99}
-[eva] local_slevel.i:43: Trace partitioning superposing up to 200 states
+[eva] local_slevel.i:42: Trace partitioning superposing up to 200 states
[eva] Recording results for main2
[eva] Done for function main2
[eva] Recording results for main