diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index a11a0dca9aa2bab2ab56cfc918b2dbb915cd0c8e..dc8c0bae4f7a55464e4331bbacf81ef69aa63e0e 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -66,3 +66,34 @@ module Unit_tests: sig
(** Runs the unit tests of Eva. *)
val run: unit -> unit
end
+
+(** Register special annotations to locally guide the partitioning of states
+ performed by an Eva analysis. *)
+module Eva_annotations: sig
+
+ (** Annotations tweaking the behavior of the -eva-slevel paramter. *)
+ type slevel_annotation =
+ | SlevelMerge (** Join all states separated by slevel. *)
+ | SlevelDefault (** Use the limit defined by -eva-slevel. *)
+ | SlevelLocal of int (** Use the given limit instead of -eva-slevel. *)
+ | SlevelFull (** Remove the limit of number of separated states. *)
+
+ (** Loop unroll annotations. *)
+ type unroll_annotation =
+ | UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
+ | UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
+
+ (** Split/merge annotations for value partitioning. *)
+ type flow_annotation =
+ | FlowSplit of Cil_types.term (** Split states according to a term. *)
+ | FlowMerge of Cil_types.term (** Merge states separated by a previous split. *)
+
+ val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+ Cil_types.stmt -> slevel_annotation -> unit
+ val add_unroll_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+ Cil_types.stmt -> unroll_annotation -> unit
+ val add_flow_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+ Cil_types.stmt -> flow_annotation -> unit
+ val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+ Cil_types.stmt -> int -> unit
+end
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index f2f107b7d71bcab897a117084bf09c75464a1e2f..22658b485c9c1ccf9cb4a8a4aeece5a4ecfeb2df 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -83,8 +83,8 @@ struct
in
match get_unroll_annot stmt with
| [] -> warn_no_loop_unroll stmt; default
- | [None] -> Partition.IntLimit default_loop_unroll
- | [(Some t)] -> begin
+ | [UnrollFull] -> Partition.IntLimit default_loop_unroll
+ | [UnrollAmount t] -> begin
(* Inlines the value of const variables in [t]. *)
let global_init vi =
try (Globals.Vars.find vi).init with Not_found -> None
diff --git a/src/plugins/value/partitioning/per_stmt_slevel.ml b/src/plugins/value/partitioning/per_stmt_slevel.ml
index a049166ade12cae16ad8544c61b0be248e0e9992..cf9f8d15a7497032db2e87127515d4fe91d1ec36 100644
--- a/src/plugins/value/partitioning/per_stmt_slevel.ml
+++ b/src/plugins/value/partitioning/per_stmt_slevel.ml
@@ -87,9 +87,14 @@ let compute kf =
Cil_datatype.Stmt.Hashtbl.add h_local s (Stack.top local_slevel);
if d <> None then Cil_datatype.Stmt.Hashtbl.add h_merge s ();
| Some (SlevelLocal i) ->
- if debug then Format.printf "Vising split %d, pushing %d@." s.sid i;
+ if debug then Format.printf "Visiting split %d, pushing %d@." s.sid i;
Cil_datatype.Stmt.Hashtbl.add h_local s i;
Stack.push i local_slevel;
+ | Some SlevelFull ->
+ let cap = max_int in
+ if debug then Format.printf "Visiting split %d, pushing %d@." s.sid cap;
+ Cil_datatype.Stmt.Hashtbl.add h_local s cap;
+ Stack.push cap local_slevel;
| Some SlevelDefault ->
let top = Stack.pop local_slevel in
if debug then
@@ -102,7 +107,7 @@ let compute kf =
and post s =
match get_slevel_annot s with
| None | Some SlevelMerge -> ()
- | Some (SlevelLocal _) ->
+ | Some (SlevelLocal _ | SlevelFull) ->
if debug then Format.printf "Leaving split %d, poping@." s.sid;
ignore (Stack.pop local_slevel);
| Some SlevelDefault ->
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 59d825232185d389fc4365e3bec52135f73c2780..600a28b386b1a43bc6db77eda4d9c015471fa0bd 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -27,8 +27,11 @@ type slevel_annotation =
| SlevelMerge
| SlevelDefault
| SlevelLocal of int
+ | SlevelFull
-type unroll_annotation = term option
+type unroll_annotation =
+ | UnrollAmount of Cil_types.term
+ | UnrollFull
type flow_annotation =
| FlowSplit of term
@@ -112,6 +115,7 @@ module Slevel = Register (struct
let parse ~typing_context:_ = function
| [{lexpr_node = PLvar "default"}] -> SlevelDefault
| [{lexpr_node = PLvar "merge"}] -> SlevelMerge
+ | [{lexpr_node = PLvar "full"}] -> SlevelFull
| [{lexpr_node = PLconstant (IntConstant i)}] ->
let i =
try int_of_string i
@@ -125,12 +129,14 @@ module Slevel = Register (struct
| SlevelDefault -> Ext_terms [Logic_const.tstring "default"]
| SlevelMerge -> Ext_terms [Logic_const.tstring "merge"]
| SlevelLocal i -> Ext_terms [Logic_const.tinteger i]
+ | SlevelFull -> Ext_terms [Logic_const.tstring "full"]
let import = function
| Ext_terms [{term_node}] ->
begin match term_node with
| TConst (LStr "default") -> SlevelDefault
| TConst (LStr "merge") -> SlevelMerge
+ | TConst (LStr "full") -> SlevelFull
| TConst (Integer (i, _)) -> SlevelLocal (Integer.to_int i)
| _ -> SlevelDefault (* be kind. Someone is bound to write a visitor
that will simplify our term into something
@@ -142,6 +148,7 @@ module Slevel = Register (struct
| SlevelDefault -> Format.pp_print_string fmt "default"
| SlevelMerge -> Format.pp_print_string fmt "merge"
| SlevelLocal i -> Format.pp_print_int fmt i
+ | SlevelFull -> Format.pp_print_string fmt "full"
end)
module SimpleTermAnnotation =
@@ -164,31 +171,32 @@ struct
let print = Printer.pp_term
end
-module OptionalTermAnnotation =
-struct
- type t = term option
+module Unroll = Register (struct
+ type t = unroll_annotation
- let parse ~typing_context = function
- | [] -> None
- | [t] ->
- let open Logic_typing in
- Some (typing_context.type_term typing_context typing_context.pre_state t)
- | _ -> raise Parse_error
+ let name = "unroll"
+ let is_loop_annot = true
- let export t =
- Ext_terms (Extlib.list_of_opt t)
+ let parse ~typing_context = function
+ | [] -> UnrollFull
+ | [t] ->
+ let open Logic_typing in
+ UnrollAmount
+ (typing_context.type_term typing_context typing_context.pre_state t)
+ | _ -> raise Parse_error
- let import = function
- | Ext_terms l -> Extlib.opt_of_list l
- | _ -> assert false
+ let export = function
+ | UnrollFull -> Ext_terms []
+ | UnrollAmount t -> Ext_terms [t]
- let print = Pretty_utils.pp_opt Printer.pp_term
-end
+ let import = function
+ | Ext_terms [] -> UnrollFull
+ | Ext_terms [t] -> UnrollAmount t
+ | _ -> assert false
-module Unroll = Register (struct
- include OptionalTermAnnotation
- let name = "unroll"
- let is_loop_annot = true
+ let print fmt = function
+ | UnrollFull -> ()
+ | UnrollAmount t -> Printer.pp_term fmt t
end)
module Split = Register (struct
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index 6a7ba48f7bee2fbf74401728d580429aaa495d20..ab29469ee7102d9232128475653456b1e7fbaff2 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -32,8 +32,11 @@ type slevel_annotation =
| SlevelMerge
| SlevelDefault
| SlevelLocal of int
+ | SlevelFull
-type unroll_annotation = Cil_types.term option
+type unroll_annotation =
+ | UnrollAmount of Cil_types.term
+ | UnrollFull
type flow_annotation =
| FlowSplit of Cil_types.term
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 6e126920273e4ea41476063cae9e3dad627250ff..573e922bde59f3540e00a19d85516740c142acdd 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -76,7 +76,6 @@ module SemanticUnrollingLevel: Parameter_sig.Int
module SlevelFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = int
-
module SlevelMergeAfterLoop: Parameter_sig.Kernel_function_set
module MinLoopUnroll : Parameter_sig.Int
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index 49addb217566afd3e16cb3c2b2b62b696fed84f9..f6e785c3e31abc712bb1928fe1560f418cd4180e 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -4,6 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+ nondet ∈ [--..--]
[eva:loop-unroll] tests/value/partitioning-annots.c:26:
loop not completely unrolled
[eva] tests/value/partitioning-annots.c:26: starting to merge loop iterations
@@ -11,16 +12,29 @@
loop not completely unrolled
[eva] tests/value/partitioning-annots.c:34: starting to merge loop iterations
[eva] tests/value/partitioning-annots.c:36: starting to merge loop iterations
-[eva:loop-unroll] tests/value/partitioning-annots.c:50:
+[eva:loop-unroll] tests/value/partitioning-annots.c:49:
loop not completely unrolled
-[eva] tests/value/partitioning-annots.c:50: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:49: starting to merge loop iterations
+[eva:loop-unroll] tests/value/partitioning-annots.c:54:
+ loop not completely unrolled
+[eva] tests/value/partitioning-annots.c:54: starting to merge loop iterations
[eva] Recording results for test_unroll
[eva] done for function test_unroll
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function test_unroll:
a[0..9] ∈ {42}
b[0..9] ∈ {42}
- c[0..9] ∈ {0}
+ c[0] ∈ {0}
+ [1] ∈ {1}
+ [2] ∈ {0}
+ [3] ∈ {1}
+ [4] ∈ {0}
+ [5] ∈ {1}
+ [6] ∈ {0}
+ [7] ∈ {1}
+ [8] ∈ {0}
+ [9] ∈ {1}
+ [10..19] ∈ {0; 1} or UNINITIALIZED
d[0..9] ∈ {0}
[10..19] ∈ {0} or UNINITIALIZED
e[0] ∈ {1}
@@ -40,7 +54,7 @@
NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function test_unroll:
- a[0..9]; b[0..9]; c[0..9]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1;
+ a[0..9]; b[0..9]; c[0..19]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1;
i_2; i_3; j_1
[inout] Inputs for function test_unroll:
\nothing
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
index 85ae6a30dc6ab58ddc54b0844b4a291cc3bc0d48..3a489cae4e139ed96a227bc728636827a423aff7 100644
--- a/tests/value/oracle/partitioning-annots.1.res.oracle
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -4,42 +4,43 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+ nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:69.
+ Called from tests/value/partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:69:
+[eva] tests/value/partitioning-annots.c:73:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:70.
-[eva] tests/value/partitioning-annots.c:70:
+ Called from tests/value/partitioning-annots.c:74.
+[eva] tests/value/partitioning-annots.c:74:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:76:
+[eva] tests/value/partitioning-annots.c:80:
Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:79:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:79:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:89:
Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
[eva] Recording results for test_split
[eva] done for function test_split
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index 343ee7f5639b073186a03ada6005301f6301d08d..64a0b52e080ccb1be2263ff9f2a956d0722b9641 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -4,50 +4,51 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+ nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:69.
+ Called from tests/value/partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:69:
+[eva] tests/value/partitioning-annots.c:73:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_split.
- Called from tests/value/partitioning-annots.c:70.
-[eva] tests/value/partitioning-annots.c:70:
+ Called from tests/value/partitioning-annots.c:74.
+[eva] tests/value/partitioning-annots.c:74:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:76:
+[eva] tests/value/partitioning-annots.c:80:
Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:79:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:79:
+[eva] tests/value/partitioning-annots.c:83:
Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:81:
+[eva] tests/value/partitioning-annots.c:85:
Frama_C_show_each_before_first_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {1}, {2}, {1}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0}, {2}, {0}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {1}, {1}, {1}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0}, {1}, {0}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {1}, {0}, {1}
-[eva] tests/value/partitioning-annots.c:83:
+[eva] tests/value/partitioning-annots.c:87:
Frama_C_show_each_before_second_merge: {0}, {0}, {0}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:89:
Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
-[eva] tests/value/partitioning-annots.c:85:
+[eva] tests/value/partitioning-annots.c:89:
Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
[eva] Recording results for test_split
[eva] done for function test_split
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index f0e69a170fe060780d968638b9a0603a27a3185d..0726db35992e2719e1cf18e08112b16089225dbc 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -4,42 +4,43 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+ nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:103.
+ Called from tests/value/partitioning-annots.c:107.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:103:
+[eva] tests/value/partitioning-annots.c:107:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:103.
+ Called from tests/value/partitioning-annots.c:107.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:101: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:105: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:103.
+ Called from tests/value/partitioning-annots.c:107.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:103.
+ Called from tests/value/partitioning-annots.c:107.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:103.
+ Called from tests/value/partitioning-annots.c:107.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- test_loop_split.
- Called from tests/value/partitioning-annots.c:103.
+ Called from tests/value/partitioning-annots.c:107.
[eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/partitioning-annots.c:110: Warning:
+[eva:alarm] tests/value/partitioning-annots.c:114: Warning:
accessing uninitialized left-value. assert \initialized(&A[i]);
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {9}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {8}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {7}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {6}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {5}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {4}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {3}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {2}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {1}, {42}
-[eva] tests/value/partitioning-annots.c:115: Frama_C_show_each: {0}, {42}
-[eva] tests/value/partitioning-annots.c:116: assertion got status valid.
-[eva] tests/value/partitioning-annots.c:119:
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {9}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {8}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {7}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {6}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {5}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {4}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {3}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {2}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {1}, {42}
+[eva] tests/value/partitioning-annots.c:119: Frama_C_show_each: {0}, {42}
+[eva] tests/value/partitioning-annots.c:120: assertion got status valid.
+[eva] tests/value/partitioning-annots.c:123:
Frama_C_show_each: {{ "Value 42 not found" }}
[eva] Recording results for test_loop_split
[eva] done for function test_loop_split
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index 81e33a3bd19fe237f19841c7c3b2a2851eab6214..95b65614d116d230e504958ec3342e0fabfeb3db 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -4,14 +4,15 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+ nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_history.
- Called from tests/value/partitioning-annots.c:125.
+ Called from tests/value/partitioning-annots.c:129.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:125:
+[eva] tests/value/partitioning-annots.c:129:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] tests/value/partitioning-annots.c:134: Warning:
+[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] tests/value/partitioning-annots.c:138: Warning:
division by zero. assert j ≢ 0;
[eva] Recording results for test_history
[eva] done for function test_history
diff --git a/tests/value/oracle/partitioning-annots.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
index 801d0587fd95fdb29ed3c12eaf718725d0ffa352..e2009fcbb60b0627e86a3d9db8d7ee5cd946709e 100644
--- a/tests/value/oracle/partitioning-annots.5.res.oracle
+++ b/tests/value/oracle/partitioning-annots.5.res.oracle
@@ -4,14 +4,15 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
k ∈ {0}
+ nondet ∈ [--..--]
[eva] computing for function Frama_C_interval <- test_history.
- Called from tests/value/partitioning-annots.c:125.
+ Called from tests/value/partitioning-annots.c:129.
[eva] using specification for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:125:
+[eva] tests/value/partitioning-annots.c:129:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {0}, {0}
-[eva] tests/value/partitioning-annots.c:131: Frama_C_show_each: {1}, {1}
+[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {0}, {0}
+[eva] tests/value/partitioning-annots.c:135: Frama_C_show_each: {1}, {1}
[eva] Recording results for test_history
[eva] done for function test_history
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/partitioning-annots.6.res.oracle b/tests/value/oracle/partitioning-annots.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..405717c890d17bf711d9670096fd4680318c231e
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.6.res.oracle
@@ -0,0 +1,30 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_slevel
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+ nondet ∈ [--..--]
+[eva] tests/value/partitioning-annots.c:152: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:157: starting to merge loop iterations
+[eva] Recording results for test_slevel
+[eva] done for function test_slevel
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_slevel:
+ a[0..9] ∈ {42}
+ b[0..9] ∈ {42} or UNINITIALIZED
+ c[0..3] ∈ {33; 42}
+ [4..9] ∈ {33; 42} or UNINITIALIZED
+ d[0..9] ∈ {33; 42}
+ e[0..3] ∈ {33; 42}
+[from] Computing for function test_slevel
+[from] Done for function test_slevel
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function test_slevel:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_slevel:
+ a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3
+[inout] Inputs for function test_slevel:
+ nondet
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 10dd8680c3840d6e85e34a656f72f7e04e090a36..8137bbab1c2ebe6ca36d520993eb22721297491c 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -6,16 +6,16 @@
STDOPT: #"-main test_loop_split -eva-partition-history 1"
STDOPT: #"-main test_history -eva-partition-history 0"
STDOPT: #"-main test_history -eva-partition-history 1"
+ STDOPT: #"-main test_slevel"
*/
#include "__fc_builtin.h"
#define N 10
-
void test_unroll()
{
- int a[N], b[N], c[N], d[2*N], e[N];
+ int a[N], b[N], c[2*N], d[2*N], e[N];
// The inner loop needs to be unrolled to allow strong updates
// The outer loops doesn't need to be unrolled
@@ -40,10 +40,14 @@ void test_unroll()
// At the end, we must have both arrays a and b to be fully initialized at 42
- // Small loops can be unrolled without giving an unroll parameter
- //@ loop unroll N;
- for (int i = 0 ; i < N ; i++)
- c[i] = 0;
+ // Small loops can be unrolled without giving an unroll amount.
+ // The actual limit of the number of iterations can be overriden with
+ // the option -eva-default-loop-unroll
+ // Here -eva-default-loop-unroll is set to a value not high enough to
+ // completely unroll the loop thus a warning should be emitted.
+ //@ loop unroll;
+ for (int i = 0 ; i < 2*N ; i++)
+ c[i] = i % 2;
// Longer loops won't be completely unrolled when not giving a parameter
//@ loop unroll N;
@@ -134,8 +138,53 @@ void test_history()
k = k / j;
}
+volatile nondet;
+
+void test_slevel()
+{
+ int a[N], b[N], c[N], d[N], e[4];
+ //@slevel 10;
+ for (int i = 0; i < N; i++) {
+ a[i] = 42;
+ }
+
+ //@slevel default;
+ for (int i = 0; i < N; i++) {
+ b[i] = 42;
+ }
+
+ //@slevel 20;
+ for (int i = 0; i < N; i++) {
+ if (nondet)
+ c[i] = 42;
+ else
+ c[i] = 33;
+ }
+
+ //@slevel 20;
+ for (int i = 0; i < N; i++) {
+ if (nondet)
+ d[i] = 42;
+ else
+ d[i] = 33;
+ //@slevel merge;
+ ; // Otherwise previous annotation is ignored
+ }
+
+ //@slevel 0;
+ ;
+ //@slevel full;
+ for (int i = 0; i < 4; i++) {
+ if (nondet)
+ e[i] = 42;
+ else
+ e[i] = 33;
+ }
+}
+
void main(void)
{
+ test_slevel();
test_unroll();
test_split();
test_loop_split();