diff --git a/tests/builtins/big_local_array.i b/tests/builtins/big_local_array.i
index 4fccf6c864f4077c49caf9bc13047919cb2c8293..a7a831f993e17349b622711fe7984a9fe522e13a 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 420cd12e426c82096ca8e4d57efc742b1e5258c8..6bd80dae89ba5fca169d028df47296559777ca93 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 c449d18f602ef2fe815b38e0f2cdc3d467e1c815..7b96f2e94e51cab584607da322f0d34ba46a8ec5 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 808418270f62f5e06476eb9e50fd35f20863a238..76c439e6ecb48dd96df0b2080d0708b32235087f 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 78f7123911b96029ba8f65fb1f55b78808c3cf65..ace8a3820e4b96eb6a92968f52328e378054de93 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 ccfdfe3bac283954913027c496493ca20a2ad1bb..bceea0310e1203cfc79a95e01516513b14a20085 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 66de8c521693ff4579ac17233e879f25471c05fd..42885ad9bdbc62fd9bedd1f25e2381f501c22782 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 e6773ed70089a517ab8a9499fbeb5b1b49304902..447af8e54b9cc316fcda4cadea36afe0a5be7da8 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 c99425be26cbf34c74234128997546d804cc4c71..3f91eac76dc2fbd97c1a2eb9aac5a0559ff88a70 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 d9f3bf03143273afe0a6337fb774e07af82cbbae..aaab1cf1b4ee9877710eaff76e3c5a682d170ed7 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 03ee6e12cddb2a8e9cbd14ff5ee1021567f27176..7d32fc00ea810473f45021f5051457d2e81f6b88 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 325b55a258c7a1b113a0f03752435b801c6826e0..685e26d6589e0aeebe4473ce7e795c64b8ca57ec 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 97f4311fa2c2676824c7646573861614d6438b3d..1a58336b78042da518eba24e8346cd4a48a33736 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 c8283fabb0a857da18cd39903303c50a59c5cfca..efe341b8fe44e7da3f12b5c6e14fed5a02684e7a 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 dab33541e614a5c024f194ca824c8de30c0ffea6..87c31a0cd4803f24b2c5b5018f665b673a2959fb 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 4f782213f01ed703bef0d0b575b3082157da09d0..b74e8cad2a6afe4ce4cd4474866f06483889c58f 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 87041b262df8317e5763a98592f01e9465aabdf5..e86b59a796a72d99358c0d28ea96ed04de105f21 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 0cd112010c6a1516ccdbe6e76edfaddbe49335fa..08fb3a9bdcb2890ef472135f26893636cc762a21 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 405f495917202b978c3261d0d6e3ac4cd4e7f36e..08097d965c8a6fd05d4b86ffc46d542f76432a72 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 74618c3ab99025771b480085e2e2bd682bbbab81..f0c9d3cb555ed51dd180efdf04d388c6377c2e8c 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 917d74c32404351945d7fe1c528c8c44e5edd7c8..55dc2642deb53e1bfecc8eeb70713abd0a5865d8 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 d46ae6220e3a57ac50904b8271caaa7d3e85268f..afdf8e4c586f7979aad2f4b6fce779126c0ffd9b 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 1833d9150a4824ba45a2985b9f59e88389e359db..73766d556e65a6db1589a45abca908fd72e4e2c0 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 5fc22e8c45428dd01421409a22f1c5243dff916f..bb61fd575af2e49d6b59434541baee456afb5878 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 ff82c0c294f09530eb2ec73dc35119118f29d5aa..406e5de193e037396e8d798c4a43cda17d4b9193 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 be5b52fd076b4d52d8caefbad8421da7416b3f39..9f5882a42c2c4e3d16b531b691bd653e12692639 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 0215cf0453ef025d905a6f4c50f1f2a824d9761a..88bc286cdc4102fba0332be6ec35876607d8ab5f 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 5af6107b14bf22bbc8b2dcd201db2440cc358eff..3288584e07b6e7358c50b37313bacb637b506a01 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 c67be6ea2becd4453a3aa2c6dd030dfbe4b6b5bd..b940344e139aa7e205c0265227695801f27f2e3b 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 6261d028e99d16cd55cd5da04af0c010485f0fd8..9fe39d03c1c24516b6676f2d4a0ea43cc87b62ab 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 c2e39d67bc98377a97e26135d65072154430f35d..e0f7e8f2d4da5bb3c1eaec7ff0d22e16ee13641e 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 c868848607c8317a18c28252430b5b6e658ae31f..483e5ebe8fc6e6780598ec2aaeee8da65b375e3a 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 f93871d21f3fde9eaf28acf59ad018384d5fb719..3b7606d2227f01b2ccedb09712cf37a1904d3fd0 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 f93871d21f3fde9eaf28acf59ad018384d5fb719..eaf782054af1fe84a61c88fedd7a0f5c12338419 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 7c96b12f0fc777d1a605fe8ecfcb87a5ede0f66c..7eb68c12cd1b4abb33d934f444fc5c915af90adb 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 0ad2853926912f539a4bef433a5310b873fc4cc9..7cc4becf9e227b9e7a1ff818c76d3065c1680d3e 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 673ba94c60385427ce22bc2f555561b36ee114d3..1f940c2ffdfddbbf54d4133446b130f89bc05550 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 673ba94c60385427ce22bc2f555561b36ee114d3..5be71f7640605995eff85a4897ecfab4e75545d6 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 673ba94c60385427ce22bc2f555561b36ee114d3..0eb3fb7b6a3060a3ba3640feacfb1c4ceef89022 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 56ad6d38938c8575282576d4ae965f91dc83adf8..92420e1afe81d45e8fde00da2d34de79fa7ac06e 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 5123b8dc0f1d5022e5d198a21a5ef39e0f01c34d..bcf018e8e29877b135285b3a37a6e90beb506882 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 6cd8687eba15553886326158692c69839fd4e061..9197ebfc48930dfdb995d557944091ea2c3e450b 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 70ac3a9bbafb983c076f2aa1f3b6960753d24444..c9072a007e75090988a4e55c2695bc3ceb120d7e 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
*/