diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index aa521c40b1790c1ce291811288a016fcc26ae1cc..6b316854a46960544bb38a7812c206217cb4304b 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -509,6 +509,7 @@ type execnow =
Shared between all copies of this EXECNOW. Do
NOT use a mutable field here, as execnows
are duplicated using OCaml 'with' syntax. *)
+ ex_timeout: string;
}
@@ -595,11 +596,12 @@ type config =
(** full path of the default toplevel. *)
dc_filter : string option; (** optional filter to apply to
standard output *)
- dc_toplevels : (string * string * string list * Macros.t) list;
+ dc_toplevels : (string * string * string list * Macros.t * string) list;
(** toplevel full path, options to launch the toplevel on, and list
of output files to monitor beyond stdout and stderr. *)
dc_dont_run : bool;
dc_default_log: string list;
+ dc_timeout: string
}
let default_macros () =
@@ -615,9 +617,10 @@ let default_config () =
dc_execnow = [];
dc_filter = None ;
dc_default_toplevel = !toplevel_path;
- dc_toplevels = [ !toplevel_path, default_options, [], Macros.empty ];
+ dc_toplevels = [ !toplevel_path, default_options, [], Macros.empty, "" ];
dc_dont_run = false;
- dc_default_log = []
+ dc_default_log = [];
+ dc_timeout = "";
}
let launch command_string =
@@ -646,7 +649,7 @@ let launch command_string =
exit 1
-let scan_execnow ~once dir (s:string) =
+let scan_execnow ~once dir ex_timeout (s:string) =
let rec aux (s:execnow) =
try
Scanf.sscanf s.ex_cmd "%_[ ]LOG%_[ ]%[-A-Za-z0-9_',+=:.\\@@]%_[ ]%s@\n"
@@ -672,12 +675,15 @@ let scan_execnow ~once dir (s:string) =
ex_bin = [];
ex_dir = dir;
ex_once = once;
- ex_done = ref false }
+ ex_done = ref false;
+ ex_timeout;
+ }
(* the default toplevel for the current level of options. *)
let current_default_toplevel = ref !toplevel_path
let current_default_log = ref []
-let current_default_cmds = ref [!toplevel_path,default_options,[], Macros.empty]
+let current_default_cmds =
+ ref [!toplevel_path,default_options,[], Macros.empty, ""]
let make_custom_opts =
let space = Str.regexp " " in
@@ -711,7 +717,9 @@ let make_custom_opts =
(* how to process options *)
let config_exec ~once dir s current =
- { current with dc_execnow = scan_execnow ~once dir s :: current.dc_execnow }
+ { current with
+ dc_execnow =
+ scan_execnow ~once dir current.dc_timeout s :: current.dc_execnow }
let config_macro _dir s current =
let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in
@@ -745,7 +753,13 @@ let config_options =
"OPT",
(fun _ s current ->
- let t = current.dc_default_toplevel, s, current.dc_default_log, current.dc_macros in
+ let t =
+ current.dc_default_toplevel,
+ s,
+ current.dc_default_log,
+ current.dc_macros,
+ current.dc_timeout
+ in
{ current with
(* dc_default_toplevel = !current_default_toplevel;*)
dc_default_log = !current_default_log;
@@ -755,7 +769,9 @@ let config_options =
(fun _ s current ->
let new_top =
List.map
- (fun (cmd,opts, log, macros) -> cmd, make_custom_opts opts s, log, current.dc_macros)
+ (fun (cmd,opts, log, macros,_) ->
+ cmd, make_custom_opts opts s, log,
+ current.dc_macros, current.dc_timeout)
!current_default_cmds
in
{ current with dc_toplevels = new_top @ current.dc_toplevels;
@@ -783,8 +799,9 @@ let config_options =
"MODULE", config_module;
"LOG",
(fun _ s current ->
- { current with dc_default_log = s :: current.dc_default_log })
-
+ { current with dc_default_log = s :: current.dc_default_log });
+ "TIMEOUT",
+ (fun _ s current -> { current with dc_timeout = s });
]
let scan_options dir scan_buffer default =
@@ -871,7 +888,8 @@ type toplevel_command =
filter : string option ;
directory : SubDir.t ;
n : int;
- execnow:bool
+ execnow:bool;
+ timeout: string;
}
type command =
@@ -997,12 +1015,16 @@ let basic_command_string =
end else options
in
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 begin
- let file = Filename.sanitize @@ get_ptest_file command in
- toplevel ^ " " ^ file ^ " " ^ options
- end
+ let raw_command =
+ if has_ptest_file_t || has_ptest_file_o || command.execnow then
+ toplevel ^ " " ^ options
+ else begin
+ let file = Filename.sanitize @@ get_ptest_file command in
+ toplevel ^ " " ^ file ^ " " ^ options
+ end
+ in
+ if command.timeout = "" then raw_command
+ else "timeout " ^ command.timeout ^ " " ^ raw_command
(* Searches for executable [s] in the directories contained in the PATH
environment variable. Returns [None] if not found, or
@@ -1088,6 +1110,16 @@ let command_string command =
in
let res = Filename.sanitize (log_prefix ^ ".res.log") in
let command_string = command_string ^ " >" ^ res in
+ let command_string =
+ match command.timeout with
+ | "" -> command_string
+ | s ->
+ Printf.sprintf
+ "%s; if test $? -eq 124; then \
+ echo 'TIMEOUT (%s); ABORTING EXECUTION' > %s; \
+ fi"
+ command_string s (Filename.sanitize stderr)
+ in
let command_string = match filter with
| None -> command_string
| Some filter ->
@@ -1664,14 +1696,14 @@ let dispatcher () =
let i = ref 0 in
let e = ref 0 in
let nb_files = List.length config.dc_toplevels in
- let make_toplevel_cmd (toplevel, options, log_files, macros) =
+ let make_toplevel_cmd (toplevel, options, log_files, macros, timeout) =
let n = !i in
{file; options; toplevel; nb_files; directory; n; log_files;
filter = config.dc_filter; macros;
- execnow=false;
+ execnow=false; timeout;
}
in
- let mk_cmd s =
+ let mk_cmd (s, timeout) =
{
file = file;
nb_files = nb_files;
@@ -1683,20 +1715,22 @@ let dispatcher () =
filter = config.dc_filter;
macros = config.dc_macros;
execnow = true;
+ timeout;
}
in
let process_macros_cmd s = basic_command_string (mk_cmd s) in
- let macros = get_macros (mk_cmd "/bin/true") in
+ let macros = get_macros (mk_cmd ("/bin/true","")) in
let process_macros s = Macros.expand macros s in
let make_execnow_cmd execnow =
let res =
{
- ex_cmd = process_macros_cmd execnow.ex_cmd;
+ ex_cmd = process_macros_cmd (execnow.ex_cmd, execnow.ex_timeout);
ex_log = List.map process_macros execnow.ex_log;
ex_bin = List.map process_macros execnow.ex_bin;
ex_dir = execnow.ex_dir;
ex_once = execnow.ex_once;
ex_done = execnow.ex_done;
+ ex_timeout = execnow.ex_timeout;
}
in
incr e; res
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 95a4c0e88dd64826296785b7eb21e683f74534c1..a739cc905cee0858db22cd8ad9f2b52a947831d4 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -66,7 +66,7 @@ let smooth_expression lst =
let end_loc = snd (Extlib.last lst).expr_loc in
{ expr_loc = (beg_loc,end_loc); expr_node = COMMA (lst) }
-let merge_string (c1,(b1,_)) (c2,(_,e2)) = c1 @ c2, (b1,e2)
+let merge_string (c1,(b1,_)) (l2,(_,e2)) = c1 :: l2, (b1,e2)
(* To be called only inside a grammar rule. *)
let make_expr e =
@@ -213,12 +213,13 @@ let int64_to_char value =
Char.chr (Int64.to_int value)
(* takes a not-nul-terminated list, and converts it to a string. *)
-let intlist_to_string (str: int64 list):string =
- let buffer = Buffer.create (List.length str) in
+let intlist_to_string str =
+ let buffer = Buffer.create 64 in
let add_char c =
Buffer.add_char buffer (int64_to_char c)
in
- List.iter add_char str ;
+ let add_char_list l = List.iter add_char l in
+ List.iter add_char_list str ;
Buffer.contents buffer
let fst3 (result, _, _) = result
@@ -407,8 +408,6 @@ let in_ghost_block ?(battrs=[]) l =
%type <Cabs.expression list> paren_comma_expression
%type <Cabs.expression list> arguments
%type <Cabs.expression list> bracket_comma_expression
-%type <int64 list * cabsloc> string_list
-%type <int64 list * cabsloc> wstring_list
%type <Cabs.initwhat * Cabs.init_expression> initializer_single
%type <(Cabs.initwhat * Cabs.init_expression) list> initializer_list
@@ -746,12 +745,12 @@ expression: /*(* 6.5.17 *)*/
constant:
- CST_INT {CONST_INT (fst $1), snd $1}
-| CST_FLOAT {CONST_FLOAT (fst $1), snd $1}
-| CST_CHAR {CONST_CHAR (fst $1), snd $1}
-| CST_WCHAR {CONST_WCHAR (fst $1), snd $1}
-| string_constant {CONST_STRING (fst $1), snd $1}
-| wstring_list {CONST_WSTRING (fst $1), snd $1}
+ CST_INT {CONST_INT (fst $1), snd $1}
+| CST_FLOAT {CONST_FLOAT (fst $1), snd $1}
+| CST_CHAR {CONST_CHAR (fst $1), snd $1}
+| CST_WCHAR {CONST_WCHAR (fst $1), snd $1}
+| string_constant {CONST_STRING (fst $1), snd $1}
+| wstring_list {CONST_WSTRING (List.concat (fst $1)), snd $1}
;
string_constant:
@@ -761,15 +760,15 @@ string_constant:
;
string_list:
- one_string { fst $1, snd $1 }
-| string_list one_string { merge_string $1 $2 }
+ one_string { [fst $1], snd $1 }
+| one_string string_list { merge_string $1 $2 }
;
wstring_list:
- CST_WSTRING { $1 }
-| wstring_list one_string { merge_string $1 $2 }
-| wstring_list CST_WSTRING { merge_string $1 $2 }
-| string_list CST_WSTRING { merge_string $1 $2 }
+ CST_WSTRING { [fst $1], snd $1 }
+| one_string wstring_list { merge_string $1 $2 }
+| CST_WSTRING wstring_list { merge_string $1 $2 }
+| CST_WSTRING string_list { merge_string $1 $2 }
/* If a wstring is present anywhere in the list, the whole is a wstring */
one_string:
@@ -1751,8 +1750,8 @@ asmattr:
| CONST asmattr { ("const", []) :: $2 }
;
asmtemplate:
- one_string { [intlist_to_string (fst $1)] }
-| one_string asmtemplate { intlist_to_string (fst $1) :: $2 }
+ one_string { [intlist_to_string [fst $1]] }
+| one_string asmtemplate { intlist_to_string [fst $1] :: $2 }
;
asmoutputs:
/* empty */ { None }
diff --git a/tests/syntax/oracle/string_concat.res.oracle b/tests/syntax/oracle/string_concat.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..53ba826eecebeda5dab364833b2aa48fb50db743
--- /dev/null
+++ b/tests/syntax/oracle/string_concat.res.oracle
@@ -0,0 +1,27 @@
+[kernel] Parsing tests/syntax/string_concat.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ test[0..65535] ∈ {97}
+ [65536] ∈ {0}
+[eva] using specification for function printf_va_1
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+ S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 4 statements reached (out of 4): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 2 valid 0 unknown 0 invalid 2 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/syntax/oracle/wstring_concat.res.oracle b/tests/syntax/oracle/wstring_concat.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c83c532eda24f38ad8b7cd5f810b465d321768f6
--- /dev/null
+++ b/tests/syntax/oracle/wstring_concat.res.oracle
@@ -0,0 +1,27 @@
+[kernel] Parsing tests/syntax/wstring_concat.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ test[0..65535] ∈ {97}
+ [65536] ∈ {0}
+[eva] using specification for function printf_va_1
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+ S___fc_stdout[0..1] ∈ [--..--]
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 4 statements reached (out of 4): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 2 valid 0 unknown 0 invalid 2 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c
new file mode 100644
index 0000000000000000000000000000000000000000..9669f9687ef7cf8cc60d35c0a1ce2f5b1610b5d3
--- /dev/null
+++ b/tests/syntax/string_concat.c
@@ -0,0 +1,17 @@
+/* run.config*
+TIMEOUT: 45s
+OPT: -eva
+*/
+
+#include <string.h>
+#include <stdio.h>
+
+#define d(a) a a
+#define dd(a) d(d(a))
+#define ddd(a) dd(dd(a))
+#define dddd(a) ddd(ddd(a))
+#define ddddd(a) dddd(dddd(a))
+
+const char test[] = ddddd("a");
+
+int main() { printf("length: %zu\n",strlen(test)); }
diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c
new file mode 100644
index 0000000000000000000000000000000000000000..86d7d3ff4ea605a03428e8bcdae6e5be9ea69642
--- /dev/null
+++ b/tests/syntax/wstring_concat.c
@@ -0,0 +1,17 @@
+/* run.config*
+TIMEOUT: 45s
+OPT: -eva
+*/
+
+#include <wchar.h>
+#include <stdio.h>
+
+#define d(a) a a
+#define dd(a) d(d(a))
+#define ddd(a) dd(dd(a))
+#define dddd(a) ddd(ddd(a))
+#define ddddd(a) dddd(dddd(a))
+
+const wchar_t test[] = ddddd(L"a");
+
+int main() { printf("length: %zu\n",wcslen(test)); }