Commit 706fcf38 authored by David Bühler's avatar David Bühler
Browse files

Merge branch 'fix/virgile/filepath-normalized' into 'master'

fix normalization of source file names

See merge request frama-c/frama-c!2493
parents 376653c0 f186f6d7
...@@ -42,5 +42,12 @@ __POP_FC_STDLIB ...@@ -42,5 +42,12 @@ __POP_FC_STDLIB
#ifdef NDEBUG #ifdef NDEBUG
#define assert(ignore) ((void)0) #define assert(ignore) ((void)0)
#else #else
#define assert(e) (__FC_assert((e) != 0,__FILE__,__LINE__,#e)) #ifndef __FC_ASSERT_FILE__
#define __FC_FILENAME__ __FILE__
#else
#define str(a) # a
#define xstr(a) str(a)
#define __FC_FILENAME__ xstr(__FC_ASSERT_FILE__)
#endif
#define assert(e) (__FC_assert((e) != 0,__FC_FILENAME__,__LINE__,#e))
#endif #endif
...@@ -35,13 +35,14 @@ let pretty_cpp_opt_kind fmt = ...@@ -35,13 +35,14 @@ let pretty_cpp_opt_kind fmt =
type file = type file =
| NeedCPP of | NeedCPP of
string (* filename of the [.c] to preprocess *) Filepath.Normalized.t (* filename of the [.c] to preprocess *)
* string (* Preprocessor command. * string (* Preprocessor command.
[filename.c -o tempfilname.i] will be appended at the [filename.c -o tempfilname.i] will be appended at the
end.*) end.*)
* cpp_opt_kind * cpp_opt_kind
| NoCPP of string (** filename of a preprocessed [.c] *) | NoCPP of Filepath.Normalized.t (** filename of a preprocessed [.c] *)
| External of string * string (* file * name of plug-in that handles it *) | External of Filepath.Normalized.t * string
(* file * name of plug-in that handles it *)
module D = module D =
Datatype.Make Datatype.Make
...@@ -50,18 +51,26 @@ module D = ...@@ -50,18 +51,26 @@ module D =
type t = file type t = file
let name = "File" let name = "File"
let reprs = let reprs =
[ NeedCPP("", "", Unknown); NoCPP ""; External("", "") ] [ NeedCPP(Filepath.Normalized.unknown, "", Unknown);
NoCPP Filepath.Normalized.unknown;
External(Filepath.Normalized.unknown, "")
]
let structural_descr = Structural_descr.t_abstract let structural_descr = Structural_descr.t_abstract
let mem_project = Datatype.never_any_project let mem_project = Datatype.never_any_project
let copy = Datatype.identity (* immutable strings *) let copy = Datatype.identity (* immutable strings *)
let internal_pretty_code p_caller fmt t = let internal_pretty_code p_caller fmt t =
let pp fmt = match t with let pp fmt = match t with
| NoCPP s -> Format.fprintf fmt "@[File.NoCPP %S@]" (s :> string) | NoCPP s ->
Format.fprintf fmt "@[File.NoCPP %a@]" Filepath.Normalized.pretty s
| External (f,p) -> | External (f,p) ->
Format.fprintf fmt "@[File.External (%S,%S)@]" (f :> string) p Format.fprintf fmt "@[File.External (%a,%S)@]"
| NeedCPP (a,b,c) -> Filepath.Normalized.pretty f p
| NeedCPP (f,cmd,kind) ->
Format.fprintf Format.fprintf
fmt "@[File.NeedCPP (%S,%S,%a)@]" (a :> string) b pretty_cpp_opt_kind c fmt "@[File.NeedCPP (%a,%S,%a)@]"
Filepath.Normalized.pretty f
cmd
pretty_cpp_opt_kind kind
in in
Type.par p_caller Type.Call fmt pp Type.par p_caller Type.Call fmt pp
end) end)
...@@ -75,7 +84,9 @@ let get_suffixes () = ...@@ -75,7 +84,9 @@ let get_suffixes () =
check_suffixes check_suffixes
[ ".c"; ".i"; ".h" ] [ ".c"; ".i"; ".h" ]
let get_name = function NeedCPP (s,_,_) | NoCPP s | External (s,_) -> s let get_name s =
let file = match s with NeedCPP (s,_,_) | NoCPP s | External (s,_) -> s in
Filepath.Normalized.to_pretty_string file
(* ************************************************************************* *) (* ************************************************************************* *)
(** {2 Preprocessor command} *) (** {2 Preprocessor command} *)
...@@ -107,13 +118,12 @@ let get_preprocessor_command () = ...@@ -107,13 +118,12 @@ let get_preprocessor_command () =
end end
let from_filename ?cpp f = let from_filename ?cpp f =
let path = Datatype.Filepath.of_string f in
let cpp, is_gnu_like = let cpp, is_gnu_like =
let cmdline = Kernel.CppCommand.get() in let cmdline = Kernel.CppCommand.get() in
if cmdline <> "" then if cmdline <> "" then
cmdline, cpp_opt_kind () cmdline, cpp_opt_kind ()
else else
let flags = Json_compilation_database.get_flags path in let flags = Json_compilation_database.get_flags f in
let cpp, gnu = let cpp, gnu =
match cpp with match cpp with
| None -> get_preprocessor_command () | None -> get_preprocessor_command ()
...@@ -121,13 +131,13 @@ let from_filename ?cpp f = ...@@ -121,13 +131,13 @@ let from_filename ?cpp f =
in in
(if flags = [] then cpp else cpp ^ " " ^ String.concat " " flags), gnu (if flags = [] then cpp else cpp ^ " " ^ String.concat " " flags), gnu
in in
if Filename.check_suffix f ".i" then begin if Filename.check_suffix (f:>string) ".i" then begin
NoCPP f NoCPP f
end else end else
let suf = let suf =
try try
let suf_idx = String.rindex f '.' in let suf_idx = String.rindex (f:>string) '.' in
String.sub f suf_idx (String.length f - suf_idx) String.sub (f:>string) suf_idx (String.length (f:>string) - suf_idx)
with Not_found -> (* raised by String.rindex if '.' \notin f *) with Not_found -> (* raised by String.rindex if '.' \notin f *)
"" ""
in in
...@@ -413,15 +423,16 @@ let build_cpp_cmd cmdl supp_args in_file out_file = ...@@ -413,15 +423,16 @@ let build_cpp_cmd cmdl supp_args in_file out_file =
let parse_cabs = function let parse_cabs = function
| NoCPP f -> | NoCPP f ->
if not (Sys.file_exists f) then if not (Sys.file_exists (f:>string)) then
Kernel.abort "preprocessed file %S does not exist" f; Kernel.abort "preprocessed file %a does not exist"
let path = Datatype.Filepath.of_string f in Filepath.Normalized.pretty f;
Kernel.feedback "Parsing %a (no preprocessing)" Kernel.feedback "Parsing %a (no preprocessing)"
Datatype.Filepath.pretty path; Datatype.Filepath.pretty f;
Frontc.parse (Datatype.Filepath.of_string f) () Frontc.parse f ()
| NeedCPP (f, cmdl, is_gnu_like) -> | NeedCPP (f, cmdl, is_gnu_like) ->
if not (Sys.file_exists (f :> string)) then if not (Sys.file_exists (f :> string)) then
Kernel.abort "source file %S does not exist" (f :> string); Kernel.abort "source file %a does not exist"
Filepath.Normalized.pretty f;
let debug = Kernel.is_debug_key_enabled Kernel.dkey_parser in let debug = Kernel.is_debug_key_enabled Kernel.dkey_parser in
let add_if_gnu opt = let add_if_gnu opt =
match is_gnu_like with match is_gnu_like with
...@@ -506,16 +517,18 @@ let parse_cabs = function ...@@ -506,16 +517,18 @@ let parse_cabs = function
include_args define_args include_args define_args
in in
Kernel.feedback ~dkey:Kernel.dkey_pp Kernel.feedback ~dkey:Kernel.dkey_pp
"@{<i>preprocessing@} with \"%s %s %s\"" cmdl supp_args f; "@{<i>preprocessing@} with \"%s %s %a\""
let path = Datatype.Filepath.of_string f in cmdl supp_args Filepath.Normalized.pretty f;
Kernel.feedback "Parsing %a (with preprocessing)" Kernel.feedback "Parsing %a (with preprocessing)"
Datatype.Filepath.pretty path; Datatype.Filepath.pretty f;
let cpp_command = build_cpp_cmd cmdl supp_args f (ppf :> string) in let cpp_command = build_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) in
if Sys.command cpp_command <> 0 then begin if Sys.command cpp_command <> 0 then begin
safe_remove_file ppf; safe_remove_file ppf;
Kernel.abort "failed to run: %s@\n\ Kernel.abort
you may set the CPP environment variable to select the proper \ "failed to run: %s@\n\
preprocessor command or use the option \"-cpp-command\"." cpp_command you may set the CPP environment variable to select the proper \
preprocessor command or use the option \"-cpp-command\"."
cpp_command
end; end;
let ppf = let ppf =
if Kernel.ReadAnnot.get() && if Kernel.ReadAnnot.get() &&
...@@ -549,19 +562,21 @@ let parse_cabs = function ...@@ -549,19 +562,21 @@ let parse_cabs = function
end else ppf end else ppf
in in
let (cil,(_,defs)) = Frontc.parse ppf () in let (cil,(_,defs)) = Frontc.parse ppf () in
cil.fileName <- path; cil.fileName <- f;
safe_remove_file ppf; safe_remove_file ppf;
(cil,(path,defs)) (cil,(f,defs))
| External (f,suf) -> | External (f,suf) ->
if not (Sys.file_exists f) then if not (Sys.file_exists (f:>string)) then
Kernel.abort "file %S does not exist." f; Kernel.abort "file %a does not exist."
Filepath.Normalized.pretty f;
try try
let path = Datatype.Filepath.of_string f in
Kernel.feedback "Parsing %a (external front-end)" Kernel.feedback "Parsing %a (external front-end)"
Datatype.Filepath.pretty path; Datatype.Filepath.pretty f;
Hashtbl.find check_suffixes suf f Hashtbl.find check_suffixes suf (f:>string)
with Not_found -> with Not_found ->
Kernel.abort "could not find a suitable plugin for parsing %S." f Kernel.abort
"could not find a suitable plugin for parsing %a."
Filepath.Normalized.pretty f
let to_cil_cabs f = let to_cil_cabs f =
try try
...@@ -1638,9 +1653,7 @@ let init_from_cmdline () = ...@@ -1638,9 +1653,7 @@ let init_from_cmdline () =
end; end;
let files = Kernel.Files.get () in let files = Kernel.Files.get () in
if files = [] && not !Config.is_gui then Kernel.warning "no input file."; if files = [] && not !Config.is_gui then Kernel.warning "no input file.";
let files = let files = List.map (fun f -> from_filename f) files in
List.map (fun f -> from_filename (Filepath.Normalized.to_pretty_string f)) files
in
try try
init_from_c_files files; init_from_c_files files;
if Kernel.Check.get () then begin if Kernel.Check.get () then begin
...@@ -1710,7 +1723,7 @@ let create_rebuilt_project_from_visitor ...@@ -1710,7 +1723,7 @@ let create_rebuilt_project_from_visitor
let ext = if preprocess then ".c" else ".i" in let ext = if preprocess then ".c" else ".i" in
let debug = Kernel.Debug.get () > 0 in let debug = Kernel.Debug.get () > 0 in
let tmp_fname = Extlib.temp_file_cleanup_at_exit ~debug name ext in let tmp_fname = Extlib.temp_file_cleanup_at_exit ~debug name ext in
tmp_fname Filepath.Normalized.of_string tmp_fname
in in
let cout = open_out (f :> string) in let cout = open_out (f :> string) in
let fmt = Format.formatter_of_out_channel cout in let fmt = Format.formatter_of_out_channel cout in
......
...@@ -30,13 +30,13 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown ...@@ -30,13 +30,13 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown
Note: [string] is used here instead of [Filepath], to preserve Note: [string] is used here instead of [Filepath], to preserve
names given in the command line, without normalization. *) names given in the command line, without normalization. *)
type file = type file =
| NeedCPP of string * string * cpp_opt_kind | NeedCPP of Filepath.Normalized.t * string * cpp_opt_kind
(** The first string is the filename of the [.c] to preprocess. (** The first string is the filename of the [.c] to preprocess.
The second one is the preprocessor command ([filename.c -o The second one is the preprocessor command ([filename.c -o
tempfilname.i] will be appended at the end).*) tempfilname.i] will be appended at the end).*)
| NoCPP of string | NoCPP of Filepath.Normalized.t
(** Already pre-processed file [.i] *) (** Already pre-processed file [.i] *)
| External of string * string | External of Filepath.Normalized.t * string
(** file that can be translated into a Cil AST through an external (** file that can be translated into a Cil AST through an external
function, together with the recognized suffix. *) function, together with the recognized suffix. *)
...@@ -145,7 +145,7 @@ val pre_register: t -> unit ...@@ -145,7 +145,7 @@ val pre_register: t -> unit
val get_all: unit -> t list val get_all: unit -> t list
(** Return the list of toplevel files. *) (** Return the list of toplevel files. *)
val from_filename: ?cpp:string -> string -> t val from_filename: ?cpp:string -> Datatype.Filepath.t -> t
(** Build a file from its name. The optional argument is the preprocessor (** Build a file from its name. The optional argument is the preprocessor
command. Default is [!get_preprocessor_command ()]. *) command. Default is [!get_preprocessor_command ()]. *)
......
...@@ -450,6 +450,21 @@ struct ...@@ -450,6 +450,21 @@ struct
module Fc_Filepath = Filepath module Fc_Filepath = Filepath
let normalize_filepath ~existence ~file_kind s =
try
Filepath.Normalized.of_string ~existence s
with
| Filepath.No_file ->
P.L.abort "%s%sfile '%s' does not exist"
file_kind
(if file_kind = "" then "" else " ")
(Filepath.Normalized.(to_pretty_string (of_string s)))
| Filepath.File_exists ->
P.L.abort "%s%sfile '%s' already exists"
file_kind
(if file_kind = "" then "" else " ")
(Filepath.Normalized.(to_pretty_string (of_string s)))
module Filepath module Filepath
(X: sig (X: sig
include Parameter_sig.Input_with_arg include Parameter_sig.Input_with_arg
...@@ -472,22 +487,7 @@ struct ...@@ -472,22 +487,7 @@ struct
f oldfp newfp f oldfp newfp
let set_str s = let set_str s =
let fp = set (normalize_filepath ~existence:X.existence ~file_kind:X.file_kind s)
try
Filepath.Normalized.of_string ~existence:X.existence s
with
| Filepath.No_file ->
P.L.abort "%s%sfile not found: '%s'"
X.file_kind
(if X.file_kind = "" then "" else " ")
s
| Filepath.File_exists ->
P.L.abort "%s file already exists: '%s'"
X.file_kind
(if X.file_kind = "" then "" else " ")
s
in
set fp
let add_option name = let add_option name =
Cmdline.add_option Cmdline.add_option
...@@ -1227,22 +1227,11 @@ struct ...@@ -1227,22 +1227,11 @@ struct
Make_list Make_list
(struct (struct
include Datatype.Filepath include Datatype.Filepath
let to_string = Fc_Filepath.Normalized.to_pretty_string let to_string s = (s : t :> string)
let of_singleton_string = no_element_of_string let of_singleton_string = no_element_of_string
let of_string s = let of_string s =
try of_string ~existence:X.existence s normalize_filepath ~existence:X.existence ~file_kind:X.file_kind s
with
| Fc_Filepath.No_file ->
P.L.abort "%s%sfile '%s' does not exist"
X.file_kind
(if X.file_kind = "" then "" else " ")
s
| Fc_Filepath.File_exists ->
P.L.abort "%s%sfile '%s' already exists"
X.file_kind
(if X.file_kind = "" then "" else " ")
s
end) end)
(struct (struct
include X include X
......
...@@ -30,15 +30,12 @@ open Cil_datatype ...@@ -30,15 +30,12 @@ open Cil_datatype
let library_files () = let library_files () =
List.map List.map
(fun d -> Options.Share.file ~error:true d) (fun d ->
Filepath.Normalized.of_string (Options.Share.file ~error:true d))
[ "e_acsl_gmp_api.h"; [ "e_acsl_gmp_api.h";
"e_acsl.h" ] "e_acsl.h" ]
let normalized_library_files = let is_library_loc (loc, _) = List.mem loc.Filepath.pos_path (library_files ())
lazy (List.map Datatype.Filepath.of_string (library_files ()))
let is_library_loc (loc, _) =
List.mem loc.Filepath.pos_path (Lazy.force normalized_library_files)
let library_functions = Datatype.String.Hashtbl.create 17 let library_functions = Datatype.String.Hashtbl.create 17
let register_library_function vi = let register_library_function vi =
......
...@@ -46,7 +46,7 @@ val result_vi: kernel_function -> varinfo ...@@ -46,7 +46,7 @@ val result_vi: kernel_function -> varinfo
(** {2 Handling the E-ACSL's C-libraries} *) (** {2 Handling the E-ACSL's C-libraries} *)
(* ************************************************************************** *) (* ************************************************************************** *)
val library_files: unit -> string list val library_files: unit -> Filepath.Normalized.t list
val is_library_loc: location -> bool val is_library_loc: location -> bool
val register_library_function: varinfo -> unit val register_library_function: varinfo -> unit
val reset: unit -> unit val reset: unit -> unit
......
/* run.config_dev /*
run.config_dev
COMMENT: Check behaviours of format functions COMMENT: Check behaviours of format functions
DONTRUN: DONTRUN:
*/ */
/*
run.config_ci
STDOPT: #"@PTEST_FILE@ -cpp-extra-args='-D__FC_ASSERT_FILE__=@PTEST_FILE@'"
*/
#include <stdlib.h> #include <stdlib.h>
#include <stdio.h> #include <stdio.h>
......
[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:16: Warning: [kernel:typing:implicit-function-declaration] tests/format/fprintf.c:21: Warning:
Calling undeclared function fork. Old style K&R code? Calling undeclared function fork. Old style K&R code?
[kernel:typing:incompatible-types-call] tests/format/fprintf.c:23: Warning: [kernel:typing:incompatible-types-call] tests/format/fprintf.c:28: Warning:
expected 'FILE *' but got argument of type 'int *': & argc expected 'FILE *' but got argument of type 'int *': & argc
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `exit': [e-acsl] Warning: annotating undefined function `exit':
...@@ -39,71 +39,71 @@ ...@@ -39,71 +39,71 @@
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] translation done in project "e-acsl". [e-acsl] translation done in project "e-acsl".
[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning: [kernel:annot:missing-spec] tests/format/fprintf.c:21: Warning:
Neither code nor specification for function fork, generating default assigns from the prototype Neither code nor specification for function fork, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning: [kernel:annot:missing-spec] tests/format/fprintf.c:21: Warning:
Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: [eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: [eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown. function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
[eva:alarm] tests/format/fprintf.c:16: Warning: [eva:alarm] tests/format/fprintf.c:21: Warning:
accessing uninitialized left-value. assert \initialized(&process_status); accessing uninitialized left-value. assert \initialized(&process_status);
[kernel:annot:missing-spec] tests/format/signalled.h:12: Warning: [kernel:annot:missing-spec] tests/format/signalled.h:17: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
[eva:invalid-assigns] tests/format/fprintf.c:17: [eva:invalid-assigns] tests/format/fprintf.c:22:
Completely invalid destination for assigns clause *stream. Ignoring. Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:17: Warning: [eva:alarm] tests/format/fprintf.c:22: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_0); accessing uninitialized left-value. assert \initialized(&process_status_0);
[eva:alarm] tests/format/fprintf.c:20: Warning: [eva:alarm] tests/format/fprintf.c:25: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_1); accessing uninitialized left-value. assert \initialized(&process_status_1);
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning: [eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/format/fprintf.c:22: Warning: [eva:alarm] tests/format/fprintf.c:27: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_2); accessing uninitialized left-value. assert \initialized(&process_status_2);
[eva:invalid-assigns] tests/format/fprintf.c:23: [eva:invalid-assigns] tests/format/fprintf.c:28:
Completely invalid destination for assigns clause *stream. Ignoring. Completely invalid destination for assigns clause *stream. Ignoring.
[eva:alarm] tests/format/fprintf.c:23: Warning: [eva:alarm] tests/format/fprintf.c:28: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_3); accessing uninitialized left-value. assert \initialized(&process_status_3);
[kernel:annot:missing-spec] tests/format/fprintf.c:28: Warning: [kernel:annot:missing-spec] tests/format/fprintf.c:33: Warning:
Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:28: Warning: [eva:alarm] tests/format/fprintf.c:33: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_4); accessing uninitialized left-value. assert \initialized(&process_status_4);
[eva:alarm] tests/format/fprintf.c:29: Warning: [eva:alarm] tests/format/fprintf.c:34: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_5); accessing uninitialized left-value. assert \initialized(&process_status_5);
[kernel:annot:missing-spec] tests/format/fprintf.c:35: Warning: [kernel:annot:missing-spec] tests/format/fprintf.c:40: Warning:
Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:35: Warning: [eva:alarm] tests/format/fprintf.c:40: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_6); accessing uninitialized left-value. assert \initialized(&process_status_6);
[eva:alarm] tests/format/fprintf.c:36: Warning: [eva:alarm] tests/format/fprintf.c:41: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_7); accessing uninitialized left-value. assert \initialized(&process_status_7);
[eva:alarm] tests/format/fprintf.c:37: Warning: [eva:alarm] tests/format/fprintf.c:42: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_8); accessing uninitialized left-value. assert \initialized(&process_status_8);
[eva:invalid-assigns] tests/format/fprintf.c:38: [eva:invalid-assigns] tests/format/fprintf.c:43:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:38: Warning: [eva:alarm] tests/format/fprintf.c:43: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_9); accessing uninitialized left-value. assert \initialized(&process_status_9);
[eva:invalid-assigns] tests/format/fprintf.c:39: [eva:invalid-assigns] tests/format/fprintf.c:44:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:39: Warning: [eva:alarm] tests/format/fprintf.c:44: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_10); accessing uninitialized left-value. assert \initialized(&process_status_10);
[kernel:annot:missing-spec] tests/format/fprintf.c:42: Warning: [kernel:annot:missing-spec] tests/format/fprintf.c:47: Warning:
Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
[eva:alarm] tests/format/fprintf.c:42: Warning: [eva:alarm] tests/format/fprintf.c:47: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_11); accessing uninitialized left-value. assert \initialized(&process_status_11);
[eva:alarm] tests/format/fprintf.c:43: Warning: [eva:alarm] tests/format/fprintf.c:48: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_12); accessing uninitialized left-value. assert \initialized(&process_status_12);
[eva:invalid-assigns] tests/format/fprintf.c:44: [eva:invalid-assigns] tests/format/fprintf.c:49:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
[eva:alarm] tests/format/fprintf.c:44: Warning: [eva:alarm] tests/format/fprintf.c:49: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_13); accessing uninitialized left-value. assert \initialized(&process_status_13);
[eva:alarm] tests/format/fprintf.c:45: Warning: [eva:alarm] tests/format/fprintf.c:50: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_14); accessing uninitialized left-value. assert \initialized(&process_status_14);
[eva:invalid-assigns] tests/format/fprintf.c:46: [eva:invalid-assigns] tests/format/fprintf.c:51:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring. Completely invalid