Skip to content
Snippets Groups Projects
Commit 9f2753ac authored by Thibault Martin's avatar Thibault Martin
Browse files

Update test oracles

parent 857e981e
No related branches found
No related tags found
No related merge requests found
...@@ -5,8 +5,10 @@ Now output intermediate result ...@@ -5,8 +5,10 @@ Now output intermediate result
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
[kernel:annot:missing-spec] assigns.cc:14: Warning: [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 [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:alarm] assigns.cc:15: Warning: assertion got status unknown.
[eva] ====== VALUES COMPUTED ====== [eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: [eva:final-states] Values at end of function main:
...@@ -19,7 +21,7 @@ Now output intermediate result ...@@ -19,7 +21,7 @@ Now output intermediate result
/*@ requires \valid(q); /*@ requires \valid(q);
requires \valid(p); requires \valid(p);
assigns *p, *q; assigns *p, *q;
assigns *p \from *q, *p; assigns *p \from *p, *q;
assigns *q \from *p; assigns *q \from *p;
behavior default: behavior default:
......
This diff is collapsed.
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
Now output intermediate result Now output intermediate result
[kernel] Warning: Assuming declared function Frama_C_memcpy can't throw any exception [kernel] Warning: Assuming declared function Frama_C_memcpy can't throw any exception
[kernel:annot:missing-spec] union.cc:8: Warning: [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] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
_frama_c_rtti_name_info.name ∈ {{ "A" }} _frama_c_rtti_name_info.name ∈ {{ "A" }}
......
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
Now output intermediate result Now output intermediate result
[kernel] Warning: Assuming declared function Frama_C_memcpy can't throw any exception [kernel] Warning: Assuming declared function Frama_C_memcpy can't throw any exception
[kernel:annot:missing-spec] union_struct.cc:17: Warning: [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] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization [eva:initial-state] Values of globals at initialization
_frama_c_rtti_name_info.name ∈ {{ "A" }} _frama_c_rtti_name_info.name ∈ {{ "A" }}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment