Merge branch 'feature/kernel/default-spec' into 'master'

Feature/kernel/default spec

See merge request frama-c/frama-clang!214

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:

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" }}

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" }}