Skip to content
Snippets Groups Projects
Commit 4c23cf3d authored by François Bobot's avatar François Bobot
Browse files

Change a message to use Filepath

parent fbdb744c
No related branches found
No related tags found
No related merge requests found
......@@ -96,11 +96,13 @@ let unsupported_specs_tbl =
let warn_unsupported_spec name =
try
let header = Hashtbl.find unsupported_specs_tbl name in
let path = Filename.(concat (concat Fc_config.datadir "libc") header) in
let path = Filepath.Normalized.of_string path in
Value_parameters.warning ~once:true ~current:true
~wkey:Value_parameters.wkey_libc_unsupported_spec
"@[The specification of function '%s' is currently not supported by Eva.@ \
Consider adding %s@ to the analyzed source files.@]"
name (Fc_config.datadir ^ "/libc/" ^ header)
Consider adding %a@ to the analyzed source files.@]"
name Filepath.Normalized.pretty path
with Not_found -> ()
......
......@@ -245,8 +245,7 @@
[eva] using specification for function strdup
[eva:libc:unsupported-spec] string_h.c:146: Warning:
The specification of function 'strdup' is currently not supported by Eva.
Consider adding FRAMA-C-INSTALL/share/frama-c/share/libc/string.c
to the analyzed source files.
Consider adding FRAMAC_SHARE/libc/string.c to the analyzed source files.
[eva] string_h.c:146: Warning: ignoring unsupported \allocates clause
[eva] string_h.c:146:
function strdup: precondition 'valid_string_s' got status valid.
......@@ -256,8 +255,7 @@
[eva] using specification for function strndup
[eva:libc:unsupported-spec] string_h.c:147: Warning:
The specification of function 'strndup' is currently not supported by Eva.
Consider adding FRAMA-C-INSTALL/share/frama-c/share/libc/string.c
to the analyzed source files.
Consider adding FRAMAC_SHARE/libc/string.c to the analyzed source files.
[eva] string_h.c:147: Warning: ignoring unsupported \allocates clause
[eva] string_h.c:147:
function strndup: precondition 'valid_string_s' got status valid.
......
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