Skip to content
Snippets Groups Projects
Commit 6643a6eb authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] multidim: fix several bugs

parent df1b4a41
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_services/abstract_interp/abstract_memory.ml
+ 60
− 33
View file @ 6643a6eb
...@@ -41,7 +41,7 @@ let pp_iter ...@@ -41,7 +41,7 @@ let pp_iter
?(pre=format_of_string "{@;<1 2>") ?(pre=format_of_string "{@;<1 2>")
?(sep=format_of_string ",@;<1 2>") ?(sep=format_of_string ",@;<1 2>")
?(suf=format_of_string "@ }") ?(suf=format_of_string "@ }")
?(format=format_of_string"@[<hv>%a@]") ?(format=format_of_string "@[<hv>%a@]")
iter pp fmt v = iter pp fmt v =
let need_sep = ref false in let need_sep = ref false in
Format.fprintf fmt pre; Format.fprintf fmt pre;
...@@ -49,10 +49,9 @@ let pp_iter ...@@ -49,10 +49,9 @@ let pp_iter
if !need_sep then Format.fprintf fmt sep else need_sep := true; if !need_sep then Format.fprintf fmt sep else need_sep := true;
Format.fprintf fmt format pp v; Format.fprintf fmt format pp v;
) v; ) v;
Format.fprintf fmt suf; Format.fprintf fmt suf
;;
let pp_iter2 ?pre ?sep ?suf ?(format=format_of_string "%a%a") let pp_iter2 ?pre ?sep ?suf ?(format=format_of_string "@[<hv>%a%a@]")
iter2 pp_key pp_val fmt v = iter2 pp_key pp_val fmt v =
let iter f = iter2 (fun k v -> f (k,v)) in let iter f = iter2 (fun k v -> f (k,v)) in
let pp fmt (k,v) = Format.fprintf fmt format pp_key k pp_val v in let pp fmt (k,v) = Format.fprintf fmt format pp_key k pp_val v in
...@@ -247,7 +246,7 @@ struct ...@@ -247,7 +246,7 @@ struct
type submemory = M.t type submemory = M.t
let pretty fmt m = let pretty fmt m =
pp_iter2 ~format:".%a%a" FieldMap.iter Field.pretty M.pretty fmt m.fields pp_iter2 ~format:"@[<hv>.%a%a@]" FieldMap.iter Field.pretty M.pretty fmt m.fields
let hash m = let hash m =
Hashtbl.hash (m.padding, FieldMap.hash m.fields) Hashtbl.hash (m.padding, FieldMap.hash m.fields)
...@@ -440,10 +439,14 @@ struct ...@@ -440,10 +439,14 @@ struct
| Const _ -> Some b | Const _ -> Some b
| Exp (e, j) -> | Exp (e, j) ->
let l = linearity vi e in let l = linearity vi e in
Some (Exp (e, Integer.(sub j (mul l i)))) if Integer.is_zero l
| Ptroffset (e, b, j) -> then Some b
else Option.map (fun i -> Exp (e, Integer.(sub j (mul l i)))) i
| Ptroffset (e, base, j) ->
let l = linearity vi e in let l = linearity vi e in
Some (Ptroffset (e, b, Integer.(sub j (mul l i)))) if Integer.is_zero l
then Some b
else Option.map (fun i -> Ptroffset (e, base, Integer.(sub j (mul l i)))) i
with NonLinear -> None with NonLinear -> None
(* Stupid oracle built from an Ival oracle *) (* Stupid oracle built from an Ival oracle *)
...@@ -506,7 +509,7 @@ sig ...@@ -506,7 +509,7 @@ sig
val is_included : t -> t -> bool val is_included : t -> t -> bool
val unify : oracle:bioracle -> (submemory -> submemory -> submemory) -> val unify : oracle:bioracle -> (submemory -> submemory -> submemory) ->
t -> t -> t t -> t -> t
val singleton : bit -> bound -> bound -> submemory -> t val single : bit -> bound -> bound -> submemory -> t
val read : val read :
oracle:(Cil_types.exp -> Ival.t) -> oracle:(Cil_types.exp -> Ival.t) ->
(submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> 'a (submemory -> 'a) -> ('a -> 'a -> 'a) -> t -> bound -> 'a
...@@ -722,7 +725,7 @@ struct ...@@ -722,7 +725,7 @@ struct
padding = Bit.join p1 p2 ; padding = Bit.join p1 p2 ;
} }
let singleton padding lindex uindex value = let single padding lindex uindex value =
{ {
padding ; padding ;
start = lindex ; start = lindex ;
...@@ -757,7 +760,7 @@ struct ...@@ -757,7 +760,7 @@ struct
1. reinforcement without loss 1. reinforcement without loss
2. weak update without singularization 2. weak update without singularization
3. update reduces the number of segments to 3 *) 3. update reduces the number of segments to 3 *)
let write ~oracle f m lindex uindex = let write ~oracle f m lindex uindex = (* lindex < uindex *)
let (<=) b1 b2 = match Bound.cmp ~oracle b1 b2 with let (<=) b1 b2 = match Bound.cmp ~oracle b1 b2 with
| Lower | Equal -> true | Lower | Equal -> true
| Greater | Uncomparable -> false | Greater | Uncomparable -> false
...@@ -765,26 +768,39 @@ struct ...@@ -765,26 +768,39 @@ struct
| Greater | Equal -> true | Greater | Equal -> true
| Lower | Uncomparable -> false | Lower | Uncomparable -> false
in in
(* (start,head) : segmentation kept identical below the write indexes,
head is a list in reverse order
(l,v,u) : the segment (l,u) beeing overwriten with previous value v
head = (_,l) :: _
*)
let rec aux_before l s = let rec aux_before l s =
(* Format.printf "aux before: %a@." pretty_segments (l,s); *)
if lindex >= l if lindex >= l
then aux_below l [] l s then aux_below l [] l s
else aux_over lindex [] lindex (M.of_raw m.padding) l s else aux_over lindex [] lindex (M.of_raw m.padding) l s
and aux_below start head l = function (* l < index *) and aux_below start head l = fun t ->
(* Format.printf "aux_below: %a [%a] %a@." pretty_segments (start,head) Bound.pretty l pretty_segments (l,t); *)
match t with (* l <= lindex *)
| [] -> | [] ->
aux_end start head l (M.of_raw m.padding) uindex [] aux_end start head l (M.of_raw m.padding) uindex []
| (v,u) :: t -> | (v,u) :: t ->
if lindex >= u if lindex >= u
then aux_below start ((v,u) :: head) u t then aux_below start ((v,u) :: head) u t
else aux_over start head l v u t else aux_over start head l v u t
and aux_over start head l v u = function (* l >= index *) and aux_over start head l v u s = (* l <= lindex *)
| [] -> (* Format.printf "aux_over: %a [%a,%a,%a] %a@." pretty_segments (start,head) Bound.pretty l M.pretty v Bound.pretty u pretty_segments (u,s); *)
aux_end start head l (M.smash ~oracle v (M.of_raw m.padding)) uindex [] if uindex <= u then
| ((v',u') :: t) as s -> aux_end start head l v u s
if uindex <= u' else
then aux_end start head l v u s match s with
(* TODO: do not smash if the slices are covered by the write *) | [] ->
else aux_over start head l (M.smash ~oracle v v') u' t aux_end start head l (M.smash ~oracle v (M.of_raw m.padding)) uindex []
and aux_end start head l v u tail = | (v',u') :: t ->
(* TODO: do not smash if the slices are covered by the write *)
aux_over start head l (M.smash ~oracle v v') u' t
and aux_end start head l v u tail = (* l <= lindex < uindex <= u*)
(* Format.printf "aux_end: %a [%a,%a,%a] %a@." pretty_segments (start,head) Bound.pretty l M.pretty v Bound.pretty u pretty_segments (u,tail); *)
let tail' = let tail' =
(if is_empty_segment ~oracle l lindex then [] else [(v,lindex)]) @ (if is_empty_segment ~oracle l lindex then [] else [(v,lindex)]) @
[(f v,uindex)] @ [(f v,uindex)] @
...@@ -803,7 +819,7 @@ struct ...@@ -803,7 +819,7 @@ struct
let rec aux acc = function let rec aux acc = function
| [] -> acc | [] -> acc
| (v,u) :: t -> | (v,u) :: t ->
match Option.bind x (fun x -> Bound.incr vi x u) with match Bound.incr vi x u with
| Some u -> aux ((v,u) :: acc) t | Some u -> aux ((v,u) :: acc) t
| None -> | None ->
match t with match t with
...@@ -814,7 +830,7 @@ struct ...@@ -814,7 +830,7 @@ struct
| (v',u') :: t -> aux ((M.smash ~oracle v v',u') :: acc) t | (v',u') :: t -> aux ((M.smash ~oracle v v',u') :: acc) t
in in
let start, segments = let start, segments =
match Option.bind x (fun x -> Bound.incr vi x m.start) with match Bound.incr vi x m.start with
| Some start -> start, m.segments | Some start -> start, m.segments
| None -> | None ->
match m.segments with match m.segments with
...@@ -905,7 +921,8 @@ struct ...@@ -905,7 +921,8 @@ struct
Format.fprintf fmt "%a" A.pretty a.array_value Format.fprintf fmt "%a" A.pretty a.array_value
let pretty fmt m = pp ~root:false fmt m let pretty fmt m = pp ~root:false fmt m
let pretty_root fmt m = pp ~root:true fmt m let pretty_root fmt m =
Format.fprintf fmt "@[<hv>%a@]" (pp ~root:true) m
let rec hash m = match m with let rec hash m = match m with
| Raw b -> Hashtbl.hash ( | Raw b -> Hashtbl.hash (
...@@ -1114,21 +1131,20 @@ struct ...@@ -1114,21 +1131,20 @@ struct
let l, u = Int_val.min_and_max index in let l, u = Int_val.min_and_max index in
let l = Option.get l and u = Option.get u in (* TODO: handle exceptions *) let l = Option.get l and u = Option.get u in (* TODO: handle exceptions *)
Bound.of_integer l, Bound.of_integer u, Bound.of_integer l, Bound.of_integer u,
weak || Integer.(equal (succ l) u) weak || Integer.equal l u
| Some e -> | Some e ->
let b = Bound.of_exp e in let b = Bound.of_exp e in
b, Bound.succ b, weak b, b, weak
in in
match m with match m with
| Array a when are_typ_compatible a.array_cell_type elem_type -> | Array a when are_typ_compatible a.array_cell_type elem_type ->
let array_value = let array_value = A.write ~oracle (aux ~weak offset') a.array_value
A.write ~oracle (aux ~weak offset') a.array_value lindex uindex lindex (Bound.succ uindex) in
in
Array { a with array_value } Array { a with array_value }
| _ -> | _ ->
let b = raw m in let b = raw m in
let new_value = aux ~weak offset' (Raw b) in let new_value = aux ~weak offset' (Raw b) in
let array_value = A.singleton b lindex uindex new_value in let array_value = A.single b lindex (Bound.succ uindex) new_value in
Array { array_cell_type = elem_type ; array_value } Array { array_cell_type = elem_type ; array_value }
in aux in aux
...@@ -1169,19 +1185,30 @@ struct ...@@ -1169,19 +1185,30 @@ struct
read ~oracle to_value V.join loc m read ~oracle to_value V.join loc m
let extract ~oracle (m : t) (loc : location) : t = let extract ~oracle (m : t) (loc : location) : t =
read ~oracle (fun _typ x -> x) (smash ~oracle) loc m let r = read ~oracle (fun _typ x -> x) (smash ~oracle) loc m in
(* Format.printf "extract %a in %a : %a@." TypedOffset.pretty loc pretty m pretty r; *)
r
let set ~oracle ~weak m offset new_v = let set ~oracle ~weak m offset new_v =
let f ~weak typ m = let f ~weak typ m =
of_value typ (if weak then V.join (to_value typ m) new_v else new_v) of_value typ (if weak then V.join (to_value typ m) new_v else new_v)
in in
write ~oracle ~weak f offset m let r = write ~oracle ~weak f offset m in
(* Format.printf "%a <- %a : %a@." TypedOffset.pretty offset V.pretty new_v pretty r; *)
r
let join ~oracle m1 m2 =
let r = join ~oracle m1 m2 in
(* Format.printf "%a join %a : %a@." pretty m1 pretty m2 pretty r; *)
r
let reinforce ~oracle f m offset = let reinforce ~oracle f m offset =
let f' ~weak typ m = let f' ~weak typ m =
if weak then m else of_value typ (f (to_value typ m)) if weak then m else of_value typ (f (to_value typ m))
in in
write ~oracle ~weak:false f' offset m let r = write ~oracle ~weak:false f' offset m in
(* Format.printf "reinforce at %a : %a@." TypedOffset.pretty offset pretty r; *)
r
let erase ~oracle ~weak m offset b = let erase ~oracle ~weak m offset b =
let f ~weak _typ m = let f ~weak _typ m =
......
tests/value/multidim.c
+ 16
− 5
View file @ 6643a6eb
/* run.config* /* run.config*
STDOPT: +"-eva-msg-key d-multidim -eva-domains multidim -eva-plevel 0" STDOPT: +"-eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
*/ */
#include "__fc_builtin.h" #include "__fc_builtin.h"
#define N 4 #define N 4
...@@ -42,14 +42,13 @@ void main(s x) { ...@@ -42,14 +42,13 @@ void main(s x) {
/* The multidim domain wont infer anything except the structure from the /* The multidim domain wont infer anything except the structure from the
assign: it considers x can contain anything including pointers, and thus no assign: it considers x can contain anything including pointers, and thus no
reduction is done by are_finite */ reduction is done by are_finite */
//@ assert \are_finite(x.t1[..].f) && \are_finite(x.t2[..].f); //@ admit \are_finite(x.t1[..].f) && \are_finite(x.t2[..].f);
Frama_C_domain_show_each(x); Frama_C_domain_show_each(x);
f(); f();
Frama_C_domain_show_each(z); Frama_C_domain_show_each(z);
/* The multidim domain doesn't implement forward logic yet */ /* The multidim domain doesn't implement forward logic yet */
//@ assert \are_finite(z[..].t1[..].f) && \are_finite(z[..].t2[..].f); //@ check \are_finite(z[..].t1[..].f) && \are_finite(z[..].t2[..].f);
for (int i = 0 ; i < M ; i ++) { for (int i = 0 ; i < M ; i ++) {
for (int j = 0 ; j < N ; j ++) { for (int j = 0 ; j < N ; j ++) {
...@@ -64,3 +63,15 @@ void main(s x) { ...@@ -64,3 +63,15 @@ void main(s x) {
Frama_C_domain_show_each(t1); Frama_C_domain_show_each(t1);
} }
void main2(void) {
int t[10] = {0};
Frama_C_domain_show_each_begin(t);
for (int i = 0 ; i < 10 ; i++) {
Frama_C_domain_show_each_before(i, t);
t[i] = 1;
Frama_C_domain_show_each_after(i, t);
}
Frama_C_domain_show_each(t);
//@ check t[0..9] == 1;
}
tests/value/oracle/multidim.res.oracle
+ 58
− 33
View file @ 6643a6eb
...@@ -10,24 +10,36 @@ ...@@ -10,24 +10,36 @@
z[0..3] ∈ {0} z[0..3] ∈ {0}
w[0..3] ∈ {0} w[0..3] ∈ {0}
nondet ∈ [--..--] nondet ∈ [--..--]
[kernel] multidim.c:33: too many locations to update in array. Approximating.
[eva] multidim.c:40: [eva] multidim.c:40:
Frama_C_domain_show_each: Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[0].i ∈ [--..--] .t1[0].i ∈ [--..--]
.t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] .t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[1].i ∈ [--..--] .t1[1].i ∈ [--..--]
.t1[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64 .t1[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[2].i ∈ [--..--]
.t1[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[3].i ∈ [--..--]
.t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] .t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[0].i ∈ [--..--] .t2[0].i ∈ [--..--]
.t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] .t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[1].i ∈ [--..--] .t2[1].i ∈ [--..--]
.t2[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64 .t2[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[2].i ∈ [--..--]
.t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[3].i ∈ [--..--]
# multidim: T # multidim: T
y1 : # cvalue: .t1[0].f ∈ {3.} y1 : # cvalue: .t1[0].f ∈ {3.}
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0} {.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0}
# multidim: { .t1[0] = { .f = [0. .. 3.], .i = {0} }, .t2[0..3] = { # multidim: {
.f = {0}, .i = {0} } } .t1[0] = { .f = {3.}, .i = {0} },
.t2{
[0] = { .f = {0}, .i = {0} },
[1] = { .f = {0}, .i = {0} },
[2] = { .f = {0}, .i = {0} },
[3] = { .f = {0}, .i = {0} }
}
}
y2 : # cvalue: .t1[0].f ∈ {4.} or UNINITIALIZED y2 : # cvalue: .t1[0].f ∈ {4.} or UNINITIALIZED
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED {.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED
# multidim: { .t1[0] = { .f = {4.} } } # multidim: { .t1[0] = { .f = {4.} } }
...@@ -35,21 +47,28 @@ ...@@ -35,21 +47,28 @@
# multidim: 0 # multidim: 0
w : # cvalue: {0} w : # cvalue: {0}
# multidim: 0 # multidim: 0
[eva:alarm] multidim.c:45: Warning: assertion got status unknown.
[eva] multidim.c:46: [eva] multidim.c:46:
Frama_C_domain_show_each: Frama_C_domain_show_each:
x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[0].i ∈ [--..--] .t1[0].i ∈ [--..--]
.t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] .t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[1].i ∈ [--..--] .t1[1].i ∈ [--..--]
.t1[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64 .t1[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[2].i ∈ [--..--]
.t1[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t1[3].i ∈ [--..--]
.t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] .t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[0].i ∈ [--..--] .t2[0].i ∈ [--..--]
.t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] .t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[1].i ∈ [--..--] .t2[1].i ∈ [--..--]
.t2[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64 .t2[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
# multidim: { .t1[0..2] = { .f = {{ ANYTHING }} }, .t2[0..2] = { .t2[2].i ∈ [--..--]
.f = {{ ANYTHING }} } } .t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[3].i ∈ [--..--]
# multidim: {
.t1[0..3] = { .f = {{ ANYTHING }} },
.t2[0..3] = { .f = {{ ANYTHING }} }
}
[eva] computing for function f <- main. [eva] computing for function f <- main.
Called from multidim.c:48. Called from multidim.c:48.
[eva] using specification for function f [eva] using specification for function f
...@@ -57,47 +76,53 @@ ...@@ -57,47 +76,53 @@
[eva] multidim.c:49: [eva] multidim.c:49:
Frama_C_domain_show_each: Frama_C_domain_show_each:
z : # cvalue: [--..--] z : # cvalue: [--..--]
# multidim: [0..2] = { .t1[0..2] = { .f = T }, .t2[0..2] = { # multidim: [0..3] = {
.f = [-3.40282346639e+38 .. 3.40282346639e+38] } } .t1[0..3] = {
[eva:alarm] multidim.c:52: Warning: assertion got status unknown. .f = [-3.40282346639e+38 .. 3.40282346639e+38]
[eva] multidim.c:55: starting to merge loop iterations },
.t2[0..3] = {
.f = [-3.40282346639e+38 .. 3.40282346639e+38]
}
}
[eva:alarm] multidim.c:51: Warning: check got status unknown.
[eva] multidim.c:54: starting to merge loop iterations [eva] multidim.c:54: starting to merge loop iterations
[eva] multidim.c:53: starting to merge loop iterations
[kernel] multidim.c:55:
more than 1(20) locations to update in array. Approximating.
[kernel] multidim.c:56: [kernel] multidim.c:56:
more than 0(20) locations to update in array. Approximating. more than 1(20) locations to update in array. Approximating.
[kernel] multidim.c:57: [kernel] multidim.c:55:
more than 0(20) locations to update in array. Approximating. more than 1(28) locations to update in array. Approximating.
[kernel] multidim.c:56: [kernel] multidim.c:56:
more than 0(28) locations to update in array. Approximating. more than 1(28) locations to update in array. Approximating.
[kernel] multidim.c:57: [eva] multidim.c:60:
more than 0(28) locations to update in array. Approximating.
[eva] multidim.c:61:
Frama_C_domain_show_each: Frama_C_domain_show_each:
w : # cvalue: [0].t1[0].f ∈ [0. .. 2.] w : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
{[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈ {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
[--..--] [--..--]
[3].t1[3].i ∈ {0; 2} [3].t1[3].i ∈ {0; 2}
[3].t2[0..3] ∈ {0} [3].t2[0..3] ∈ {0}
# multidim: [0..3] = { .t1[0..3] = { .f = [0. .. 2.], .i = {0; 2} } } # multidim: [0..3] = { .t1[-1..3] = { .f = [0. .. 2.], .i = {0; 2} } }
[eva] computing for function Frama_C_interval <- main. [eva] computing for function Frama_C_interval <- main.
Called from multidim.c:63. Called from multidim.c:62.
[eva] using specification for function Frama_C_interval [eva] using specification for function Frama_C_interval
[eva] multidim.c:63: [eva] multidim.c:62:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- main. [eva] computing for function Frama_C_interval <- main.
Called from multidim.c:63. Called from multidim.c:62.
[eva] multidim.c:63: [eva] multidim.c:62:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [eva] Done for function Frama_C_interval
[eva] multidim.c:65: [eva] multidim.c:64:
Frama_C_domain_show_each: Frama_C_domain_show_each:
t1 : # cvalue: [--..--] t1 : # cvalue: [--..--]
# multidim: [--..--] # multidim: T
[eva] Recording results for main [eva] Recording results for main
[kernel] multidim.c:56: more than 0(28) elements to enumerate. Approximating. [kernel] multidim.c:55: more than 1(28) elements to enumerate. Approximating.
[kernel] multidim.c:57: more than 0(28) elements to enumerate. Approximating. [kernel] multidim.c:56: more than 1(28) elements to enumerate. Approximating.
[eva] done for function main [eva] done for function main
[kernel] multidim.c:52: more than 0(28) elements to enumerate. Approximating. [kernel] multidim.c:51: more than 1(28) elements to enumerate. Approximating.
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--] Frama_C_entropy_source ∈ [--..--]
...@@ -115,8 +140,8 @@ ...@@ -115,8 +140,8 @@
[from] Computing for function main [from] Computing for function main
[from] Computing for function f <-main [from] Computing for function f <-main
[from] Done for function f [from] Done for function f
[kernel] multidim.c:56: more than 0(28) dependencies to update. Approximating. [kernel] multidim.c:55: more than 1(28) dependencies to update. Approximating.
[kernel] multidim.c:57: more than 0(28) dependencies to update. Approximating. [kernel] multidim.c:56: more than 1(28) dependencies to update. Approximating.
[from] Computing for function Frama_C_interval <-main [from] Computing for function Frama_C_interval <-main
[from] Done for function Frama_C_interval [from] Done for function Frama_C_interval
[from] Done for function main [from] Done for function main
......
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