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

[Eva] multidim: better handling of assigns 

- fixed incorrect assigns
- imprecise but correct handling of allocates
- handling imprecise assigns on sub parts of a base
- always normalize the domain by removing tops when updating the map
parent 842197d0
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 71 additions and 4220 deletions
src/plugins/value/domains/multidim/multidim_domain.ml
+ 25
− 20
View file @ d63e0d47
......@@ -343,7 +343,7 @@ struct
include Datatype.Pair (Memory) (References)
let pretty_debug = pretty
let top = Memory.top, References.empty
let _istop (m,r) = Memory.is_top m && References.is_empty r
let is_top (m,r) = Memory.is_top m && References.is_empty r
end
module BaseMap =
......@@ -356,15 +356,17 @@ struct
let find_or_top (state : t) (b : Base.t) =
try find b state with Not_found -> V.top
(* Update or remove if top *)
let add (b : Base.t) (v : V.t) (state : t) =
if V.is_top v
then remove b state
else add b v state
let remove_var (state : t) (v : Cil_types.varinfo) =
remove (Base.of_varinfo v) state
let remove_vars (state : t) (l : Cil_types.varinfo list) =
List.fold_left remove_var state l
let remove_loc (state : t) (loc : Precise_locs.precise_location) =
let loc = Precise_locs.imprecise_location loc in
Locations.(Location_Bits.fold_bases remove loc.loc state)
end
include Datatype.Pair_with_collections
......@@ -512,10 +514,13 @@ struct
let oracle = convert_oracle oracle in
write (fun m off -> Memory.overwrite ~oracle ~weak m off value) state dst
let erase ~oracle
let erase ~oracle ?(weak: bool option)
(state : state) (dst : mdlocation) (b : Abstract_memory.bit): state =
let weak = not (Location.is_singleton dst)
and oracle = convert_oracle oracle in
let oracle = convert_oracle oracle
and weak = match weak with
| None -> not (Location.is_singleton dst)
| Some weak -> weak
in
write (fun m off -> Memory.erase ~oracle ~weak m off b) state dst
let reinforce
......@@ -764,18 +769,18 @@ struct
let (base_map,tracked) = state in
BaseMap.remove_vars base_map vars, tracked
let logic_assign assign location (base_map,tracked as state) =
match assign with
| None -> BaseMap.remove_loc base_map location, tracked
| Some ((Frees _ | Allocates _), _) -> state
| Some (Assigns (_dest, sources), _pre_state) ->
match sources with
| [] ->
let dst = Location.of_precise_loc location in
let oracle = mk_oracle state in
erase ~oracle state dst Abstract_memory.Bit.numerical
| _ ->
BaseMap.remove_loc base_map location, tracked
let logic_assign assign location state =
let oracle = mk_oracle state
and dst = Location.of_precise_loc location
and b =
match assign with
| None
| Some (Frees _, _)
| Some (Allocates _, _)
| Some (Assigns (_, _ :: _), _) -> Abstract_memory.Bit.top
| Some (Assigns (_, []), _) -> Abstract_memory.Bit.numerical
in
erase ~oracle ~weak:true state dst b
let reduce_by_papp env li _labels args positive state =
match li.l_var_info.lv_name, args with
......
tests/builtins/oracle_multidim/alloc-vla.res.oracle deleted 100644 → 0
+ 0
− 50
View file @ 842197d0
12,19d11
< [eva] alloc-vla.c:7: Call to builtin free
< [eva:alarm] alloc-vla.c:7: Warning:
< function free: precondition 'freeable' got status invalid.
< [eva] alloc-vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] alloc-vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva:alarm] alloc-vla.c:8: Warning:
< accessing left-value that contains escaping addresses.
< assert ¬\dangling(&a);
24d15
< [eva] alloc-vla.c:8: assertion 'Eva,dangling_pointer' got final status invalid.
27,29c18
< __fc_heap_status ∈ [--..--]
< a ∈ ESCAPINGADDR
< __lengthof_a ∈ {4}
---
> NON TERMINATING FUNCTION
35,38c24
< [from] Computing for function free <-f
< [from] Done for function free
< [from] Computing for function __fc_vla_free <-f
< [from] Done for function __fc_vla_free
---
> [from] Non-terminating function f (no dependencies)
47,50d32
< [from] Function __fc_vla_free:
< NO EFFECTS
< [from] Function free:
< __fc_heap_status FROM __fc_heap_status (and SELF)
52,53c34
< __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
< \result FROM \nothing
---
> NON TERMINATING - NO EFFECTS
58c39
< __fc_heap_status; a; __lengthof_a
---
> a; __lengthof_a
60c41
< __fc_heap_status; nondet
---
> \nothing
62c43
< __fc_heap_status; t
---
> t
64c45
< __fc_heap_status; nondet
---
> \nothing
tests/builtins/oracle_multidim/allocated.0.res.oracle deleted 100644 → 0
+ 0
− 94
View file @ 842197d0
96a97
> [eva] allocated.c:73: Call to builtin malloc
159,200d159
< [eva] allocated.c:131: Frama_C_show_each: {0}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva:malloc] allocated.c:127:
< resizing variable `__malloc_main_l127' (0..31) to fit 0..63
< [eva] allocated.c:128: starting to merge loop iterations
< [eva:alarm] allocated.c:129: Warning: out of bounds write. assert \valid(a + j);
< [eva] allocated.c:131: Frama_C_show_each: {0; 1}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:126: starting to merge loop iterations
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva:malloc] allocated.c:127:
< resizing variable `__malloc_main_l127' (0..31/63) to fit 0..63/95
< [eva] allocated.c:131: Frama_C_show_each: {0; 1; 2}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva:malloc] allocated.c:127:
< resizing variable `__malloc_main_l127' (0..31/95) to fit 0..63/127
< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva:malloc] allocated.c:127:
< resizing variable `__malloc_main_l127' (0..31/127) to fit 0..63/159
< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva:malloc] allocated.c:127:
< resizing variable `__malloc_main_l127' (0..31/159) to fit 0..63/191
< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva:malloc] allocated.c:127:
< resizing variable `__malloc_main_l127' (0..31/191) to fit 0..63/319
< [eva] allocated.c:131: Frama_C_show_each: [0..2147483647]
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
208,217c167
< __fc_heap_status ∈ [--..--]
< i ∈ {10}
< j ∈ [1..2147483647]
< p ∈ ESCAPINGADDR
< k ∈ {8; 12}
< size ∈ [1..100]
< pb ∈ ESCAPINGADDR
< __retres ∈ {0}
< __malloc_w_main_l82[0..1] ∈ [7..2147483647] or UNINITIALIZED
< [2] ∈ [7..27] or UNINITIALIZED
---
> NON TERMINATING FUNCTION
225,226c175
< [from] Computing for function __fc_vla_free <-main
< [from] Done for function __fc_vla_free
---
> [from] Non-terminating function main (no dependencies)
232,233d180
< [from] Function __fc_vla_free:
< NO EFFECTS
240,250c187
< __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l25 FROM __fc_heap_status
< __malloc_main_l36[0..1] FROM __fc_heap_status; nondet
< __malloc_main_l50[0..2] FROM __fc_heap_status; nondet
< __malloc_main_l63 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l73 FROM __fc_heap_status; nondet (and SELF)
< __malloc_w_main_l82[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l97[0] FROM __fc_heap_status; nondet
< __malloc_main_l114[0..3] FROM __fc_heap_status; nondet
< __malloc_main_l127[0..9] FROM \nothing (and SELF)
< \result FROM \nothing
---
> NON TERMINATING - NO EFFECTS
254,257c191,193
< __retres; __malloc_main_l25; __malloc_main_l36[0..1];
< __malloc_main_l50[0..2]; __malloc_main_l63; __malloc_main_l73;
< __malloc_w_main_l82[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127[0..9]
---
> __malloc_main_l25; __malloc_main_l36[0..1]; __malloc_main_l50[0..2];
> __malloc_main_l63; __malloc_main_l73; __malloc_w_main_l82[0..2];
> __malloc_main_l97[0]; __malloc_main_l114[0..3]
261,262c197
< __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0];
< __malloc_main_l127[0..9]
---
> __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0]
tests/builtins/oracle_multidim/allocated.1.res.oracle
+ 45
− 262
View file @ d63e0d47
......@@ -165,275 +165,58 @@
< [eva:malloc] allocated.c:87: strong free on bases: {__malloc_main_l82_7}
---
> [eva] allocated.c:81: Trace partitioning superposing up to 500 states
646,693d763
< [eva] allocated.c:131: Frama_C_show_each: {0}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_0
< [eva] allocated.c:131: Frama_C_show_each: {1}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_0}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_1
< [eva] allocated.c:131: Frama_C_show_each: {2}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_1}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_2
< [eva] allocated.c:131: Frama_C_show_each: {3}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_2}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_3
< [eva] allocated.c:131: Frama_C_show_each: {4}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_3}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_4
< [eva] allocated.c:131: Frama_C_show_each: {5}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_4}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_5
< [eva] allocated.c:131: Frama_C_show_each: {6}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_5}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_6
< [eva] allocated.c:131: Frama_C_show_each: {7}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_6}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_7
< [eva] allocated.c:131: Frama_C_show_each: {8}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_7}
< [eva] allocated.c:127: Call to builtin __fc_vla_alloc
< [eva] allocated.c:127: allocating variable __malloc_main_l127_8
< [eva] allocated.c:131: Frama_C_show_each: {9}
< [eva] allocated.c:127: Call to builtin __fc_vla_free
< [eva:malloc] allocated.c:127: strong free on bases: {__malloc_main_l127_8}
701,792c771
< __fc_heap_status ∈ [--..--]
< i ∈ {10}
< j ∈ {10}
< p ∈ ESCAPINGADDR
< k ∈ {12}
< size ∈ [1..100]
< pb ∈ ESCAPINGADDR
< __retres ∈ {0}
< __malloc_main_l82_0 ∈ {7} or UNINITIALIZED
< __malloc_main_l82_1 ∈ {7} or UNINITIALIZED
< __malloc_main_l82_2[0] ∈ {14} or UNINITIALIZED
< [1] ∈ {17} or UNINITIALIZED
< __malloc_main_l82_3[0] ∈ {14} or UNINITIALIZED
< [1] ∈ {17} or UNINITIALIZED
< __malloc_main_l82_4[0] ∈ {14} or UNINITIALIZED
< [1] ∈ {17} or UNINITIALIZED
< __malloc_main_l82_5[0] ∈ {14} or UNINITIALIZED
< [1] ∈ {17} or UNINITIALIZED
< __malloc_main_l82_6[0] ∈ {14} or UNINITIALIZED
< [1] ∈ {17} or UNINITIALIZED
721,723c839,840
< __malloc_main_l82_7[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_8[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_9[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_10[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_11[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_12[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_13[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_14[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_15[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_16[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_17[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_18[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_19[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_20[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_21[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_22[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_23[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_24[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_25[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_26[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_27[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_28[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_29[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
< __malloc_main_l82_30[0] ∈ {21} or UNINITIALIZED
< [1] ∈ {24} or UNINITIALIZED
< [2] ∈ {27} or UNINITIALIZED
---
> NON TERMINATING FUNCTION
800,801c779
< [from] Computing for function __fc_vla_free <-main
< [from] Done for function __fc_vla_free
---
> [from] Non-terminating function main (no dependencies)
807,808d784
< [from] Function __fc_vla_free:
< NO EFFECTS
815,872c791
< __fc_heap_status FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l25 FROM __fc_heap_status
< __malloc_main_l36[0..1] FROM __fc_heap_status; nondet
< __malloc_main_l50[0..1] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l50_0[0..1] FROM __fc_heap_status; nondet (and SELF)
< [2] FROM __fc_heap_status; nondet
< __malloc_main_l63 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l63_0 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l63_1 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l63_2 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l73 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l73_0 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l73_1 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l73_2 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_0 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_1 FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_2[0..1] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_3[0..1] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_4[0..1] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_5[0..1] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_6[0..1] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_7[0] ∈ {14} or UNINITIALIZED
> [1] ∈ {17} or UNINITIALIZED
792a910,930
> __malloc_main_l82_31[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
> __malloc_main_l82_32[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
> __malloc_main_l82_33[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
> __malloc_main_l82_34[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
> __malloc_main_l82_35[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
> __malloc_main_l82_36[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
> __malloc_main_l82_37[0] ∈ {21} or UNINITIALIZED
> [1] ∈ {24} or UNINITIALIZED
> [2] ∈ {27} or UNINITIALIZED
836c974
< __malloc_main_l82_7[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_8[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_9[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_10[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_11[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_12[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_13[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_14[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_15[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_16[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_17[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_18[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_19[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_20[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_21[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_22[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_23[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_24[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_25[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_26[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_27[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_28[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_29[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l82_30[0..2] FROM __fc_heap_status; nondet (and SELF)
< __malloc_main_l97[0] FROM __fc_heap_status; nondet
< __malloc_main_l114[0..3] FROM __fc_heap_status; nondet
< __malloc_main_l127 FROM \nothing (and SELF)
< __malloc_main_l127_0[0..1] FROM \nothing (and SELF)
< __malloc_main_l127_1[0..2] FROM \nothing (and SELF)
< __malloc_main_l127_2[0..3] FROM \nothing (and SELF)
< __malloc_main_l127_3[0..4] FROM \nothing (and SELF)
< __malloc_main_l127_4[0..5] FROM \nothing (and SELF)
< __malloc_main_l127_5[0..6] FROM \nothing (and SELF)
< __malloc_main_l127_6[0..7] FROM \nothing (and SELF)
< __malloc_main_l127_7[0..8] FROM \nothing (and SELF)
< __malloc_main_l127_8[0..9] FROM \nothing (and SELF)
< \result FROM \nothing
---
> NON TERMINATING - NO EFFECTS
876,900c795,817
< __retres; __malloc_main_l25; __malloc_main_l36[0..1];
< __malloc_main_l50[0..1]; __malloc_main_l50_0[0..2]; __malloc_main_l63;
< __malloc_main_l63_0; __malloc_main_l63_1; __malloc_main_l63_2;
< __malloc_main_l73; __malloc_main_l73_0; __malloc_main_l73_1;
< __malloc_main_l73_2; __malloc_main_l82_0; __malloc_main_l82_1;
< __malloc_main_l82_2[0..1]; __malloc_main_l82_3[0..1];
< __malloc_main_l82_4[0..1]; __malloc_main_l82_5[0..1];
> __malloc_main_l82_7[0..1] FROM __fc_heap_status; nondet (and SELF)
859a998,1004
> __malloc_main_l82_31[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_32[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_33[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_34[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_35[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_36[0..2] FROM __fc_heap_status; nondet (and SELF)
> __malloc_main_l82_37[0..2] FROM __fc_heap_status; nondet (and SELF)
883c1028
< __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..2];
< __malloc_main_l82_8[0..2]; __malloc_main_l82_9[0..2];
< __malloc_main_l82_10[0..2]; __malloc_main_l82_11[0..2];
< __malloc_main_l82_12[0..2]; __malloc_main_l82_13[0..2];
< __malloc_main_l82_14[0..2]; __malloc_main_l82_15[0..2];
< __malloc_main_l82_16[0..2]; __malloc_main_l82_17[0..2];
< __malloc_main_l82_18[0..2]; __malloc_main_l82_19[0..2];
< __malloc_main_l82_20[0..2]; __malloc_main_l82_21[0..2];
< __malloc_main_l82_22[0..2]; __malloc_main_l82_23[0..2];
< __malloc_main_l82_24[0..2]; __malloc_main_l82_25[0..2];
< __malloc_main_l82_26[0..2]; __malloc_main_l82_27[0..2];
< __malloc_main_l82_28[0..2]; __malloc_main_l82_29[0..2];
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
< __malloc_main_l127_2[0..3]; __malloc_main_l127_3[0..4];
< __malloc_main_l127_4[0..5]; __malloc_main_l127_5[0..6];
< __malloc_main_l127_6[0..7]; __malloc_main_l127_7[0..8];
< __malloc_main_l127_8[0..9]
---
> __malloc_main_l25; __malloc_main_l36[0..1]; __malloc_main_l50[0..1];
> __malloc_main_l50_0[0..2]; __malloc_main_l63; __malloc_main_l63_0;
> __malloc_main_l63_1; __malloc_main_l63_2; __malloc_main_l73;
> __malloc_main_l73_0; __malloc_main_l73_1; __malloc_main_l73_2;
> __malloc_main_l82_0; __malloc_main_l82_1; __malloc_main_l82_2[0..1];
> __malloc_main_l82_3[0..1]; __malloc_main_l82_4[0..1];
> __malloc_main_l82_5[0..1]; __malloc_main_l82_6[0..1];
> __malloc_main_l82_7[0..1]; __malloc_main_l82_8[0..2];
> __malloc_main_l82_9[0..2]; __malloc_main_l82_10[0..2];
> __malloc_main_l82_11[0..2]; __malloc_main_l82_12[0..2];
> __malloc_main_l82_13[0..2]; __malloc_main_l82_14[0..2];
> __malloc_main_l82_15[0..2]; __malloc_main_l82_16[0..2];
> __malloc_main_l82_17[0..2]; __malloc_main_l82_18[0..2];
> __malloc_main_l82_19[0..2]; __malloc_main_l82_20[0..2];
> __malloc_main_l82_21[0..2]; __malloc_main_l82_22[0..2];
> __malloc_main_l82_23[0..2]; __malloc_main_l82_24[0..2];
> __malloc_main_l82_25[0..2]; __malloc_main_l82_26[0..2];
> __malloc_main_l82_27[0..2]; __malloc_main_l82_28[0..2];
> __malloc_main_l82_29[0..2]; __malloc_main_l82_30[0..2];
> __malloc_main_l82_31[0..2]; __malloc_main_l82_32[0..2];
> __malloc_main_l82_33[0..2]; __malloc_main_l82_34[0..2];
> __malloc_main_l82_35[0..2]; __malloc_main_l82_36[0..2];
> __malloc_main_l82_37[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3]
906,911c823
< __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0];
> __malloc_main_l82_6[0..1]; __malloc_main_l82_7[0..1];
895,896c1040,1045
< __malloc_main_l82_30[0..2]; __malloc_main_l97[0]; __malloc_main_l114[0..3];
< __malloc_main_l127; __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
< __malloc_main_l127_2[0..3]; __malloc_main_l127_3[0..4];
< __malloc_main_l127_4[0..5]; __malloc_main_l127_5[0..6];
< __malloc_main_l127_6[0..7]; __malloc_main_l127_7[0..8];
< __malloc_main_l127_8[0..9]
---
> __malloc_main_l97[0][bits 0 to 0]; __malloc_main_l114[0][bits 0 to 0]
> __malloc_main_l82_30[0..2]; __malloc_main_l82_31[0..2];
> __malloc_main_l82_32[0..2]; __malloc_main_l82_33[0..2];
> __malloc_main_l82_34[0..2]; __malloc_main_l82_35[0..2];
> __malloc_main_l82_36[0..2]; __malloc_main_l82_37[0..2];
> __malloc_main_l97[0]; __malloc_main_l114[0..3]; __malloc_main_l127;
> __malloc_main_l127_0[0..1]; __malloc_main_l127_1[0..2];
tests/builtins/oracle_multidim/malloc-optimistic.res.oracle deleted 100644 → 0
+ 0
− 3655
View file @ 842197d0
This diff is collapsed.
tests/builtins/oracle_multidim/vla.res.oracle deleted 100644 → 0
+ 0
− 138
View file @ 842197d0
12,14d11
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
17,106d13
< [eva] vla.c:20: freeing automatic bases: {__malloc_f_l6}
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6: resizing variable `__malloc_f_l6' (0..63) to fit 0..95
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva:alarm] vla.c:8: Warning: out of bounds write. assert \valid(t + i);
< [eva:alarm] vla.c:9: Warning: out of bounds read. assert \valid_read(t + i);
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6: resizing variable `__malloc_f_l6' (0..63/95) to fit 0..127
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6:
< resizing variable `__malloc_f_l6' (0..63/127) to fit 0..159
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6:
< resizing variable `__malloc_f_l6' (0..63/159) to fit 0..191
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6:
< resizing variable `__malloc_f_l6' (0..63/191) to fit 0..223
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6:
< resizing variable `__malloc_f_l6' (0..63/223) to fit 0..255
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6:
< resizing variable `__malloc_f_l6' (0..63/255) to fit 0..287
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
< [eva] computing for function f <- main.
< Called from vla.c:20.
< [eva] vla.c:6: Call to builtin __fc_vla_alloc
< [eva:malloc] vla.c:6:
< resizing variable `__malloc_f_l6' (0..63/287) to fit 0..319
< [eva] vla.c:7: Frama_C_show_each: {{ &__malloc_f_l6 }}
< [eva] vla.c:6: Call to builtin __fc_vla_free
< [eva:malloc] vla.c:6: strong free on bases: {__malloc_f_l6}
< [eva] Recording results for f
< [eva] Done for function f
< [eva:malloc] vla.c:20: strong free on bases: {__malloc_f_l6}
111,112c18
< t ∈ ESCAPINGADDR
< __lengthof_t ∈ [2..10]
---
> NON TERMINATING FUNCTION
114c20
< i ∈ {10}
---
> NON TERMINATING FUNCTION
118,119c24
< [from] Computing for function __fc_vla_free <-f
< [from] Done for function __fc_vla_free
---
> [from] Non-terminating function f (no dependencies)
121a27
> [from] Non-terminating function main (no dependencies)
127,128d32
< [from] Function __fc_vla_free:
< NO EFFECTS
130c34
< __malloc_f_l6[1..9] FROM i (and SELF)
---
> NON TERMINATING - NO EFFECTS
132c36
< __malloc_f_l6[1..9] FROM \nothing (and SELF)
---
> NON TERMINATING - NO EFFECTS
135c39
< t; __lengthof_t; __malloc_f_l6[1..9]
---
> t; __lengthof_t
137c41
< __malloc_f_l6[1..9]
---
> \nothing
139c43
< i; __malloc_f_l6[1..9]
---
> i
141c45
< __malloc_f_l6[1..9]
---
> \nothing
tests/value/oracle_multidim/multidim.res.oracle
+ 1
− 1
View file @ d63e0d47
4d3
2d1
< [eva:experimental] Warning: The multidim domain is experimental.
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