diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 226880e6fa4d3e127c358cf6c08a5657b6c43be2..ec82db98286c67838bafc8e3bb48291755e069bd 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -31,6 +31,7 @@ let system =
else
fun f ->
Unix.system f
+
module Filename = struct
include Filename
let concat =
@@ -56,6 +57,8 @@ module Filename = struct
cygpath r
else
fun a b -> temp_file a b
+
+ let sanitize f = String.escaped f
end
let string_del_suffix suffix s =
@@ -963,7 +966,7 @@ let get_macros cmd =
"PTEST_DIR", SubDir.get cmd.directory;
"PTEST_RESULT",
SubDir.get cmd.directory ^ "/" ^ redefine_name "result";
- "PTEST_FILE", ptest_file;
+ "PTEST_FILE", Filename.sanitize ptest_file;
"PTEST_NAME", ptest_name;
"PTEST_NUMBER", string_of_int cmd.n;
]
@@ -971,14 +974,16 @@ let get_macros cmd =
Macros.add_list macros cmd.macros
let basic_command_string =
- let contains_toplevel_or_frama_c =
+ let contains_toplevel_or_frama_c =
Str.regexp "[^( ]*\\(\\(toplevel\\)\\|\\(viewer\\)\\|\\(frama-c\\)\\).*"
in
fun command ->
let macros = get_macros command in
let logfiles = List.map (Macros.expand macros) command.log_files in
command.log_files <- logfiles;
- let has_ptest_file_t, toplevel = Macros.does_expand macros command.toplevel in
+ let has_ptest_file_t, toplevel =
+ Macros.does_expand macros command.toplevel
+ in
let has_ptest_file_o, options = Macros.does_expand macros command.options in
let toplevel = if !use_byte then opt_to_byte toplevel else toplevel in
let options =
@@ -994,8 +999,10 @@ let basic_command_string =
let options = if !use_byte then opt_to_byte_options options else options in
if has_ptest_file_t || has_ptest_file_o || command.execnow then
toplevel ^ " " ^ options
- else
- toplevel ^ " " ^ get_ptest_file command ^ " " ^ options
+ else begin
+ let file = Filename.sanitize @@ get_ptest_file command in
+ toplevel ^ " " ^ file ^ " " ^ options
+ end
(* Searches for executable [s] in the directories contained in the PATH
environment variable. Returns [None] if not found, or
@@ -1073,18 +1080,23 @@ let command_string command =
in
let command_string = basic_command_string command in
let command_string =
- command_string ^ " 2>" ^ stderr
+ command_string ^ " 2>" ^ (Filename.sanitize stderr)
in
let command_string = match filter with
| None -> command_string
| Some filter -> command_string ^ " | " ^ filter
in
- let command_string = command_string ^ " >" ^ log_prefix ^ ".res.log" in
+ let res = Filename.sanitize (log_prefix ^ ".res.log") in
+ let command_string = command_string ^ " >" ^ res in
let command_string = match filter with
| None -> command_string
| Some filter ->
Printf.sprintf "%s && %s < %s >%s && rm -f %s"
- command_string filter stderr errlog stderr
+ command_string
+ filter
+ (Filename.sanitize stderr)
+ (Filename.sanitize errlog)
+ (Filename.sanitize stderr)
in
command_string
@@ -1367,8 +1379,8 @@ let compare_one_file cmp log_prefix oracle_prefix log_kind =
-1
end else
let ext = log_ext log_kind in
- let log_file = log_prefix ^ ext ^ ".log" in
- let oracle_file = oracle_prefix ^ ext ^ ".oracle" in
+ let log_file = Filename.sanitize (log_prefix ^ ext ^ ".log") in
+ let oracle_file = Filename.sanitize (oracle_prefix ^ ext ^ ".oracle") in
if log_kind = Err && not (Sys.file_exists oracle_file) then
check_file_is_empty_or_nonexisting (Command_error (cmp,log_kind)) ~log_file
else begin
@@ -1391,8 +1403,8 @@ let compare_one_log_file dir file =
Condition.signal shared.diff_available;
unlock()
end else
- let log_file = SubDir.make_result_file dir file in
- let oracle_file = SubDir.make_oracle_file dir file in
+ let log_file = Filename.sanitize (SubDir.make_result_file dir file) in
+ let oracle_file = Filename.sanitize (SubDir.make_oracle_file dir file) in
let cmp_string = !do_cmp ^ " " ^ log_file ^ " " ^ oracle_file ^ " > /dev/null 2> /dev/null" in
if !verbosity >= 2 then lock_printf "%% cmplog: %s / %s@." (SubDir.get dir) file;
ignore (launch_and_check_compare_file (Log_error (dir,file))
@@ -1465,28 +1477,33 @@ let do_diff = function
| Command_error (diff, kind) ->
let log_prefix = log_prefix diff in
let log_ext = log_ext kind in
+ let log_file = Filename.sanitize (log_prefix ^ log_ext ^ ".log") in
let command_string = command_string diff in
lock_printf "%tCommand:@\n%s@." print_default_env command_string;
if !behavior = Show
- then ignore (launch ("cat " ^ log_prefix ^ log_ext ^ ".log"))
+ then ignore (launch ("cat " ^ log_file))
else
let oracle_prefix = oracle_prefix diff in
- let diff_string =
- !do_diffs ^ " " ^
- oracle_prefix ^ log_ext ^ ".oracle " ^
- log_prefix ^ log_ext ^ ".log"
+ let oracle_file =
+ Filename.sanitize (oracle_prefix ^ log_ext ^ ".oracle")
in
+ let diff_string = !do_diffs ^ " " ^ oracle_file ^ " " ^ log_file in
ignore (launch diff_string)
| Target_error execnow ->
lock_printf "Custom command failed: %s@\n" execnow.ex_cmd
| Log_error(dir, file) ->
- let result_file = SubDir.make_result_file dir file in
+ let result_file =
+ Filename.sanitize (SubDir.make_result_file dir file)
+ in
lock_printf "Log of %s:@." result_file;
if !behavior = Show
then ignore (launch ("cat " ^ result_file))
else
+ let oracle_file =
+ Filename.sanitize (SubDir.make_oracle_file dir file)
+ in
let diff_string =
- !do_diffs ^ " " ^ SubDir.make_oracle_file dir file ^ " " ^ result_file
+ !do_diffs ^ " " ^ oracle_file ^ " " ^ result_file
in
ignore (launch diff_string)
@@ -1519,7 +1536,10 @@ let default_config () =
if Sys.file_exists general_config_file
then begin
let scan_buffer = Scanf.Scanning.from_file general_config_file in
- scan_options (SubDir.create ~with_subdir:false Filename.current_dir_name) scan_buffer (default_config ())
+ scan_options
+ (SubDir.create ~with_subdir:false Filename.current_dir_name)
+ scan_buffer
+ (default_config ())
end
else default_config ()
diff --git a/share/libc/assert.h b/share/libc/assert.h
index 8d81f75752504f1902b89d3d1c5e14830714e8dd..807927b994c23871ef75e63a985044dd860d8986 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -42,12 +42,8 @@ __POP_FC_STDLIB
#ifdef NDEBUG
#define assert(ignore) ((void)0)
#else
-#ifndef __FC_ASSERT_FILE__
+#ifndef __FRAMAC__
#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
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 045d1ee3d24008dedb4d6ad449bc22da006b158a..5c0d4bf41ff4826450d4cb0064455b69cf484e45 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -196,6 +196,17 @@ let init_lexicon _ =
THREAD loc
else
IDENT "__thread"));
+ ("__FC_FILENAME__",
+ (fun loc ->
+ let filename =
+ Filepath.Normalized.to_pretty_string (fst loc).pos_path
+ in
+ (* TODO: when 4.07 becomes minimal OCaml version,
+ use String.to_seq and Seq.fold_left. *)
+ let l = ref [] in
+ let convert_char c = l:=Int64.of_int (Char.code c) :: !l in
+ String.iter convert_char filename;
+ CST_STRING (List.rev !l,loc)))
]
@@ -742,7 +753,9 @@ and file = parse
| '"' ([^ '\012' '\t' '"']* as d) "//\"" {
E.setCurrentWorkingDirectory d;
endline lexbuf }
-| '"' ([^ '\012' '\t' '"']* as f) '"' {
+| '"' (([^ '\012' '\t' '"']|"\\\"")* as f) '"' {
+ let unescape = Str.regexp_string "\\\"" in
+ let f = Str.global_replace unescape "\"" f in
E.setCurrentFile f;
endline lexbuf}
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index cf1317591f60695924090c66eccaf3871f191ab0..07071b3e13a346cdd04a0827752b5aa5896fb005 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -81,77 +81,95 @@
if flag then Hashtbl.add c_kw i t
)
[
- "allocates", ALLOCATES, false;
- "assert", ASSERT, false;
- "assigns", ASSIGNS, false;
- "assumes", ASSUMES, false;
- "at", EXT_AT, false;(* ACSL extension for external spec file *)
- "axiom", AXIOM, false;
- "axiomatic", AXIOMATIC, false;
- "behavior", BEHAVIOR, false;
- "behaviors", BEHAVIORS, false;
- "_Bool", BOOL, true;
- "breaks", BREAKS, false;
- "case", CASE, true;
- "char", CHAR, true;
- "check", CHECK, false;
- "complete", COMPLETE, false;
- "const", CONST, true;
- "continues", CONTINUES, false;
- "contract", CONTRACT, false;(* ACSL extension for external spec file *)
- "custom", CUSTOM, false; (* ACSL extension for custom annotations *)
- "decreases", DECREASES, false;
- "disjoint", DISJOINT, false;
- "double", DOUBLE, true;
- "else", ELSE, true;
- "ensures", ENSURES, false ;
- "enum", ENUM, true;
- "exits", EXITS, false;
- "frees", FREES, false;
- "function", FUNCTION, false;(* ACSL extension for external spec file *)
- "float", FLOAT, true;
- "for", FOR, true;
- "global", GLOBAL, false;
- "if", IF, true;
- "impact", IMPACT, false;
- "inductive", INDUCTIVE, false;
- "include", INCLUDE, false;(* ACSL extension for external spec file *)
- "int", INT, true;
- "invariant", INVARIANT, false;
- "label", LABEL, false;
- "lemma", LEMMA, false;
- "let", EXT_LET, false;(* ACSL extension for external spec file *)
- "logic", LOGIC, false;
- "long", LONG, true;
- "loop", LOOP, false;
- "model", MODEL, false;(* ACSL extension for model fields *)
- "module", MODULE, false;(* ACSL extension for external spec file *)
- "pragma", PRAGMA, false;
- "predicate", PREDICATE, false;
- "reads", READS, true; (* treated specifically in the parser to
- avoid issue in volatile clause. *)
- "requires", REQUIRES, false;
- "returns", RETURNS, false;
- "short", SHORT, true;
- "signed", SIGNED, true;
- "sizeof", SIZEOF, true;
- "slice", SLICE, false;
- "struct", STRUCT, true;
- "terminates", TERMINATES, false;
- "type", TYPE, false;
- "union", UNION, true;
- "unsigned", UNSIGNED, true;
- "variant", VARIANT, false;
- "void", VOID, true;
- "volatile", VOLATILE, true;
- "writes", WRITES, true; (* treated specifically in the parser to
- avoid issue in volatile clause. *)
+ "allocates", (fun _ -> ALLOCATES), false;
+ "assert", (fun _ -> ASSERT), false;
+ "assigns", (fun _ -> ASSIGNS), false;
+ "assumes", (fun _ -> ASSUMES), false;
+ "at", (fun _ -> EXT_AT), false;
+ (* ACSL extension for external spec file *)
+ "axiom", (fun _ -> AXIOM), false;
+ "axiomatic", (fun _ -> AXIOMATIC), false;
+ "behavior", (fun _ -> BEHAVIOR), false;
+ "behaviors", (fun _ -> BEHAVIORS), false;
+ "_Bool", (fun _ -> BOOL), true;
+ "breaks", (fun _ -> BREAKS), false;
+ "case", (fun _ -> CASE), true;
+ "char", (fun _ -> CHAR), true;
+ "check", (fun _ -> CHECK), false;
+ "complete", (fun _ -> COMPLETE), false;
+ "const", (fun _ -> CONST), true;
+ "continues", (fun _ -> CONTINUES), false;
+ "contract", (fun _ -> CONTRACT), false;
+ (* ACSL extension for external spec file *)
+ "custom", (fun _ -> CUSTOM), false;
+ (* ACSL extension for custom annotations *)
+ "decreases", (fun _ -> DECREASES), false;
+ "disjoint", (fun _ -> DISJOINT), false;
+ "double", (fun _ -> DOUBLE), true;
+ "else", (fun _ -> ELSE), true;
+ "ensures", (fun _ -> ENSURES), false ;
+ "enum", (fun _ -> ENUM), true;
+ "exits", (fun _ -> EXITS), false;
+ "frees", (fun _ -> FREES), false;
+ "function", (fun _ -> FUNCTION), false;
+ (* ACSL extension for external spec file *)
+ "float", (fun _ -> FLOAT), true;
+ "for", (fun _ -> FOR), true;
+ "global", (fun _ -> GLOBAL), false;
+ "if", (fun _ -> IF), true;
+ "impact", (fun _ -> IMPACT), false;
+ "inductive", (fun _ -> INDUCTIVE), false;
+ "include", (fun _ -> INCLUDE), false;
+ (* ACSL extension for external spec file *)
+ "int", (fun _ -> INT), true;
+ "invariant", (fun _ -> INVARIANT), false;
+ "label", (fun _ -> LABEL), false;
+ "lemma", (fun _ -> LEMMA), false;
+ "let", (fun _ -> EXT_LET), false;
+ (* ACSL extension for external spec file *)
+ "logic", (fun _ -> LOGIC), false;
+ "long", (fun _ -> LONG), true;
+ "loop", (fun _ -> LOOP), false;
+ "model", (fun _ -> MODEL), false;
+ (* ACSL extension for model fields *)
+ "module", (fun _ -> MODULE), false;
+ (* ACSL extension for external spec file *)
+ "pragma", (fun _ -> PRAGMA), false;
+ "predicate", (fun _ -> PREDICATE), false;
+ "reads", (fun _ -> READS), true;
+ (* treated specifically in the parser to
+ avoid issue in volatile clause. *)
+ "requires", (fun _ -> REQUIRES), false;
+ "returns", (fun _ -> RETURNS), false;
+ "short", (fun _ -> SHORT), true;
+ "signed", (fun _ -> SIGNED), true;
+ "sizeof", (fun _ -> SIZEOF), true;
+ "slice", (fun _ -> SLICE), false;
+ "struct", (fun _ -> STRUCT), true;
+ "terminates", (fun _ -> TERMINATES), false;
+ "type", (fun _ -> TYPE), false;
+ "union", (fun _ -> UNION), true;
+ "unsigned", (fun _ -> UNSIGNED), true;
+ "variant", (fun _ -> VARIANT), false;
+ "void", (fun _ -> VOID), true;
+ "volatile", (fun _ -> VOLATILE), true;
+ "writes", (fun _ -> WRITES), true;
+ (* treated specifically in the parser to
+ avoid issue in volatile clause. *)
+ "__FC_FILENAME__",
+ (fun loc ->
+ let filename =
+ Filepath.(Normalized.to_pretty_string (fst loc).pos_path)
+ in
+ STRING_LITERAL (false,filename)),
+ true;
];
List.iter (fun (x, y) -> Hashtbl.add type_kw x y)
["integer", INTEGER; "real", REAL; "boolean", BOOLEAN; ];
- (fun s ->
+ (fun s loc ->
try
- Hashtbl.find (if Logic_utils.is_kw_c_mode () then c_kw else all_kw) s
+ (Hashtbl.find (if Logic_utils.is_kw_c_mode () then c_kw else all_kw) s)
+ loc
with Not_found ->
let res =
if not (Logic_utils.is_kw_c_mode ()) then begin
@@ -292,7 +310,12 @@ rule token = parse
}
| '\\' rL (rL | rD)* { bs_identifier lexbuf }
- | rL (rL | rD)* { let s = lexeme lexbuf in identifier s }
+ | rL (rL | rD)* {
+ let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
+ let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
+ let s = lexeme lexbuf in
+ identifier s cabsloc
+ }
| '0'['x''X'] rH+ rIS? { CONSTANT (IntConstant (lexeme lexbuf)) }
| '0'['b''B'] rB+ rIS? { CONSTANT (IntConstant (lexeme lexbuf)) }
@@ -446,14 +469,15 @@ and hash = parse
and file = parse
'\n' { update_newline_loc lexbuf; token lexbuf}
| [' ''\t''\r'] { file lexbuf}
-| '"' [^ '\012' '\t' '"']* '"'
- {
- let n = Lexing.lexeme lexbuf in
- let n1 = String.sub n 1
- ((String.length n) - 2) in
- update_file_loc lexbuf n1;
- endline lexbuf
- }
+| '"' ([^ '\012' '\t' '"']|"\\\"")* '"' {
+ let n = Lexing.lexeme lexbuf in
+ let n1 = String.sub n 1
+ ((String.length n) - 2) in
+ let unescape = Str.regexp_string "\\\"" in
+ let n1 = Str.global_replace unescape "\"" n1 in
+ update_file_loc lexbuf n1;
+ endline lexbuf
+ }
| _ { endline lexbuf}
diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c
index 8bbf8600c66e713f5daa2124d59676d88af2bf0f..5e19a187ff302ce100ed2f8d7ebe9eade5468742 100644
--- a/src/plugins/e-acsl/tests/format/fprintf.c
+++ b/src/plugins/e-acsl/tests/format/fprintf.c
@@ -3,10 +3,6 @@
COMMENT: Check behaviours of format functions
DONTRUN:
*/
-/*
- run.config_ci
- STDOPT: #"@PTEST_FILE@ -cpp-extra-args='-D__FC_ASSERT_FILE__=@PTEST_FILE@'"
-*/
#include <stdlib.h>
#include <stdio.h>
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
index b1591588c9c1010fa57e062426441e8889a9acce..fe3bcf6a7cbf709979c4537344e12abe5f0b0d37 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
@@ -1,6 +1,6 @@
-[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:21: Warning:
+[kernel:typing:implicit-function-declaration] tests/format/fprintf.c:17: Warning:
Calling undeclared function fork. Old style K&R code?
-[kernel:typing:incompatible-types-call] tests/format/fprintf.c:28: Warning:
+[kernel:typing:incompatible-types-call] tests/format/fprintf.c:24: Warning:
expected 'FILE *' but got argument of type 'int *': & argc
[e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `exit':
@@ -39,71 +39,71 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/format/fprintf.c:21: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:17: Warning:
Neither code nor specification for function fork, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/format/fprintf.c:21: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:17: Warning:
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:
function __e_acsl_assert: precondition got status unknown.
[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.
-[eva:alarm] tests/format/fprintf.c:21: Warning:
+[eva:alarm] tests/format/fprintf.c:17: Warning:
accessing uninitialized left-value. assert \initialized(&process_status);
-[kernel:annot:missing-spec] tests/format/signalled.h:17: Warning:
+[kernel:annot:missing-spec] tests/format/signalled.h:15: Warning:
Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
-[eva:invalid-assigns] tests/format/fprintf.c:22:
+[eva:invalid-assigns] tests/format/fprintf.c:18:
Completely invalid destination for assigns clause *stream. Ignoring.
-[eva:alarm] tests/format/fprintf.c:22: Warning:
+[eva:alarm] tests/format/fprintf.c:18: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_0);
-[eva:alarm] tests/format/fprintf.c:25: Warning:
+[eva:alarm] tests/format/fprintf.c:21: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_1);
[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/format/fprintf.c:27: Warning:
+[eva:alarm] tests/format/fprintf.c:23: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_2);
-[eva:invalid-assigns] tests/format/fprintf.c:28:
+[eva:invalid-assigns] tests/format/fprintf.c:24:
Completely invalid destination for assigns clause *stream. Ignoring.
-[eva:alarm] tests/format/fprintf.c:28: Warning:
+[eva:alarm] tests/format/fprintf.c:24: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_3);
-[kernel:annot:missing-spec] tests/format/fprintf.c:33: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:29: Warning:
Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
-[eva:alarm] tests/format/fprintf.c:33: Warning:
+[eva:alarm] tests/format/fprintf.c:29: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_4);
-[eva:alarm] tests/format/fprintf.c:34: Warning:
+[eva:alarm] tests/format/fprintf.c:30: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_5);
-[kernel:annot:missing-spec] tests/format/fprintf.c:40: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:36: Warning:
Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
-[eva:alarm] tests/format/fprintf.c:40: Warning:
+[eva:alarm] tests/format/fprintf.c:36: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_6);
-[eva:alarm] tests/format/fprintf.c:41: Warning:
+[eva:alarm] tests/format/fprintf.c:37: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_7);
-[eva:alarm] tests/format/fprintf.c:42: Warning:
+[eva:alarm] tests/format/fprintf.c:38: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_8);
-[eva:invalid-assigns] tests/format/fprintf.c:43:
+[eva:invalid-assigns] tests/format/fprintf.c:39:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-[eva:alarm] tests/format/fprintf.c:43: Warning:
+[eva:alarm] tests/format/fprintf.c:39: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_9);
-[eva:invalid-assigns] tests/format/fprintf.c:44:
+[eva:invalid-assigns] tests/format/fprintf.c:40:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-[eva:alarm] tests/format/fprintf.c:44: Warning:
+[eva:alarm] tests/format/fprintf.c:40: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_10);
-[kernel:annot:missing-spec] tests/format/fprintf.c:47: Warning:
+[kernel:annot:missing-spec] tests/format/fprintf.c:43: Warning:
Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
-[eva:alarm] tests/format/fprintf.c:47: Warning:
+[eva:alarm] tests/format/fprintf.c:43: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_11);
-[eva:alarm] tests/format/fprintf.c:48: Warning:
+[eva:alarm] tests/format/fprintf.c:44: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_12);
-[eva:invalid-assigns] tests/format/fprintf.c:49:
+[eva:invalid-assigns] tests/format/fprintf.c:45:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-[eva:alarm] tests/format/fprintf.c:49: Warning:
+[eva:alarm] tests/format/fprintf.c:45: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_13);
-[eva:alarm] tests/format/fprintf.c:50: Warning:
+[eva:alarm] tests/format/fprintf.c:46: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_14);
-[eva:invalid-assigns] tests/format/fprintf.c:51:
+[eva:invalid-assigns] tests/format/fprintf.c:47:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-[eva:alarm] tests/format/fprintf.c:51: Warning:
+[eva:alarm] tests/format/fprintf.c:47: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_15);
-[eva:invalid-assigns] tests/format/fprintf.c:52:
+[eva:invalid-assigns] tests/format/fprintf.c:48:
Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-[eva:alarm] tests/format/fprintf.c:52: Warning:
+[eva:alarm] tests/format/fprintf.c:48: Warning:
accessing uninitialized left-value. assert \initialized(&process_status_16);
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index ec5c8f048c1bb5887438f817bed686f2da7f22ca..97a3f9b0d6c2ae37cd984948fdca68ac1e710137 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
@@ -47,94 +47,94 @@ void __e_acsl_globals_init(void)
static char __e_acsl_already_run = 0;
if (! __e_acsl_already_run) {
__e_acsl_already_run = 1;
- __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:52";
+ __gen_e_acsl_literal_string_31 = "tests/format/fprintf.c:48";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
- sizeof("tests/format/fprintf.c:52"));
+ sizeof("tests/format/fprintf.c:48"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
- __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:51";
+ __gen_e_acsl_literal_string_30 = "tests/format/fprintf.c:47";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
- sizeof("tests/format/fprintf.c:51"));
+ sizeof("tests/format/fprintf.c:47"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
- __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:50";
+ __gen_e_acsl_literal_string_29 = "tests/format/fprintf.c:46";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
- sizeof("tests/format/fprintf.c:50"));
+ sizeof("tests/format/fprintf.c:46"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
- __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:49";
+ __gen_e_acsl_literal_string_28 = "tests/format/fprintf.c:45";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
- sizeof("tests/format/fprintf.c:49"));
+ sizeof("tests/format/fprintf.c:45"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
- __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:48";
+ __gen_e_acsl_literal_string_27 = "tests/format/fprintf.c:44";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
- sizeof("tests/format/fprintf.c:48"));
+ sizeof("tests/format/fprintf.c:44"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
- __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:47";
+ __gen_e_acsl_literal_string_26 = "tests/format/fprintf.c:43";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
- sizeof("tests/format/fprintf.c:47"));
+ sizeof("tests/format/fprintf.c:43"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
- __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:44";
+ __gen_e_acsl_literal_string_25 = "tests/format/fprintf.c:40";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
- sizeof("tests/format/fprintf.c:44"));
+ sizeof("tests/format/fprintf.c:40"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
- __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:43";
+ __gen_e_acsl_literal_string_24 = "tests/format/fprintf.c:39";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/format/fprintf.c:43"));
+ sizeof("tests/format/fprintf.c:39"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
- __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:42";
+ __gen_e_acsl_literal_string_23 = "tests/format/fprintf.c:38";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/format/fprintf.c:42"));
+ sizeof("tests/format/fprintf.c:38"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
- __gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:41";
+ __gen_e_acsl_literal_string_21 = "tests/format/fprintf.c:37";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
- sizeof("tests/format/fprintf.c:41"));
+ sizeof("tests/format/fprintf.c:37"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
- __gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:40";
+ __gen_e_acsl_literal_string_19 = "tests/format/fprintf.c:36";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
- sizeof("tests/format/fprintf.c:40"));
+ sizeof("tests/format/fprintf.c:36"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
- __gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:34";
+ __gen_e_acsl_literal_string_16 = "tests/format/fprintf.c:30";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/format/fprintf.c:34"));
+ sizeof("tests/format/fprintf.c:30"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
- __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:33";
+ __gen_e_acsl_literal_string_15 = "tests/format/fprintf.c:29";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/format/fprintf.c:33"));
+ sizeof("tests/format/fprintf.c:29"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:28";
+ __gen_e_acsl_literal_string_14 = "tests/format/fprintf.c:24";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/format/fprintf.c:28"));
+ sizeof("tests/format/fprintf.c:24"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:27";
+ __gen_e_acsl_literal_string_13 = "tests/format/fprintf.c:23";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/format/fprintf.c:27"));
+ sizeof("tests/format/fprintf.c:23"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:25";
+ __gen_e_acsl_literal_string_12 = "tests/format/fprintf.c:21";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/format/fprintf.c:25"));
+ sizeof("tests/format/fprintf.c:21"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:22";
+ __gen_e_acsl_literal_string_9 = "tests/format/fprintf.c:18";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/format/fprintf.c:22"));
+ sizeof("tests/format/fprintf.c:18"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:21";
+ __gen_e_acsl_literal_string_8 = "tests/format/fprintf.c:17";
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("tests/format/fprintf.c:21"));
+ sizeof("tests/format/fprintf.c:17"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
__e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
__gen_e_acsl_literal_string_11 = "foobar %s\n";
diff --git a/src/plugins/e-acsl/tests/format/signalled.h b/src/plugins/e-acsl/tests/format/signalled.h
index 4021210a5dbb4648b83965e08e8e62b45ba2115c..58483ffd0d5eac1ae8081fd196520d56acd79ed4 100644
--- a/src/plugins/e-acsl/tests/format/signalled.h
+++ b/src/plugins/e-acsl/tests/format/signalled.h
@@ -4,12 +4,10 @@
#define STRINGIFY(x) #x
#define TOSTRING(x) STRINGIFY(x)
-#ifdef __FC_ASSERT_FILE__
-#define __EACSL_FILENAME__ TOSTRING(__FC_ASSERT_FILE__)
-#else
-#define __EACSL_FILENAME__ __FILE__
+#ifndef __FRAMAC__
+#define __FC_FILENAME__ __FILE__
#endif
-#define AT __EACSL_FILENAME__ ":" TOSTRING(__LINE__)
+#define AT __FC_FILENAME__ ":" TOSTRING(__LINE__)
int testno = 0;
diff --git a/tests/slicing/bts709.c b/tests/slicing/bts709.c
index 21c78aea4715b85d310312e4ab669ecd91d4acff..325e6ba28661753469776de28c3d337255b0523f 100644
--- a/tests/slicing/bts709.c
+++ b/tests/slicing/bts709.c
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"@PTEST_FILE@ -cpp-extra-args='-D__FC_ASSERT_FILE__=@PTEST_FILE@' -slice-pragma func -no-unicode -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
+ STDOPT: +"-slice-pragma func -no-unicode -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps"
*/
#include <assert.h>
diff --git a/tests/syntax/assert_location.c b/tests/syntax/assert_location.c
new file mode 100644
index 0000000000000000000000000000000000000000..b9575ad6a324872dcae8e455980260682fb84217
--- /dev/null
+++ b/tests/syntax/assert_location.c
@@ -0,0 +1,5 @@
+#include "assert_location.h"
+
+void c() {
+ assert("I'm in assert_location.c");
+}
diff --git a/tests/syntax/assert_location.h b/tests/syntax/assert_location.h
new file mode 100644
index 0000000000000000000000000000000000000000..772012e2415b9bd42b34a888e09982c0888ee221
--- /dev/null
+++ b/tests/syntax/assert_location.h
@@ -0,0 +1,5 @@
+#include "assert.h"
+
+void h() {
+ assert("I'm in assert_location.h");
+}
diff --git a/tests/syntax/fc_filename.c b/tests/syntax/fc_filename.c
new file mode 100644
index 0000000000000000000000000000000000000000..428237cc331dbd6895f22316f1d3d74cba2796c8
--- /dev/null
+++ b/tests/syntax/fc_filename.c
@@ -0,0 +1,7 @@
+const char* test = "string concatenation test: " __FC_FILENAME__ ". end test";
+
+int f() {
+ return test[2] == 'r';
+}
+
+/*@ lemma test: "string cst in ACSL: " __FC_FILENAME__ ".end test"[3] == 'i'; */
diff --git "a/tests/syntax/foo\".c" "b/tests/syntax/foo\".c"
new file mode 100644
index 0000000000000000000000000000000000000000..fa4ba0ab9ae9b4f51247cc78b369db0154bdfa9a
--- /dev/null
+++ "b/tests/syntax/foo\".c"
@@ -0,0 +1,7 @@
+#include "share/libc/assert.h"
+
+int test = 1;
+
+int main () {
+ assert(test);
+}
diff --git a/tests/syntax/oracle/assert_location.res.oracle b/tests/syntax/oracle/assert_location.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..330495a75d028e011333663a694d7bcaa435c18f
--- /dev/null
+++ b/tests/syntax/oracle/assert_location.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/syntax/assert_location.c (with preprocessing)
+/* Generated by Frama-C */
+#include "assert.h"
+void h(void)
+{
+ __FC_assert("I\'m in assert_location.h" != (char const *)0,
+ "tests/syntax/assert_location.h",4,
+ "\"I\'m in assert_location.h\"");
+ return;
+}
+
+void c(void)
+{
+ __FC_assert("I\'m in assert_location.c" != (char const *)0,
+ "tests/syntax/assert_location.c",4,
+ "\"I\'m in assert_location.c\"");
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/fc_filename.res.oracle b/tests/syntax/oracle/fc_filename.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1d842ed812f2fd1ed04732ca4f8d2a62743b9885
--- /dev/null
+++ b/tests/syntax/oracle/fc_filename.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing tests/syntax/fc_filename.c (with preprocessing)
+/* Generated by Frama-C */
+char const *test =
+ "string concatenation test: tests/syntax/fc_filename.c. end test";
+int f(void)
+{
+ int __retres;
+ __retres = (int)*(test + 2) == 'r';
+ return __retres;
+}
+
+/*@
+lemma test{L}:
+ *("string cst in ACSL: tests/syntax/fc_filename.c.end test" + 3) ≡ 'i';
+
+*/
+
diff --git "a/tests/syntax/oracle/foo\".res.oracle" "b/tests/syntax/oracle/foo\".res.oracle"
new file mode 100644
index 0000000000000000000000000000000000000000..ad66d6d1d2a99d868ff98d09a19696fe20ac787c
--- /dev/null
+++ "b/tests/syntax/oracle/foo\".res.oracle"
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/foo".c (with preprocessing)
+/* Generated by Frama-C */
+#include "assert.h"
+int test = 1;
+int main(void)
+{
+ int __retres;
+ __FC_assert(test != 0,"tests/syntax/foo\".c",6,"test");
+ __retres = 0;
+ return __retres;
+}
+
+