Skip to content
Snippets Groups Projects
Commit f721012f authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/martin/kernel/add-loc-argument-for-populate-spec' into 'master'

Feature/martin/kernel/add loc argument for populate spec

See merge request frama-c/frama-clang!219
parents f5716595 a6b679e1
No related branches found
No related tags found
No related merge requests found
...@@ -4,7 +4,7 @@ Now output intermediate result ...@@ -4,7 +4,7 @@ Now output intermediate result
[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
[kernel:annot:missing-spec] assigns.cc:14: Warning: [kernel:annot:missing-spec] assigns.cc:8: Warning:
Neither code nor explicit assigns for function swap, Neither code nor explicit assigns for function swap,
generating default clauses from the specification. See -generated-spec-* options for more info 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
......
...@@ -254,7 +254,7 @@ Now output intermediate result ...@@ -254,7 +254,7 @@ Now output intermediate result
_frama_c_rtti_name_info.name ∈ {{ "ClassTemplate" }} _frama_c_rtti_name_info.name ∈ {{ "ClassTemplate" }}
{.base_classes; .number_of_base_classes; .pvmt} ∈ {.base_classes; .number_of_base_classes; .pvmt} ∈
{0} {0}
[kernel:annot:missing-spec] stl_unique_ptr.cpp:9: Warning: [kernel:annot:missing-spec] <builtin>:0: Warning:
Neither code nor specification for function malloc, Neither code nor specification for function malloc,
generating default assigns. See -generated-spec-* options for more info generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function malloc [eva] using specification for function malloc
......
[kernel] Parsing union.cc (external front-end) [kernel] Parsing union.cc (external front-end)
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] <builtin>:0: Warning:
Neither code nor specification for function Frama_C_memcpy, Neither code nor specification for function Frama_C_memcpy,
generating default assigns. See -generated-spec-* options for more info 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
......
[kernel] Parsing union_struct.cc (external front-end) [kernel] Parsing union_struct.cc (external front-end)
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] <builtin>:0: Warning:
Neither code nor specification for function Frama_C_memcpy, Neither code nor specification for function Frama_C_memcpy,
generating default assigns. See -generated-spec-* options for more info 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
......
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