From ae7ce06ddaeed222af36407d4344aa507e1eeaff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 3 Sep 2020 16:44:14 +0200
Subject: [PATCH] tests in tests/slicing pass
---
ptests/ptests.ml | 4 +-
.../plugin_entry_points/plugin.ml | 6 +-
src/plugins/constant_propagation/dune | 2 +-
tests/builtins/alloc.c | 2 +-
tests/builtins/from_result.c | 2 +-
tests/builtins/malloc_individual.c | 2 +-
tests/constant_propagation/test_config | 1 +
tests/journal/intra.i | 1 +
tests/libc/coverage.c | 3 +-
tests/libc/fc_libc.c | 2 +-
tests/libc/runtime.c | 3 +-
tests/libc/string_c_generic.c | 3 +-
tests/libc/string_c_strchr.c | 3 +-
tests/libc/string_c_strstr.c | 3 +-
tests/pdg/test_config | 1 +
tests/rte/divmod.c | 2 +-
tests/rte/divmod_typedef.c | 2 +-
tests/saveload/bool.c | 2 +-
tests/slicing/bts1684.i | 2 +-
tests/slicing/combine.i | 2 +-
tests/slicing/dune | 4 +-
tests/slicing/ex_spec_interproc.i | 2 +-
tests/slicing/horwitz.i | 2 +-
tests/slicing/mark_all_slices.i | 2 +-
tests/slicing/merge.i | 2 +-
tests/slicing/min_call.i | 2 +-
tests/slicing/oracle/bts1684.res.oracle | 2 +-
tests/slicing/oracle/bts336.3.res.oracle | 28 +++---
.../oracle/select_by_annot.1.res.oracle | 14 +--
.../oracle/select_by_annot.10.res.oracle | 14 +--
.../oracle/select_by_annot.11.res.oracle | 14 +--
.../oracle/select_by_annot.12.res.oracle | 14 +--
.../oracle/select_by_annot.13.res.oracle | 14 +--
.../oracle/select_by_annot.14.res.oracle | 14 +--
.../oracle/select_by_annot.2.res.oracle | 14 +--
.../oracle/select_by_annot.3.res.oracle | 14 +--
.../oracle/select_by_annot.4.res.oracle | 14 +--
.../oracle/select_by_annot.5.res.oracle | 14 +--
.../oracle/select_by_annot.6.res.oracle | 14 +--
.../oracle/select_by_annot.7.res.oracle | 14 +--
.../oracle/select_by_annot.8.res.oracle | 14 +--
.../oracle/select_by_annot.9.res.oracle | 14 +--
tests/slicing/oracle/variadic.0.res.oracle | 76 ++++++++++++++--
tests/slicing/oracle/variadic.1.res.oracle | 73 +++++++++++++--
tests/slicing/oracle/variadic.2.res.oracle | 90 ++++++++++++++++--
tests/slicing/oracle/variadic.3.res.oracle | 91 +++++++++++++++++--
tests/slicing/oracle/variadic.4.res.oracle | 91 +++++++++++++++++--
tests/slicing/select_by_annot.i | 4 +-
tests/slicing/select_simple.i | 2 +-
tests/slicing/simple_intra_slice.i | 2 +-
tests/slicing/slice_no_body.i | 2 +-
tests/slicing/switch.i | 2 +-
tests/slicing/test_config | 1 +
tests/slicing/variadic.c | 3 +-
tests/spec/acsl_basic_allocator.c | 2 +-
tests/spec/purse.c | 2 +-
tests/syntax/assert_location.c | 5 +
"tests/syntax/foo\".c" | 2 +-
tests/syntax/gcc_builtins.c | 2 +-
tests/syntax/merge_unused.c | 1 +
tests/syntax/multiple_decls_contracts.c | 6 +-
tests/syntax/offsetof.c | 2 +-
tests/value/CruiseControl.c | 1 +
tests/value/CruiseControl_const.c | 1 +
tests/value/abstract_struct_1.c | 2 +-
tests/value/inline.c | 1 +
tests/value/wide_string.c | 2 +-
67 files changed, 535 insertions(+), 219 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 879a964f598..797713750dc 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -596,7 +596,6 @@ type config =
let default_macros () =
let l = [
"frama-c", !toplevel_path;
- "PTEST_MAKE_MODULE", "make -s"
] in
Macros.add_list l Macros.empty
@@ -1007,7 +1006,8 @@ let basic_command_string =
(Macros.get "PTEST_LOAD_MODULES" macros) in
let opt_pre = Macros.expand macros !additional_options_pre in
let opt_post = Macros.expand macros !additional_options in
- "-check " ^ opt_modules ^ " " ^ opt_pre ^ " " ^ options ^ " " ^ opt_post
+ let opt_plugin = String.concat " " (List.map (Printf.sprintf "-load-module %s") command.plugins) in
+ String.concat " " ["-check -no-autoload-plugins";opt_plugin;opt_modules;opt_pre;options;opt_post]
end else options
in
let options = if !use_byte then opt_to_byte_options options else options in
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 06ec07489dc..eb6788d998d 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
module CamlString = String
+module FramacFilepath = Filepath
let empty_string = ""
@@ -322,12 +323,13 @@ struct
end)
let mk_dir d =
+ let d' = FramacFilepath.Normalized.of_string d in
try
Extlib.mkdir ~parents:true d 0o755;
- L.warning "creating %s directory `%s'" O.option_name d;
+ L.warning "creating %s directory `%a'" O.option_name FramacFilepath.Normalized.pretty d';
d
with Unix.Unix_error _ ->
- L.abort "cannot create %s directory `%s'" O.option_name d
+ L.abort "cannot create %s directory `%a'" O.option_name FramacFilepath.Normalized.pretty d'
let set filepath = Dir_name.set filepath
let get () = Dir_name.get ()
diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune
index 4ba43a8084d..0d5e5e25cb3 100644
--- a/src/plugins/constant_propagation/dune
+++ b/src/plugins/constant_propagation/dune
@@ -1,5 +1,5 @@
( library
- (name constant_propagation)
+ (name Constant_Propagation)
(public_name frama-c-constant_propagation.core)
(flags -open Frama_c_kernel)
(libraries frama-c.kernel)
diff --git a/tests/builtins/alloc.c b/tests/builtins/alloc.c
index 36f4a7c0333..a12737dae2d 100644
--- a/tests/builtins/alloc.c
+++ b/tests/builtins/alloc.c
@@ -5,7 +5,7 @@
*/
-#include "share/libc/stdlib.c"
+#include "stdlib.c"
int *p,*q,*r,a,b;
char *t,*u,*v;
diff --git a/tests/builtins/from_result.c b/tests/builtins/from_result.c
index 89e1f89ae0d..e38ba72eb1c 100644
--- a/tests/builtins/from_result.c
+++ b/tests/builtins/from_result.c
@@ -2,7 +2,7 @@
OPT: @EVA_CONFIG@ -eva-alloc-builtin fresh -deps -journal-disable
*/
-#include "../../share/libc/stdlib.c"
+#include "stdlib.c"
struct T { int a; int b; };
diff --git a/tests/builtins/malloc_individual.c b/tests/builtins/malloc_individual.c
index 790ffba5e5b..bf5218700c9 100644
--- a/tests/builtins/malloc_individual.c
+++ b/tests/builtins/malloc_individual.c
@@ -2,7 +2,7 @@
STDOPT: #"-eva-alloc-builtin fresh"
*/
-#include "share/libc/stdlib.c"
+#include "stdlib.c"
int *p;
int A,B,C;
diff --git a/tests/constant_propagation/test_config b/tests/constant_propagation/test_config
index 850779adb25..77b08230a76 100644
--- a/tests/constant_propagation/test_config
+++ b/tests/constant_propagation/test_config
@@ -1 +1,2 @@
+PLUGIN: constant_propagation
OPT: -journal-disable -scf @EVA_OPTIONS@
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 2e8031e2e2a..268a1ad8530 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,4 +1,5 @@
/* run.config
+ PLUGIN: sparecode
CMXS: @PTEST_NAME@
EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs}
diff --git a/tests/libc/coverage.c b/tests/libc/coverage.c
index 2fa988b1e5d..8c2b1421bfd 100644
--- a/tests/libc/coverage.c
+++ b/tests/libc/coverage.c
@@ -1,5 +1,6 @@
/* run.config*
- OPT: -eva-no-builtins-auto @EVA_OPTIONS@ share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
+ DEPS: ../../share/libc/string.c
+ OPT: -eva-no-builtins-auto @EVA_OPTIONS@ ../../share/libc/string.c -eva -slevel 6 -metrics-eva-cover -then -metrics-libc
*/
#include "string.h"
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index f4fb5d0a126..0a73ba18d49 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -22,7 +22,7 @@
#define _POSIX_C_SOURCE 200112L
#define _GNU_SOURCE 1
-#include "share/libc/__fc_runtime.c"
+#include "__fc_runtime.c"
#include "alloca.h"
#include "arpa/inet.h"
diff --git a/tests/libc/runtime.c b/tests/libc/runtime.c
index 69ea8ad3649..37647e76af9 100644
--- a/tests/libc/runtime.c
+++ b/tests/libc/runtime.c
@@ -1,6 +1,7 @@
/* run.config*
COMMENT: tests that the runtime can compile without errors (for PathCrawler, E-ACSL, ...)
- CMD: gcc -D__FC_MACHDEP_X86_64 share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
+ DEPS: ../../share/libc/__fc_runtime.c
+ CMD: gcc -D__FC_MACHDEP_X86_64 ../../share/libc/__fc_runtime.c -Wno-attributes -std=c99 -o /dev/null
OPT:
*/
diff --git a/tests/libc/string_c_generic.c b/tests/libc/string_c_generic.c
index 9168f43d736..d960a9b44fc 100644
--- a/tests/libc/string_c_generic.c
+++ b/tests/libc/string_c_generic.c
@@ -1,5 +1,6 @@
/* run.config
- STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-includeshare/libc/string.c -slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
+ DEPS: ../../share/libc/string.c
+ STDOPT: #"-eva-no-builtins-auto -cpp-extra-args=-include../../share/libc/string.c -slevel-function strcpy:20,strncpy:5,strcmp:6,strchr:20,strrchr:20,strncat:4,memset:32,strlen:20,memcmp:8 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/string_c_strchr.c b/tests/libc/string_c_strchr.c
index 54ed8fab06e..4179b4f27cb 100644
--- a/tests/libc/string_c_strchr.c
+++ b/tests/libc/string_c_strchr.c
@@ -1,5 +1,6 @@
/* run.config
- STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
+ DEPS: ../../share/libc/string.c
+ STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -slevel-function strchr:256,main:256 -eva-slevel-merge-after-loop main -eva-no-builtins-auto -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/libc/string_c_strstr.c b/tests/libc/string_c_strstr.c
index 9f0613b3515..2bfbbdbe125 100644
--- a/tests/libc/string_c_strstr.c
+++ b/tests/libc/string_c_strstr.c
@@ -1,5 +1,6 @@
/* run.config
- STDOPT: #"-cpp-extra-args=-includeshare/libc/string.c -slevel-function strstr:30 -eva-no-skip-stdlib-specs"
+ DEPS: ../../share/libc/string.c
+ STDOPT: #"-cpp-extra-args=-include../../share/libc/string.c -slevel-function strstr:30 -eva-no-skip-stdlib-specs"
*/
/* This file has been adapted from libc-test, which is licensed under the
following standard MIT license:
diff --git a/tests/pdg/test_config b/tests/pdg/test_config
index d9d741191d1..b5c1a82645a 100644
--- a/tests/pdg/test_config
+++ b/tests/pdg/test_config
@@ -1 +1,2 @@
+PLUGIN: pdg
OPT: -journal-disable @EVA_OPTIONS@ -pdg-print -pdg-verbose 2
diff --git a/tests/rte/divmod.c b/tests/rte/divmod.c
index 8920e6031b5..13d9737ece5 100644
--- a/tests/rte/divmod.c
+++ b/tests/rte/divmod.c
@@ -2,7 +2,7 @@
OPT: -rte -warn-signed-overflow -warn-signed-downcast -print -machdep x86_32 -journal-disable
*/
-#include "share/libc/limits.h"
+#include "limits.h"
int main() {
diff --git a/tests/rte/divmod_typedef.c b/tests/rte/divmod_typedef.c
index 3fd9e3f6beb..d3c6b330e52 100644
--- a/tests/rte/divmod_typedef.c
+++ b/tests/rte/divmod_typedef.c
@@ -2,7 +2,7 @@
OPT: -rte -warn-signed-overflow -warn-signed-downcast -print -machdep x86_32 -journal-disable
*/
-#include "share/libc/limits.h"
+#include "limits.h"
typedef int tint;
typedef unsigned int tuint;
diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c
index f0752a78127..c79e10630fd 100644
--- a/tests/saveload/bool.c
+++ b/tests/saveload/bool.c
@@ -5,7 +5,7 @@
*/
#include "stdbool.h"
-#include "share/libc/stdio.h"
+#include "stdio.h"
bool x;
int y;
diff --git a/tests/slicing/bts1684.i b/tests/slicing/bts1684.i
index 75f95e0c4ea..4bcbd970713 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 ocode_@PTEST_NUMBER@_@PTEST_NAME@.i -then ocode_@PTEST_NUMBER@_@PTEST_NAME@.i"
+ STDOPT: +"-session .frama-c -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/combine.i b/tests/slicing/combine.i
index 6a8df7c51cc..678556ebe03 100644
--- a/tests/slicing/combine.i
+++ b/tests/slicing/combine.i
@@ -1,6 +1,6 @@
/* run.config
PLUGIN: constant_propagation
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -load-plugin constant_propagation -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
OPT: @EVA_OPTIONS@ -deps -journal-disable
*/
diff --git a/tests/slicing/dune b/tests/slicing/dune
index d07d4048038..f602968810b 100644
--- a/tests/slicing/dune
+++ b/tests/slicing/dune
@@ -15,7 +15,7 @@
(executables
(names merge adpcm ex_spec_interproc 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)
+ (modules merge adpcm ex_spec_interproc 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)
)
@@ -25,6 +25,6 @@
(names combine)
(modes plugin)
(modules combine)
- (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core frama-c-constant-propagation.core libSelect libAnim)
+ (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-slicing.core frama-c-constant_propagation.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 38c8a95b01d..e31d5f2bb82 100644
--- a/tests/slicing/ex_spec_interproc.i
+++ b/tests/slicing/ex_spec_interproc.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
OPT: @EVA_OPTIONS@ -deps -journal-disable
*/
diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i
index 10ec91fffb8..66888cbb0f3 100644
--- a/tests/slicing/horwitz.i
+++ b/tests/slicing/horwitz.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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/mark_all_slices.i b/tests/slicing/mark_all_slices.i
index fd186b11a78..7f9994fc771 100644
--- a/tests/slicing/mark_all_slices.i
+++ b/tests/slicing/mark_all_slices.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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 690517f1428..d831f24fe1c 100644
--- a/tests/slicing/merge.i
+++ b/tests/slicing/merge.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:libAnim.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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 7078fc13c26..a268f001ff9 100644
--- a/tests/slicing/min_call.i
+++ b/tests/slicing/min_call.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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/oracle/bts1684.res.oracle b/tests/slicing/oracle/bts1684.res.oracle
index 305c7d7c0f7..96c61a1f0a0 100644
--- a/tests/slicing/oracle/bts1684.res.oracle
+++ b/tests/slicing/oracle/bts1684.res.oracle
@@ -59,5 +59,5 @@ int main(void)
[kernel] Parsing ocode_0_bts1684.i (no preprocessing)
-[kernel] Warning: creating session directory `/home/bobot/Sources/frama-c/_build/default/result/.frama-c'
+[kernel] Warning: creating session directory `.frama-c'
[kernel] writing journal in file `.frama-c/frama_c_journal.ml'.
diff --git a/tests/slicing/oracle/bts336.3.res.oracle b/tests/slicing/oracle/bts336.3.res.oracle
index 3ec5777dbbc..e5747bf0754 100644
--- a/tests/slicing/oracle/bts336.3.res.oracle
+++ b/tests/slicing/oracle/bts336.3.res.oracle
@@ -37,20 +37,6 @@
[from] entry point:
\result FROM \nothing
[from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] InOut (internal) for function f3:
- Operational inputs:
- p; a; b; c
- Operational inputs on termination:
- p; a; b; c
- Sure outputs:
- \nothing
-[inout] InOut (internal) for function main3:
- Operational inputs:
- \nothing
- Operational inputs on termination:
- \nothing
- Sure outputs:
- a; b; c
[slicing] slicing requests in progress...
[slicing] initializing slicing ...
[slicing] interpreting slicing requests from the command line...
@@ -68,6 +54,20 @@
[slicing] applying 0 actions...
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
+[inout] InOut (internal) for function f3:
+ Operational inputs:
+ p; a; b; c
+ Operational inputs on termination:
+ p; a; b; c
+ Sure outputs:
+ \nothing
+[inout] InOut (internal) for function main3:
+ Operational inputs:
+ \nothing
+ Operational inputs on termination:
+ \nothing
+ Sure outputs:
+ a; b; c
/* Generated by Frama-C */
void f3_slice_1(int *p)
{
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index f50b98ea8fd..c0f3575f5dc 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -176,4 +172,4 @@ void main(void)
}
-[kernel] Parsing result/ocode_1_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_1_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index 9cb53dcddf2..c30f26887f6 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -182,4 +178,4 @@ void f7_slice_1(int cond)
}
-[kernel] Parsing result/ocode_10_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_10_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.11.res.oracle b/tests/slicing/oracle/select_by_annot.11.res.oracle
index 88a16c2a643..5b27209920b 100644
--- a/tests/slicing/oracle/select_by_annot.11.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.11.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -174,4 +170,4 @@ void f8_slice_1(int cond)
}
-[kernel] Parsing result/ocode_11_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_11_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index 43b2000555a..0c6fe54f4cf 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -181,4 +177,4 @@ void f8_slice_1(int cond)
}
-[kernel] Parsing result/ocode_12_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_12_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.13.res.oracle b/tests/slicing/oracle/select_by_annot.13.res.oracle
index e0fe78aed78..8f680bd8056 100644
--- a/tests/slicing/oracle/select_by_annot.13.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.13.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -180,4 +176,4 @@ void f8_slice_1(int cond)
}
-[kernel] Parsing result/ocode_13_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_13_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index 15ddc697da2..69d8673daf1 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -173,4 +169,4 @@ void f9_slice_1(int c1, int c2)
}
-[kernel] Parsing result/ocode_14_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_14_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.2.res.oracle b/tests/slicing/oracle/select_by_annot.2.res.oracle
index 8fbdf856640..2447ad2d338 100644
--- a/tests/slicing/oracle/select_by_annot.2.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.2.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -172,4 +168,4 @@ void main(void)
}
-[kernel] Parsing result/ocode_2_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_2_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index cdb1a6cc2c0..25a50f5cd59 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -175,4 +171,4 @@ void modifS_slice_1(int a)
}
-[kernel] Parsing result/ocode_3_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_3_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 41ac22a88b8..8d2642c6fa8 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -175,4 +171,4 @@ void f1_slice_1(void)
}
-[kernel] Parsing result/ocode_4_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_4_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index 954a303d7ef..165cc861ab7 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -174,4 +170,4 @@ void f2_slice_1(void)
}
-[kernel] Parsing result/ocode_5_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_5_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index d476c481b8f..fb469fe2139 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -170,4 +166,4 @@ void f3_slice_1(int cond)
}
-[kernel] Parsing result/ocode_6_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_6_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index e4910e63167..540bcb17efb 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -178,4 +174,4 @@ void f4_slice_1(int cond)
}
-[kernel] Parsing result/ocode_7_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_7_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index cff1da9a6ee..31a3e7b2447 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -170,4 +166,4 @@ void f5_slice_1(int cond)
}
-[kernel] Parsing result/ocode_8_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_8_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index 6c0b33b045b..8140a0c2883 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -26,14 +26,12 @@
[eva] Done for function new_int
[eva] computing for function f1 <- main.
Called from select_by_annot.i:141.
-[eva:alarm] select_by_annot.i:29: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:29: Warning: assertion got status unknown.
[eva] Recording results for f1
[eva] Done for function f1
[eva] computing for function f2 <- main.
Called from select_by_annot.i:142.
-[eva:alarm] select_by_annot.i:39: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:39: Warning: assertion got status unknown.
[eva] Recording results for f2
[eva] Done for function f2
[eva] computing for function f3 <- main.
@@ -62,10 +60,8 @@
[eva] Done for function f7
[eva] computing for function f8 <- main.
Called from select_by_annot.i:148.
-[eva:alarm] select_by_annot.i:97: Warning:
- loop invariant got status unknown.
-[eva:alarm] select_by_annot.i:100: Warning:
- assertion got status unknown.
+[eva:alarm] select_by_annot.i:97: Warning: loop invariant got status unknown.
+[eva:alarm] select_by_annot.i:100: Warning: assertion got status unknown.
[eva:alarm] select_by_annot.i:104: Warning:
signed overflow. assert S.a + 1 ≤ 2147483647;
[eva] Recording results for f8
@@ -180,4 +176,4 @@ void f6_slice_1(int cond)
}
-[kernel] Parsing result/ocode_9_select_by_annot.i (no preprocessing)
+[kernel] Parsing ocode_9_select_by_annot.i (no preprocessing)
diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle
index 75216a2d96c..5db81403d65 100644
--- a/tests/slicing/oracle/variadic.0.res.oracle
+++ b/tests/slicing/oracle/variadic.0.res.oracle
@@ -1,8 +1,70 @@
[kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.cf732ce.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning:
+ Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function f3
+[from] Computing for function lib_f
+[from] Done for function lib_f
+[pdg] done for function f3
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f3_slice_1(void)
+{
+ int tmp;
+ {
+ void *__va_args[3];
+ tmp = lib_f(3,(void * const *)(__va_args));
+ }
+ return tmp;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.1.res.oracle b/tests/slicing/oracle/variadic.1.res.oracle
index ba6e34a3bc6..d7485ec33c9 100644
--- a/tests/slicing/oracle/variadic.1.res.oracle
+++ b/tests/slicing/oracle/variadic.1.res.oracle
@@ -1,8 +1,67 @@
[kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.c65331d.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning:
+ Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function f3
+[from] Computing for function lib_f
+[from] Done for function lib_f
+[pdg] done for function f3
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n , ...);
+
+int f3_slice_1(int a, int b, int c)
+{
+ int tmp;
+ tmp = lib_f(3,a,b,c);
+ return tmp;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.2.res.oracle b/tests/slicing/oracle/variadic.2.res.oracle
index 967e256337f..9e85774a6e5 100644
--- a/tests/slicing/oracle/variadic.2.res.oracle
+++ b/tests/slicing/oracle/variadic.2.res.oracle
@@ -1,8 +1,84 @@
[kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.c329fe5.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning:
+ Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function f3
+[from] Computing for function lib_f
+[from] Done for function lib_f
+[pdg] done for function f3
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function main
+[from] Computing for function f1
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[pdg] done for function main
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f3_slice_1(void)
+{
+ int tmp;
+ {
+ void *__va_args[3];
+ tmp = lib_f(3,(void * const *)(__va_args));
+ }
+ return tmp;
+}
+
+void main(void)
+{
+ f3_slice_1();
+ return;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.3.res.oracle b/tests/slicing/oracle/variadic.3.res.oracle
index 55bbb63c595..e4cedf8c754 100644
--- a/tests/slicing/oracle/variadic.3.res.oracle
+++ b/tests/slicing/oracle/variadic.3.res.oracle
@@ -1,8 +1,85 @@
[kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.ce8a359.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning:
+ Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function main
+[from] Computing for function f1
+[from] Computing for function lib_f <-f1
+[from] Done for function lib_f
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[pdg] done for function main
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function f2
+[pdg] done for function f2
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f2_slice_1(void)
+{
+ int tmp;
+ {
+ void *__va_args[2];
+ tmp = lib_f(2,(void * const *)(__va_args));
+ }
+ return tmp;
+}
+
+int main(void)
+{
+ int s;
+ s = f2_slice_1();
+ return s;
+}
+
+
diff --git a/tests/slicing/oracle/variadic.4.res.oracle b/tests/slicing/oracle/variadic.4.res.oracle
index cc0e55b1e04..e4cedf8c754 100644
--- a/tests/slicing/oracle/variadic.4.res.oracle
+++ b/tests/slicing/oracle/variadic.4.res.oracle
@@ -1,8 +1,85 @@
[kernel] Parsing variadic.c (with preprocessing)
-[kernel] User Error: failed to run: gcc -E -C -I. -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 -o '/tmp/variadic.cdcb684.i' '/home/bobot/Sources/frama-c/_build/default/result/variadic.c'
- this is possibly due to missing preprocessor flags;
- consider options -cpp-extra-args, -json-compilation-database or -cpp-command.
- See chapter "Preparing the Sources" in the Frama-C user manual for more details.
-[kernel] User Error: stopping on file "variadic.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[slicing] slicing requests in progress...
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] computing for function f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:37.
+[eva] computing for function lib_f <- f1 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23.
+[kernel:annot:missing-spec] /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:23: Warning:
+ Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] using specification for function lib_f
+[eva] Done for function lib_f
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:38.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:39.
+[eva] computing for function lib_f <- f3 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:31.
+[eva] Done for function lib_f
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:40.
+[eva] computing for function lib_f <- f2 <- main.
+ Called from /home/bobot/Sources/frama-c/_build/default/tests/pdg/variadic.c:27.
+[eva] Done for function lib_f
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] Recording results for main
+[eva] done for function main
+[slicing] initializing slicing ...
+[slicing] interpreting slicing requests from the command line...
+[pdg] computing for function main
+[from] Computing for function f1
+[from] Computing for function lib_f <-f1
+[from] Done for function lib_f
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[pdg] done for function main
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function f2
+[pdg] done for function f2
+[slicing] exporting project to 'Slicing export'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Slicing export tmp'
+[sparecode] removed unused global declarations in new project 'Slicing export'
+/* Generated by Frama-C */
+int lib_f(int n, void * const *__va_params);
+
+int f2_slice_1(void)
+{
+ int tmp;
+ {
+ void *__va_args[2];
+ tmp = lib_f(2,(void * const *)(__va_args));
+ }
+ return tmp;
+}
+
+int main(void)
+{
+ int s;
+ s = f2_slice_1();
+ return s;
+}
+
+
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index 06069b98128..1a70a1cd5ad 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -1,8 +1,8 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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
+ CMD: frama-c
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
diff --git a/tests/slicing/select_simple.i b/tests/slicing/select_simple.i
index 2ff216ec85d..8452d2a73e5 100644
--- a/tests/slicing/select_simple.i
+++ b/tests/slicing/select_simple.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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 085ceb13737..76a3f94515b 100644
--- a/tests/slicing/simple_intra_slice.i
+++ b/tests/slicing/simple_intra_slice.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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/slice_no_body.i b/tests/slicing/slice_no_body.i
index 75786a6ef32..83937bd0838 100644
--- a/tests/slicing/slice_no_body.i
+++ b/tests/slicing/slice_no_body.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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/switch.i b/tests/slicing/switch.i
index 7e0a12e0555..de3807ffdbe 100644
--- a/tests/slicing/switch.i
+++ b/tests/slicing/switch.i
@@ -1,6 +1,6 @@
/* run.config
- CMD: @frama-c@ -load-module %{dep:libSelect.cmxs} -load-module %{dep:@PTEST_NAME@.cmxs}
+ CMD: @frama-c@ -load-plugin slicing -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/test_config b/tests/slicing/test_config
index 1712a20359b..d33c6619cf5 100644
--- a/tests/slicing/test_config
+++ b/tests/slicing/test_config
@@ -1 +1,2 @@
+PLUGIN: slicing
OPT: @EVA_OPTIONS@
diff --git a/tests/slicing/variadic.c b/tests/slicing/variadic.c
index 9de40fa3f81..4629542db44 100644
--- a/tests/slicing/variadic.c
+++ b/tests/slicing/variadic.c
@@ -1,4 +1,5 @@
/* run.config
+ DEPS: ../pdg/variadic.c
STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -then-on 'Slicing export' -print"
STDOPT: +"-slice-return f3 -no-slice-callers -journal-disable -variadic-no-translation -then-last -print"
STDOPT: +"-slice-return f3 -journal-disable -then-on 'Slicing export' -print"
@@ -6,4 +7,4 @@
STDOPT: +"-slice-return main -slicing-level 3 -journal-disable -then-on 'Slicing export' -print"
*/
-#include "../pdg/variadic.c"
+#include "../../pdg/variadic.c"
diff --git a/tests/spec/acsl_basic_allocator.c b/tests/spec/acsl_basic_allocator.c
index 6a964f453b7..1390061b451 100644
--- a/tests/spec/acsl_basic_allocator.c
+++ b/tests/spec/acsl_basic_allocator.c
@@ -8,7 +8,7 @@
/* This file presents the basic version of the allocator. */
/*****************************************************************************/
-#include "share/libc/stdlib.h"
+#include "stdlib.h"
#define DEFAULT_BLOCK_SIZE 1000
diff --git a/tests/spec/purse.c b/tests/spec/purse.c
index 2d444b25ee4..fdef9a9ee1a 100644
--- a/tests/spec/purse.c
+++ b/tests/spec/purse.c
@@ -21,7 +21,7 @@
/* (enclosed in the file GPL). */
/* */
/**************************************************************************/
-#include "share/libc/stdlib.h"
+#include "stdlib.h"
typedef struct purse {
int balance;
} purse;
diff --git a/tests/syntax/assert_location.c b/tests/syntax/assert_location.c
index b9575ad6a32..d52518141f2 100644
--- a/tests/syntax/assert_location.c
+++ b/tests/syntax/assert_location.c
@@ -1,3 +1,8 @@
+/* run.config
+DEPS: assert_location.h
+
+*/
+
#include "assert_location.h"
void c() {
diff --git "a/tests/syntax/foo\".c" "b/tests/syntax/foo\".c"
index fa4ba0ab9ae..5933f9603a0 100644
--- "a/tests/syntax/foo\".c"
+++ "b/tests/syntax/foo\".c"
@@ -1,4 +1,4 @@
-#include "share/libc/assert.h"
+#include "assert.h"
int test = 1;
diff --git a/tests/syntax/gcc_builtins.c b/tests/syntax/gcc_builtins.c
index d6ff8e598a2..00a9054c8b1 100644
--- a/tests/syntax/gcc_builtins.c
+++ b/tests/syntax/gcc_builtins.c
@@ -2,7 +2,7 @@
STDOPT: +"-machdep gcc_x86_32"
*/
-#include "share/libc/stdint.h"
+#include "stdint.h"
#define likely(x) __builtin_expect((x),1)
#define unlikely(x) __builtin_expect((x),0)
diff --git a/tests/syntax/merge_unused.c b/tests/syntax/merge_unused.c
index b7233c675d0..c8283fabb0a 100644
--- a/tests/syntax/merge_unused.c
+++ b/tests/syntax/merge_unused.c
@@ -1,4 +1,5 @@
/* run.config
+DEPS: merge_unused.h
OPT: -cpp-extra-args="-I@PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c -print
*/
diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c
index 3ac56b12d72..4f782213f01 100644
--- a/tests/syntax/multiple_decls_contracts.c
+++ b/tests/syntax/multiple_decls_contracts.c
@@ -1,7 +1,7 @@
/* run.config
-OPT: share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
-OPT: @PTEST_FILE@ share/libc/string.h @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
-OPT: @PTEST_FILE@ @PTEST_FILE@ share/libc/string.h -cpp-extra-args="-Ishare/libc" -print
+OPT: string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
+OPT: @PTEST_FILE@ string.h @PTEST_FILE@ -cpp-extra-args="-Ishare/libc" -print
+OPT: @PTEST_FILE@ @PTEST_FILE@ string.h -cpp-extra-args="-Ishare/libc" -print
*/
#include "string.h"
diff --git a/tests/syntax/offsetof.c b/tests/syntax/offsetof.c
index 06a79ecae3b..1d378d9b658 100644
--- a/tests/syntax/offsetof.c
+++ b/tests/syntax/offsetof.c
@@ -1,4 +1,4 @@
-#include "share/libc/stddef.h"
+#include "stddef.h"
struct c {char ca;};
void main(void) {
diff --git a/tests/value/CruiseControl.c b/tests/value/CruiseControl.c
index 1a445a21b26..858b6fcc1e7 100644
--- a/tests/value/CruiseControl.c
+++ b/tests/value/CruiseControl.c
@@ -1,4 +1,5 @@
/* run.config*
+ DEPS: CruiseControl.h
GCC:
STDOPT: #"-float-normal CruiseControl_const.c -lib-entry -main CruiseControl -context-depth 10 -context-valid-pointers"
diff --git a/tests/value/CruiseControl_const.c b/tests/value/CruiseControl_const.c
index 92a1f42e65f..7b8f5cf661b 100644
--- a/tests/value/CruiseControl_const.c
+++ b/tests/value/CruiseControl_const.c
@@ -1,4 +1,5 @@
/* run.config*
+ DEPS: CruiseControl.h
GCC:
DONTRUN:
*/
diff --git a/tests/value/abstract_struct_1.c b/tests/value/abstract_struct_1.c
index 3660041bcab..9b66ac139f5 100644
--- a/tests/value/abstract_struct_1.c
+++ b/tests/value/abstract_struct_1.c
@@ -1,7 +1,7 @@
/* run.config*
STDOPT: #"abstract_struct_2.c -lib-entry -eva-msg-key initial-state"
*/
-#include "share/libc/stdlib.h"
+#include "stdlib.h"
struct abstracttype;
struct something {
diff --git a/tests/value/inline.c b/tests/value/inline.c
index b0264d3f0cb..38fccd7c9f2 100644
--- a/tests/value/inline.c
+++ b/tests/value/inline.c
@@ -1,4 +1,5 @@
/* run.config*
+ DEPS: inline.h
DONTRUN: test for the gui only
*/
diff --git a/tests/value/wide_string.c b/tests/value/wide_string.c
index bf27d1585cf..75a975feaec 100644
--- a/tests/value/wide_string.c
+++ b/tests/value/wide_string.c
@@ -1,4 +1,4 @@
-#include "share/libc/stddef.h"
+#include "stddef.h"
int main(volatile int v) {
--
GitLab