diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index 35efe1542310ce184496e43c2f808a86c0a73262..7290c7b8cbddd3042a277d52a87968f87aa3788f 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -509,6 +509,16 @@ struct
| Exp (e, i) -> Ival.add_singleton_int i (oracle e)
| Ptroffset _ -> raise Not_implemented
+ let to_const ~oracle = function
+ | Const i -> Some i
+ | Exp (e, i) ->
+ begin try
+ Some (Integer.add (Ival.project_int (oracle e)) i)
+ with Ival.Not_Singleton_Int ->
+ None
+ end
+ | Ptroffset _ -> raise Not_implemented
+
let succ = function
| Const i -> Const (Integer.succ i)
| Exp (e, i) -> Exp (e, Integer.succ i)
@@ -535,6 +545,11 @@ struct
else Option.map (fun i -> Ptroffset (e, base, Integer.(sub j (mul l i)))) i
with NonLinear -> None
+ let incr_or_constantify ~oracle vi i b =
+ match incr vi i b with
+ | Some v -> Some v
+ | None -> Option.map (fun c -> Const c) (to_const ~oracle b)
+
let cmp_int i1 i2 =
let r = Integer.sub i1 i2 in
if Integer.is_zero r
@@ -597,11 +612,13 @@ struct
Bound.compare b1 b2 <?> (Integer.compare, a1, a2)
let equal (b1,a1) (b2,a2) =
Bound.equal b1 b2 && Integer.equal a1 a2
- let of_integer i a = Bound.of_integer i, a
+ let _of_integer i a = Bound.of_integer i, a
let _of_exp e a = Bound.of_exp e, a
let _succ (b,a) = (Bound.succ b, a)
let pred (b,a) = (Bound.pred b, a)
- let incr vi i (b,a) = Bound.incr vi i b |> Option.map (fun b -> b,a)
+ let _incr vi i (b,a) = Bound.incr vi i b |> Option.map (fun b -> b,a)
+ let incr_or_constantify ~oracle vi i (b,a) =
+ Bound.incr_or_constantify ~oracle vi i b |> Option.map (fun b -> b,a)
let _to_ival ~oracle (b,_a) = Bound.to_ival ~oracle b
let cmp ~oracle (b1,_a1) (b2,_a2) = Bound.cmp ~oracle b1 b2
let eq ?oracle (b1,_a1) (b2,_a2) = Bound.eq ?oracle b1 b2
@@ -615,7 +632,7 @@ struct
Bound.upper_const ~oracle b
let born b = b, Integer.zero
- let age (_,a) = a
+ let _age (_,a) = a
let operators oracle : (module Operators with type t = t) =
operators (cmp ~oracle)
end
@@ -823,9 +840,15 @@ struct
in
match left_slice_emerges, right_slice_emerges with
| Some (v1,u1,t1), None -> (* left slice emerges *)
- aux u1 t1 s2 ((v1,u1) :: acc)
+ if equals Left l u1 then (* actually empty both sides*)
+ aux l t1 s2 acc
+ else
+ aux u1 t1 s2 ((v1,u1) :: acc)
| None, Some (v2,u2,t2) -> (* right slice emerges *)
- aux u2 s1 t2 ((v2,u2) :: acc)
+ if equals Right l u2 then (* actually empty both sides *)
+ aux l s1 t2 acc
+ else
+ aux u2 s1 t2 ((v2,u2) :: acc)
| Some _, Some _ (* both emerges, can't choose *)
| None, None -> (* none emerges *)
match s1, s2 with (* Are we done yet ? *)
@@ -960,16 +983,7 @@ struct
aux_before m.start m.segments
let incr_bound ~oracle vi x m =
- let incr b =
- match B.incr vi x b with
- | Some b -> Some b
- | None ->
- try
- let i = Ival.project_int (oracle (Cil.evar vi)) in
- Some (B.of_integer i (B.age b))
- with Ival.Not_Singleton_Int ->
- None
- in
+ let incr = B.incr_or_constantify ~oracle vi x in
let rec aux acc = function
| [] -> acc
| (v,u) :: t ->
diff --git a/tests/value/multidim.c b/tests/value/multidim.c
index ee8bdd889a853d6b3c0905470263d1ec1cc811a4..9ec307546d8cabda19207687182a98058d974cdc 100644
--- a/tests/value/multidim.c
+++ b/tests/value/multidim.c
@@ -2,6 +2,7 @@
STDOPT: #"-main main -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
STDOPT: #"-main main2 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
STDOPT: #"-main main3 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
+ STDOPT: #"-main main4 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
*/
#include "__fc_builtin.h"
#define N 4
@@ -27,7 +28,7 @@ s z[M];
/*@ assigns z[..] \from \nothing;
ensures \are_finite(z[..].t1[..].f) && \are_finite(z[..].t2[..].f);
*/
-void f();
+void f(void);
volatile int nondet;
@@ -57,8 +58,8 @@ void main2(void) {
for (int i = 0 ; i < 10 ; i++) {
t[i] = 1;
}
- Frama_C_domain_show_each(t);
//@ check t[0..9] == 1;
+ Frama_C_domain_show_each(t);
}
void main3(void) {
@@ -69,10 +70,21 @@ void main3(void) {
}
}
- Frama_C_domain_show_each(z);
-
int a = Frama_C_interval(0,M-1);
int b = Frama_C_interval(0,N-1);
t r = z[a].t1[b];
- Frama_C_domain_show_each(r);
+ Frama_C_domain_show_each(z, r);
+}
+
+void main4(void) { // How trace partitioning changes array partitioning ?
+ int t[N];
+
+ //@ loop unroll 1;
+ for (int i = 0; i < M; i++) {
+ //@ loop unroll N;
+ for (int j = 0; j < N; j++) {
+ t[j] = 42;
+ }
+ }
+ Frama_C_domain_show_each(t);
}
diff --git a/tests/value/oracle/multidim.0.res.oracle b/tests/value/oracle/multidim.0.res.oracle
index e088682cb917b4a7efc3edeb15a8f882df15a24d..05a95cd5a3b81db4e640353d4501b46f96405a86 100644
--- a/tests/value/oracle/multidim.0.res.oracle
+++ b/tests/value/oracle/multidim.0.res.oracle
@@ -1,7 +1,4 @@
[kernel] Parsing multidim.c (with preprocessing)
-[kernel:typing:no-proto] multidim.c:49: Warning:
- Calling function f that is declared without prototype.
- Its formals will be inferred from actual arguments
[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -9,7 +6,7 @@
[eva:initial-state] Values of globals at initialization
z[0..3] ∈ {0}
nondet ∈ [--..--]
-[eva] multidim.c:41:
+[eva] multidim.c:42:
Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[0].i ∈ [--..--]
@@ -44,7 +41,7 @@
# multidim: { .t1[0] = { .f = {4.} } }
z : # cvalue: {0}
# multidim: 0
-[eva] multidim.c:47:
+[eva] multidim.c:48:
Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[0].i ∈ [--..--]
@@ -63,29 +60,29 @@
.t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[3].i ∈ [--..--]
# multidim: {
- .t1[0 .. 4] = { .f = {{ ANYTHING }} },
- .t2[0 .. 4] = { .f = {{ ANYTHING }} }
+ .t1[0 .. 3] = { .f = {{ ANYTHING }} },
+ .t2[0 .. 3] = { .f = {{ ANYTHING }} }
}
[eva] computing for function f <- main.
- Called from multidim.c:49.
+ Called from multidim.c:50.
[eva] using specification for function f
[eva] Done for function f
-[eva] multidim.c:50:
+[eva] multidim.c:51:
Frama_C_domain_show_each:
z : # cvalue: [--..--]
- # multidim: [0 .. 4] = {
- .t1[0 .. 4] = {
+ # multidim: [0 .. 3] = {
+ .t1[0 .. 3] = {
.f = [-3.40282346639e+38 .. 3.40282346639e+38]
},
- .t2[0 .. 4] = {
+ .t2[0 .. 3] = {
.f = [-3.40282346639e+38 .. 3.40282346639e+38]
}
}
-[eva:alarm] multidim.c:52: Warning: check got status unknown.
+[eva:alarm] multidim.c:53: Warning: check got status unknown.
[eva] Recording results for main
[eva] done for function main
-[kernel] multidim.c:52: more than 1(28) elements to enumerate. Approximating.
-[kernel] multidim.c:52: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:53: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:53: more than 1(28) elements to enumerate. Approximating.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
z[0..3] ∈ [--..--]
diff --git a/tests/value/oracle/multidim.1.res.oracle b/tests/value/oracle/multidim.1.res.oracle
index fecc3076b5e7ce6f2bd571c2ea764aecef811440..253201525cd9bc0ca2e56c56d4a05ef7db5f8e2a 100644
--- a/tests/value/oracle/multidim.1.res.oracle
+++ b/tests/value/oracle/multidim.1.res.oracle
@@ -1,7 +1,4 @@
[kernel] Parsing multidim.c (with preprocessing)
-[kernel:typing:no-proto] multidim.c:49: Warning:
- Calling function f that is declared without prototype.
- Its formals will be inferred from actual arguments
[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main2
[eva] Computing initial state
@@ -9,12 +6,12 @@
[eva:initial-state] Values of globals at initialization
z[0..3] ∈ {0}
nondet ∈ [--..--]
-[eva] multidim.c:57: starting to merge loop iterations
-[eva] multidim.c:60:
+[eva] multidim.c:58: starting to merge loop iterations
+[eva:alarm] multidim.c:61: Warning: check got status unknown.
+[eva] multidim.c:62:
Frama_C_domain_show_each:
t : # cvalue: {0; 1}
# multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} }
-[eva:alarm] multidim.c:61: Warning: check got status unknown.
[eva] Recording results for main2
[eva] done for function main2
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/multidim.2.res.oracle b/tests/value/oracle/multidim.2.res.oracle
index 6288a0d7a9579c400915b7a974e7100ca930a0ff..6a6d57ae5a586254041c0b4ff0c02f0b90eda763 100644
--- a/tests/value/oracle/multidim.2.res.oracle
+++ b/tests/value/oracle/multidim.2.res.oracle
@@ -1,7 +1,4 @@
[kernel] Parsing multidim.c (with preprocessing)
-[kernel:typing:no-proto] multidim.c:49: Warning:
- Calling function f that is declared without prototype.
- Its formals will be inferred from actual arguments
[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main3
[eva] Computing initial state
@@ -9,47 +6,40 @@
[eva:initial-state] Values of globals at initialization
z[0..3] ∈ {0}
nondet ∈ [--..--]
+[eva] multidim.c:67: starting to merge loop iterations
[eva] multidim.c:66: starting to merge loop iterations
-[eva] multidim.c:65: starting to merge loop iterations
-[kernel] multidim.c:67:
- more than 1(20) locations to update in array. Approximating.
[kernel] multidim.c:68:
more than 1(20) locations to update in array. Approximating.
-[kernel] multidim.c:67:
- more than 1(28) locations to update in array. Approximating.
+[kernel] multidim.c:69:
+ more than 1(20) locations to update in array. Approximating.
[kernel] multidim.c:68:
more than 1(28) locations to update in array. Approximating.
-[eva] multidim.c:72:
- Frama_C_domain_show_each:
- z : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
- {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
- [--..--]
- [3].t1[3].i ∈ {0; 2}
- [3].t2[0..3] ∈ {0}
- # multidim: [0 .. 3] = {
- .t1{
- [0 .. 3] = { .f = [0. .. 2.], .i = {0; 2} },
- [4 .. 3] = 0
- }
- }
+[kernel] multidim.c:69:
+ more than 1(28) locations to update in array. Approximating.
[eva] computing for function Frama_C_interval <- main3.
- Called from multidim.c:74.
+ Called from multidim.c:73.
[eva] using specification for function Frama_C_interval
-[eva] multidim.c:74:
+[eva] multidim.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 <- main3.
- Called from multidim.c:75.
-[eva] multidim.c:75:
+ Called from multidim.c:74.
+[eva] multidim.c:74:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] multidim.c:77:
+[eva] multidim.c:76:
Frama_C_domain_show_each:
+ z : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
+ {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
+ [--..--]
+ [3].t1[3].i ∈ {0; 2}
+ [3].t2[0..3] ∈ {0}
+ # multidim: [0 .. 3] = { .t1[0 .. 3] = { .f = [0. .. 2.], .i = {0; 2} } }
r : # cvalue: [--..--]
# multidim: { .f = [0. .. 2.], .i = {0; 2} }
[eva] Recording results for main3
-[kernel] multidim.c:67: more than 1(28) elements to enumerate. Approximating.
[kernel] multidim.c:68: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:69: more than 1(28) elements to enumerate. Approximating.
[eva] done for function main3
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main3:
@@ -63,8 +53,8 @@
b ∈ {0; 1; 2; 3}
r ∈ [--..--]
[from] Computing for function main3
-[kernel] multidim.c:67: more than 1(28) dependencies to update. Approximating.
[kernel] multidim.c:68: more than 1(28) dependencies to update. Approximating.
+[kernel] multidim.c:69: more than 1(28) dependencies to update. Approximating.
[from] Computing for function Frama_C_interval <-main3
[from] Done for function Frama_C_interval
[from] Done for function main3
diff --git a/tests/value/oracle/multidim.3.res.oracle b/tests/value/oracle/multidim.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a560275847d7f334713675616cc1072b6ab0a335
--- /dev/null
+++ b/tests/value/oracle/multidim.3.res.oracle
@@ -0,0 +1,31 @@
+[kernel] Parsing multidim.c (with preprocessing)
+[eva:experimental] Warning: The multidim domain is experimental.
+[eva] Analyzing a complete application starting at main4
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ z[0..3] ∈ {0}
+ nondet ∈ [--..--]
+[eva:loop-unroll:partial] multidim.c:83: loop not completely unrolled
+[eva] multidim.c:83: starting to merge loop iterations
+[eva] multidim.c:85: starting to merge loop iterations
+[eva] multidim.c:89:
+ Frama_C_domain_show_each:
+ t : # cvalue: {42}
+ # multidim: { [0] = {42}, [1] = {42}, [2] = {42}, [3] = {42} }
+[eva] Recording results for main4
+[eva] done for function main4
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main4:
+ t[0..3] ∈ {42}
+[from] Computing for function main4
+[from] Done for function main4
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function main4:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main4:
+ t[0..3]; i; j
+[inout] Inputs for function main4:
+ \nothing