diff --git a/tests/specs/oracle/assigns.res.oracle b/tests/specs/oracle/assigns.res.oracle
index 64da5ca26a74e91db6998b0cdaf9df5498c91394..b92679e0f0276ea6309e41be8cfd2d616b62309b 100644
--- a/tests/specs/oracle/assigns.res.oracle
+++ b/tests/specs/oracle/assigns.res.oracle
@@ -5,8 +5,10 @@ Now output intermediate result
[eva:initial-state] Values of globals at initialization
[kernel:annot:missing-spec] assigns.cc:14: Warning:
- Neither code nor explicit assigns clause for function swap, generating default assigns from the specification
+ Neither code nor explicit assigns for function swap,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[eva] using specification for function swap
+[kernel] assigns.cc:14: Warning: keeping only assigns from behaviors: default!
[eva:alarm] assigns.cc:15: Warning: assertion got status unknown.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
@@ -19,7 +21,7 @@ Now output intermediate result
/*@ requires \valid(q);
requires \valid(p);
assigns *p, *q;
- assigns *p \from *q, *p;
+ assigns *p \from *p, *q;
assigns *q \from *p;
behavior default:
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index 29d4c6aa5f2466de4e1d21989683cc368f5b5bcf..f6e48157e8a0ec12875bf676d6f38613ee93fa94 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -21,10 +21,10 @@ Now output intermediate result
[kernel] Warning: Assuming declared function free can't throw any exception
[kernel] Warning: Assuming declared function malloc can't throw any exception
[kernel] Warning: Assuming declared function free can't throw any exception
-[kernel:annot:missing-spec] stl_unique_ptr.cpp:105: Warning:
- Neither code nor specification for function malloc, generating default assigns from the prototype
-[kernel:annot:missing-spec] stl_unique_ptr.cpp:105: Warning:
- Neither code nor specification for function free, generating default assigns from the prototype
+[eva:builtins:missing-spec] <builtin>:0: Warning:
+ The builtin for function malloc will not be used, as its frama-c libc specification is not available.
+[eva:builtins:missing-spec] <builtin>:0: Warning:
+ The builtin for function free will not be used, as its frama-c libc specification is not available.
[eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization
_frama_c_rtti_name_info.name ∈ {{ "integral_constant" }}
@@ -254,552 +254,57 @@ Now output intermediate result
_frama_c_rtti_name_info.name ∈ {{ "ClassTemplate" }}
{.base_classes; .number_of_base_classes; .pvmt} ∈
{0}
-[eva] stl_unique_ptr.cpp:9:
- allocating variable __malloc_test_primitive_payload_l9
+[kernel:annot:missing-spec] stl_unique_ptr.cpp:9: Warning:
+ Neither code nor specification for function malloc,
+ generating default assigns. See -generated-spec-* options for more info
+[eva] using specification for function malloc
[eva:alarm] share/libc++/memory:477: Warning:
- function operator*: postcondition got status unknown.
-[eva] stl_unique_ptr.cpp:15:
- allocating variable __malloc_test_primitive_payload_l15
-[eva:alarm] share/libc++/memory:577: Warning:
- function operator[]: postcondition got status unknown.
-[eva:alarm] stl_unique_ptr.cpp:17: Warning:
- signed overflow.
- assert *tmp_6 + 1 ≤ 2147483647;
- (tmp_6 from
- _ZNK3std10unique_ptrIA_iN3stdE14default_deleteIA_iEEEixRij((struct _ZN3stdE10unique_ptrIA_iN3stdE14default_deleteIA_iEE const *)(& up3), (_ZN3stdE6size_t)0))
-[eva:alarm] stl_unique_ptr.cpp:29: Warning:
- out of bounds read. assert \valid_read(up5_raw + 0);
-[eva] stl_unique_ptr.cpp:44:
- allocating variable __malloc_test_struct_payload_l44
-[eva:alarm] stl_unique_ptr.cpp:44: Warning:
- function PlainOldStruct::Ctor: precondition got status unknown.
-[eva] stl_unique_ptr.cpp:78:
- allocating variable __malloc_test_template_payload_l78
-[eva:alarm] stl_unique_ptr.cpp:78: Warning:
- function ClassTemplate<int,0>::Ctor: precondition got status unknown.
+ function operator*: postcondition got status invalid.
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 74 functions analyzed (out of 100): 74% coverage.
- In these functions, 262 statements reached (out of 293): 89% coverage.
+ 5 functions analyzed (out of 100): 5% coverage.
+ In these functions, 16 statements reached (out of 55): 29% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
- by the Eva analyzer: 0 errors 0 warnings
- by the Frama-C kernel: 0 errors 21 warnings
+ by the Eva analyzer: 0 errors 2 warnings
+ by the Frama-C kernel: 0 errors 20 warnings
----------------------------------------------------------------------------
- 2 alarms generated by the analysis:
- 1 invalid memory access
- 1 integer overflow
+ 0 alarms generated by the analysis.
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 0 unknown 0 invalid 0 total
- Preconditions 142 valid 2 unknown 0 invalid 144 total
- 98% of the logical properties reached have been proven.
+ Preconditions 5 valid 0 unknown 0 invalid 5 total
+ 100% of the logical properties reached have been proven.
----------------------------------------------------------------------------
-[from] Computing for function pull
-[from] Done for function pull
-[from] Computing for function push
-[from] Done for function push
-[from] Computing for function ClassTemplate<int,0>::Ctor
-[from] Done for function ClassTemplate<int,0>::Ctor
-[from] Computing for function ClassTemplate<int,0>::Dtor
-[from] Done for function ClassTemplate<int,0>::Dtor
-[from] Computing for function pull
-[from] Done for function pull
-[from] Computing for function push
-[from] Done for function push
-[from] Computing for function PlainOldStruct::Ctor
-[from] Done for function PlainOldStruct::Ctor
-[from] Computing for function PlainOldStruct::Dtor
-[from] Done for function PlainOldStruct::Dtor
-[from] Computing for function release
-[from] Done for function release
-[from] Computing for function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Dtor
-[from] Done for function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Dtor
-[from] Computing for function release
-[from] Done for function release
-[from] Computing for function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Dtor
-[from] Done for function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Dtor
-[from] Computing for function release
-[from] Done for function release
-[from] Computing for function unique_ptr<int[],std::default_delete<int[]>>::Dtor
-[from] Done for function unique_ptr<int[],std::default_delete<int[]>>::Dtor
-[from] Computing for function release
-[from] Done for function release
-[from] Computing for function unique_ptr<int,std::default_delete<int>>::Dtor
-[from] Done for function unique_ptr<int,std::default_delete<int>>::Dtor
-[from] Computing for function default_delete<ClassTemplate<int,0>>::Ctor
-[from] Done for function default_delete<ClassTemplate<int,0>>::Ctor
-[from] Computing for function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Ctor
-[from] Done for function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Ctor
-[from] Computing for function default_delete<ClassTemplate<int,0>>::Ctor
-[from] Done for function default_delete<ClassTemplate<int,0>>::Ctor
-[from] Computing for function default_delete<ClassTemplate<int,0>>::Ctor
-[from] Done for function default_delete<ClassTemplate<int,0>>::Ctor
-[from] Computing for function default_delete<ClassTemplate<int,0>>::Dtor
-[from] Done for function default_delete<ClassTemplate<int,0>>::Dtor
-[from] Computing for function operator=
-[from] Done for function operator=
-[from] Computing for function default_delete<PlainOldStruct>::Ctor
-[from] Done for function default_delete<PlainOldStruct>::Ctor
-[from] Computing for function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Ctor
-[from] Done for function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Ctor
-[from] Computing for function default_delete<PlainOldStruct>::Ctor
-[from] Done for function default_delete<PlainOldStruct>::Ctor
-[from] Computing for function default_delete<PlainOldStruct>::Ctor
-[from] Done for function default_delete<PlainOldStruct>::Ctor
-[from] Computing for function default_delete<PlainOldStruct>::Dtor
-[from] Done for function default_delete<PlainOldStruct>::Dtor
-[from] Computing for function operator=
-[from] Done for function operator=
-[from] Computing for function default_delete<int[]>::Ctor
-[from] Done for function default_delete<int[]>::Ctor
-[from] Computing for function unique_ptr<int[],std::default_delete<int[]>>::Ctor
-[from] Done for function unique_ptr<int[],std::default_delete<int[]>>::Ctor
-[from] Computing for function default_delete<int[]>::Ctor
-[from] Done for function default_delete<int[]>::Ctor
[from] Computing for function default_delete<int>::Ctor
[from] Done for function default_delete<int>::Ctor
[from] Computing for function unique_ptr<int,std::default_delete<int>>::Ctor
[from] Done for function unique_ptr<int,std::default_delete<int>>::Ctor
-[from] Computing for function default_delete<int>::Ctor
-[from] Done for function default_delete<int>::Ctor
-[from] Computing for function default_delete<int>::Dtor
-[from] Done for function default_delete<int>::Dtor
-[from] Computing for function operator=
-[from] Done for function operator=
-[from] Computing for function move<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>&>
-[from] Done for function move<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>&>
-[from] Computing for function move<std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>&>
-[from] Done for function move<std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>&>
-[from] Computing for function move<std::unique_ptr<int[],std::default_delete<int[]>>&>
-[from] Done for function move<std::unique_ptr<int[],std::default_delete<int[]>>&>
-[from] Computing for function swap<std::default_delete<ClassTemplate<int,0>>>
-[from] Done for function swap<std::default_delete<ClassTemplate<int,0>>>
-[from] Computing for function swap<std::default_delete<PlainOldStruct>>
-[from] Done for function swap<std::default_delete<PlainOldStruct>>
-[from] Computing for function swap<std::default_delete<int>>
-[from] Done for function swap<std::default_delete<int>>
-[from] Computing for function swap<ClassTemplate<int,0>*>
-[from] Done for function swap<ClassTemplate<int,0>*>
-[from] Computing for function swap
-[from] Done for function swap
-[from] Computing for function swap<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>
-[from] Done for function swap<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>
-[from] Computing for function swap<PlainOldStruct*>
-[from] Done for function swap<PlainOldStruct*>
-[from] Computing for function swap
-[from] Done for function swap
-[from] Computing for function swap<PlainOldStruct,std::default_delete<PlainOldStruct>>
-[from] Done for function swap<PlainOldStruct,std::default_delete<PlainOldStruct>>
-[from] Computing for function swap<int*>
-[from] Done for function swap<int*>
-[from] Computing for function swap
-[from] Done for function swap
-[from] Computing for function swap<int,std::default_delete<int>>
-[from] Done for function swap<int,std::default_delete<int>>
-[from] Computing for function forward<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>>
-[from] Done for function forward<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>>
-[from] Computing for function forward<std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>>
-[from] Done for function forward<std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>>
-[from] Computing for function forward<std::unique_ptr<int[],std::default_delete<int[]>>>
-[from] Done for function forward<std::unique_ptr<int[],std::default_delete<int[]>>>
-[from] Computing for function forward<std::default_delete<ClassTemplate<int,0>>>
-[from] Done for function forward<std::default_delete<ClassTemplate<int,0>>>
-[from] Computing for function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Ctor
-[from] Done for function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Ctor
-[from] Computing for function forward<std::default_delete<PlainOldStruct>>
-[from] Done for function forward<std::default_delete<PlainOldStruct>>
-[from] Computing for function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Ctor
-[from] Done for function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Ctor
-[from] Computing for function forward<std::default_delete<int[]>>
-[from] Done for function forward<std::default_delete<int[]>>
-[from] Computing for function unique_ptr<int[],std::default_delete<int[]>>::Ctor
-[from] Done for function unique_ptr<int[],std::default_delete<int[]>>::Ctor
-[from] Computing for function std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::operator->
-[from] Done for function std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::operator->
-[from] Computing for function std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::operator->
-[from] Done for function std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::operator->
-[from] Computing for function operator[]
-[from] Done for function operator[]
[from] Computing for function operator*
[from] Done for function operator*
-[from] Computing for function operator()
-[from] Computing for function free <-operator()
-[from] Done for function free
-[from] Done for function operator()
-[from] Computing for function reset
-[from] Done for function reset
-[from] Computing for function operator()
-[from] Done for function operator()
-[from] Computing for function reset
-[from] Done for function reset
-[from] Computing for function operator()
-[from] Done for function operator()
-[from] Computing for function reset
-[from] Done for function reset
-[from] Computing for function test_struct_payload
-[from] Computing for function malloc <-test_struct_payload
-[from] Done for function malloc
-[from] Done for function test_struct_payload
-[from] Computing for function test_template_payload
-[from] Done for function test_template_payload
[from] Computing for function test_primitive_payload
+[from] Computing for function malloc <-test_primitive_payload
+[from] Done for function malloc
+[from] Non-terminating function test_primitive_payload (no dependencies)
[from] Done for function test_primitive_payload
[from] Computing for function main
+[from] Non-terminating function main (no dependencies)
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
-[from] Function pull:
- \result FROM this
-[from] Function push:
- ct FROM this; x; var
-[from] Function ClassTemplate<int,0>::Ctor:
- NO EFFECTS
-[from] Function ClassTemplate<int,0>::Dtor:
- NO EFFECTS
-[from] Function pull:
- \result FROM this; pos
-[from] Function push:
- pos FROM this; x (and SELF)
- __malloc_test_struct_payload_l44 FROM this; x (and SELF)
-[from] Function PlainOldStruct::Ctor:
- NO EFFECTS
-[from] Function PlainOldStruct::Dtor:
- NO EFFECTS
-[from] Function release:
- up4 FROM this
- \result FROM this; up4
-[from] Function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Dtor:
- NO EFFECTS
-[from] Function release:
- up4 FROM this
- \result FROM this; up4
-[from] Function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Dtor:
- NO EFFECTS
-[from] Function release:
- up5 FROM this
- \result FROM this; up5
-[from] Function unique_ptr<int[],std::default_delete<int[]>>::Dtor:
- NO EFFECTS
-[from] Function release:
- up2 FROM this
- \result FROM this; up2
-[from] Function unique_ptr<int,std::default_delete<int>>::Dtor:
- NO EFFECTS
-[from] Function default_delete<ClassTemplate<int,0>>::Ctor:
- NO EFFECTS
-[from] Function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Ctor:
- up1 FROM this; p (and SELF)
- up2 FROM this; p (and SELF)
-[from] Function default_delete<ClassTemplate<int,0>>::Ctor:
- NO EFFECTS
-[from] Function default_delete<ClassTemplate<int,0>>::Ctor:
- NO EFFECTS
-[from] Function default_delete<ClassTemplate<int,0>>::Dtor:
- NO EFFECTS
-[from] Function operator=:
- \result FROM this
-[from] Function default_delete<PlainOldStruct>::Ctor:
- NO EFFECTS
-[from] Function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Ctor:
- up1 FROM this; p (and SELF)
- up2 FROM this; p (and SELF)
-[from] Function default_delete<PlainOldStruct>::Ctor:
- NO EFFECTS
-[from] Function default_delete<PlainOldStruct>::Ctor:
- NO EFFECTS
-[from] Function default_delete<PlainOldStruct>::Dtor:
- NO EFFECTS
-[from] Function operator=:
- \result FROM this
-[from] Function default_delete<int[]>::Ctor:
- NO EFFECTS
-[from] Function unique_ptr<int[],std::default_delete<int[]>>::Ctor:
- up3 FROM this; p
-[from] Function default_delete<int[]>::Ctor:
- NO EFFECTS
[from] Function default_delete<int>::Ctor:
NO EFFECTS
[from] Function unique_ptr<int,std::default_delete<int>>::Ctor:
up1 FROM this; p (and SELF)
up2 FROM this; p (and SELF)
-[from] Function default_delete<int>::Ctor:
- NO EFFECTS
-[from] Function default_delete<int>::Dtor:
- NO EFFECTS
-[from] Function operator=:
- \result FROM this
-[from] Function move<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>&>:
- \result FROM t
-[from] Function move<std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>&>:
- \result FROM t
-[from] Function move<std::unique_ptr<int[],std::default_delete<int[]>>&>:
- \result FROM t
-[from] Function swap<std::default_delete<ClassTemplate<int,0>>>:
- NO EFFECTS
-[from] Function swap<std::default_delete<PlainOldStruct>>:
- NO EFFECTS
-[from] Function swap<std::default_delete<int>>:
- NO EFFECTS
-[from] Function swap<ClassTemplate<int,0>*>:
- up1 FROM a; b; up2
- up2 FROM a; b; up1
-[from] Function swap:
- up1 FROM this; u; up2
- up2 FROM this; u; up1
-[from] Function swap<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>:
- up1 FROM x; y; up2
- up2 FROM x; y; up1
-[from] Function swap<PlainOldStruct*>:
- up1 FROM a; b; up2
- up2 FROM a; b; up1
-[from] Function swap:
- up1 FROM this; u; up2
- up2 FROM this; u; up1
-[from] Function swap<PlainOldStruct,std::default_delete<PlainOldStruct>>:
- up1 FROM x; y; up2
- up2 FROM x; y; up1
-[from] Function swap<int*>:
- up1 FROM a; b; up2
- up2 FROM a; b; up1
-[from] Function swap:
- up1 FROM this; u; up2
- up2 FROM this; u; up1
-[from] Function swap<int,std::default_delete<int>>:
- up1 FROM x; y; up2
- up2 FROM x; y; up1
-[from] Function forward<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>>:
- \result FROM t
-[from] Function forward<std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>>:
- \result FROM t
-[from] Function forward<std::unique_ptr<int[],std::default_delete<int[]>>>:
- \result FROM t
-[from] Function forward<std::default_delete<ClassTemplate<int,0>>>:
- \result FROM t
-[from] Function unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::Ctor:
- up2 FROM u (and SELF)
- up3 FROM this; u; up2; up3 (and SELF)
- up4 FROM this; u; up2; up3 (and SELF)
-[from] Function forward<std::default_delete<PlainOldStruct>>:
- \result FROM t
-[from] Function unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::Ctor:
- up2 FROM u (and SELF)
- up3 FROM this; u; up2; up3 (and SELF)
- up4 FROM this; u; up2; up3 (and SELF)
-[from] Function forward<std::default_delete<int[]>>:
- \result FROM t
-[from] Function unique_ptr<int[],std::default_delete<int[]>>::Ctor:
- up3 FROM u (and SELF)
- up4 FROM this; u; up3; up4 (and SELF)
- up5 FROM this; u; up3; up4 (and SELF)
-[from] Function std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>::operator->:
- \result FROM this; up1; up4
-[from] Function std::unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>>::operator->:
- \result FROM this; up1; up2; up4
-[from] Function operator[]:
- \result FROM this; i; up3
[from] Function operator*:
\result FROM this; up1; up2
-[from] Function free:
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
-[from] Function operator():
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
-[from] Function reset:
- up1 FROM this; p
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
-[from] Function operator():
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
-[from] Function reset:
- up1 FROM this; p
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
-[from] Function operator():
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
-[from] Function reset:
- up1 FROM this; p
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
[from] Function malloc:
\result FROM size
-[from] Function test_struct_payload:
- __malloc_test_primitive_payload_l9[0..3] FROM var;
- __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM var;
- __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM var;
- __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM var;
- __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- \result FROM var
-[from] Function test_template_payload:
- __malloc_test_primitive_payload_l9[0..3] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_primitive_payload_l15[0..7] FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_struct_payload_l44 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM __malloc_test_primitive_payload_l9[0..3];
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- \result FROM var
[from] Function test_primitive_payload:
- __malloc_test_primitive_payload_l9[0..3] FROM var;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78
- __malloc_test_primitive_payload_l15[0..7] FROM var;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78
- __malloc_test_struct_payload_l44 FROM var;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM var;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- \result FROM var
+ NON TERMINATING - NO EFFECTS
[from] Function main:
- __malloc_test_primitive_payload_l9[0..3] FROM argc;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78
- __malloc_test_primitive_payload_l15[0..7] FROM argc;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78
- __malloc_test_struct_payload_l44 FROM argc;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- __malloc_test_template_payload_l78 FROM argc;
- __malloc_test_primitive_payload_l15[0..7];
- __malloc_test_struct_payload_l44;
- __malloc_test_template_payload_l78 (and SELF)
- \result FROM argc
+ NON TERMINATING - NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
/* Generated by Frama-C */
struct _frama_c_vmt_content {
@@ -944,9 +449,6 @@ struct ClassTemplate<int,0> {
assigns \result \from size; */
void *malloc(unsigned int size);
-/*@ assigns *((char *)ptr + (0 ..));
- assigns *((char *)ptr + (0 ..)) \from *((char *)ptr + (0 ..));
- */
void free(void *ptr);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
@@ -3890,7 +3392,6 @@ int test_primitive_payload(int var)
(size_t)1);
tmp_6 = operator[]((struct unique_ptr<int[],std::default_delete<int[]>> const *)(& up3),
(size_t)0);
- /*@ assert Eva: signed_overflow: *tmp_6 + 1 ≤ 2147483647; */
*tmp_5 = *tmp_6 + 1;
int *up2_raw = release(& up2);
if (up2_raw != & var) {
@@ -3909,7 +3410,6 @@ int test_primitive_payload(int var)
struct unique_ptr<int[],std::default_delete<int[]>> up5;
unique_ptr<int[],std::default_delete<int[]>>::Ctor(& up5,tmp_9);
int *up5_raw = release(& up5);
- /*@ assert Eva: mem_access: \valid_read(up5_raw + 0); */
int result = *(up5_raw + 0);
free((void *)up5_raw);
__retres = result;
diff --git a/tests/val_analysis/oracle/union.res.oracle b/tests/val_analysis/oracle/union.res.oracle
index 0e33669957ef8446b58e478bf8c63a86097450f7..405c988678910e2bc548e112b857066e2a5fbca6 100644
--- a/tests/val_analysis/oracle/union.res.oracle
+++ b/tests/val_analysis/oracle/union.res.oracle
@@ -2,7 +2,8 @@
Now output intermediate result
[kernel] Warning: Assuming declared function Frama_C_memcpy can't throw any exception
[kernel:annot:missing-spec] union.cc:8: Warning:
- Neither code nor specification for function Frama_C_memcpy, generating default assigns from the prototype
+ Neither code nor specification for function Frama_C_memcpy,
+ generating default assigns. See -generated-spec-* options for more info
[eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization
_frama_c_rtti_name_info.name ∈ {{ "A" }}
diff --git a/tests/val_analysis/oracle/union_struct.res.oracle b/tests/val_analysis/oracle/union_struct.res.oracle
index 7134aa77fb233323c7d77210068f1842ddcae9f7..310b41e160fe9a773f8fa16e08e9520b9b6a66be 100644
--- a/tests/val_analysis/oracle/union_struct.res.oracle
+++ b/tests/val_analysis/oracle/union_struct.res.oracle
@@ -2,7 +2,8 @@
Now output intermediate result
[kernel] Warning: Assuming declared function Frama_C_memcpy can't throw any exception
[kernel:annot:missing-spec] union_struct.cc:17: Warning:
- Neither code nor specification for function Frama_C_memcpy, generating default assigns from the prototype
+ Neither code nor specification for function Frama_C_memcpy,
+ generating default assigns. See -generated-spec-* options for more info
[eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization
_frama_c_rtti_name_info.name ∈ {{ "A" }}