diff --git a/.gitignore b/.gitignore index 7343b6eb873ae129de4a268773e8aac76a18c1ab..7af9b4730c1604afa1dd26e817b1f26ec55700bd 100644 --- a/.gitignore +++ b/.gitignore @@ -3,9 +3,6 @@ ########### TAGS -*.cm* -*.o -*.a *.annot #ocamlyacc -v *.output diff --git a/ptests/ptests.ml b/ptests/ptests.ml index c8eff47171d25e13c024603ab59db95975d2a084..1de9faaf1d72de8a9f2904c57ac64eace0e501db 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -569,6 +569,10 @@ struct add name (get name macros ^ expand macros def) macros end +type compile_cmxs = + { dir: SubDir.t; + cmxs: string; + } (** configuration of a directory/test. *) type config = @@ -577,6 +581,8 @@ type config = dc_execnow : execnow list; (** command to be launched before the toplevel(s) *) + dc_cmxs : compile_cmxs list; (** cmxs to compile *) + dc_deps : string list; (** deps *) dc_macros: Macros.t; (** existing macros. *) dc_default_toplevel : string; (** full path of the default toplevel. *) @@ -602,6 +608,8 @@ let default_config () = { dc_test_regexp = test_file_regexp ; dc_macros = default_macros (); dc_execnow = []; + dc_cmxs = []; + dc_deps = []; dc_filter = None ; dc_default_toplevel = !toplevel_path; dc_toplevels = [ !toplevel_path, default_options, [], Macros.empty, "" ]; @@ -686,6 +694,12 @@ let config_exec ~once dir s current = dc_execnow = scan_execnow ~once dir current.dc_timeout s :: current.dc_execnow } +let config_cmxs dir s current = + { current with dc_cmxs = {dir;cmxs=s} :: current.dc_cmxs } + +let config_deps _dir s current = + { current with dc_deps = (String.split_on_char ' ' s) @ current.dc_deps } + let config_macro _dir s current = let regex = Str.regexp "[ \t]*\\([^ \t@]+\\)\\([ \t]+\\(.*\\)\\|$\\)" in Mutex.lock str_mutex; @@ -760,6 +774,8 @@ let config_options = "EXECNOW", config_exec ~once:true; "EXEC", config_exec ~once:false; + "CMXS", config_cmxs; + "DEPS", config_deps; "MACRO", config_macro; "MODULE", config_module; "LOG", @@ -866,6 +882,7 @@ type toplevel_command = n : int; execnow:bool; timeout: string; + deps: string list; } type command = @@ -944,7 +961,7 @@ let gen_prefix gen_file cmd = let log_prefix = gen_prefix SubDir.make_result_file let oracle_prefix = gen_prefix SubDir.make_oracle_file -let get_ptest_file cmd = Filename.concat ".." cmd.file +let get_ptest_file cmd = cmd.file let get_macros cmd = let ptest_config = @@ -1037,86 +1054,130 @@ let find_in_path s = with Exit -> Some !found -let command_string cout command = +let command_string ~result_cout ~oracle_cout command = let log_prefix = log_prefix command in let errlog = log_prefix ^ ".err.log" in - let stderr = match command.filter with - None -> errlog - | Some _ -> - let stderr = - Filename.temp_file (Filename.basename log_prefix) ".err.log" - in - at_exit (fun () -> unlink stderr); - stderr - in - let filter = match command.filter with - | None -> None - | Some filter -> - let len = String.length filter in - let rec split_filter i = - if i < len && filter.[i] = ' ' then split_filter (i+1) - else - try - let idx = String.index_from filter i ' ' in - String.sub filter i idx, - String.sub filter idx (len - idx) - with Not_found -> - String.sub filter i (len - i), "" - in - let exec_name, params = split_filter 0 in - let exec_name = - if Sys.file_exists exec_name || not (Filename.is_relative exec_name) - then exec_name - else - match find_in_path exec_name with - | Some full_exec_name -> full_exec_name - | None -> - Filename.concat - (Filename.dirname (Filename.dirname log_prefix)) - (Filename.basename exec_name) - in - Some (exec_name ^ params) - in + (* let stderr = match command.filter with + * None -> errlog + * | Some _ -> + * let stderr = + * Filename.temp_file (Filename.basename log_prefix) ".err.log" + * in + * at_exit (fun () -> unlink stderr); + * stderr + * in *) + (* let filter = match command.filter with + * | None -> None + * | Some filter -> + * let len = String.length filter in + * let rec split_filter i = + * if i < len && filter.[i] = ' ' then split_filter (i+1) + * else + * try + * let idx = String.index_from filter i ' ' in + * String.sub filter i idx, + * String.sub filter idx (len - idx) + * with Not_found -> + * String.sub filter i (len - i), "" + * in + * let exec_name, params = split_filter 0 in + * let exec_name = + * if Sys.file_exists exec_name || not (Filename.is_relative exec_name) + * then exec_name + * else + * match find_in_path exec_name with + * | Some full_exec_name -> full_exec_name + * | None -> + * Filename.concat + * (Filename.dirname (Filename.dirname log_prefix)) + * (Filename.basename exec_name) + * in + * Some (exec_name ^ params) + * in *) let command_string = basic_command_string command in - let command_string = - command_string ^ " 2>" ^ (Filename.sanitize stderr) - in - let command_string = match filter with - | None -> command_string - | Some filter -> command_string ^ " | " ^ filter - 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 $? -gt 127; 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 -> - Printf.sprintf "%s && %s < %s >%s && rm -f %s" - command_string - filter - (Filename.sanitize stderr) - (Filename.sanitize errlog) - (Filename.sanitize stderr) - in - Printf.fprintf cout + (* let command_string = match filter with + * | None -> command_string + * | Some filter -> command_string ^ " | " ^ filter + * in *) + let res = (log_prefix ^ ".res.log") in + (* let command_string = + * match command.timeout with + * | "" -> command_string + * | s -> + * Printf.sprintf + * "%s; if test $? -gt 127; 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 -> + * Printf.sprintf "%s && %s < %s >%s && rm -f %s" + * command_string + * filter + * (Filename.sanitize stderr) + * (Filename.sanitize errlog) + * (Filename.sanitize stderr) + * in *) + Printf.fprintf result_cout "(rule\n \ (targets %S %S %t)\n \ - (deps (universe))\n \ - (action (system %S))\n\ + (deps %t %S (package frama-c) (universe))\n \ + (action (with-stderr-to %S (with-stdout-to %S (with-accepted-exit-codes (or 0 1) (system %S)))))\n\ )\n" errlog res (fun cout -> List.iter (Printf.fprintf cout "%S") command.log_files) - command_string + (fun cout -> List.iter (fun d -> Printf.fprintf cout "%S" (Filename.concat ".." d)) command.deps) + (get_ptest_file command) + errlog + res + command_string; + Printf.fprintf result_cout + "(rule\n \ + (alias %S)\n \ + (deps %S (package frama-c) (universe))\n \ + (action (system %S))\n\ + )\n" + command.file + (get_ptest_file command) + command_string; + + let oracle_prefix = oracle_prefix command in + (* Update oracle *) + Printf.fprintf result_cout + "(rule\n \ + (alias %S)\n \ + (action (diff %S %S))\n\ + )\n" + ("diff-"^log_prefix) + (Filename.concat ".." (oracle_prefix ^ ".res.oracle")) + (log_prefix ^ ".res.log"); + Printf.fprintf result_cout + "(rule\n \ + (alias %S)\n \ + (action (diff %S %S))\n\ + )\n" + ("diff-"^log_prefix) + (Filename.concat ".." (oracle_prefix ^ ".err.oracle")) + (log_prefix ^ ".err.log"); + Printf.fprintf result_cout + "(alias (deps (alias %S)) (name ptests))\n" + ("diff-"^log_prefix); + Printf.fprintf oracle_cout + "(rule (target %S) (mode fallback) (action (write-file %S \"\")))\n" + (Filename.basename (oracle_prefix ^ ".err.oracle")) + (Filename.basename (oracle_prefix ^ ".err.oracle")); + Printf.fprintf oracle_cout + "(rule (target %S) (mode fallback) (action (write-file %S \"\")))\n" + (Filename.basename (oracle_prefix ^ ".res.oracle")) + (Filename.basename (oracle_prefix ^ ".res.oracle")); + () + + + + let update_log_files dir file = mv (SubDir.make_result_file dir file) (SubDir.make_oracle_file dir file) @@ -1575,8 +1636,7 @@ let update_dir_ref dir config = let dc_execnow = List.map update_execnow config.dc_execnow in { config with dc_execnow } -let dispatcher cout file directory config = - Printf.fprintf cout "(alias (name ptests) (deps %S))\n" file; +let dispatcher ~result_cout ~oracle_cout file directory config = let config = scan_test_file config directory file in let i = ref 0 in @@ -1587,6 +1647,7 @@ let dispatcher cout file directory config = {file; options; toplevel; nb_files; directory; n; log_files; filter = config.dc_filter; macros; execnow=false; timeout; + deps = config.dc_deps; } in let mk_cmd (s, timeout) = @@ -1602,6 +1663,7 @@ let dispatcher cout file directory config = macros = config.dc_macros; execnow = true; timeout; + deps = config.dc_deps; } in let process_macros_cmd s = basic_command_string (mk_cmd s) in @@ -1623,9 +1685,16 @@ let dispatcher cout file directory config = in let treat_option option = let toplevel = make_toplevel_cmd option in - command_string cout toplevel; + command_string ~result_cout ~oracle_cout toplevel; incr i in + List.iter (fun cmxs -> + let file = Macros.expand macros cmxs.cmxs in + Printf.fprintf result_cout "\ + (executable (name %s) (modules %s) (modes plugin) (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel) (flags -open Frama_c_kernel))\n \ +" + file file + ) config.dc_cmxs; begin (match config.dc_execnow with | hd :: tl -> @@ -1670,8 +1739,11 @@ let () = if !verbosity >= 2 then lock_printf "%% producer now treating test %s\n%!" suite; (* the "suite" may be a directory or a single file *) let directory = SubDir.create suite in - let dune_file = Filename.concat (SubDir.make_file directory SubDir.result_dirname) "dune" in - let cout = open_out dune_file in + let result_dune_file = Filename.concat (SubDir.make_file directory SubDir.result_dirname) "dune" in + let result_cout = open_out result_dune_file in + Printf.fprintf result_cout "(copy_files ../*.*)\n"; + let oracle_dune_file = Filename.concat (SubDir.make_file directory SubDir.oracle_dirname) "dune" in + let oracle_cout = open_out oracle_dune_file in let config = SubDir.make_file directory dir_config_file in let default = default_config () in let default = update_dir_ref directory default in @@ -1689,10 +1761,11 @@ let () = assert (Filename.is_relative file); if test_pattern dir_config file then begin - dispatcher cout file directory dir_config; + dispatcher ~result_cout ~oracle_cout file directory dir_config; end; done; - close_out cout; + close_out result_cout; + close_out oracle_cout; ) suites diff --git a/tests/builtins/Longinit_sequencer.i b/tests/builtins/Longinit_sequencer.i index 919f247cf5d6fb7f63b2b76707794dbf2b09428a..865538e6d3614ae679d0a4f26b552c85a5ae32dd 100644 --- a/tests/builtins/Longinit_sequencer.i +++ b/tests/builtins/Longinit_sequencer.i @@ -1,4 +1,4 @@ /* run.config* - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@ + CMXS: @PTEST_NAME@ + OPT: @EVA_OPTIONS@ -load-module %{dep:@PTEST_NAME@.cmxs} -res-file @PTEST_RESULT@ */ diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i index 84322912cb6c9b8a476d38e523f53629faab6d0a..fea99debc14badafb0949fac4b10af433343a447 100644 --- a/tests/builtins/big_local_array.i +++ b/tests/builtins/big_local_array.i @@ -1,5 +1,5 @@ /* run.config* - EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs + CMXS: big_local_array_script OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva diff --git a/tests/callgraph/function_pointer.i b/tests/callgraph/function_pointer.i index b28287119069e61b95d7115a89eeb8592e7e8412..b728da3dedd5540c03de58b50a1783c299dad3af 100644 --- a/tests/callgraph/function_pointer.i +++ b/tests/callgraph/function_pointer.i @@ -1,6 +1,6 @@ /* run.config COMMENT: Test option -cg-function-pointers - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ OPT: -cg-function-pointers -no-autoload-plugins -load-module eva,@PTEST_DIR@/@PTEST_NAME@.cmxs OPT: -cg-no-services -cg-function-pointers -no-autoload-plugins -load-module eva,@PTEST_DIR@/@PTEST_NAME@.cmxs OPT: -cg-no-function-pointers -no-autoload-plugins -load-module eva,@PTEST_DIR@/@PTEST_NAME@.cmxs diff --git a/tests/cil/change_formals.c b/tests/cil/change_formals.c index 5ac6f89b75edfa8287197e7faefe404870c75820..03afa8e5e154a63644671792ceda24462593f36c 100644 --- a/tests/cil/change_formals.c +++ b/tests/cil/change_formals.c @@ -1,8 +1,8 @@ /* run.config -EXECNOW: make -s tests/cil/Change_formals.cmxs -OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print -OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print -OPT: -load-module tests/cil/Change_formals.cmxs -then-on test -print +CMXS: Change_formals +OPT: -load-module %{dep:Change_formals.cmxs} -cpp-extra-args="-DNO_PROTO" -then-on test -print +OPT: -load-module %{dep:Change_formals.cmxs} -cpp-extra-args="-DNO_IMPLEM" -then-on test -print +OPT: -load-module %{dep:Change_formals.cmxs} -then-on test -print */ #ifndef NO_PROTO diff --git a/tests/cil/change_to_instr.i b/tests/cil/change_to_instr.i index b83b32608f67b7918cae94834696592bc19cf770..6539a2560a2599cbec14b19e35771b8e33255ffa 100644 --- a/tests/cil/change_to_instr.i +++ b/tests/cil/change_to_instr.i @@ -1,5 +1,5 @@ /* run.config -OPT: -load-script tests/cil/change_to_instr.ml -print +OPT: -load-script %{dep:change_to_instr.ml} -print */ diff --git a/tests/cil/cpu_b.c b/tests/cil/cpu_b.c index 66280560447f97a5913fc7accbcd946494a938ff..9af03e9fbb804e110b4070bd5618c58bb6e67f4c 100644 --- a/tests/cil/cpu_b.c +++ b/tests/cil/cpu_b.c @@ -1,5 +1,5 @@ /* run.config - OPT: tests/cil/cpu_a.c -machdep x86_16 -print + OPT: %{dep:cpu_a.c} -machdep x86_16 -print */ typedef unsigned int DWORD ; diff --git a/tests/cil/mkBinOp.i b/tests/cil/mkBinOp.i index 1bab30cf83cef46281180438db232f21b9d1224b..f6d3c59d93a9800e7182be9036ee7fc0ebaa7472 100644 --- a/tests/cil/mkBinOp.i +++ b/tests/cil/mkBinOp.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -constfold +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print -constfold */ int main(void) { diff --git a/tests/cil/queue_ghost_instr.i b/tests/cil/queue_ghost_instr.i index 3bae2b6f40b0ef3824806fb03117f9af8f5e9610..9daed07fd9b2412221e776c1254a9f69450e391b 100644 --- a/tests/cil/queue_ghost_instr.i +++ b/tests/cil/queue_ghost_instr.i @@ -1,5 +1,5 @@ /* run.config -OPT: -load-script tests/cil/queue_ghost_instr.ml -print +OPT: -load-script %{dep:queue_ghost_instr.ml} -print */ diff --git a/tests/constant_propagation/introduction_of_non_explicit_cast.c b/tests/constant_propagation/introduction_of_non_explicit_cast.c index 959842971acaa01ca6b96c2891898086bd098d45..c4204d7b3fdd1fbf9a3e25e8b4130b9098d5a52c 100644 --- a/tests/constant_propagation/introduction_of_non_explicit_cast.c +++ b/tests/constant_propagation/introduction_of_non_explicit_cast.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -deps -journal-disable + CMXS: @PTEST_NAME@ + OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -deps -journal-disable */ int x,y,z; diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c index d3e15e1b85ec9976597846dcbf9b4be241b9e69b..2b3b065d5b8857c4ad2ebc4afac2c39d99b99d5a 100644 --- a/tests/fc_script/main.c +++ b/tests/fc_script/main.c @@ -1,11 +1,11 @@ /* run.config NOFRAMAC: testing frama-c-script, not frama-c itself EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err cd @PTEST_DIR@ && PTESTS_TESTING= ../../bin/frama-c-script make-template result < make_template.input > result/make_template.res 2> result/make_template.err - EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err - EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > @PTEST_DIR@/result/flamegraph.res 2> @PTEST_DIR@/result/flamegraph.err && rm -f @PTEST_DIR@/result/flamegraph.svg - EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun1.res 2> @PTEST_DIR@/result/find_fun1.err - EXECNOW: LOG find_fun2.res LOG find_fun2.err bin/frama-c-script find-fun main3 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun2.res 2> @PTEST_DIR@/result/find_fun2.err - EXECNOW: LOG find_fun3.res LOG find_fun3.err bin/frama-c-script find-fun false_positive @PTEST_DIR@ > @PTEST_DIR@/result/find_fun3.res 2> @PTEST_DIR@/result/find_fun3.err + EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > list_files.res 2> list_files.err + EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > flamegraph.res 2> flamegraph.err && rm -f flamegraph.svg + EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > find_fun1.res 2> find_fun1.err + EXECNOW: LOG find_fun2.res LOG find_fun2.err bin/frama-c-script find-fun main3 @PTEST_DIR@ > find_fun2.res 2> find_fun2.err + EXECNOW: LOG find_fun3.res LOG find_fun3.err bin/frama-c-script find-fun false_positive @PTEST_DIR@ > find_fun3.res 2> find_fun3.err */ void main() { diff --git a/tests/float/absorb.c b/tests/float/absorb.c index a71117b1674d5f6ba2b6dc97aeacd836c6f275cd..0f89d00949a7e5bdfdb1a709238df0637e4e8ee1 100644 --- a/tests/float/absorb.c +++ b/tests/float/absorb.c @@ -1,8 +1,8 @@ /* run.config COMMENT: run.config is intentionally not-* - EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err - EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err - OPT: -load @PTEST_DIR@/result/absorb.sav2 -deps -out -input + EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save absorb.sav @PTEST_FILE@ > absorb_sav.res 2> absorb_sav.err + EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err + OPT: -load absorb.sav2 -deps -out -input */ /* run.config* DONTRUN: diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c index f2389fe2e8ada1276a640ceb2689b7ff4f5a6f76..24adf4033f0e913590a0b38208870743d8e077b4 100644 --- a/tests/jcdb/jcdb.c +++ b/tests/jcdb/jcdb.c @@ -1,9 +1,9 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ OPT: -json-compilation-database @PTEST_DIR@ -print OPT: @PTEST_DIR@/jcdb2.c -json-compilation-database @PTEST_DIR@/with_arguments.json -print -OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err +OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} +EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > list_files.res 2> list_files.err */ #include <stdio.h> diff --git a/tests/journal/control.i b/tests/journal/control.i index a136fc4ec7a9ab6ed04a524260be23695e81cb7d..e5e3a07a19c20f39e9487bee2dce161c3cd1e5a3 100644 --- a/tests/journal/control.i +++ b/tests/journal/control.i @@ -5,10 +5,10 @@ OPT: -load-script tests/journal/result/control_journal -journal-disable CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte OPT: -load-script tests/journal/result/control_journal_bis -calldeps -journal-disable - EXECNOW: make -s @PTEST_DIR@/abstract_cpt.cmxs - EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null + CMXS: abstract_cpt + EXECNOW: BIN abstract_cpt_journal.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-module @PTEST_DIR@/abstract_cpt -load-script %{dep:use_cpt.ml} -journal-name tests/journal/result/abstract_cpt_journal.ml > /dev/null 2> /dev/null CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte - OPT: -load-script tests/journal/result/abstract_cpt_journal.ml -load-module @PTEST_DIR@/abstract_cpt -load-script tests/journal/use_cpt.ml + OPT: -load-script %{dep:result/abstract_cpt_journal.ml} -load-module @PTEST_DIR@/abstract_cpt -load-script %{dep:use_cpt.ml} */ int x,y,c,d; diff --git a/tests/journal/control2.c b/tests/journal/control2.c index 8e04f8022b2c5bddd51246e207e48be678a99c8f..72b6b64794a946e8a78b41ec3db5588c6307a2d4 100644 --- a/tests/journal/control2.c +++ b/tests/journal/control2.c @@ -1,6 +1,6 @@ /* run.config EXECNOW: BIN control_journal2.ml ./bin/toplevel.opt -journal-enable -eva -deps -out -main f -journal-name tests/journal/result/control_journal2.ml tests/journal/control2.c > /dev/null 2> /dev/null - EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script tests/journal/result/control_journal2 -lib-entry -journal-name tests/journal/result/control_journal_next2.ml tests/journal/control2.c > ./tests/journal/result/control2_sav.res 2> ./tests/journal/result/control2_sav.err + EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script %{dep:result/control_journal2 -lib-entry -journal-name tests/journal/result/control_journal_next2.ml} tests/journal/control2.c > ./tests/journal/result/control2_sav.res 2> ./tests/journal/result/control2_sav.err CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte OPT: -load-script tests/journal/result/control_journal_next2 */ diff --git a/tests/journal/intra.i b/tests/journal/intra.i index dea5fdbface5e49569a2d52996e69ac8b4d52f06..6ebe0f8822045aede7db39ae94e5a20cc67c04dd 100644 --- a/tests/journal/intra.i +++ b/tests/journal/intra.i @@ -1,7 +1,7 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null - CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name tests/journal/result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null + CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} OPT: -load-script tests/journal/result/intra_journal -journal-disable */ diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c index 5ad226916ca36cd0496df4992e45e78d79a22da2..e27df601aed53da458a20f076d8b76794729c9e8 100644 --- a/tests/libc/fc_libc.c +++ b/tests/libc/fc_libc.c @@ -1,9 +1,9 @@ /* run.config* - EXECNOW: make -s @PTEST_DIR@/check_libc_naming_conventions.cmxs - EXECNOW: make -s @PTEST_DIR@/check_const.cmxs - EXECNOW: make -s @PTEST_DIR@/check_parsing_individual_headers.cmxs - EXECNOW: make -s @PTEST_DIR@/check_libc_anonymous_tags.cmxs - EXECNOW: make -s @PTEST_DIR@/check_compliance.cmxs + CMXS: check_libc_naming_conventions + CMXS: check_const + CMXS: check_parsing_individual_headers + CMXS: check_libc_anonymous_tags + CMXS: check_compliance OPT: -load-module @PTEST_DIR@/check_libc_naming_conventions -print -cpp-extra-args='-nostdinc -Ishare/libc' -metrics -metrics-libc -load-module @PTEST_DIR@/check_const -load-module metrics -eva @EVA_CONFIG@ -then -lib-entry -no-print -metrics-no-libc OPT: -print -print-libc OPT: -load-module @PTEST_DIR@/check_parsing_individual_headers diff --git a/tests/misc/custom_machdep/__fc_machdep_custom.h b/tests/misc/__fc_machdep_custom.h similarity index 100% rename from tests/misc/custom_machdep/__fc_machdep_custom.h rename to tests/misc/__fc_machdep_custom.h diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i index a6a820ecce977ef9f528f95bcb149fe3df18001a..8165be2e42b963354c94f2f9f0d97c498b66c30f 100644 --- a/tests/misc/add_assigns.i +++ b/tests/misc/add_assigns.i @@ -1,5 +1,5 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ OPT: -no-autoload-plugins -load-module report,@PTEST_DIR@/@PTEST_NAME@.cmxs -then -report -then -print */ diff --git a/tests/misc/bts0452.i b/tests/misc/bts0452.i index 1f3fc795582b79b21aad809bf852bfb655ce3cd7..a8eebfb6832b91a1ce206ef57876f0028f6fd345 100644 --- a/tests/misc/bts0452.i +++ b/tests/misc/bts0452.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -typecheck -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -typecheck -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /* must emit falls-through warning. */ int f (int foo, char** args) { diff --git a/tests/misc/bts0489.i b/tests/misc/bts0489.i index c33db7d4c1a3f7b4d29d0fc48a0aeaf37101775b..f920a1fc09388d61bab16eef5145c9f52dced563 100644 --- a/tests/misc/bts0489.i +++ b/tests/misc/bts0489.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ typedef unsigned char uint8_t; diff --git a/tests/misc/bts1201.i b/tests/misc/bts1201.i index cbaf4a4e3d114ba17709f3f7fc7bfe0c6f8f5d27..fff261907b0ca153e35550984aa71a793bade5b8 100644 --- a/tests/misc/bts1201.i +++ b/tests/misc/bts1201.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -eva-verbose 2 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print + CMXS: @PTEST_NAME@ + OPT: -eva-verbose 2 -load-module %{dep:@PTEST_NAME@.cmxs} -print */ void main() { //@ assert \true; } diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i index 5650e0651c86a321f57387978b130a56e1f889b6..235b3db280db98f752a2d788ce4cf66b8b2a7b9a 100644 --- a/tests/misc/bts1347.i +++ b/tests/misc/bts1347.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -report + CMXS: @PTEST_NAME@ + OPT: @EVA_OPTIONS@ -load-module %{dep:@PTEST_NAME@.cmxs} -then -report */ int f(int *x) { return *x; } int g(int *x) { return *(x++); } diff --git a/tests/misc/bug_0209.c b/tests/misc/bug_0209.c index a345a39f3b0ce1c51d4d918965de6620914abbde..d235913913f90e7363c563bce728f6991db94224 100644 --- a/tests/misc/bug_0209.c +++ b/tests/misc/bug_0209.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ // Everything is done by the script diff --git a/tests/misc/callsite.i b/tests/misc/callsite.i index 7dcfc493a8c89c38f1bb6189b0c562cccb8841e9..ab6149b8732a7922f050b5b94daa4d9d0aedef3b 100644 --- a/tests/misc/callsite.i +++ b/tests/misc/callsite.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ // Don't use -debug 1 option in the test command. diff --git a/tests/misc/change_main.i b/tests/misc/change_main.i index c6f70943352c91f4348680131c67bb9e27329040..627d22668d5fae9c6299ee49193d53faa35d5a11 100644 --- a/tests/misc/change_main.i +++ b/tests/misc/change_main.i @@ -1,6 +1,6 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -eva -main f -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then-on change_main -main g -eva +CMXS: @PTEST_NAME@ +OPT: -eva -main f -load-module %{dep:@PTEST_NAME@.cmxs} -then-on change_main -main g -eva */ int f(int x) { return x; } diff --git a/tests/misc/cli_string_multiple_map.i b/tests/misc/cli_string_multiple_map.i index b4a7c3bc23730ae8b09c9d851046c6b3e300b520..4c91d501d72cd510deb77d68f0d3d0b00508e976 100644 --- a/tests/misc/cli_string_multiple_map.i +++ b/tests/misc/cli_string_multiple_map.i @@ -1,4 +1,4 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -multiple-map a:1,b:2,a:3 + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -multiple-map a:1,b:2,a:3 */ diff --git a/tests/misc/copy_kf.i b/tests/misc/copy_kf.i index 15fe7d6bc47b3ae91e25275f2bc159cebaeca86d..245afeacb0bec543efe1fd891f2d35e339767f9c 100644 --- a/tests/misc/copy_kf.i +++ b/tests/misc/copy_kf.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ requires \valid(p); assigns *p; ensures *p == x; */ diff --git a/tests/misc/copy_machdep.i b/tests/misc/copy_machdep.i index 0b6f32f439f5a76fcda2d18135977d049f386d84..704c0406024b1c4429e7c2bfa0e0f4d2d9460b4e 100644 --- a/tests/misc/copy_machdep.i +++ b/tests/misc/copy_machdep.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -machdep x86_64 -enums int -no-unicode +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -machdep x86_64 -enums int -no-unicode */ int main () { return 0; } diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c index f7a377dc16250f21911dbc5f014d7a50b33bac3f..fe0382ca4d6fe3465bc3103f1c13b354041f9303 100644 --- a/tests/misc/custom_machdep.c +++ b/tests/misc/custom_machdep.c @@ -1,6 +1,6 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.cmxs -OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-module @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@ -machdep custom -print -then -print +CMXS: @PTEST_NAME@ +OPT: -cpp-extra-args="-D__FC_MACHDEP_CUSTOM" -load-module %{dep:@PTEST_NAME@.cmxs} -machdep custom -print -then -print COMMENT: we need a -then to test double registering of a machdep */ diff --git a/tests/misc/custom_machdep/custom_machdep.ml b/tests/misc/custom_machdep.ml similarity index 100% rename from tests/misc/custom_machdep/custom_machdep.ml rename to tests/misc/custom_machdep.ml diff --git a/tests/misc/ensures.i b/tests/misc/ensures.i index ae04e6fb897e157311e2131e8c00117972aaa048..41a96a18a21b26a8bfab804500ba694c8d12fbe9 100644 --- a/tests/misc/ensures.i +++ b/tests/misc/ensures.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -load-module %{dep:@PTEST_NAME@.cmxs} */ //@ ensures *p==1; void main(int * p){ *p = 0; } diff --git a/tests/misc/exception.i b/tests/misc/exception.i index a6e5006eb7dbab9286b39fbeaf6ea28e5c22be19..16e3d60c420593e2affb2bc4e837958bfe95a27b 100644 --- a/tests/misc/exception.i +++ b/tests/misc/exception.i @@ -1,7 +1,7 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -remove-exn -print + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -remove-exn -print */ struct my_exn { int e; }; diff --git a/tests/misc/find_enclosing_loop.c b/tests/misc/find_enclosing_loop.c index 76cc35a53187fc9e58ea906527669b5a9482e117..a4ea50d6d6343c6324b1eedd39f9c8e2786d72bf 100644 --- a/tests/misc/find_enclosing_loop.c +++ b/tests/misc/find_enclosing_loop.c @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ void f () { diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i index d13cbce847364dbce968f270f47d9cae11260cd8..f66f06ee2da70d0ef977b6fa27cdf5fc23b93caa 100644 --- a/tests/misc/global_decl_loc.i +++ b/tests/misc/global_decl_loc.i @@ -1,4 +1,4 @@ /* run.config - OPT: @PTEST_DIR@/global_decl_loc2.i -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + OPT: @PTEST_DIR@/global_decl_loc2.i -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int g; diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i index 08fe31aa7b67c33420527175fdcfeeedce5ac8b6..b1e507943a67bb2126e700398e47cf04976f60c7 100644 --- a/tests/misc/global_decl_loc2.i +++ b/tests/misc/global_decl_loc2.i @@ -1,5 +1,5 @@ /* run.config - OPT: @PTEST_DIR@/global_decl_loc.i -load-module @PTEST_DIR@/global_decl_loc.cmxs + OPT: @PTEST_DIR@/global_decl_loc.i -load-module %{dep:global_decl_loc.cmxs} */ extern int g; diff --git a/tests/misc/init_from_cil.i b/tests/misc/init_from_cil.i index 7d767032b7e6c7ef1acc8f6a4a7e1ff655cab5f7..e38ff8d3e44bd3850ef5c6888d576724f191f83d 100644 --- a/tests/misc/init_from_cil.i +++ b/tests/misc/init_from_cil.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int f(int x); diff --git a/tests/misc/interpreted_automata_dataflow.i b/tests/misc/interpreted_automata_dataflow.i index 9446609755e0db82db642ed1331e1ec2ae8e9b6e..94d7ec297518c1447a14375bf1c998b855018275 100644 --- a/tests/misc/interpreted_automata_dataflow.i +++ b/tests/misc/interpreted_automata_dataflow.i @@ -1,5 +1,5 @@ /* run.config -OPT: -load-script tests/misc/interpreted_automata_dataflow.ml +OPT: -load-script %{dep:interpreted_automata_dataflow.ml} */ /* Tests the dataflow functor of interpreted automata via a caml script diff --git a/tests/misc/issue109.i b/tests/misc/issue109.i index e6d7a20671adcc1bc1e8fd39bb40fec6d3986a45..9c1d45bdde57ca67d4c7d18042aaf35ef4d6af98 100644 --- a/tests/misc/issue109.i +++ b/tests/misc/issue109.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -eva @EVA_CONFIG@ -slevel-function main:10 -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -eva @EVA_CONFIG@ -slevel-function main:10 -load-module %{dep:@PTEST_NAME@.cmxs} */ void main() { int i, j = 0; diff --git a/tests/misc/issue_191.c b/tests/misc/issue_191.c index a345a39f3b0ce1c51d4d918965de6620914abbde..d235913913f90e7363c563bce728f6991db94224 100644 --- a/tests/misc/issue_191.c +++ b/tests/misc/issue_191.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ // Everything is done by the script diff --git a/tests/misc/justcopy.i b/tests/misc/justcopy.i index 8cfd1982b8925ce6626f5d9b9d91594011759c5a..33ffb04bc44c39470855ff963ae9dfabb532b04e 100644 --- a/tests/misc/justcopy.i +++ b/tests/misc/justcopy.i @@ -1,4 +1,4 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ diff --git a/tests/misc/keep_entry_point.i b/tests/misc/keep_entry_point.i index 6ade640dbb8933cb359dac79d608f7acf33fc4d3..b25fc87da1c50bd3cba85de62a0855e23a11156e 100644 --- a/tests/misc/keep_entry_point.i +++ b/tests/misc/keep_entry_point.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -main f -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print +CMXS: @PTEST_NAME@ +OPT: -main f -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print */ static int f(void); diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i index 833ee51da34f8228cc4ab373fe8573b430b7ca3f..3e30b03a472cc07da5e467992666ed50848b2f74 100644 --- a/tests/misc/log-file.i +++ b/tests/misc/log-file.i @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/plugin_log.cmxs + CMXS: plugin_log LOG: log-file-kernel-warnings.txt LOG: log-file-kernel-results.txt LOG: log-file-feedback.txt diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i index 1c1ed1cb63f2918ef0516de494e301c62fd70f04..4b872982212269a56eeb8643a7ae93f00461748b 100644 --- a/tests/misc/log_twice.i +++ b/tests/misc/log_twice.i @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ OPT: @EVA_CONFIG@ -load-module @PTEST_DIR@/@PTEST_NAME@ */ diff --git a/tests/misc/my_visitor.c b/tests/misc/my_visitor.c index 9ce70834706be3ccc9798f57e77d6e9e52258308..a4acec4aeca0cc5d04c0314a5fdf0ee108ef2d4b 100644 --- a/tests/misc/my_visitor.c +++ b/tests/misc/my_visitor.c @@ -1,7 +1,7 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav FRAMAC_PLUGIN=./lib/plugins @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@_sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@_sav.err -OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -no-my-visitor -print +CMXS: @PTEST_NAME@ +EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav FRAMAC_PLUGIN=./lib/plugins @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err +OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -no-my-visitor -print OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -no-autoload-plugins -print */ int f() { diff --git a/tests/misc/pp_bin_hex.i b/tests/misc/pp_bin_hex.i index a53499be69922b6d91cd0d4926968829ccf22a93..7b267b69c498e4bef6182abd049b7922444b8bc6 100644 --- a/tests/misc/pp_bin_hex.i +++ b/tests/misc/pp_bin_hex.i @@ -1,3 +1,3 @@ /* run.config - OPT: -no-autoload-plugins -load-script tests/misc/pp_bin_hex.ml + OPT: -no-autoload-plugins -load-script %{dep:pp_bin_hex.ml} */ diff --git a/tests/misc/pp_int.i b/tests/misc/pp_int.i index d6da6546ebd7eceeb7f3e589508b388adc949278..685adc627b4a0e8f4d158ab913623898247ce6a8 100644 --- a/tests/misc/pp_int.i +++ b/tests/misc/pp_int.i @@ -1,4 +1,4 @@ /* run.config COMMENT: test of Integer.pp_bin and Integer.pp_hex - OPT: -load-script tests/misc/pp_int.ml + OPT: -load-script %{dep:pp_int.ml} */ diff --git a/tests/misc/remove_status_hyps.i b/tests/misc/remove_status_hyps.i index a436356626c8169ba8c349bf26bb5d2d31c72a52..b62c85f1c6d396bede6422962fa95c3785dbba40 100644 --- a/tests/misc/remove_status_hyps.i +++ b/tests/misc/remove_status_hyps.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int main(void) { diff --git a/tests/misc/save_comments.i b/tests/misc/save_comments.i index aaf7cccdef62fdaaaea56d6e6b5160163941eea4..ac5457f42b150ed8257d0c54ade00ef09cff02b8 100644 --- a/tests/misc/save_comments.i +++ b/tests/misc/save_comments.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -keep-comments + CMXS: @PTEST_NAME@ + OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -keep-comments */ int f() { diff --git a/tests/misc/static.i b/tests/misc/static.i index b0863c3a2b3908f34f1bfe07919867975270aa3c..bf9737025ee13ae2229622e316fbeea666ba8b80 100644 --- a/tests/misc/static.i +++ b/tests/misc/static.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int x; diff --git a/tests/misc/test_datatype.i b/tests/misc/test_datatype.i index 19405eb11ec4c3d5e608f535e9aeab5f595fb19a..2de60116213af5a0dd353f174e487b98fe406393 100644 --- a/tests/misc/test_datatype.i +++ b/tests/misc/test_datatype.i @@ -1,4 +1,4 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ diff --git a/tests/misc/version.i b/tests/misc/version.i index 3a762af550b5fb818f962ec7d88d225747f95e50..55b838eefadabd84facd4ca185eb0398948f6111 100644 --- a/tests/misc/version.i +++ b/tests/misc/version.i @@ -1,4 +1,4 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ diff --git a/tests/misc/vis_queueInstr.i b/tests/misc/vis_queueInstr.i index 61fd2bb820de4616e9e18edfc2cd55a5eedd711b..1524969c741304d0bf5568738eb99ca292df6f4d 100644 --- a/tests/misc/vis_queueInstr.i +++ b/tests/misc/vis_queueInstr.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print -then-on A -print +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print -then-on A -print */ int main(){ diff --git a/tests/misc/vis_spec.i b/tests/misc/vis_spec.i index c40858396b4be923663a262dc97a0cdc4b187771..bd51666e94768e4cee525250f7fe6d9c029c2dc3 100644 --- a/tests/misc/vis_spec.i +++ b/tests/misc/vis_spec.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ //@ assigns \nothing; diff --git a/tests/misc/visitor_creates_func_bts_1349.i b/tests/misc/visitor_creates_func_bts_1349.i index a03c0cd1c45050418effd185243b6dff7a1f7e3e..1ff0a2ebac6d4ac428523cbbc0a34d54634b3d6d 100644 --- a/tests/misc/visitor_creates_func_bts_1349.i +++ b/tests/misc/visitor_creates_func_bts_1349.i @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -then-on test -print */ diff --git a/tests/misc/well_typed_alarm.i b/tests/misc/well_typed_alarm.i index 236200877af3a87006d77bafa01de09eef090645..83a2141b638650c074b49f471873cffda7327918 100644 --- a/tests/misc/well_typed_alarm.i +++ b/tests/misc/well_typed_alarm.i @@ -1,6 +1,6 @@ /* run.config* -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -load-module %{dep:@PTEST_NAME@.cmxs} */ int main(int c) { int x = 0; diff --git a/tests/misc/wstring_phase6.c b/tests/misc/wstring_phase6.c index 82b35af07aafd25c3b780feed53159d006ff34a7..f56786327811937280f9850407e80cf891e625f5 100644 --- a/tests/misc/wstring_phase6.c +++ b/tests/misc/wstring_phase6.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -journal-disable -print -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -variadic-no-translation + CMXS: @PTEST_NAME@ + OPT: -journal-disable -print -load-module %{dep:@PTEST_NAME@.cmxs} -variadic-no-translation */ #include <stdio.h> diff --git a/tests/pdg/dyn_dpds.c b/tests/pdg/dyn_dpds.c index 8c40c94f19d036b5c74abead1be0f9f33f9b4c93..ab01c06618846aebb79cff92d208539fe6d4cc61 100644 --- a/tests/pdg/dyn_dpds.c +++ b/tests/pdg/dyn_dpds.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -deps" + CMXS: @PTEST_NAME@ + STDOPT: +"-load-module %{dep:@PTEST_NAME@.cmxs} -deps" */ diff --git a/tests/pdg/sets.c b/tests/pdg/sets.c index 7b8f05dda8ace56c924d35a30447621d1971e2ff..2c2b7a5a8b5f27a5be98916c9bcdc0b898e9caf0 100644 --- a/tests/pdg/sets.c +++ b/tests/pdg/sets.c @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@ -lib-entry -main f -pdg -inout " */ diff --git a/tests/rte/compute_annot/compute_annot.ml b/tests/rte/compute_annot.ml similarity index 100% rename from tests/rte/compute_annot/compute_annot.ml rename to tests/rte/compute_annot.ml diff --git a/tests/rte/my_annot_proxy/my_annot_proxy.ml b/tests/rte/my_annot_proxy.ml similarity index 100% rename from tests/rte/my_annot_proxy/my_annot_proxy.ml rename to tests/rte/my_annot_proxy.ml diff --git a/tests/rte/my_annotation/my_annotation.ml b/tests/rte/my_annotation.ml similarity index 100% rename from tests/rte/my_annotation/my_annotation.ml rename to tests/rte/my_annotation.ml diff --git a/tests/rte/precond2.c b/tests/rte/precond2.c index 72d360e0d96667335f976b60727fdeb9843b965c..82cdc9b21ade8e141c24a38e32ff2a0d1e1d3746 100644 --- a/tests/rte/precond2.c +++ b/tests/rte/precond2.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/compute_annot/compute_annot.cmxs - OPT: -warn-special-float none -load-module @PTEST_DIR@/compute_annot/compute_annot -journal-disable + CMXS: compute_annot + OPT: -warn-special-float none -load-module %{dep:compute_annot.cmxs} -journal-disable */ int global = 15; diff --git a/tests/rte/rte_api/rte_get_annot.ml b/tests/rte/rte_get_annot.ml similarity index 100% rename from tests/rte/rte_api/rte_get_annot.ml rename to tests/rte/rte_get_annot.ml diff --git a/tests/rte/threefunc.c b/tests/rte/threefunc.c index 03b2ad3b373fd5dcc26253574999f9bccfa59a30..ce939930c960b347f4c206d360b8f428319184c3 100644 --- a/tests/rte/threefunc.c +++ b/tests/rte/threefunc.c @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/my_annotation/my_annotation.cmxs -OPT: -load-module @PTEST_DIR@/my_annotation/my_annotation +CMXS: my_annotation +OPT: -load-module %{dep:my_annotation.cmxs} */ diff --git a/tests/rte/twofunc.c b/tests/rte/twofunc.c index 2732ad9f1f99b79c79b2f9450870d3904a69cd71..92cce68a7e912db26250caf5284e86a35a322b72 100644 --- a/tests/rte/twofunc.c +++ b/tests/rte/twofunc.c @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/my_annot_proxy/my_annot_proxy.cmxs -OPT: -load-module @PTEST_DIR@/my_annot_proxy/my_annot_proxy +CMXS: my_annot_proxy +OPT: -load-module %{dep:my_annot_proxy.cmxs} */ diff --git a/tests/rte/twofunc3.c b/tests/rte/twofunc3.c index fab3e66a5abf45ebcf5d3ea1c88983614b468ef6..dd0b7781dcc65212a9867b12e60b94ac36bdcb54 100644 --- a/tests/rte/twofunc3.c +++ b/tests/rte/twofunc3.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/rte_api/rte_get_annot.cmxs - OPT: -rte-select @@all -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable + CMXS: rte_get_annot + OPT: -rte-select @@all -load-module %{dep:rte_get_annot} -journal-disable */ diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i index 1f733301b5c7942857df1515ef02528852f4a8bf..c7727a46ac28ac41d667fa0f3c7b90b5cc6ce12c 100644 --- a/tests/saveload/basic.i +++ b/tests/saveload/basic.i @@ -1,12 +1,12 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err + CMXS: @PTEST_NAME@ + EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} -eva @EVA_OPTIONS@ -out -input -deps ./@PTEST_DIR@/@PTEST_NAME@.i -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav ./bin/toplevel.opt -save ./tests/saveload/result/basic.1.sav @PTEST_DIR@/@PTEST_NAME@.i -eva @EVA_OPTIONS@ -out -input -deps > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err STDOPT: +"-load ./tests/saveload/result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable" - CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable -print" STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -journal-disable" - EXECNOW: make -s @PTEST_DIR@/status.cmxs + CMXS: status EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -load-module @PTEST_DIR@/status -save ./tests/saveload/result/status.sav @PTEST_DIR@/@PTEST_NAME@.i > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err STDOPT: +"-load-module @PTEST_DIR@/status -load ./tests/saveload/result/status.sav" STDOPT: +"-load ./tests/saveload/result/status.sav" diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i index ee704399b403bbf61ee9da3eab241d193b7a9426..6fdbbc5db272ba81019acb9c14a28d7ee1cc2c4f 100644 --- a/tests/saveload/deps.i +++ b/tests/saveload/deps.i @@ -1,6 +1,6 @@ /* run.config EXECNOW: make -s ./tests/saveload/deps_A.cmxs ./tests/saveload/deps_B.cmxs ./tests/saveload/deps_C.cmxs ./tests/saveload/deps_D.cmxs ./tests/saveload/deps_E.cmxs - EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module ./tests/saveload/deps_A.cmxs -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/deps.i -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err + EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -load-module %{dep:deps_A.cmxs} -eva @EVA_OPTIONS@ -out -input -deps ./tests/saveload/deps.i -save ./tests/saveload/result/deps.sav > ./tests/saveload/result/deps_sav.res 2> ./tests/saveload/result/deps_sav.err STDOPT: +"-load-module ./tests/saveload/deps_A -load ./tests/saveload/result/deps.sav -eva @EVA_OPTIONS@ -out -input -deps " STDOPT: +"-load-module ./tests/saveload/deps_B -load ./tests/saveload/result/deps.sav -out -input -deps " STDOPT: +"-load-module ./tests/saveload/deps_C -load ./tests/saveload/result/deps.sav -out -input -deps " diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i index 75dde3f72926e6957c0fdfb898dbd3c3ba37932d..808418270f62f5e06476eb9e50fd35f20863a238 100644 --- a/tests/saveload/load_one.i +++ b/tests/saveload/load_one.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - STDOPT: +"-load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" + CMXS: @PTEST_NAME@ + STDOPT: +"-load-module %{dep:@PTEST_NAME@.cmxs}" */ int G; diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i index ab0d9a44fd15de6c80394627618705578bd54744..101d6b9ef988ad582314cfb319db84fa879bf08d 100644 --- a/tests/saveload/multi_project.i +++ b/tests/saveload/multi_project.i @@ -1,8 +1,8 @@ /* run.config EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err ./bin/toplevel.opt -save ./tests/saveload/result/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > tests/saveload/result/multi_project_sav.res 2> tests/saveload/result/multi_project_sav.err - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ STDOPT: +"-load ./tests/saveload/result/multi_project.sav -journal-disable" - CMD: @frama-c@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs} OPT: -eva @EVA_OPTIONS@ */ int f(int x) { diff --git a/tests/saveload/serialized_queue.i b/tests/saveload/serialized_queue.i index 3d2c450536e513b1580c0197708c6f78599e4c31..b5673fd361bc96910c8c1d8a06d2d5cbbb57fe67 100644 --- a/tests/saveload/serialized_queue.i +++ b/tests/saveload/serialized_queue.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ // empty C file, we're only interested in the script itself diff --git a/tests/scope/bts971.c b/tests/scope/bts971.c index b50076a1a38082a0c1f3d15ae9b1cfa66e8fa6e0..dc7a4da3197a34fc43dba11dc47c1760238226aa 100644 --- a/tests/scope/bts971.c +++ b/tests/scope/bts971.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -journal-disable -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then -main main2 + CMXS: @PTEST_NAME@ + OPT: -journal-disable -load-module %{dep:@PTEST_NAME@.cmxs} -then -main main2 */ /* bug 971: */ volatile foo; diff --git a/tests/scope/zones.c b/tests/scope/zones.c index acafbd74299ae375c471c6e8fd9274ea62343f4a..2022615414c8a2c11dd2a875a770b96903a59c0f 100644 --- a/tests/scope/zones.c +++ b/tests/scope/zones.c @@ -1,5 +1,5 @@ /* run.config -# EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs +# CMXS: @PTEST_NAME@ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@ -eva @EVA_OPTIONS@ -journal-disable */ diff --git a/tests/slicing/adpcm.c b/tests/slicing/adpcm.c index 559291e8913aa6ed077a415db585d843f46c7667..83dedf9a0f09d66956e102db0d21fa850668f0b6 100644 --- a/tests/slicing/adpcm.c +++ b/tests/slicing/adpcm.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - STDOPT: +"-load-module ./tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -ulevel -1 -deps -slicing-level 2 -journal-disable" + DEPS: ../test/adpcm.c + STDOPT: +"-add-symbolic-path TESTS_DIR:../.. -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} -ulevel -1 -deps -slicing-level 2 -journal-disable" */ -#include "tests/test/adpcm.c" +#include "../../test/adpcm.c" diff --git a/tests/slicing/annot.i b/tests/slicing/annot.i index ae8621780d40f807eb8b8cc6373613b8447a8576..91b2a0a4d4f630fbac311d5bfce03fda3364d1a7 100644 --- a/tests/slicing/annot.i +++ b/tests/slicing/annot.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-main f1 -slice-assert f1 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-main f2 -slice-assert f2 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-main f1 -slice-assert f1 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-main f2 -slice-assert f2 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " */ extern int x, z; diff --git a/tests/slicing/bts0184.i b/tests/slicing/bts0184.i index f4e31d0e286fea142d40fc5b737aa7ae3b40c90e..e99ea6ac66183c3efeae21035e48b66e65d8d8a7 100644 --- a/tests/slicing/bts0184.i +++ b/tests/slicing/bts0184.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-pragma x -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-pragma x -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " **/ int x(int y, int z) { diff --git a/tests/slicing/bts0190.i b/tests/slicing/bts0190.i index 1cec1079cde8eddfbcd5ab3d7e4c261c2769f12e..efdbb88eb418326f521ceec7efdad7724df76434 100644 --- a/tests/slicing/bts0190.i +++ b/tests/slicing/bts0190.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-slicing-warn-key cmdline=active -check -slice-rd y -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " +STDOPT: +"-slicing-warn-key cmdline=active -check -slice-rd y -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " */ int z1(void); diff --git a/tests/slicing/bts0950_annot.i b/tests/slicing/bts0950_annot.i index 5b0af4a955d6b575a63b83c2590a36d021ee5b9a..8c6e58eee6f9901fa99b283bab9c87c646343549 100644 --- a/tests/slicing/bts0950_annot.i +++ b/tests/slicing/bts0950_annot.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-eva -slice-value a -then-on 'Slicing export' -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-eva -slice-value a -then-on 'Slicing export' -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" */ /*@ requires \valid(dest); */ extern void cpy(int *dest, const int *src); diff --git a/tests/slicing/bts1248.i b/tests/slicing/bts1248.i index b1b634ca8b90581cab435b19a4985a04d5f3de88..73099ffb4debb9bcc3e14a80d8ef5ca6b74917a2 100644 --- a/tests/slicing/bts1248.i +++ b/tests/slicing/bts1248.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-slice-rd x -main f -slicing-project-name p -then-on 'p export' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" +STDOPT: +"-slice-rd x -main f -slicing-project-name p -then-on 'p export' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" */ int f(void) { diff --git a/tests/slicing/bts1445.i b/tests/slicing/bts1445.i index 90953815c397ad6768933e3a4fe6e926892d2143..370c3e0f7847fef75a875f802af5c876b4a835a1 100644 --- a/tests/slicing/bts1445.i +++ b/tests/slicing/bts1445.i @@ -1,6 +1,6 @@ /* run.config -STDOPT: +"-slice-calls main -then-on 'Slicing export' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" -STDOPT: +"-slice-calls f -main f -then-on 'Slicing export' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" +STDOPT: +"-slice-calls main -then-on 'Slicing export' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" +STDOPT: +"-slice-calls f -main f -then-on 'Slicing export' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" */ int x = 0; diff --git a/tests/slicing/bts1684.i b/tests/slicing/bts1684.i index de3db5c51eff1ea3843b2a110e1ef860e5898788..75f95e0c4ea31ba3274ff65fa9fddd7c4032dc79 100644 --- a/tests/slicing/bts1684.i +++ b/tests/slicing/bts1684.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-calls main -journal-enable -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" + STDOPT: +"-slice-calls main -journal-enable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" */ // one bug about JOURNALIZATION and another one about slicing CALLS TO MAIN function. double d1, d2, d3; diff --git a/tests/slicing/bts1768.i b/tests/slicing/bts1768.i index 4f8d7725029efb6a79923752a60d6aa412e7e2f1..4bf2e1c93f0100ea0f64789d6aa4007f1159ff04 100644 --- a/tests/slicing/bts1768.i +++ b/tests/slicing/bts1768.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-main main -slice-pragma main -ulevel 10 -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" + STDOPT: +"-main main -slice-pragma main -ulevel 10 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" */ int choix ; int state = 1; diff --git a/tests/slicing/bts179.i b/tests/slicing/bts179.i index f3c27eeb3d4a59acfa6be2bc18b709c8da80530b..41f9b772654fd54d921101e5ac8ffffbb3e92888 100644 --- a/tests/slicing/bts179.i +++ b/tests/slicing/bts179.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-slice-return main -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" - STDOPT: +"-slice-pragma main -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" + STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" + STDOPT: +"-slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" STDOPT: +"-sparecode-analysis -journal-disable" */ diff --git a/tests/slicing/bts283.i b/tests/slicing/bts283.i index 95c10baf058b9ef65528a343d11dd3a5006a8a29..e953143a97d5e54e24423fd396d3ab2fce7ca489 100644 --- a/tests/slicing/bts283.i +++ b/tests/slicing/bts283.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-return main -slice-undef-functions -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" + STDOPT: +"-slice-return main -slice-undef-functions -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" */ int x,y,z; diff --git a/tests/slicing/bts326.i b/tests/slicing/bts326.i index 48f60d41072374c23556b017c0609cba491b0d5f..c641c24aeac99d740fc19ec84ef984b83488b1a9 100644 --- a/tests/slicing/bts326.i +++ b/tests/slicing/bts326.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-calldeps -slice-return main -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-calldeps" + STDOPT: +"-calldeps -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" */ /* Problem : f(1) should be sliced out. See BTS#326 */ int t[2] ; diff --git a/tests/slicing/bts335.i b/tests/slicing/bts335.i index 11ca698199d18bd2ce253c7d6f7c249773c6d1e0..7ae7cc4df95ee28baf2a57e26d9c7a1af7bc5e5b 100644 --- a/tests/slicing/bts335.i +++ b/tests/slicing/bts335.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-pragma g -calldeps -slicing-level 3 -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-calldeps" + STDOPT: +"-slice-pragma g -calldeps -slicing-level 3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" */ /* diff --git a/tests/slicing/bts335b.i b/tests/slicing/bts335b.i index d63ae4eea19a27e9d3b5c9e29135bc4c271571a3..754c50804cf248a263d3212cf9d27ad76100c3a6 100644 --- a/tests/slicing/bts335b.i +++ b/tests/slicing/bts335b.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-return main -calldeps -slicing-level 3 -slicing-verbose 2 -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-calldeps" + STDOPT: +"-slice-return main -calldeps -slicing-level 3 -slicing-verbose 2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" */ int X, Y; diff --git a/tests/slicing/bts336.i b/tests/slicing/bts336.i index ddeee83be06b686bfe260bd8d0ee16cf9d59d907..6ab18521c8894d102cf1995de88f819d29d56b88 100644 --- a/tests/slicing/bts336.i +++ b/tests/slicing/bts336.i @@ -1,12 +1,12 @@ /* run.config - STDOPT: +"-slice-return main -calldeps -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-calldeps" - STDOPT: +"-main main2 -slice-return main2 -calldeps -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-calldeps" - STDOPT: +"-main main3 -slice-return main3 -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-calldeps" - STDOPT: +"-journal-disable -main main3 -inout -calldeps -slice-return main3 -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-calldeps -no-inout" - STDOPT: +"-journal-disable -main main -calldeps -slice-return main -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-calldeps" - STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -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-calldeps" - STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -slicing-level 3 -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-calldeps" - STDOPT: +"-journal-disable -main main5 -calldeps -slice-return main5 -then-on 'Slicing export' -set-project-as-default -print @EVA_OPTIONS@ -calldeps -slice-return main5 -then-on 'Slicing export 2' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-slice-return main -calldeps -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-main main2 -slice-return main2 -calldeps -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-main main3 -slice-return main3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-journal-disable -main main3 -inout -calldeps -slice-return main3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps -no-inout" + STDOPT: +"-journal-disable -main main -calldeps -slice-return main -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-journal-disable -main main4 -calldeps -slice-return main4 -slicing-level 3 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-journal-disable -main main5 -calldeps -slice-return main5 -then-on 'Slicing export' -set-project-as-default -print @EVA_OPTIONS@ -calldeps -slice-return main5 -then-on 'Slicing export 2' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" */ // something to do to have better results... int T[10]; diff --git a/tests/slicing/bts341.i b/tests/slicing/bts341.i index af5b43d5a31e603a48a6f80e08274a36ab795d04..92450bfff6effcd0ff5baf8434539cd535dda46e 100644 --- a/tests/slicing/bts341.i +++ b/tests/slicing/bts341.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" */ int main (int c) { if (c) diff --git a/tests/slicing/bts344.i b/tests/slicing/bts344.i index a560db415505a8f644ce713676aac0a0c462c019..11504503748407adf3e1e8275ac8a36563322164 100644 --- a/tests/slicing/bts344.i +++ b/tests/slicing/bts344.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-slice-return main -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-return main_bis -main main_bis -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-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-slice-return main_bis -main main_bis -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ int X, Y ; diff --git a/tests/slicing/bts345.i b/tests/slicing/bts345.i index 76db76d7b5fe2958408d2450c5359dbfcab0a005..4c760875a7c40538ffdc592aa8af967853d46d9e 100644 --- a/tests/slicing/bts345.i +++ b/tests/slicing/bts345.i @@ -1,9 +1,9 @@ /* run.config - STDOPT: +"-slice-return call_top -main call_top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return top -main top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return top -main call_top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return called_by_top -main top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return called_by_top -main call_top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return call_top -main call_top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return top -main top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return top -main call_top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return called_by_top -main top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return called_by_top -main call_top -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " */ int called_indirectly_by_top (int x) { diff --git a/tests/slicing/bts679.i b/tests/slicing/bts679.i index 902dd771327daeb279238eb309f36141c0340ff4..47e1be42aafff8ca944c6821c02be8e4af97cb33 100644 --- a/tests/slicing/bts679.i +++ b/tests/slicing/bts679.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-slice-return main -then-on 'Slicing export' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" +STDOPT: +"-slice-return main -then-on 'Slicing export' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" */ void f(void) { return; } int X = 1 ; diff --git a/tests/slicing/bts679b.i b/tests/slicing/bts679b.i index 2e350641583eff884e288450f2d1e95588e5f179..0470c9d695db6df4d31313c8e61268a22b191789 100644 --- a/tests/slicing/bts679b.i +++ b/tests/slicing/bts679b.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-slice-assert main -then-on 'Slicing export' -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-assert main -then-on 'Slicing export' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ int X = 1 ; diff --git a/tests/slicing/bts709.c b/tests/slicing/bts709.c index 325e6ba28661753469776de28c3d337255b0523f..bc988abefd5232cb55da6f7ea6d5d81fba1887fb 100644 --- a/tests/slicing/bts709.c +++ b/tests/slicing/bts709.c @@ -1,5 +1,5 @@ /* run.config - 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" + STDOPT: +"-slice-pragma func -no-unicode -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ #include <assert.h> diff --git a/tests/slicing/bts808.i b/tests/slicing/bts808.i index 74fb4cf1e22df2e29a2c09e76e00df0b8e415c98..56b54309c4e0c57bf17048077e6e2cdd7692bfb6 100644 --- a/tests/slicing/bts808.i +++ b/tests/slicing/bts808.i @@ -1,5 +1,5 @@ /* run.config -* STDOPT: +"-slice-return main -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 " +* STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ int f0 (void) { diff --git a/tests/slicing/bts827.i b/tests/slicing/bts827.i index cd0ec9d931f304471ebc5ae220897ba7e9b98ea8..c7771c763b26a8709084dc1b8f7463be943459e6 100644 --- a/tests/slicing/bts827.i +++ b/tests/slicing/bts827.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-return main -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-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ /* The problem was a mix-up between f outputs and retrun value. */ diff --git a/tests/slicing/call_accuracy.i b/tests/slicing/call_accuracy.i index cecb3ba3a5eba24681d18f6e50cbec16dabdbeb9..70bbd692070175e00dd3cba95d1914399b8f67d4 100644 --- a/tests/slicing/call_accuracy.i +++ b/tests/slicing/call_accuracy.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-calldeps -slice-return main -slicing-level 3 -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-calldeps" + STDOPT: +"-calldeps -slice-return main -slicing-level 3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" */ int f_cond (int c, int a, int b) { ++a; diff --git a/tests/slicing/call_demo.i b/tests/slicing/call_demo.i index b391349193dbe7e581939966ba604e6d12d8ee99..8625aa042a4fd92303666cc0334ad00df5fca61f 100644 --- a/tests/slicing/call_demo.i +++ b/tests/slicing/call_demo.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-slice-calls call1 -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-calls call2 -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-calls call1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-slice-calls call2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ //@ assigns \result \from v; diff --git a/tests/slicing/callwise.i b/tests/slicing/callwise.i index 35c6b5f9f2208a1fab0da9eb44fa00e9d60e966e..8adce92f62879436a271a24a06898664a0e7eb14 100644 --- a/tests/slicing/callwise.i +++ b/tests/slicing/callwise.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-calldeps -slice-return main -slicing-level 2 -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-calldeps" + STDOPT: +"-calldeps -slice-return main -slicing-level 2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" */ int a = 1, b = 1, c = 1, d = 1, *p; diff --git a/tests/slicing/combine.i b/tests/slicing/combine.i index df980abab596c1ed34198d2c0a314bf7166c5f91..1a02c107dcd4f8de2d22e9072b2db17e2a85c614 100644 --- a/tests/slicing/combine.i +++ b/tests/slicing/combine.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -journal-disable */ diff --git a/tests/slicing/csmith.i b/tests/slicing/csmith.i index 822f71d984f2fe0141487ebb3f4ea06f85c81151..d5eb265eddd1b4c9540c21fa7dc06cbf73c69b3e 100644 --- a/tests/slicing/csmith.i +++ b/tests/slicing/csmith.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-return main -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 " + STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " COMMENT: STDOPT: +"-main bts906b -fct-pdg bts906b -pdg-print -pdg-verbose 2" STDOPT: +"-main bts906c -fct-pdg bts906c -pdg-print -pdg-verbose 2" diff --git a/tests/slicing/dune b/tests/slicing/dune new file mode 100644 index 0000000000000000000000000000000000000000..3d73324fe84dfd1d67a72d6722a34c06cf5bfb69 --- /dev/null +++ b/tests/slicing/dune @@ -0,0 +1,21 @@ +(library + (name libSelect) + (modules libSelect) + (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core) + (flags -open Frama_c_kernel) +) + +(library + (name libAnim) + (modules libAnim) + (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core) + (flags -open Frama_c_kernel) +) + +(executables + (names merge adpcm ex_spec_interproc combine horwitz mark_all_slices min_call select_by_annot select_simple simple_intra_slice slice_no_body switch) + (modes plugin) + (modules merge adpcm ex_spec_interproc combine horwitz mark_all_slices min_call select_by_annot select_simple simple_intra_slice slice_no_body switch) + (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core libSelect libAnim) + (flags -open Frama_c_kernel) +) diff --git a/tests/slicing/ex_spec_interproc.i b/tests/slicing/ex_spec_interproc.i index 57bc27bc9ff4f32a1bf28d68be996bca9e4ac8c4..38c8a95b01dc86eaaef470cf7cc60ab25fd05414 100644 --- a/tests/slicing/ex_spec_interproc.i +++ b/tests/slicing/ex_spec_interproc.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -journal-disable */ diff --git a/tests/slicing/filter.i b/tests/slicing/filter.i index 6c100e071154a75119c61db99cb0a4599a5fc489..f3a5d439e54b0ba3bc80659d552455c619c06b47 100644 --- a/tests/slicing/filter.i +++ b/tests/slicing/filter.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-return main -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 " + STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " **/ /* TESTS: this is about [filter] optimisations since sometimes, * slicing results are ok, but the generated new project is not correct. */ diff --git a/tests/slicing/forall_loop_invariant.i b/tests/slicing/forall_loop_invariant.i index a959f703b524493cfa0d4c1560c65ed5cc7c7bd7..51f312e3103fddec40b3bb53e7601283a5d3ef62 100644 --- a/tests/slicing/forall_loop_invariant.i +++ b/tests/slicing/forall_loop_invariant.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-assert main -then-on 'Slicing export' -print -then-on default -slice-value t -then-on 'Slicing export 2' -print -check -set-project-as-default -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-slice-assert main -then-on 'Slicing export' -print -then-on default -slice-value t -then-on 'Slicing export 2' -print -check -set-project-as-default -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" **/ diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i index d12de9261ad6bc3aeafd7a22b559eb3ecb9ade0e..10ec91fffb8670454383458ce29fa09b35706f22 100644 --- a/tests/slicing/horwitz.i +++ b/tests/slicing/horwitz.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -slicing-level 0 -journal-disable */ diff --git a/tests/slicing/if_many_values.i b/tests/slicing/if_many_values.i index 11bf03bc16c2907a4eb2eb466a28e8bac5de15d6..80f9ae39b6cc5dcc3803c1e308ebff6f58aeaa53 100644 --- a/tests/slicing/if_many_values.i +++ b/tests/slicing/if_many_values.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-value r -journal-disable -slevel 101 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-slice-value r -journal-disable -slevel 101 -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" **/ int r=1; diff --git a/tests/slicing/initialized.i b/tests/slicing/initialized.i index f1f2fd51e921bd12e3bfe8d221d839c726b24001..78d1d618afad9b325db02888ca1dd240d0fdd4a1 100644 --- a/tests/slicing/initialized.i +++ b/tests/slicing/initialized.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-assert main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-assert main -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " **/ void main() { diff --git a/tests/slicing/keep_annot.i b/tests/slicing/keep_annot.i index ae570853dfd277f7d4d21ce5cd9431a8ffa98a79..9f7ae5a7fa6d5f0ab6cabf244de498c5e5e71992 100644 --- a/tests/slicing/keep_annot.i +++ b/tests/slicing/keep_annot.i @@ -1,9 +1,9 @@ /* run.config - STDOPT: +"-context-valid-pointers -lib-entry -main f -slice-assert f -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: +"-context-valid-pointers -lib-entry -main f -slice-assert f -slicing-keep-annotations -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: +"-context-valid-pointers -lib-entry -main L -slice-pragma L -slicing-keep-annotations -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: +"-context-valid-pointers -lib-entry -main L -slice-pragma L -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-return bts1110 -main bts1110 -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: +"-context-valid-pointers -lib-entry -main f -slice-assert f -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-context-valid-pointers -lib-entry -main f -slice-assert f -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-context-valid-pointers -lib-entry -main L -slice-pragma L -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-context-valid-pointers -lib-entry -main L -slice-pragma L -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-slice-return bts1110 -main bts1110 -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ diff --git a/tests/slicing/loop_infinite.i b/tests/slicing/loop_infinite.i index 5b3b69abc0755098050aaf3257ff1693be2b1be7..c2132150eb21d79e788560913a4fc57e1dfcd26d 100644 --- a/tests/slicing/loop_infinite.i +++ b/tests/slicing/loop_infinite.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-deps -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" */ int main() { volatile int a=0,b,c; diff --git a/tests/slicing/loop_simple.i b/tests/slicing/loop_simple.i index 210466de5c7b3476236e23f62dfeb5932306b5cf..4c7e4a5047c4ec80afcfcf23b500fab6fcc9b715 100644 --- a/tests/slicing/loop_simple.i +++ b/tests/slicing/loop_simple.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-deps -slice-return main -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: +"-deps -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ int main() { int a,c; volatile int b = 0; diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i index 2c87381695469c4e081392e9abba0f876c44a2b8..f31a03c877e42912c5b3aac66fa928ed8e331edf 100644 --- a/tests/slicing/loops.i +++ b/tests/slicing/loops.i @@ -1,29 +1,29 @@ /* run.config - STDOPT: +"-deps -lib-entry -main f1 -slice-pragma f1 -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: +"-deps -lib-entry -main f1 -slice-assert f1 -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: +"-deps -lib-entry -main f2 -slice-pragma f2 -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: +"-deps -lib-entry -main f2 -slice-assert f2 -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: +"-deps -main test_infinite_loop_3 -slice-value G -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: +"-deps -main test_infinite_loop_4 -slice-value G -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: +"-deps -main test_infinite_loop_5 -slice-value G -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: +"-deps -main loop -slice-value Z -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: +"-deps -slice-calls loop -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: +"-deps -slice-pragma loop -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: +"-deps -slice-assert loop -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: +"-deps -main loop -slice-rd Y -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: +"-deps -main loop -slice-rd Z -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: +"-deps -main loop -slice-wr Y -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: +"-deps -main loop -slice-wr Z -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: +"-deps -lib-entry -main stop_f1 -slice-pragma stop_f1 -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: +"-deps -lib-entry -main stop_f1 -slice-assert stop_f1 -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: +"-deps -lib-entry -main stop_f2 -slice-pragma stop_f2 -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: +"-deps -lib-entry -main stop_f2 -slice-assert stop_f2 -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: +"-deps -slice-value Z -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: +"-deps -slice-rd Y -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: +"-deps -slice-rd Z -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: +"-deps -slice-wr Y -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: +"-deps -slice-wr Z -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: +"-deps -lib-entry -main alarm -slice-threat alarm -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: +"-deps -lib-entry -main f1 -slice-pragma f1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main f1 -slice-assert f1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main f2 -slice-pragma f2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main f2 -slice-assert f2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main test_infinite_loop_3 -slice-value G -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main test_infinite_loop_4 -slice-value G -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main test_infinite_loop_5 -slice-value G -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main loop -slice-value Z -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-calls loop -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-pragma loop -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-assert loop -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main loop -slice-rd Y -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main loop -slice-rd Z -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main loop -slice-wr Y -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -main loop -slice-wr Z -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main stop_f1 -slice-pragma stop_f1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main stop_f1 -slice-assert stop_f1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main stop_f2 -slice-pragma stop_f2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main stop_f2 -slice-assert stop_f2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-value Z -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-rd Y -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-rd Z -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-wr Y -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -slice-wr Z -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" + STDOPT: +"-deps -lib-entry -main alarm -slice-threat alarm -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-deps" */ diff --git a/tests/slicing/mark_all_slices.i b/tests/slicing/mark_all_slices.i index d3008f37ba96e674dd9947b0e430a3aaf3faea41..fd186b11a78f45ee2af6f9b49ebc86158c5f1053 100644 --- a/tests/slicing/mark_all_slices.i +++ b/tests/slicing/mark_all_slices.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -no-slice-callers -journal-disable */ int A, B, C, D; diff --git a/tests/slicing/merge.i b/tests/slicing/merge.i index b255a2c2fe73a442d5b5f2d56918a257aa820c91..690517f142835685c921472c0d9eb7813db77fa1 100644 --- a/tests/slicing/merge.i +++ b/tests/slicing/merge.i @@ -1,6 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module tests/slicing/libAnim.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:libAnim.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -slicing-level 3 -journal-disable */ diff --git a/tests/slicing/min_call.i b/tests/slicing/min_call.i index a06325b8a588960a7b3d3c0978a35b97bf7fd4d8..f3ec11a3a16e701418e5e357b55a047b655b1445 100644 --- a/tests/slicing/min_call.i +++ b/tests/slicing/min_call.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -lib-entry -main g -journal-disable -slicing-level 3 */ diff --git a/tests/slicing/ptr_fct.i b/tests/slicing/ptr_fct.i index c972063ed05fbbcd0b6374104b6d54a49ffeba24..7f66b63cb0553a915ead2726361232605809ea5e 100644 --- a/tests/slicing/ptr_fct.i +++ b/tests/slicing/ptr_fct.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-main h -slice-return h -slicing-level 1 -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 " + STDOPT: +"-main h -slice-return h -slicing-level 1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ int X ; diff --git a/tests/slicing/same_sliced_name_bts1422.i b/tests/slicing/same_sliced_name_bts1422.i index e16a0f6bf0bfabbd83fd7c1fbe519c572c4e8d68..cf8010808ff5ba66caee83bd0d9fd818c67d9d66 100644 --- a/tests/slicing/same_sliced_name_bts1422.i +++ b/tests/slicing/same_sliced_name_bts1422.i @@ -1,5 +1,5 @@ /* run.config -STDOPT: +"-main foo -slice-value y -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " +STDOPT: +"-main foo -slice-value y -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " */ int y; diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i index b7411c47212a70801cbf4c81efff1831369cccd7..06069b98128d2bd399460b9c2f4b27f197792352 100644 --- a/tests/slicing/select_by_annot.i +++ b/tests/slicing/select_by_annot.i @@ -1,22 +1,22 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -lib-entry -main main -journal-disable CMD: bin/toplevel.opt - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps - OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma modifS -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f4 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f5 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f6 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f7 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-loop-inv f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-assert f8 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps + OPT: @EVA_OPTIONS@ -check -deps -lib-entry -main main -slice-pragma f9 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps */ diff --git a/tests/slicing/select_calls.i b/tests/slicing/select_calls.i index 3377326ccb50246fe19de789f1ca0c078ea81eff..6341edc62e580a88c01e2fb13f5d70f089e43c15 100644 --- a/tests/slicing/select_calls.i +++ b/tests/slicing/select_calls.i @@ -1,6 +1,6 @@ /* run.config - STDOPT: +"-lib-entry -main f -slice-calls send -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 " - STDOPT: +"-lib-entry -main g -slice-calls nothing -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 " + STDOPT: +"-lib-entry -main f -slice-calls send -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-lib-entry -main g -slice-calls nothing -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ void nothing (void); diff --git a/tests/slicing/select_return.i b/tests/slicing/select_return.i index f2455c4f86e04b184a52d0a7408c9f6f5d1f1e38..2c0afa470c3c14d4371a6dc7d61fe9a3f542963a 100644 --- a/tests/slicing/select_return.i +++ b/tests/slicing/select_return.i @@ -1,26 +1,26 @@ /* run.config - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " - STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-return f -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-pragma f -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " + STDOPT: +"-slice-value H -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " */ int G,H,I; diff --git a/tests/slicing/select_return_bis.i b/tests/slicing/select_return_bis.i index d156bfe29a6da127f4a819892677803a1b7ff7a0..98afb7cb2e33f9c388c8a87e3c8c9d99fb1bee0c 100644 --- a/tests/slicing/select_return_bis.i +++ b/tests/slicing/select_return_bis.i @@ -1,15 +1,15 @@ /* run.config - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" - STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 0 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" + STDOPT: +"-slice-calls send,send_bis -lib-entry -main g -slicing-level 3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" */ int G,H,I; diff --git a/tests/slicing/select_simple.i b/tests/slicing/select_simple.i index 28face32afaf3a7c8e2dbf76ff7cdbb1ca51221f..49583442f3af37fbf43bee0e50761d86d0af848b 100644 --- a/tests/slicing/select_simple.i +++ b/tests/slicing/select_simple.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -journal-disable */ diff --git a/tests/slicing/simple_intra_slice.i b/tests/slicing/simple_intra_slice.i index b4d995b86b2d258f30cc8ed55cc12dd5b303bfbb..085ceb13737735481d8631d042219b0df636f838 100644 --- a/tests/slicing/simple_intra_slice.i +++ b/tests/slicing/simple_intra_slice.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -no-slice-callers -journal-disable */ int Unknown; diff --git a/tests/slicing/sizeof.i b/tests/slicing/sizeof.i index 7595f180d7bf239a2a9f7ab201492c6a88849f80..889042a2c2ae5f36e3e5af08d7dad9b01ce1c35d 100644 --- a/tests/slicing/sizeof.i +++ b/tests/slicing/sizeof.i @@ -1,17 +1,17 @@ /* run.config - STDOPT: +"-deps -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOf_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOf_2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_pt1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_pt2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_pt3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_pt_deref_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_tab_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_pt_tab_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_pt_tab_2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-return SizeOfE_tab_acces_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" - STDOPT: +"-deps -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOf_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOf_2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_pt1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_pt2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_pt3 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_pt_deref_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_tab_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_pt_tab_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_pt_tab_2 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-return SizeOfE_tab_acces_1 -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" + STDOPT: +"-deps -slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-deps" */ struct St { int i, *p, tab[5] ; } st ; diff --git a/tests/slicing/slice_behavior.i b/tests/slicing/slice_behavior.i index f5d52985ed95aa8cc8226b68f7d236d27e5d3452..483afc376a85ce88cbf5a3f566684e994d0c5f82 100644 --- a/tests/slicing/slice_behavior.i +++ b/tests/slicing/slice_behavior.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-eva -slice-assert f -slicing-level 0 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-eva" + STDOPT: +"-eva -slice-assert f -slicing-level 0 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check -no-eva" */ /*@ requires a > 0; */ int f(int a) { diff --git a/tests/slicing/slice_no_body.i b/tests/slicing/slice_no_body.i index e2be30cc3c617fc32f374986687e8bfa8d4d8f79..75786a6ef323420c33889ded183e67ba650c21df 100644 --- a/tests/slicing/slice_no_body.i +++ b/tests/slicing/slice_no_body.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -lib-entry -main h -journal-disable */ diff --git a/tests/slicing/slice_pragma_stmt.i b/tests/slicing/slice_pragma_stmt.i index fee7a33722ddebefddbb2d453838a5861b03d7c8..5e106bbb276d8064728fe096ebd347fd4a8b309a 100644 --- a/tests/slicing/slice_pragma_stmt.i +++ b/tests/slicing/slice_pragma_stmt.i @@ -1,27 +1,27 @@ /* run.config STDOPT: +"-print -journal-disable" - STDOPT: +"-main nop1 -slice-pragma nop1 -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 " - STDOPT: +"-main nop2 -slice-pragma nop2 -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 " - STDOPT: +"-main nop3 -slice-pragma nop3 -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 " - STDOPT: +"-main nop4 -slice-pragma nop4 -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 " - STDOPT: +"-main nop5 -slice-pragma nop5 -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 " - STDOPT: +"-main nop6 -slice-pragma nop6 -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 " - STDOPT: +"-main nop7 -slice-pragma nop7 -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 " - STDOPT: +"-main nop8 -slice-pragma nop8 -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 " - STDOPT: +"-main double_effect1 -slice-pragma double_effect1 -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 " - STDOPT: +"-main double_effect2 -slice-pragma double_effect2 -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 " - STDOPT: +"-main double_effect3 -slice-pragma double_effect3 -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 " - STDOPT: +"-main double_effect4 -slice-pragma double_effect4 -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 " - STDOPT: +"-main double_effect5 -slice-pragma double_effect5 -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 " - STDOPT: +"-main test1 -slice-pragma test1 -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 " - STDOPT: +"-main test2 -slice-pragma test2 -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 " - STDOPT: +"-main test3 -slice-pragma test3 -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 " - STDOPT: +"-main test4 -slice-pragma test4 -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 " - STDOPT: +"-main test5 -slice-pragma test5 -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 " - STDOPT: +"-main test6 -slice-pragma test6 -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 " - STDOPT: +"-main test7 -slice-pragma test7 -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 " - STDOPT: +"-main test8 -slice-pragma test8 -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 " - STDOPT: +"-main test9 -slice-pragma test9 -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 " + STDOPT: +"-main nop1 -slice-pragma nop1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop2 -slice-pragma nop2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop3 -slice-pragma nop3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop4 -slice-pragma nop4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop5 -slice-pragma nop5 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop6 -slice-pragma nop6 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop7 -slice-pragma nop7 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main nop8 -slice-pragma nop8 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main double_effect1 -slice-pragma double_effect1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main double_effect2 -slice-pragma double_effect2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main double_effect3 -slice-pragma double_effect3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main double_effect4 -slice-pragma double_effect4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main double_effect5 -slice-pragma double_effect5 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test1 -slice-pragma test1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test2 -slice-pragma test2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test3 -slice-pragma test3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test4 -slice-pragma test4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test5 -slice-pragma test5 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test6 -slice-pragma test6 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test7 -slice-pragma test7 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test8 -slice-pragma test8 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-main test9 -slice-pragma test9 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ typedef int stmt, expr, slice; int x, y ; diff --git a/tests/slicing/switch.i b/tests/slicing/switch.i index 2d7bc906d95ae09e4116b73334ad37a405301b2d..7e0a12e0555514382e0b63d7bf7b27503e033c43 100644 --- a/tests/slicing/switch.i +++ b/tests/slicing/switch.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - CMD: @frama-c@ -load-module tests/slicing/libSelect.cmxs -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + + CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs} OPT: @EVA_OPTIONS@ -deps -journal-disable */ int main (char choix) { diff --git a/tests/slicing/top.i b/tests/slicing/top.i index 7dac65d4ec60080d9923253f50bcab5439029a02..429713426bf7b21345c9867cef76b04cadd3b4f1 100644 --- a/tests/slicing/top.i +++ b/tests/slicing/top.i @@ -1,7 +1,7 @@ /* run.config -* STDOPT: +"-eva-no-builtins-auto -check -slicing-level 0 -slice-return uncalled -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" -* STDOPT: +"-eva-no-builtins-auto -check -slicing-level 2 -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" -* STDOPT: +"-eva-no-builtins-auto -check -slicing-level 2 -slice-return strlen -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" +* STDOPT: +"-eva-no-builtins-auto -check -slicing-level 0 -slice-return uncalled -no-slice-callers -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" +* STDOPT: +"-eva-no-builtins-auto -check -slicing-level 2 -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" +* STDOPT: +"-eva-no-builtins-auto -check -slicing-level 2 -slice-return strlen -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check" * * * diff --git a/tests/slicing/top2.i b/tests/slicing/top2.i index b84b8b994252dcf043460f2d9419cc76ae247b60..12ea16e1f82c96fbf813778a56b7d0596e26b6b7 100644 --- a/tests/slicing/top2.i +++ b/tests/slicing/top2.i @@ -1,6 +1,6 @@ /* run.config -* STDOPT: +"-slicing-level 2 -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " -* STDOPT: +"-slicing-level 2 -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " +* STDOPT: +"-slicing-level 2 -slice-pragma main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " +* STDOPT: +"-slicing-level 2 -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -check -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -check " */ diff --git a/tests/slicing/undef-fun.i b/tests/slicing/undef-fun.i index 59ac0c5e6482e4d83b4491ebd8f042665080c043..c1db855c2c6004c5e049db4656fc593bc54ffdf3 100644 --- a/tests/slicing/undef-fun.i +++ b/tests/slicing/undef-fun.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-undef-functions -slice-return f -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 " + STDOPT: +"-slice-undef-functions -slice-return f -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " diff --git a/tests/slicing/unitialized.c b/tests/slicing/unitialized.c index ed41732199c096ccf6de91d770fbc71a187316ec..4eaae1c3cebd2b7c91e7b8f01538b05a995b4739 100644 --- a/tests/slicing/unitialized.c +++ b/tests/slicing/unitialized.c @@ -1,8 +1,8 @@ /* run.config - STDOPT: +"-slice-pragma g -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 " - STDOPT: +"-slice-assert g -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 " - STDOPT: +"-slice-assert main -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 " - STDOPT: +"-slice-return g -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 " + STDOPT: +"-slice-pragma g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-assert g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-assert main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-return g -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ #ifdef __FRAMAC__ //@ assigns \result \from \nothing; diff --git a/tests/slicing/unravel-flavors.i b/tests/slicing/unravel-flavors.i index 29815de861cc7622c718d4113c506235222aec6c..60ea46b19709b24fa2886c0340cf68b78dd4b481 100644 --- a/tests/slicing/unravel-flavors.i +++ b/tests/slicing/unravel-flavors.i @@ -1,8 +1,8 @@ /* run.config - STDOPT: +"-slice-undef-functions -slice-return send1 -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 " - STDOPT: +"-slice-undef-functions -slice-return send2 -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 " - STDOPT: +"-slice-undef-functions -slice-return send3 -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 " - STDOPT: +"-slice-undef-functions -slice-return send4 -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 " + STDOPT: +"-slice-undef-functions -slice-return send1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-undef-functions -slice-return send2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-undef-functions -slice-return send3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-undef-functions -slice-return send4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ /* Small example derived from examples given for UNRAVEL tool : */ diff --git a/tests/slicing/unravel-point.i b/tests/slicing/unravel-point.i index dc07a8049c2ceb736ad00d0ea289b81c8a5393e6..abbde13b45218f1b055fec14d17b98d201de23e8 100644 --- a/tests/slicing/unravel-point.i +++ b/tests/slicing/unravel-point.i @@ -1,9 +1,9 @@ /* run.config - STDOPT: +"-calldeps -slice-return send1 -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-calldeps" - STDOPT: +"-calldeps -slice-return send2 -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-calldeps" - STDOPT: +"-calldeps -slice-return send3 -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-calldeps" - STDOPT: +"-calldeps -slice-return send4 -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-calldeps" - STDOPT: +"-calldeps -slice-return send1 -slice-return send4 -journal-disable -then-on 'Slicing export' @EVA_OPTIONS@ -calldeps -slice-return send1_slice_1 -print -then-on 'Slicing export 2' -print -then -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-calldeps -slice-return send1 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-calldeps -slice-return send2 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-calldeps -slice-return send3 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-calldeps -slice-return send4 -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" + STDOPT: +"-calldeps -slice-return send1 -slice-return send4 -journal-disable -then-on 'Slicing export' @EVA_OPTIONS@ -calldeps -slice-return send1_slice_1 -print -then-on 'Slicing export 2' -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -no-calldeps" diff --git a/tests/slicing/unravel-variance.i b/tests/slicing/unravel-variance.i index e30a4aebcb2fa7acd21f6d33caa29b6cfa798426..a892debf34a6a4665fca66af10368941eb903911 100644 --- a/tests/slicing/unravel-variance.i +++ b/tests/slicing/unravel-variance.i @@ -1,9 +1,9 @@ /* run.config - STDOPT: +"-slice-calls printf1 -journal-disable -float-normal -remove-redundant-alarms -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 " - STDOPT: +"-slice-calls printf2 -journal-disable -float-normal -remove-redundant-alarms -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 " - STDOPT: +"-slice-calls printf3 -journal-disable -float-normal -remove-redundant-alarms -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 " - STDOPT: +"-slice-calls printf4 -journal-disable -float-normal -remove-redundant-alarms -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 " - STDOPT: +"-slice-calls printf5 -journal-disable -float-normal -remove-redundant-alarms -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 " + STDOPT: +"-slice-calls printf1 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-calls printf2 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-calls printf3 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-calls printf4 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " + STDOPT: +"-slice-calls printf5 -journal-disable -float-normal -remove-redundant-alarms -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " */ /* Small example devired from examples given for UNRAVEL tool : */ diff --git a/tests/slicing/unsupported.i b/tests/slicing/unsupported.i index c7c3afd735d40652698ba492ebea0fba5f503b85..79cc4525e55a1134972d063091584e0399b66a8d 100644 --- a/tests/slicing/unsupported.i +++ b/tests/slicing/unsupported.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-slice-return main -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 " + STDOPT: +"-slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i " STDOPT: +"-sparecode" */ diff --git a/tests/slicing/use_spec.i b/tests/slicing/use_spec.i index 72c572818b14025c278fec1863331efcaa55f49a..7eba9f29bccf8d478a8851c04f669b83ae9e6062 100644 --- a/tests/slicing/use_spec.i +++ b/tests/slicing/use_spec.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +" -eva-use-spec f -slice-return main -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" + STDOPT: +" -eva-use-spec f -slice-return main -journal-disable -then-on 'Slicing export' -set-project-as-default -print -then -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i" STDOPT: +"-main main2 -slicing-level 3 -slice-undef-functions -eva-use-spec h -slice-return main2 -journal-disable -slicing-keep-annotations -then-on 'Slicing export' -set-project-as-default -print -eva @EVA_OPTIONS@ -eva-use-spec='-@all'" diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i index ff81bb51cab62adebb757548a563b5c5c4ac1a00..5664d0c98e76211deb39e2a0ace49d326818940e 100644 --- a/tests/spec/Extend.i +++ b/tests/spec/Extend.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -copy -kernel-warn-key=annot-error=active +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -copy -kernel-warn-key=annot-error=active */ /*@ foo x == 0; diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i index 568f3561f8b22dbb8022ed9baed7acb122ed7f0e..ace4e346de692cf86d1392bb3068e14155d5fe7b 100644 --- a/tests/spec/Extend_short_print.i +++ b/tests/spec/Extend_short_print.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ diff --git a/tests/spec/add_global.i b/tests/spec/add_global.i index 7ed406648a9ae0f6d2d9f3d5357314714edf358c..060e91bc160525f15cdc36132100287282d87e17 100644 --- a/tests/spec/add_global.i +++ b/tests/spec/add_global.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print */ int main () { return 0; } diff --git a/tests/spec/bts0578.i b/tests/spec/bts0578.i index c94e20665e6bda514c2d2f3460c2c132504d509c..2e1bf64bb4c52accb79a6adf81d4e8a16a2f3c22 100644 --- a/tests/spec/bts0578.i +++ b/tests/spec/bts0578.i @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ OPT: -print -load-module ./@PTEST_DIR@/@PTEST_NAME@ */ diff --git a/tests/spec/bts0655.i b/tests/spec/bts0655.i index b5947620ab99b29f05efcec6781e7549d0ff63c8..721f5b4037710aba83651a2cc9c45412cad02634 100644 --- a/tests/spec/bts0655.i +++ b/tests/spec/bts0655.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ @ ensures \result == \max( a, b ); diff --git a/tests/spec/clash_double_file_bts1598.c b/tests/spec/clash_double_file_bts1598.c index b30f925efab799c5b1c0a2e6306285564e878cac..f601dd3260381f1d346ef7e29bd9865f5391306e 100644 --- a/tests/spec/clash_double_file_bts1598.c +++ b/tests/spec/clash_double_file_bts1598.c @@ -1,7 +1,7 @@ /* run.config COMMENT: checks that linking string.h and its FC-pretty-printed version COMMENT: does not get rejected by name clash in the logic. See bts 1598 -OPT: @PTEST_FILE@ -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode @PTEST_DIR@/result/foo.c -print -then @PTEST_FILE@ @PTEST_DIR@/result/foo.c -ocode="" -print +OPT: @PTEST_FILE@ -cpp-extra-args " -Ishare/libc -nostdinc" -print -then -ocode foo.c -print -then @PTEST_FILE@ foo.c -ocode="" -print */ #include "__fc_builtin.h" diff --git a/tests/spec/comparison.i b/tests/spec/comparison.i index a62a8a65c779ed28e8b1795d4182dc1a0897c66e..3efacf43f66562d0a951392b5b50aa82df1c2b1e 100644 --- a/tests/spec/comparison.i +++ b/tests/spec/comparison.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ predicate foo(boolean a, boolean b) = a == b; */ diff --git a/tests/spec/heterogeneous_set_bts1146.i b/tests/spec/heterogeneous_set_bts1146.i index 98c508eb2fd3422ae25f8f98047f6ca9989216e9..baae6878e916e9d5ce7bf153d5590b00341ca316 100644 --- a/tests/spec/heterogeneous_set_bts1146.i +++ b/tests/spec/heterogeneous_set_bts1146.i @@ -1,7 +1,6 @@ /* run.config DONTRUN: bugfix in progress - EXECNOW: make -s tests/spec/Type_of_term.cmxs - OPT: -load-module ./tests/spec/Type_of_term.cmxs -print + OPT: -load-module %{dep:Type_of_term.cmxs} -print */ /*@ lemma foo: \union(1) == \union(1.0); */ diff --git a/tests/spec/location_char.c b/tests/spec/location_char.c index 99339a087cfd144ae6a400c10249fa9394530e4b..66ac3187cf15707f7b090be7a7a8f6decc9099ca 100644 --- a/tests/spec/location_char.c +++ b/tests/spec/location_char.c @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ requires x <= 0; diff --git a/tests/spec/model.i b/tests/spec/model.i index 840ab0193bc7883a50f8671c43f01ad4264e3c08..2d9b486e635c860bd9e71ec0e0850cdc3b543f22 100644 --- a/tests/spec/model.i +++ b/tests/spec/model.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" +CMXS: @PTEST_NAME@ +STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}" */ struct S { int x; int y; }; typedef struct S T; diff --git a/tests/spec/pp_empty_spec.i b/tests/spec/pp_empty_spec.i index 6d337f8500a51c4c764145969e8ef1c73bcff1f0..3f70a8fcfda7b236b0f5fbc9a5d2e52c5272289d 100644 --- a/tests/spec/pp_empty_spec.i +++ b/tests/spec/pp_empty_spec.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int main(void) { int x = 0; diff --git a/tests/spec/property_test.i b/tests/spec/property_test.i index 6f1de940f0cb8b128f6d9fefa4c635c806f5a267..328aeed58978849783980787f3bb66cd0e1ea062 100644 --- a/tests/spec/property_test.i +++ b/tests/spec/property_test.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int X; diff --git a/tests/spec/rm_qualifiers.i b/tests/spec/rm_qualifiers.i index 66d6d336519ad00ab153d800784078580d692d82..05a41ac5cbd20f203d5dc6525d9aa141b2a6a5ba 100644 --- a/tests/spec/rm_qualifiers.i +++ b/tests/spec/rm_qualifiers.i @@ -1,5 +1,5 @@ /* run.config -OPT: @PTEST_FILE@ -ocode @PTEST_DIR@/result/@PTEST_NAME@_res.i -print -then @PTEST_DIR@/result/@PTEST_NAME@_res.i -ocode="" -print +OPT: @PTEST_FILE@ -ocode @PTEST_NAME@_res.i -print -then @PTEST_NAME@_res.i -ocode="" -print */ extern void G(const void* p); typedef volatile int ARR[42][3]; diff --git a/tests/spec/type_constructors_in_env.i b/tests/spec/type_constructors_in_env.i index 636049ed329cfd848d51760fd52d2d84701261fc..97b266e4814a70dc2c7fd42d046708021af2d7c3 100644 --- a/tests/spec/type_constructors_in_env.i +++ b/tests/spec/type_constructors_in_env.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ type foo = A | B; */ diff --git a/tests/spec/type_of_term.i b/tests/spec/type_of_term.i index 81964fc9dbe8b52e417a7aac83b5e34436a2d08d..38c08465470065d1195125bef16d7f627c38eda0 100644 --- a/tests/spec/type_of_term.i +++ b/tests/spec/type_of_term.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s tests/spec/Type_of_term.cmxs - OPT: -load-module tests/spec/Type_of_term.cmxs -print + CMXS: Type_of_term + OPT: -load-module %{dep:Type_of_term.cmxs} -print */ int t [42]; diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i index edf44c1c372287804691d41291d1cbd5f120a9b7..8de4eb4bbb52576308294f07bcf435cc9515155a 100644 --- a/tests/syntax/Refresh_visitor.i +++ b/tests/syntax/Refresh_visitor.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @EVA_OPTIONS@ +CMXS: @PTEST_NAME@ +OPT: -load-module %{dep:@PTEST_NAME@.cmxs} @EVA_OPTIONS@ */ struct S { int i; }; diff --git a/tests/syntax/add_allocates.i b/tests/syntax/add_allocates.i index 2153e41ea67e6f54eeaf4a2b2719f3abb359eeac..0dd2e067ee54ac2e3b6fdbe38f63076ab054523a 100644 --- a/tests/syntax/add_allocates.i +++ b/tests/syntax/add_allocates.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print */ diff --git a/tests/syntax/anon_enum_libc.c b/tests/syntax/anon_enum_libc.c index 3c420cf6e6fe62b7f6becb62555d2708a710c471..afc114aca89a489855d97b55e011179d315f428b 100644 --- a/tests/syntax/anon_enum_libc.c +++ b/tests/syntax/anon_enum_libc.c @@ -1,6 +1,6 @@ /* run.config FILTER: sed -e 's|#include *"\([^/]*[/]\)*\([^/]*\)"|#include "PTESTS_DIR/\2"|' -OPT: -cpp-extra-args="-I @PTEST_DIR@" -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -ocode="" @PTEST_DIR@/result/@PTEST_NAME@.c -print +OPT: -cpp-extra-args="-I @PTEST_DIR@" -ocode @PTEST_NAME@.c -print -then -ocode="" @PTEST_NAME@.c -print */ struct { int x; float y; } s1; diff --git a/tests/syntax/ast_init.i b/tests/syntax/ast_init.i index 1e9aad67b5d3289f2c50f423edf4697fb2fb77fa..090ec68974b926fb688a7cdf1d3172a364f19b90 100644 --- a/tests/syntax/ast_init.i +++ b/tests/syntax/ast_init.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int f(int x) { return x; } diff --git a/tests/syntax/char_is_unsigned.i b/tests/syntax/char_is_unsigned.i index a3fbe427e1e26c1733ff8eecd4e4bd29fa9270d3..bbece923fe9f90570a7bbc89f224f1bc374ab8ca 100644 --- a/tests/syntax/char_is_unsigned.i +++ b/tests/syntax/char_is_unsigned.i @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/machdep_char_unsigned.cmxs + CMXS: machdep_char_unsigned OPT:-print -load-module @PTEST_DIR@/machdep_char_unsigned -machdep unsigned_char -then -constfold -rte */ char t[10]; diff --git a/tests/syntax/clone_test.i b/tests/syntax/clone_test.i index 7d94b47b61384b15dac0b60062acd1148947726a..f8d2bef0878f37d74705840baab0d2f0a724ef1b 100644 --- a/tests/syntax/clone_test.i +++ b/tests/syntax/clone_test.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ /*@ diff --git a/tests/syntax/copy_visitor_bts_1073.c b/tests/syntax/copy_visitor_bts_1073.c index a20b81af83fc0cb5b769207afd287f77450a2a17..5105c6e8a3710a1059cf0b87c14dc9675c7bece7 100644 --- a/tests/syntax/copy_visitor_bts_1073.c +++ b/tests/syntax/copy_visitor_bts_1073.c @@ -1,7 +1,7 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@_bis.cmxs -OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +CMXS: @PTEST_NAME@_bis +OPT: -load-module %{dep:@PTEST_NAME@.cmxs} OPT: -load-module @PTEST_DIR@/@PTEST_NAME@_bis -test -then-on filtered -print */ diff --git a/tests/syntax/enum_repr.i b/tests/syntax/enum_repr.i index 455e1c4aad4a1d5b923538016a82773032a30a24..1ccb7935c91e1b5bc237329a2b8a7381ebd9c3ac 100644 --- a/tests/syntax/enum_repr.i +++ b/tests/syntax/enum_repr.i @@ -1,8 +1,8 @@ /* run.config -EXECNOW: make -s tests/syntax/Enum_repr.cmxs -OPT: -load-module tests/syntax/Enum_repr.cmxs -enums int -print -OPT: -load-module tests/syntax/Enum_repr.cmxs -enums gcc-short-enums -print -OPT: -load-module tests/syntax/Enum_repr.cmxs -enums gcc-enums -print +CMXS: Enum_repr +OPT: -load-module %{dep:Enum_repr.cmxs} -enums int -print +OPT: -load-module %{dep:Enum_repr.cmxs} -enums gcc-short-enums -print +OPT: -load-module %{dep:Enum_repr.cmxs} -enums gcc-enums -print */ // is represented by | int | gcc-enums | gcc-short-enums diff --git a/tests/syntax/forloophook.i b/tests/syntax/forloophook.i index d9e38bd7b222e52182a102421f32151e285020ec..5d88397da3bfb9dd32972441303c521d33757bdf 100644 --- a/tests/syntax/forloophook.i +++ b/tests/syntax/forloophook.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ void f() { for (int i=0; i< 10; i++); diff --git a/tests/syntax/formals_decl_leak.i b/tests/syntax/formals_decl_leak.i index 93a7dc265a729926ce94aac380f8ec67a67198b8..c99425be26cbf34c74234128997546d804cc4c71 100644 --- a/tests/syntax/formals_decl_leak.i +++ b/tests/syntax/formals_decl_leak.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -print -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs @PTEST_DIR@/@PTEST_NAME@_1.i +CMXS: @PTEST_NAME@ +OPT: -print -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} @PTEST_DIR@/@PTEST_NAME@_1.i */ void f(int x); diff --git a/tests/syntax/get_astinfo_bts1136.i b/tests/syntax/get_astinfo_bts1136.i index 694aacdf37979df8db7e8043f9ed6268c82efa73..8d25ddc0bd0d12c2f9d020d4d2923e10d7320af9 100644 --- a/tests/syntax/get_astinfo_bts1136.i +++ b/tests/syntax/get_astinfo_bts1136.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int f (int x) { return x; } int g (int x) { return x; } diff --git a/tests/syntax/ghost_parameters_formals_status.i b/tests/syntax/ghost_parameters_formals_status.i index 4698b9f77e2e313d832db47fc4a41b83371508e5..ff6234d3d265558943219bb32810c07df6cc2f92 100644 --- a/tests/syntax/ghost_parameters_formals_status.i +++ b/tests/syntax/ghost_parameters_formals_status.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs + CMXS: @PTEST_NAME@ + OPT: -load-module %{dep:@PTEST_NAME@.cmxs} */ void declaration_void(void) /*@ ghost (int x, int y) */ ; diff --git a/tests/syntax/inserted_casts.c b/tests/syntax/inserted_casts.c index 805496d3d23a36a8bb973199a0e95203a72363ab..fb708329abc0d007b7099675c41af17d341f937d 100644 --- a/tests/syntax/inserted_casts.c +++ b/tests/syntax/inserted_casts.c @@ -1,7 +1,7 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" - STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" +"-machdep x86_64" + CMXS: @PTEST_NAME@ + STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}" + STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}" +"-machdep x86_64" */ #include "stddef.h" int f(int b) diff --git a/tests/syntax/label_decl.i b/tests/syntax/label_decl.i index f47ca2a64a658bbc9161ae8faf0e7a852c480b19..66af80ba65f1d9b6fe558b266c596ae6cb3c5430 100644 --- a/tests/syntax/label_decl.i +++ b/tests/syntax/label_decl.i @@ -1,5 +1,5 @@ /* run.config -MACRO: TMP @PTEST_DIR@/result/@PTEST_NAME@.i +MACRO: TMP @PTEST_NAME@.i OPT: -print -then -print -ocode @TMP@ -then @TMP@ -print -ocode="" */ struct s { int i; }; diff --git a/tests/syntax/logic_env.i b/tests/syntax/logic_env.i index 9570e109382c07d8d19a57248a384cbc372b9e66..9e39b9b120ce835427c80c929b774a9917893f6b 100644 --- a/tests/syntax/logic_env.i +++ b/tests/syntax/logic_env.i @@ -1,5 +1,5 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/logic_env_script.cmxs +CMXS: logic_env_script OPT: -load-module @PTEST_DIR@/logic_env_script */ diff --git a/tests/syntax/merge_loc.i b/tests/syntax/merge_loc.i index 8f08173f151e39627df74d38288858a1a2d9d68d..bb5604134d82f05ee4a5c3555ee8f35ecb6868f4 100644 --- a/tests/syntax/merge_loc.i +++ b/tests/syntax/merge_loc.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s tests/syntax/pp_lines.cmxs - STDOPT: #"-load-module tests/syntax/pp_lines.cmxs" + CMXS: pp_lines + STDOPT: #"-load-module %{dep:pp_lines.cmxs}" */ // Test locations when cabs2cil merges declarations and tentative definitions diff --git a/tests/syntax/mutable_test.i b/tests/syntax/mutable_test.i index 3c480aa053427eebf9bcf9ca6c5dcfd257cad058..c14b31adc5a0643589b27643c5fb6845d4522b35 100644 --- a/tests/syntax/mutable_test.i +++ b/tests/syntax/mutable_test.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -print */ struct R_1 { diff --git a/tests/syntax/no-print-libc-reparse.c b/tests/syntax/no-print-libc-reparse.c index bf0b39507c3aa985e8c30eef3ab7c52166399f8a..2c73778b8eb7c4888bc01661cb61e2112bbb65c8 100644 --- a/tests/syntax/no-print-libc-reparse.c +++ b/tests/syntax/no-print-libc-reparse.c @@ -1,5 +1,5 @@ /*run.config - STDOPT: #"-no-print-libc -print -ocode @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -then @PTEST_DIR@/result/ocode_@PTEST_NUMBER@_@PTEST_NAME@.c" + STDOPT: #"-no-print-libc -print -ocode ocode_@PTEST_NUMBER@_@PTEST_NAME@.c -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.c" */ // tests that using -no-print-libc on a file with an enum produces output that diff --git a/tests/syntax/reorder.i b/tests/syntax/reorder.i index a611137930713ae5fbb4db09a2cbefdf59513905..647f6f9cea62343e958d96e170317cf1801f2bd8 100644 --- a/tests/syntax/reorder.i +++ b/tests/syntax/reorder.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int x; diff --git a/tests/syntax/syntactic_hook.i b/tests/syntax/syntactic_hook.i index d887e89667ec5464d71f2d68e749dfe68465f196..aabc12a7e6141304817d70705c2eeeb7b07acaf6 100644 --- a/tests/syntax/syntactic_hook.i +++ b/tests/syntax/syntactic_hook.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs" + CMXS: @PTEST_NAME@ + STDOPT: +"-no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs}" */ int f(void); diff --git a/tests/syntax/temporary_location.c b/tests/syntax/temporary_location.c index 765e6bccedee2df52e4d8551c4fac28faa06523e..11ce2caffb0c5cb2dccb453a454498f343b718c3 100644 --- a/tests/syntax/temporary_location.c +++ b/tests/syntax/temporary_location.c @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print + CMXS: @PTEST_NAME@ + OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -print */ int f(void) { diff --git a/tests/syntax/transient_block.i b/tests/syntax/transient_block.i index bfc8874399c9bb1e29a30b523ac5fbec9b52e77e..689cac478935ff34888aae67cbeab49780377a19 100644 --- a/tests/syntax/transient_block.i +++ b/tests/syntax/transient_block.i @@ -1,6 +1,6 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs - OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -kernel-warn-key transient-block=active + CMXS: @PTEST_NAME@ + OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -kernel-warn-key transient-block=active */ void f(void) { } diff --git a/tests/syntax/typedef_incorrect_pretty_print_bts1518.i b/tests/syntax/typedef_incorrect_pretty_print_bts1518.i index ce8d5fb7c501c54454ec795114ada76504e5578a..6ea6db2214d546cd4ab67bef619a4d2c234892fe 100644 --- a/tests/syntax/typedef_incorrect_pretty_print_bts1518.i +++ b/tests/syntax/typedef_incorrect_pretty_print_bts1518.i @@ -1,7 +1,7 @@ /* run.config DONTRUN: bug fix in progress MACRO: OUT @PTEST_NAME@_res.i -EXECNOW: LOG @OUT@ @frama-c@ @PTEST_FILE@ -ocode @PTEST_DIR@/result/@OUT@ -print -then @PTEST_DIR@/result/@OUT@ -print +EXECNOW: LOG @OUT@ @frama-c@ @PTEST_FILE@ -ocode @OUT@ -print -then @OUT@ -print */ /* Generated by Frama-C */ /* Generated by Frama-C */ diff --git a/tests/syntax/typedef_multi_1.c b/tests/syntax/typedef_multi_1.c index 33a8d6c3537a3452d299e6a481c5514bbdb93022..c3b3da57ba49726e2e07a252a4b3d605d0effe36 100644 --- a/tests/syntax/typedef_multi_1.c +++ b/tests/syntax/typedef_multi_1.c @@ -1,5 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/typedef_multi.cmxs + CMXS: typedef_multi OPT: -load-module @PTEST_DIR@/typedef_multi tests/syntax/typedef_multi_2.c */ diff --git a/tests/syntax/vdescr_bts1387.i b/tests/syntax/vdescr_bts1387.i index b20b1226bd2c890329ecea47201df49299e8f69b..9ad26b98011cde070ec318ec65fccef660fe0f5a 100644 --- a/tests/syntax/vdescr_bts1387.i +++ b/tests/syntax/vdescr_bts1387.i @@ -1,6 +1,6 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} */ int f(int); int g(int); diff --git a/tests/syntax/visit_create_local.i b/tests/syntax/visit_create_local.i index 6d9a88989bca1c8106862f9bb5dd304b6da357c0..21caf17f85477ed351eb0715ad637c04d102528b 100644 --- a/tests/syntax/visit_create_local.i +++ b/tests/syntax/visit_create_local.i @@ -1,5 +1,5 @@ /* run.config -EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs -OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -then-on bidon -print +CMXS: @PTEST_NAME@ +OPT: -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} -then-on bidon -print */ void main() { int x,y; x = y; }