From 7f55a56f9f36eb5b3efd2b7d645b564715d90cf4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 24 Sep 2020 12:31:32 +0200
Subject: [PATCH] Fix some oracles
---
tests/builtins/big_local_array.i | 1 +
tests/constant_propagation/bts117.c | 1 +
tests/impact/test_config | 1 +
tests/saveload/load_one.i | 1 +
tests/syntax/aggressive_merging_1.i | 2 +-
tests/syntax/bts0323.c | 1 +
tests/syntax/enum1.c | 1 +
tests/syntax/extern_init.i | 4 +-
tests/syntax/formals_decl_leak.i | 4 +-
tests/syntax/inline_def_1.i | 2 +-
tests/syntax/inline_def_bad_1.i | 2 +-
tests/syntax/merge_inline_1.c | 2 +-
tests/syntax/merge_union.c | 5 +-
tests/syntax/merge_unused.c | 2 +-
tests/syntax/merge_variadic.i | 2 +-
tests/syntax/multiple_decls_contracts.c | 7 +-
.../oracle/aggressive_merging_1.res.oracle | 23 +-
tests/syntax/oracle/anon_enum_libc.res.oracle | 2 +-
.../syntax/oracle/assert_location.res.oracle | 24 +-
tests/syntax/oracle/bts0323.res.oracle | 28 +-
tests/syntax/oracle/cpp-command.0.res.oracle | 2 +-
tests/syntax/oracle/cpp-command.1.res.oracle | 2 +-
tests/syntax/oracle/enum1.res.oracle | 104 ++++-
tests/syntax/oracle/extern_init.0.res.oracle | 44 +-
tests/syntax/oracle/extern_init.1.res.oracle | 44 +-
"tests/syntax/oracle/foo\".res.oracle" | 19 +-
.../oracle/formals_decl_leak.res.oracle | 20 +-
tests/syntax/oracle/gcc_builtins.res.oracle | 376 +++++++++++++++++-
.../oracle/ghost_cv_var_decl.1.res.oracle | 2 +-
tests/syntax/oracle/inline_def_1.res.oracle | 67 +++-
.../syntax/oracle/inline_def_bad_1.res.oracle | 29 +-
tests/syntax/oracle/merge_inline_1.res.oracle | 42 +-
tests/syntax/oracle/merge_union.0.res.oracle | 56 ++-
tests/syntax/oracle/merge_union.1.res.oracle | 39 +-
tests/syntax/oracle/merge_unused.res.oracle | 33 +-
tests/syntax/oracle/merge_variadic.res.oracle | 38 +-
.../multiple_decls_contracts.0.res.oracle | 18 +-
.../multiple_decls_contracts.1.res.oracle | 16 +-
.../multiple_decls_contracts.2.res.oracle | 17 +-
tests/syntax/oracle/offsetof.res.oracle | 17 +-
.../syntax/oracle/static_formals_1.res.oracle | 26 +-
tests/syntax/static_formals_1.c | 3 +-
tests/syntax/unroll_property_status_bts1442.i | 1 +
43 files changed, 1039 insertions(+), 91 deletions(-)
diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index 4fccf6c864f..a7a831f993e 100644
--- a/tests/builtins/big_local_array.i
+++ b/tests/builtins/big_local_array.i
@@ -1,4 +1,5 @@
/* run.config*
+ PLUGIN: report
CMXS: big_local_array_script
OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
OPT: @EVA_OPTIONS@ -load-module big_local_array_script -then-on prj -print -report
diff --git a/tests/constant_propagation/bts117.c b/tests/constant_propagation/bts117.c
index 420cd12e426..6bd80dae89b 100644
--- a/tests/constant_propagation/bts117.c
+++ b/tests/constant_propagation/bts117.c
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: sparecode
OPT: -journal-disable -print
OPT: -journal-disable -semantic-const-folding @EVA_OPTIONS@
OPT: -journal-disable -sparecode-analysis @EVA_OPTIONS@
diff --git a/tests/impact/test_config b/tests/impact/test_config
index c449d18f602..7b96f2e94e5 100644
--- a/tests/impact/test_config
+++ b/tests/impact/test_config
@@ -1 +1,2 @@
+PLUGIN: impact
OPT: -journal-disable -impact-print @EVA_OPTIONS@
diff --git a/tests/saveload/load_one.i b/tests/saveload/load_one.i
index 808418270f6..76c439e6ecb 100644
--- a/tests/saveload/load_one.i
+++ b/tests/saveload/load_one.i
@@ -1,4 +1,5 @@
/* run.config
+ PLUGIN: sparecode
CMXS: @PTEST_NAME@
STDOPT: +"-load-module %{dep:@PTEST_NAME@.cmxs}"
*/
diff --git a/tests/syntax/aggressive_merging_1.i b/tests/syntax/aggressive_merging_1.i
index 78f7123911b..ace8a3820e4 100644
--- a/tests/syntax/aggressive_merging_1.i
+++ b/tests/syntax/aggressive_merging_1.i
@@ -1,5 +1,5 @@
/* run.config
- STDOPT: +"@PTEST_DIR@/aggressive_merging_2.i -aggressive-merging"
+ STDOPT: +"%{dep:aggressive_merging_2.i} -aggressive-merging"
*/
static inline void f(void) {
return;
diff --git a/tests/syntax/bts0323.c b/tests/syntax/bts0323.c
index ccfdfe3bac2..bceea0310e1 100644
--- a/tests/syntax/bts0323.c
+++ b/tests/syntax/bts0323.c
@@ -1,4 +1,5 @@
/* run.config
+ DEPS: bts0323.h
STDOPT: +"bts0323-2.c"
*/
#include "bts0323.h"
diff --git a/tests/syntax/enum1.c b/tests/syntax/enum1.c
index 66de8c52169..42885ad9bdb 100644
--- a/tests/syntax/enum1.c
+++ b/tests/syntax/enum1.c
@@ -1,4 +1,5 @@
/* run.config
+ DEPS: enum.h
STDOPT: +"enum2.c"
*/
diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i
index e6773ed7008..447af8e54b9 100644
--- a/tests/syntax/extern_init.i
+++ b/tests/syntax/extern_init.i
@@ -1,6 +1,6 @@
/* run.config
-OPT: @PTEST_DIR@/@PTEST_NAME@_1.i @PTEST_DIR@/@PTEST_NAME@_2.i -eva @EVA_CONFIG@
-OPT: @PTEST_DIR@/@PTEST_NAME@_2.i @PTEST_DIR@/@PTEST_NAME@_1.i -eva @EVA_CONFIG@
+OPT: %{dep:@PTEST_NAME@_1.i} %{dep:@PTEST_NAME@_2.i} -eva @EVA_CONFIG@
+OPT: %{dep:@PTEST_NAME@_2.i} %{dep:@PTEST_NAME@_1.i} -eva @EVA_CONFIG@
*/
extern int a[] ;
diff --git a/tests/syntax/formals_decl_leak.i b/tests/syntax/formals_decl_leak.i
index c99425be26c..3f91eac76dc 100644
--- a/tests/syntax/formals_decl_leak.i
+++ b/tests/syntax/formals_decl_leak.i
@@ -1,6 +1,6 @@
/* run.config
-CMXS: @PTEST_NAME@
-OPT: -print -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} @PTEST_DIR@/@PTEST_NAME@_1.i
+MODULE: @PTEST_NAME@.cmxs
+OPT: -print %{dep:@PTEST_NAME@_1.i}
*/
void f(int x);
diff --git a/tests/syntax/inline_def_1.i b/tests/syntax/inline_def_1.i
index d9f3bf03143..aaab1cf1b4e 100644
--- a/tests/syntax/inline_def_1.i
+++ b/tests/syntax/inline_def_1.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"@PTEST_DIR@/inline_def_2.i"
+STDOPT: +"%{dep:inline_def_2.i}"
*/
// inline definition can be used in this translation unit, but does not
diff --git a/tests/syntax/inline_def_bad_1.i b/tests/syntax/inline_def_bad_1.i
index 03ee6e12cdd..7d32fc00ea8 100644
--- a/tests/syntax/inline_def_bad_1.i
+++ b/tests/syntax/inline_def_bad_1.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"@PTEST_DIR@/inline_def_bad_2.i"
+STDOPT: +"%{dep:inline_def_bad_2.i}"
*/
extern inline f() { return 1; }
diff --git a/tests/syntax/merge_inline_1.c b/tests/syntax/merge_inline_1.c
index 325b55a258c..685e26d6589 100644
--- a/tests/syntax/merge_inline_1.c
+++ b/tests/syntax/merge_inline_1.c
@@ -1,5 +1,5 @@
/* run.config
-OPT: @PTEST_DIR@/merge_inline_2.c -aggressive-merging -print
+OPT: %{dep:merge_inline_2.c} -aggressive-merging -print
*/
/* Test that we rename properly inlines even if they have prototypes and
diff --git a/tests/syntax/merge_union.c b/tests/syntax/merge_union.c
index 97f4311fa2c..1a58336b780 100644
--- a/tests/syntax/merge_union.c
+++ b/tests/syntax/merge_union.c
@@ -1,6 +1,7 @@
/* run.config
-OPT: -cpp-extra-args="-I @PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c @PTEST_DIR@/@PTEST_NAME@_3.c -print
-OPT: -cpp-extra-args="-I @PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c @PTEST_DIR@/@PTEST_NAME@_3.c -print -kernel-warn-key="linker:drop-conflicting-unused=inactive"
+DEPS: merge_union.h
+OPT: -cpp-extra-args="-I @PTEST_DIR@" %{dep:@PTEST_NAME@_2.c} %{dep:@PTEST_NAME@_3.c} -print
+OPT: -cpp-extra-args="-I @PTEST_DIR@" %{dep:@PTEST_NAME@_2.c} %{dep:@PTEST_NAME@_3.c} -print -kernel-warn-key="linker:drop-conflicting-unused=inactive"
*/
#include "merge_union.h"
diff --git a/tests/syntax/merge_unused.c b/tests/syntax/merge_unused.c
index c8283fabb0a..efe341b8fe4 100644
--- a/tests/syntax/merge_unused.c
+++ b/tests/syntax/merge_unused.c
@@ -1,6 +1,6 @@
/* run.config
DEPS: merge_unused.h
-OPT: -cpp-extra-args="-I@PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c -print
+OPT: -cpp-extra-args="-I@PTEST_DIR@" %{dep:@PTEST_NAME@_2.c} -print
*/
#pragma pack(1)
diff --git a/tests/syntax/merge_variadic.i b/tests/syntax/merge_variadic.i
index dab33541e61..87c31a0cd48 100644
--- a/tests/syntax/merge_variadic.i
+++ b/tests/syntax/merge_variadic.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: @PTEST_DIR@/@PTEST_NAME@_aux.i -print
+OPT: %{dep:@PTEST_NAME@_aux.i} -print
*/
int open (const char* file, int flags, int mode) {
return -1;
diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c
index 4f782213f01..b74e8cad2a6 100644
--- a/tests/syntax/multiple_decls_contracts.c
+++ b/tests/syntax/multiple_decls_contracts.c
@@ -1,7 +1,8 @@
/* run.config
-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
+DEPS: ../../../share/libc/string.h
+OPT: ../../../share/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -print
+OPT: @PTEST_FILE@ ../../../share/libc/string.h @PTEST_FILE@ -print
+OPT: @PTEST_FILE@ @PTEST_FILE@ ../../../share/libc/string.h -print
*/
#include "string.h"
diff --git a/tests/syntax/oracle/aggressive_merging_1.res.oracle b/tests/syntax/oracle/aggressive_merging_1.res.oracle
index 87041b262df..e86b59a796a 100644
--- a/tests/syntax/oracle/aggressive_merging_1.res.oracle
+++ b/tests/syntax/oracle/aggressive_merging_1.res.oracle
@@ -1,2 +1,21 @@
-[kernel] User Error: source file 'aggressive_merging_2.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing aggressive_merging_1.i (no preprocessing)
+[kernel] Parsing aggressive_merging_2.i (no preprocessing)
+/* Generated by Frama-C */
+__inline static void f(void)
+{
+ return;
+}
+
+void foo(void)
+{
+ f();
+ return;
+}
+
+void bar(void)
+{
+ f();
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/anon_enum_libc.res.oracle b/tests/syntax/oracle/anon_enum_libc.res.oracle
index 0cd112010c6..08fb3a9bdcb 100644
--- a/tests/syntax/oracle/anon_enum_libc.res.oracle
+++ b/tests/syntax/oracle/anon_enum_libc.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing anon_enum_libc.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 -I tmp/anon_enum_libc.c7cac46.i' '/home/bobot/Sources/frama-c/_build/default/result/anon_enum_libc.c'
+[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 -I tests/syntax -dD -nostdinc -m32 -o '/tmp/anon_enum_libc.c98bd8a.i' '/home/bobot/Sources/frama-c/_build/default/tests/syntax/result/anon_enum_libc.c'
See chapter "Preparing the Sources" in the Frama-C user manual for more details.
[kernel] User Error: stopping on file "anon_enum_libc.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
diff --git a/tests/syntax/oracle/assert_location.res.oracle b/tests/syntax/oracle/assert_location.res.oracle
index 405f4959172..08097d965c8 100644
--- a/tests/syntax/oracle/assert_location.res.oracle
+++ b/tests/syntax/oracle/assert_location.res.oracle
@@ -1,8 +1,18 @@
[kernel] Parsing assert_location.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/assert_location.c3861fd.i' '/home/bobot/Sources/frama-c/_build/default/result/assert_location.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 "assert_location.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+#include "assert.h"
+void h(void)
+{
+ __FC_assert("I\'m in assert_location.h" != (char const *)0,
+ "assert_location.h",4,"\"I\'m in assert_location.h\"");
+ return;
+}
+
+void c(void)
+{
+ __FC_assert("I\'m in assert_location.c" != (char const *)0,
+ "assert_location.c",9,"\"I\'m in assert_location.c\"");
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/bts0323.res.oracle b/tests/syntax/oracle/bts0323.res.oracle
index 74618c3ab99..f0c9d3cb555 100644
--- a/tests/syntax/oracle/bts0323.res.oracle
+++ b/tests/syntax/oracle/bts0323.res.oracle
@@ -1,8 +1,22 @@
[kernel] Parsing bts0323.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/bts0323.c61bb8a.i' '/home/bobot/Sources/frama-c/_build/default/result/bts0323.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 "bts0323.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing bts0323-2.c (with preprocessing)
+/* Generated by Frama-C */
+int x;
+
+void g(void);
+
+void f(void)
+{
+ x = 0;
+ return;
+}
+
+int x = 1;
+/*@ ensures x ≢ 0; */
+void g(void)
+{
+ x = 2;
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/cpp-command.0.res.oracle b/tests/syntax/oracle/cpp-command.0.res.oracle
index 917d74c3240..55dc2642deb 100644
--- a/tests/syntax/oracle/cpp-command.0.res.oracle
+++ b/tests/syntax/oracle/cpp-command.0.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing cpp-command.c (with preprocessing)
-[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [/tmp/cpp-command.c94773e.i /tmp/cpp-command.c94773e.i /tmp/cpp-command.c94773e.i /tmp/cpp-command.c94773e.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]
+[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [/tmp/cpp-command.cd485c4.i /tmp/cpp-command.cd485c4.i /tmp/cpp-command.cd485c4.i /tmp/cpp-command.cd485c4.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]
diff --git a/tests/syntax/oracle/cpp-command.1.res.oracle b/tests/syntax/oracle/cpp-command.1.res.oracle
index d46ae6220e3..afdf8e4c586 100644
--- a/tests/syntax/oracle/cpp-command.1.res.oracle
+++ b/tests/syntax/oracle/cpp-command.1.res.oracle
@@ -1,2 +1,2 @@
[kernel] Parsing cpp-command.c (with preprocessing)
-%1 = cpp-command.c %2 = /tmp/cpp-command.c95395d.i %args = -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32
+%1 = cpp-command.c %2 = /tmp/cpp-command.c125b21.i %args = -I/home/bobot/Sources/frama-c/_build/install/default/share/frama-c/share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32
diff --git a/tests/syntax/oracle/enum1.res.oracle b/tests/syntax/oracle/enum1.res.oracle
index 1833d9150a4..73766d556e6 100644
--- a/tests/syntax/oracle/enum1.res.oracle
+++ b/tests/syntax/oracle/enum1.res.oracle
@@ -1,8 +1,98 @@
[kernel] Parsing enum1.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/enum1.c8c47b1.i' '/home/bobot/Sources/frama-c/_build/default/result/enum1.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 "enum1.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing enum2.c (with preprocessing)
+[kernel] Warning: merging definitions of enum f using int type
+ (different names for enumeration items); items {F21=0, F22=1} and {F11=0,
+ F12=1}
+/* Generated by Frama-C */
+enum e {
+ E1 = 0,
+ E2 = 1
+};
+enum __anonenum_1 {
+ K11 = 0,
+ K12 = 1
+};
+enum __anonenum_3 {
+ I1 = 0,
+ I2 = 1
+};
+enum Foo {
+ EN1 = 0,
+ EN2 = 1,
+ EN3 = 2
+};
+enum __anonenum_0 {
+ K21 = 0,
+ K22 = 1
+};
+int e1(void)
+{
+ int __retres;
+ __retres = E1;
+ return __retres;
+}
+
+int f1(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+int k1(void)
+{
+ int __retres;
+ __retres = K11;
+ return __retres;
+}
+
+int i1(void)
+{
+ int __retres;
+ __retres = I1;
+ return __retres;
+}
+
+int f(void)
+{
+ int __retres;
+ __retres = ! EN1;
+ return __retres;
+}
+
+int g(void)
+{
+ int __retres;
+ __retres = EN1;
+ return __retres;
+}
+
+int e2(void)
+{
+ int __retres;
+ __retres = E2;
+ return __retres;
+}
+
+int f2(void)
+{
+ int __retres;
+ __retres = 1;
+ return __retres;
+}
+
+int k2(void)
+{
+ int __retres;
+ __retres = K22;
+ return __retres;
+}
+
+int i2(void)
+{
+ int __retres;
+ __retres = I2;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/extern_init.0.res.oracle b/tests/syntax/oracle/extern_init.0.res.oracle
index 5fc22e8c454..bb61fd575af 100644
--- a/tests/syntax/oracle/extern_init.0.res.oracle
+++ b/tests/syntax/oracle/extern_init.0.res.oracle
@@ -1,2 +1,42 @@
-[kernel] User Error: source file 'extern_init_1.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing extern_init.i (no preprocessing)
+[kernel] Parsing extern_init_1.i (no preprocessing)
+[kernel] Parsing extern_init_2.i (no preprocessing)
+[kernel:typing:no-proto] extern_init_2.i:10: Warning:
+ Calling function f that is declared without prototype.
+ Its formals will be inferred from actual arguments
+[kernel:typing:no-proto] extern_init_2.i:11: Warning:
+ Calling function g that is declared without prototype.
+ Its formals will be inferred from actual arguments
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ a[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ [3] ∈ {4}
+ [4] ∈ {5}
+[eva] computing for function f <- main.
+ Called from extern_init_2.i:10.
+[eva] Recording results for f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from extern_init_2.i:11.
+[eva] using specification for function g
+[eva] Done for function g
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function f:
+ a[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {12}
+ [3] ∈ {4}
+ [4] ∈ {5}
+[eva:final-states] Values at end of function main:
+ a[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {12}
+ [3] ∈ [--..--]
+ [4] ∈ {5}
+ __retres ∈ {2}
diff --git a/tests/syntax/oracle/extern_init.1.res.oracle b/tests/syntax/oracle/extern_init.1.res.oracle
index ff82c0c294f..406e5de193e 100644
--- a/tests/syntax/oracle/extern_init.1.res.oracle
+++ b/tests/syntax/oracle/extern_init.1.res.oracle
@@ -1,2 +1,42 @@
-[kernel] User Error: source file 'extern_init_2.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing extern_init.i (no preprocessing)
+[kernel] Parsing extern_init_2.i (no preprocessing)
+[kernel:typing:no-proto] extern_init_2.i:10: Warning:
+ Calling function f that is declared without prototype.
+ Its formals will be inferred from actual arguments
+[kernel:typing:no-proto] extern_init_2.i:11: Warning:
+ Calling function g that is declared without prototype.
+ Its formals will be inferred from actual arguments
+[kernel] Parsing extern_init_1.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ a[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ [3] ∈ {4}
+ [4] ∈ {5}
+[eva] computing for function f <- main.
+ Called from extern_init_2.i:10.
+[eva] Recording results for f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from extern_init_2.i:11.
+[eva] using specification for function g
+[eva] Done for function g
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function f:
+ a[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {12}
+ [3] ∈ {4}
+ [4] ∈ {5}
+[eva:final-states] Values at end of function main:
+ a[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {12}
+ [3] ∈ [--..--]
+ [4] ∈ {5}
+ __retres ∈ {2}
diff --git "a/tests/syntax/oracle/foo\".res.oracle" "b/tests/syntax/oracle/foo\".res.oracle"
index be5b52fd076..9f5882a42c2 100644
--- "a/tests/syntax/oracle/foo\".res.oracle"
+++ "b/tests/syntax/oracle/foo\".res.oracle"
@@ -1,8 +1,13 @@
[kernel] Parsing foo".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/foo".c43a120.i' '/home/bobot/Sources/frama-c/_build/default/result/foo".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 "foo\".c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+#include "assert.h"
+int test = 1;
+int main(void)
+{
+ int __retres;
+ __FC_assert(test != 0,"foo\".c",6,"test");
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/formals_decl_leak.res.oracle b/tests/syntax/oracle/formals_decl_leak.res.oracle
index 0215cf0453e..88bc286cdc4 100644
--- a/tests/syntax/oracle/formals_decl_leak.res.oracle
+++ b/tests/syntax/oracle/formals_decl_leak.res.oracle
@@ -1,2 +1,18 @@
-[kernel] User Error: source file 'formals_decl_leak_1.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing formals_decl_leak.i (no preprocessing)
+[kernel] Parsing formals_decl_leak_1.i (no preprocessing)
+/* Generated by Frama-C */
+void f(int x);
+
+void g(void)
+{
+ f(3);
+ return;
+}
+
+void h(void)
+{
+ f(4);
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/gcc_builtins.res.oracle b/tests/syntax/oracle/gcc_builtins.res.oracle
index 5af6107b14b..3288584e07b 100644
--- a/tests/syntax/oracle/gcc_builtins.res.oracle
+++ b/tests/syntax/oracle/gcc_builtins.res.oracle
@@ -1,8 +1,370 @@
[kernel] Parsing gcc_builtins.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_GCC_X86_32 -dD -nostdinc -m32 -o '/tmp/gcc_builtins.ce908f3.i' '/home/bobot/Sources/frama-c/_build/default/result/gcc_builtins.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 "gcc_builtins.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+#include "stdint.h"
+/* compiler builtin:
+ short __sync_add_and_fetch_int16_t(short volatile *ptr, short value,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_add_and_fetch_int32_t(int volatile *ptr, int value,
+ void * const *__va_params); */
+/* compiler builtin:
+ long long __sync_add_and_fetch_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_bool_compare_and_swap_uint16_t(unsigned short volatile *ptr,
+ unsigned short oldval,
+ unsigned short newval,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_bool_compare_and_swap_uint32_t(unsigned int volatile *ptr,
+ unsigned int oldval,
+ unsigned int newval,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_bool_compare_and_swap_uint64_t(unsigned long long volatile *ptr,
+ unsigned long long oldval,
+ unsigned long long newval,
+ void * const *__va_params); */
+/* compiler builtin:
+ short __sync_fetch_and_add_int16_t(short volatile *ptr, short value,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_fetch_and_add_int32_t(int volatile *ptr, int value,
+ void * const *__va_params); */
+/* compiler builtin:
+ long long __sync_fetch_and_add_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params); */
+/* compiler builtin:
+ short __sync_fetch_and_sub_int16_t(short volatile *ptr, short value,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_fetch_and_sub_int32_t(int volatile *ptr, int value,
+ void * const *__va_params); */
+/* compiler builtin:
+ long long __sync_fetch_and_sub_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params); */
+/* compiler builtin:
+ short __sync_sub_and_fetch_int16_t(short volatile *ptr, short value,
+ void * const *__va_params); */
+/* compiler builtin:
+ int __sync_sub_and_fetch_int32_t(int volatile *ptr, int value,
+ void * const *__va_params); */
+/* compiler builtin:
+ long long __sync_sub_and_fetch_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params); */
+short __sync_fetch_and_add_int16_t(short volatile *ptr, short value,
+ void * const *__va_params)
+{
+ int16_t tmp = *ptr;
+ *ptr = (short)((int)*ptr + (int)value);
+ return tmp;
+}
+
+short __sync_fetch_and_sub_int16_t(short volatile *ptr, short value,
+ void * const *__va_params)
+{
+ int16_t tmp = *ptr;
+ *ptr = (short)((int)*ptr - (int)value);
+ return tmp;
+}
+
+int __sync_fetch_and_add_int32_t(int volatile *ptr, int value,
+ void * const *__va_params)
+{
+ int32_t tmp = *ptr;
+ *ptr += value;
+ return tmp;
+}
+
+int __sync_fetch_and_sub_int32_t(int volatile *ptr, int value,
+ void * const *__va_params)
+{
+ int32_t tmp = *ptr;
+ *ptr -= value;
+ return tmp;
+}
+
+long long __sync_fetch_and_add_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params)
+{
+ int64_t tmp = *ptr;
+ *ptr += value;
+ return tmp;
+}
+
+long long __sync_fetch_and_sub_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params)
+{
+ int64_t tmp = *ptr;
+ *ptr -= value;
+ return tmp;
+}
+
+short __sync_add_and_fetch_int16_t(short volatile *ptr, short value,
+ void * const *__va_params)
+{
+ short __retres;
+ *ptr = (short)((int)*ptr + (int)value);
+ __retres = *ptr;
+ return __retres;
+}
+
+short __sync_sub_and_fetch_int16_t(short volatile *ptr, short value,
+ void * const *__va_params)
+{
+ short __retres;
+ *ptr = (short)((int)*ptr - (int)value);
+ __retres = *ptr;
+ return __retres;
+}
+
+int __sync_add_and_fetch_int32_t(int volatile *ptr, int value,
+ void * const *__va_params)
+{
+ int __retres;
+ *ptr += value;
+ __retres = *ptr;
+ return __retres;
+}
+
+int __sync_sub_and_fetch_int32_t(int volatile *ptr, int value,
+ void * const *__va_params)
+{
+ int __retres;
+ *ptr -= value;
+ __retres = *ptr;
+ return __retres;
+}
+
+long long __sync_add_and_fetch_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params)
+{
+ long long __retres;
+ *ptr += value;
+ __retres = *ptr;
+ return __retres;
+}
+
+long long __sync_sub_and_fetch_int64_t(long long volatile *ptr,
+ long long value,
+ void * const *__va_params)
+{
+ long long __retres;
+ *ptr -= value;
+ __retres = *ptr;
+ return __retres;
+}
+
+int __sync_bool_compare_and_swap_uint16_t(unsigned short volatile *ptr,
+ unsigned short oldval,
+ unsigned short newval,
+ void * const *__va_params)
+{
+ int __retres;
+ if ((int)*ptr == (int)oldval) {
+ *ptr = newval;
+ __retres = 1;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
+int __sync_bool_compare_and_swap_uint32_t(unsigned int volatile *ptr,
+ unsigned int oldval,
+ unsigned int newval,
+ void * const *__va_params)
+{
+ int __retres;
+ if (*ptr == oldval) {
+ *ptr = newval;
+ __retres = 1;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
+int __sync_bool_compare_and_swap_uint64_t(unsigned long long volatile *ptr,
+ unsigned long long oldval,
+ unsigned long long newval,
+ void * const *__va_params)
+{
+ int __retres;
+ if (*ptr == oldval) {
+ *ptr = newval;
+ __retres = 1;
+ goto return_label;
+ }
+ else {
+ __retres = 0;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
+void main(void)
+{
+ int tmp;
+ {
+ int16_t result;
+ int16_t content = (short)100;
+ int16_t volatile *ptr = (int16_t volatile *)(& content);
+ int16_t value = (short)33;
+ {
+ void *__va_args[1] = {(void *)0};
+ result = __sync_fetch_and_add_int16_t(ptr,value,
+ (void * const *)(__va_args));
+ }
+ /*@ assert result ≡ 100 ∧ content ≡ 133; */ ;
+ {
+ void *__va_args_35[1] = {(void *)0};
+ result = __sync_fetch_and_add_int16_t(ptr,(short)(-11),
+ (void * const *)(__va_args_35));
+ }
+ /*@ assert result ≡ 133 ∧ content ≡ 122; */ ;
+ {
+ void *__va_args_37[1] = {(void *)0};
+ result = __sync_fetch_and_sub_int16_t(ptr,value,
+ (void * const *)(__va_args_37));
+ }
+ /*@ assert result ≡ 122 ∧ content ≡ 89; */ ;
+ {
+ void *__va_args_39[1] = {(void *)0};
+ result = __sync_fetch_and_sub_int16_t(ptr,(short)(-11),
+ (void * const *)(__va_args_39));
+ }
+ /*@ assert result ≡ 89 ∧ content ≡ 100; */ ;
+ }
+ {
+ int32_t result_0;
+ int32_t content_0 = 100;
+ int32_t volatile *ptr_0 = (int32_t volatile *)(& content_0);
+ int32_t value_0 = 33;
+ {
+ void *__va_args_41[1] = {(void *)0};
+ result_0 = __sync_fetch_and_add_int32_t(ptr_0,value_0,
+ (void * const *)(__va_args_41));
+ }
+ /*@ assert result_0 ≡ 100 ∧ content_0 ≡ 133; */ ;
+ {
+ void *__va_args_43[1] = {(void *)0};
+ result_0 = __sync_fetch_and_add_int32_t(ptr_0,-11,
+ (void * const *)(__va_args_43));
+ }
+ /*@ assert result_0 ≡ 133 ∧ content_0 ≡ 122; */ ;
+ {
+ void *__va_args_45[1] = {(void *)0};
+ result_0 = __sync_fetch_and_sub_int32_t(ptr_0,value_0,
+ (void * const *)(__va_args_45));
+ }
+ /*@ assert result_0 ≡ 122 ∧ content_0 ≡ 89; */ ;
+ {
+ void *__va_args_47[1] = {(void *)0};
+ result_0 = __sync_fetch_and_sub_int32_t(ptr_0,-11,
+ (void * const *)(__va_args_47));
+ }
+ /*@ assert result_0 ≡ 89 ∧ content_0 ≡ 100; */ ;
+ }
+ {
+ int64_t result_1;
+ int64_t content_1 = (long long)100;
+ int64_t volatile *ptr_1 = (int64_t volatile *)(& content_1);
+ int64_t value_1 = (long long)33;
+ {
+ void *__va_args_49[1] = {(void *)0};
+ result_1 = __sync_fetch_and_add_int64_t(ptr_1,value_1,
+ (void * const *)(__va_args_49));
+ }
+ /*@ assert result_1 ≡ 100 ∧ content_1 ≡ 133; */ ;
+ {
+ void *__va_args_51[1] = {(void *)0};
+ result_1 = __sync_fetch_and_add_int64_t(ptr_1,(long long)(-11),
+ (void * const *)(__va_args_51));
+ }
+ /*@ assert result_1 ≡ 133 ∧ content_1 ≡ 122; */ ;
+ {
+ void *__va_args_53[1] = {(void *)0};
+ result_1 = __sync_fetch_and_sub_int64_t(ptr_1,value_1,
+ (void * const *)(__va_args_53));
+ }
+ /*@ assert result_1 ≡ 122 ∧ content_1 ≡ 89; */ ;
+ {
+ void *__va_args_55[1] = {(void *)0};
+ result_1 = __sync_fetch_and_sub_int64_t(ptr_1,(long long)(-11),
+ (void * const *)(__va_args_55));
+ }
+ /*@ assert result_1 ≡ 89 ∧ content_1 ≡ 100; */ ;
+ }
+ {
+ int result_2;
+ uint16_t content_2 = (unsigned short)100;
+ uint16_t volatile *ptr_2 = (uint16_t volatile *)(& content_2);
+ uint16_t oldval = (unsigned short)100;
+ uint16_t newval = (unsigned short)133;
+ {
+ void *__va_args_57[1] = {(void *)0};
+ result_2 = __sync_bool_compare_and_swap_uint16_t(ptr_2,oldval,newval,
+ (void * const *)(__va_args_57));
+ }
+ /*@ assert result_2 ≡ 1 ∧ *ptr_2 ≡ newval; */ ;
+ }
+ {
+ int result_3;
+ uint32_t content_3 = (unsigned int)100;
+ uint32_t volatile *ptr_3 = (uint32_t volatile *)(& content_3);
+ uint32_t oldval_0 = (unsigned int)100;
+ uint32_t newval_0 = (unsigned int)133;
+ {
+ void *__va_args_59[1] = {(void *)0};
+ result_3 = __sync_bool_compare_and_swap_uint32_t(ptr_3,oldval_0,
+ newval_0,
+ (void * const *)(__va_args_59));
+ }
+ /*@ assert result_3 ≡ 1 ∧ *ptr_3 ≡ newval_0; */ ;
+ }
+ {
+ int result_4;
+ uint64_t content_4 = (unsigned long long)100;
+ uint64_t volatile *ptr_4 = (uint64_t volatile *)(& content_4);
+ uint64_t oldval_1 = (unsigned long long)100;
+ uint64_t newval_1 = (unsigned long long)133;
+ {
+ void *__va_args_61[1] = {(void *)0};
+ result_4 = __sync_bool_compare_and_swap_uint64_t(ptr_4,oldval_1,
+ newval_1,
+ (void * const *)(__va_args_61));
+ }
+ /*@ assert result_4 ≡ 1 ∧ *ptr_4 ≡ newval_1; */ ;
+ }
+ if ((long)(4 == 4)) {
+ int x = 1;
+ }
+ if ((long)(3 == 4)) {
+ int x_0 = 0;
+ }
+ int x_1 = 2;
+ ;
+ tmp = x_1;
+ x_1 ++;
+ ;
+ if ((long)tmp) {
+ int y = x_1;
+ }
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
index c67be6ea2be..b940344e139 100644
--- a/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
@@ -1,3 +1,3 @@
-[kernel] User Error: Missing source file 'ghost_cv_var_decl.ml'
+[kernel] User Error: Missing source file 'tests/syntax/ghost_cv_var_decl.ml'
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inline_def_1.res.oracle b/tests/syntax/oracle/inline_def_1.res.oracle
index 6261d028e99..9fe39d03c1c 100644
--- a/tests/syntax/oracle/inline_def_1.res.oracle
+++ b/tests/syntax/oracle/inline_def_1.res.oracle
@@ -1,2 +1,65 @@
-[kernel] User Error: source file 'inline_def_2.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing inline_def_1.i (no preprocessing)
+[kernel] Parsing inline_def_2.i (no preprocessing)
+/* Generated by Frama-C */
+__inline static int f__fc_inline(int x)
+{
+ return x;
+}
+
+__inline int f(int x);
+
+__inline static int f1__fc_inline(void)
+{
+ int __retres;
+ __retres = 1;
+ return __retres;
+}
+
+extern int f2(void)
+{
+ int __retres;
+ __retres = 3;
+ return __retres;
+}
+
+int g(int x)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ int tmp_1;
+ tmp = f__fc_inline(x);
+ tmp_0 = f1__fc_inline();
+ tmp_1 = f2();
+ __retres = (tmp + tmp_0) + tmp_1;
+ return __retres;
+}
+
+__inline int f(int x)
+{
+ int __retres;
+ __retres = x + 1;
+ return __retres;
+}
+
+__inline static int f1__fc_inline_0(void)
+{
+ int __retres;
+ __retres = 2;
+ return __retres;
+}
+
+int h(int x)
+{
+ int __retres;
+ int tmp;
+ int tmp_0;
+ int tmp_1;
+ tmp = f(x);
+ tmp_0 = f1__fc_inline_0();
+ tmp_1 = f2();
+ __retres = (tmp + tmp_0) + tmp_1;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/inline_def_bad_1.res.oracle b/tests/syntax/oracle/inline_def_bad_1.res.oracle
index c2e39d67bc9..e0f7e8f2d4d 100644
--- a/tests/syntax/oracle/inline_def_bad_1.res.oracle
+++ b/tests/syntax/oracle/inline_def_bad_1.res.oracle
@@ -1,2 +1,27 @@
-[kernel] User Error: source file 'inline_def_bad_2.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing inline_def_bad_1.i (no preprocessing)
+[kernel] Parsing inline_def_bad_2.i (no preprocessing)
+[kernel] inline_def_bad_2.i:6: Warning:
+ dropping duplicate def'n of func f at inline_def_bad_2.i:6 in favor of that at inline_def_bad_1.i:5
+/* Generated by Frama-C */
+extern int f(void)
+{
+ int __retres;
+ __retres = 1;
+ return __retres;
+}
+
+int g(void)
+{
+ int tmp;
+ tmp = f();
+ return tmp;
+}
+
+int h(void)
+{
+ int tmp;
+ tmp = f();
+ return tmp;
+}
+
+
diff --git a/tests/syntax/oracle/merge_inline_1.res.oracle b/tests/syntax/oracle/merge_inline_1.res.oracle
index c868848607c..483e5ebe8fc 100644
--- a/tests/syntax/oracle/merge_inline_1.res.oracle
+++ b/tests/syntax/oracle/merge_inline_1.res.oracle
@@ -1,2 +1,40 @@
-[kernel] User Error: source file 'merge_inline_2.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing merge_inline_1.c (with preprocessing)
+[kernel] Parsing merge_inline_2.c (with preprocessing)
+/* Generated by Frama-C */
+int foo(int x);
+
+int foo(int x)
+{
+ return x;
+}
+
+int getfoo2(void);
+
+int main(void)
+{
+ int __retres;
+ int tmp;
+ tmp = getfoo2();
+ if (tmp != (int)(& foo)) {
+ __retres = 1;
+ goto return_label;
+ }
+ __retres = 0;
+ return_label: return __retres;
+}
+
+int bar(int x);
+
+int getfoo2(void)
+{
+ int __retres;
+ __retres = (int)(& bar);
+ return __retres;
+}
+
+int bar(int x)
+{
+ return x;
+}
+
+
diff --git a/tests/syntax/oracle/merge_union.0.res.oracle b/tests/syntax/oracle/merge_union.0.res.oracle
index f93871d21f3..3b7606d2227 100644
--- a/tests/syntax/oracle/merge_union.0.res.oracle
+++ b/tests/syntax/oracle/merge_union.0.res.oracle
@@ -1,2 +1,54 @@
-[kernel] User Error: source file 'merge_union_2.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing merge_union.c (with preprocessing)
+[kernel] Parsing merge_union_2.c (with preprocessing)
+[kernel] Parsing merge_union_3.c (with preprocessing)
+[kernel:linker:drop-conflicting-unused] Warning:
+ Incompatible declaration for G1:
+ Definitions of type st are not isomorphic. Reason follows:
+ Definitions of struct __anonstruct_st_2 are not isomorphic. Reason follows:
+ incompatible attributes in composite types and/or field u
+ struct __anonstruct_st_2 {
+ char c ;
+ un u ;
+ };
+ struct __anonstruct_st_2 {
+ char c __attribute__((__aligned__(1)));
+ un u __attribute__((__aligned__(1)));
+ } __attribute__((__packed__, __aligned__(1)));
+
+ First declaration was at merge_union.h:11
+ Current declaration is at merge_union.h:11
+ Old declaration is unused, silently removing it
+/* Generated by Frama-C */
+union __anonunion_un_1 {
+ char t ;
+ short s ;
+} __attribute__((__packed__, __aligned__(1)));
+typedef union __anonunion_un_1 un;
+struct __anonstruct_st_3 {
+ char c __attribute__((__aligned__(1)));
+ un u __attribute__((__aligned__(1)));
+} __attribute__((__packed__, __aligned__(1)));
+typedef struct __anonstruct_st_3 st_2;
+int f(un *u);
+
+#pragma noalign
+extern st_2 G1;
+
+int g(un *u)
+{
+ int __retres;
+ f(& G1.u);
+ __retres = 0;
+ return __retres;
+}
+
+#pragma noalign
+int main(un *u)
+{
+ int __retres;
+ g(& G1.u);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/merge_union.1.res.oracle b/tests/syntax/oracle/merge_union.1.res.oracle
index f93871d21f3..eaf782054af 100644
--- a/tests/syntax/oracle/merge_union.1.res.oracle
+++ b/tests/syntax/oracle/merge_union.1.res.oracle
@@ -1,2 +1,37 @@
-[kernel] User Error: source file 'merge_union_2.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing merge_union.c (with preprocessing)
+[kernel] Parsing merge_union_2.c (with preprocessing)
+[kernel] Parsing merge_union_3.c (with preprocessing)
+/* Generated by Frama-C */
+union __anonunion_un_1 {
+ char t ;
+ short s ;
+} __attribute__((__packed__, __aligned__(1)));
+typedef union __anonunion_un_1 un;
+struct __anonstruct_st_3 {
+ char c __attribute__((__aligned__(1)));
+ un u __attribute__((__aligned__(1)));
+} __attribute__((__packed__, __aligned__(1)));
+typedef struct __anonstruct_st_3 st_2;
+int f(un *u);
+
+#pragma noalign
+extern st_2 G1;
+
+int g(un *u)
+{
+ int __retres;
+ f(& G1.u);
+ __retres = 0;
+ return __retres;
+}
+
+#pragma noalign
+int main(un *u)
+{
+ int __retres;
+ g(& G1.u);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/merge_unused.res.oracle b/tests/syntax/oracle/merge_unused.res.oracle
index 7c96b12f0fc..7eb68c12cd1 100644
--- a/tests/syntax/oracle/merge_unused.res.oracle
+++ b/tests/syntax/oracle/merge_unused.res.oracle
@@ -1,2 +1,33 @@
-[kernel] User Error: source file 'merge_unused_2.c' does not exist
+[kernel] Parsing merge_unused.c (with preprocessing)
+[kernel] Parsing merge_unused_2.c (with preprocessing)
+[kernel:linker:drop-conflicting-unused] Warning:
+ Incompatible declaration for G1:
+ Definitions of struct s are not isomorphic. Reason follows:
+ incompatible attributes in composite types and/or field i
+ struct s {
+ char c __attribute__((__aligned__(1)));
+ int i __attribute__((__aligned__(1)));
+ } __attribute__((__packed__, __aligned__(1)));
+ struct s {
+ char c ;
+ int i ;
+ };
+
+ First declaration was at merge_unused.c:12
+ Current declaration is at merge_unused.h:7
+ Current declaration is unused, silently removing it
+[kernel] User Error: Incompatible declaration for G3:
+ Definitions of struct s are not isomorphic. Reason follows:
+ incompatible attributes in composite types and/or field i
+ struct s {
+ char c __attribute__((__aligned__(1)));
+ int i __attribute__((__aligned__(1)));
+ } __attribute__((__packed__, __aligned__(1)));
+ struct s {
+ char c ;
+ int i ;
+ };
+
+ First declaration was at merge_unused.h:9
+ Current declaration is at merge_unused.h:9
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/merge_variadic.res.oracle b/tests/syntax/oracle/merge_variadic.res.oracle
index 0ad28539269..7cc4becf9e2 100644
--- a/tests/syntax/oracle/merge_variadic.res.oracle
+++ b/tests/syntax/oracle/merge_variadic.res.oracle
@@ -1,2 +1,36 @@
-[kernel] User Error: source file 'merge_variadic_aux.i' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing merge_variadic.i (no preprocessing)
+[kernel] Parsing merge_variadic_aux.i (no preprocessing)
+[kernel:linker:drop-conflicting-unused] Warning:
+ Incompatible declaration for open:
+ different vararg specifiers
+ First declaration was at merge_variadic.i:4
+ Current declaration is at merge_variadic_aux.i:5
+ Current declaration is unused, silently removing it
+[kernel:linker:drop-conflicting-unused] Warning:
+ Incompatible declaration for foo:
+ different vararg specifiers
+ First declaration was at merge_variadic.i:8
+ Current declaration is at merge_variadic_aux.i:8
+ Old declaration is unused, silently removing it
+/* Generated by Frama-C */
+int open(char const *file, int flags, int mode)
+{
+ int __retres;
+ __retres = -1;
+ return __retres;
+}
+
+extern int foo(int x, void * const *__va_params);
+
+int bar(void)
+{
+ int tmp;
+ {
+ int __va_arg0 = 4;
+ void *__va_args[1] = {& __va_arg0};
+ tmp = foo(3,(void * const *)(__va_args));
+ }
+ return tmp;
+}
+
+
diff --git a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle
index 673ba94c603..1f940c2ffdf 100644
--- a/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle
+++ b/tests/syntax/oracle/multiple_decls_contracts.0.res.oracle
@@ -1,2 +1,16 @@
-[kernel] User Error: source file 'share/libc/string.h' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing /home/bobot/Sources/frama-c/_build/default/share/libc/string.h (with preprocessing)
+[kernel] Parsing multiple_decls_contracts.c (with preprocessing)
+[kernel] Parsing multiple_decls_contracts.c (with preprocessing)
+[kernel] multiple_decls_contracts.c:11: Warning:
+ dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11
+/* Generated by Frama-C */
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_alloc_axiomatic.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_define_size_t.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_define_wchar_t.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_string_axiomatic.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/string.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/strings.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+
diff --git a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle
index 673ba94c603..5be71f76406 100644
--- a/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle
+++ b/tests/syntax/oracle/multiple_decls_contracts.1.res.oracle
@@ -1,2 +1,14 @@
-[kernel] User Error: source file 'share/libc/string.h' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing multiple_decls_contracts.c (with preprocessing)
+[kernel] Parsing /home/bobot/Sources/frama-c/_build/default/share/libc/string.h (with preprocessing)
+[kernel] Parsing multiple_decls_contracts.c (with preprocessing)
+[kernel] multiple_decls_contracts.c:11: Warning:
+ dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11
+/* Generated by Frama-C */
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_alloc_axiomatic.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/string.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/strings.h"
+#include "stddef.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+
diff --git a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle
index 673ba94c603..0eb3fb7b6a3 100644
--- a/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle
+++ b/tests/syntax/oracle/multiple_decls_contracts.2.res.oracle
@@ -1,2 +1,15 @@
-[kernel] User Error: source file 'share/libc/string.h' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing multiple_decls_contracts.c (with preprocessing)
+[kernel] Parsing multiple_decls_contracts.c (with preprocessing)
+[kernel] Parsing /home/bobot/Sources/frama-c/_build/default/share/libc/string.h (with preprocessing)
+[kernel] multiple_decls_contracts.c:11: Warning:
+ dropping duplicate def'n of func strdup at multiple_decls_contracts.c:11 in favor of that at multiple_decls_contracts.c:11
+/* Generated by Frama-C */
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_alloc_axiomatic.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/__fc_string_axiomatic.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/string.h"
+#include "/home/bobot/Sources/frama-c/_build/default/share/libc/strings.h"
+#include "stddef.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+
diff --git a/tests/syntax/oracle/offsetof.res.oracle b/tests/syntax/oracle/offsetof.res.oracle
index 56ad6d38938..92420e1afe8 100644
--- a/tests/syntax/oracle/offsetof.res.oracle
+++ b/tests/syntax/oracle/offsetof.res.oracle
@@ -1,8 +1,11 @@
[kernel] Parsing offsetof.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/offsetof.c3510db.i' '/home/bobot/Sources/frama-c/_build/default/result/offsetof.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 "offsetof.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+/* Generated by Frama-C */
+#include "stddef.h"
+void main(void)
+{
+ size_t S;
+ S = 0U;
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index 5123b8dc0f1..bcf018e8e29 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -1,2 +1,24 @@
-[kernel] User Error: source file 'static_formals_2.c' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing static_formals_1.c (with preprocessing)
+[kernel] Parsing static_formals_2.c (with preprocessing)
+/* Generated by Frama-C */
+/*@ requires /* vid:23, lvid:23 */x < 10; */
+static int /* vid:56 */f(int /* vid:23, lvid:23 */x);
+
+int /* vid:28 */g(void)
+{
+ int /* vid:29 */tmp;
+ /* vid:29 */tmp = /* vid:56 */f(4);
+ return /* vid:29 */tmp;
+}
+
+/*@ requires /* vid:51, lvid:51 */x < 10; */
+static int /* vid:57 */f_0(int /* vid:51, lvid:51 */x);
+
+int /* vid:54 */h(void)
+{
+ int /* vid:55 */tmp;
+ /* vid:55 */tmp = /* vid:57 */f_0(6);
+ return /* vid:55 */tmp;
+}
+
+
diff --git a/tests/syntax/static_formals_1.c b/tests/syntax/static_formals_1.c
index 6cd8687eba1..9197ebfc489 100644
--- a/tests/syntax/static_formals_1.c
+++ b/tests/syntax/static_formals_1.c
@@ -1,5 +1,6 @@
/* run.config
-STDOPT: +"@PTEST_DIR@/static_formals_2.c" +"-cpp-extra-args=\"-I @PTEST_DIR@\"" +"-kernel-msg-key printer:vid"
+DEPS: static_formals.h
+STDOPT: +"%{dep:static_formals_2.c}" +"-cpp-extra-args=\"-I @PTEST_DIR@\"" +"-kernel-msg-key printer:vid"
*/
#include "static_formals.h"
diff --git a/tests/syntax/unroll_property_status_bts1442.i b/tests/syntax/unroll_property_status_bts1442.i
index 70ac3a9bbaf..c9072a007e7 100644
--- a/tests/syntax/unroll_property_status_bts1442.i
+++ b/tests/syntax/unroll_property_status_bts1442.i
@@ -1,4 +1,5 @@
/* run.config
+PLUGIN: report
OPT: -report
OPT: -ulevel -1 -report
*/
--
GitLab