diff --git a/src/plugins/report/tests/report/oracle/classified.0.json b/src/plugins/report/tests/report/oracle/classified.0.json
index e9c382db69c473058f1aa9cf59aeb11173d6b2a8..f25ccd19078c6d97a591f2edde69d3a0b207ad12 100644
--- a/src/plugins/report/tests/report/oracle/classified.0.json
+++ b/src/plugins/report/tests/report/oracle/classified.0.json
@@ -1,5 +1,5 @@
[
{ "classid": "unclassified.untried", "action": "REVIEW",
"title": "f_requires", "descr": "Untried status",
- "file": "tests/report/classify.c", "line": 22 }
+ "file": "tests/report/classify.c", "line": 23 }
]
diff --git a/src/plugins/report/tests/report/oracle/classified.1.json b/src/plugins/report/tests/report/oracle/classified.1.json
index 27e60abed79c035bb078fbee24c576854802ce37..c8821c7ebaf7858583a891804c2cdccbcad35adb 100644
--- a/src/plugins/report/tests/report/oracle/classified.1.json
+++ b/src/plugins/report/tests/report/oracle/classified.1.json
@@ -2,7 +2,7 @@
{ "classid": "kernel.unclassified.warning", "action": "ERROR",
"title": "Unclassified Warning (Plugin 'kernel')",
"descr": "unbound logic variable ignored. Ignoring code annotation",
- "file": "tests/report/classify.c", "line": 27 },
+ "file": "tests/report/classify.c", "line": 28 },
{ "classid": "wp.unclassified.warning", "action": "ERROR",
"title": "Unclassified Warning (Plugin 'wp')",
"descr": "Missing RTE guards" }
diff --git a/src/plugins/report/tests/report/oracle/classified.2.json b/src/plugins/report/tests/report/oracle/classified.2.json
index 27e60abed79c035bb078fbee24c576854802ce37..c8821c7ebaf7858583a891804c2cdccbcad35adb 100644
--- a/src/plugins/report/tests/report/oracle/classified.2.json
+++ b/src/plugins/report/tests/report/oracle/classified.2.json
@@ -2,7 +2,7 @@
{ "classid": "kernel.unclassified.warning", "action": "ERROR",
"title": "Unclassified Warning (Plugin 'kernel')",
"descr": "unbound logic variable ignored. Ignoring code annotation",
- "file": "tests/report/classify.c", "line": 27 },
+ "file": "tests/report/classify.c", "line": 28 },
{ "classid": "wp.unclassified.warning", "action": "ERROR",
"title": "Unclassified Warning (Plugin 'wp')",
"descr": "Missing RTE guards" }
diff --git a/src/plugins/report/tests/report/oracle/classified.3.json b/src/plugins/report/tests/report/oracle/classified.3.json
index 8af0cb6a445af179fe0b8d2d4d521890f12c81b4..aed33faf82e82794640d4e01c12729ed0c9f29ec 100644
--- a/src/plugins/report/tests/report/oracle/classified.3.json
+++ b/src/plugins/report/tests/report/oracle/classified.3.json
@@ -1,10 +1,10 @@
[
{ "classid": "Parsing", "action": "ERROR", "title": "",
"descr": "unbound logic variable ignored. Ignoring code annotation",
- "file": "tests/report/classify.c", "line": 27 },
+ "file": "tests/report/classify.c", "line": 28 },
{ "classid": "RTE", "action": "REVIEW", "title": "Missing RTE guards",
"descr": "Shall run Eva plug-in" },
{ "classid": "UNIT", "action": "INFO", "title": "Precondition 'f'",
"descr": "Property Untried", "file": "tests/report/classify.c",
- "line": 22 }
+ "line": 23 }
]
diff --git a/src/plugins/report/tests/report/oracle/classified.4.json b/src/plugins/report/tests/report/oracle/classified.4.json
index 8af0cb6a445af179fe0b8d2d4d521890f12c81b4..aed33faf82e82794640d4e01c12729ed0c9f29ec 100644
--- a/src/plugins/report/tests/report/oracle/classified.4.json
+++ b/src/plugins/report/tests/report/oracle/classified.4.json
@@ -1,10 +1,10 @@
[
{ "classid": "Parsing", "action": "ERROR", "title": "",
"descr": "unbound logic variable ignored. Ignoring code annotation",
- "file": "tests/report/classify.c", "line": 27 },
+ "file": "tests/report/classify.c", "line": 28 },
{ "classid": "RTE", "action": "REVIEW", "title": "Missing RTE guards",
"descr": "Shall run Eva plug-in" },
{ "classid": "UNIT", "action": "INFO", "title": "Precondition 'f'",
"descr": "Property Untried", "file": "tests/report/classify.c",
- "line": 22 }
+ "line": 23 }
]
diff --git a/src/plugins/report/tests/report/oracle/classified.5.json b/src/plugins/report/tests/report/oracle/classified.5.json
index 81e4ec8552e5d75bd10bd115b7ece07d6b619e37..e55c70dfe28355ab3df65c673b1bfef821f87aff 100644
--- a/src/plugins/report/tests/report/oracle/classified.5.json
+++ b/src/plugins/report/tests/report/oracle/classified.5.json
@@ -1,16 +1,16 @@
[
{ "classid": "Parsing", "action": "ERROR", "title": "",
"descr": "unbound logic variable ignored. Ignoring code annotation",
- "file": "tests/report/classify.c", "line": 27 },
+ "file": "tests/report/classify.c", "line": 28 },
{ "classid": "RTE", "action": "REVIEW", "title": "Missing RTE guards",
"descr": "Shall run Eva plug-in" },
{ "classid": "UNIT", "action": "INFO", "title": "Precondition 'f'",
"descr": "Property Untried", "file": "tests/report/classify.c",
- "line": 22 },
+ "line": 23 },
{ "classid": "GOAL", "action": "ERROR", "title": "Postcondition 'f'",
"descr": "Property Untried", "file": "tests/report/classify.c",
- "line": 23 },
+ "line": 24 },
{ "classid": "unclassified.untried", "action": "REVIEW",
"title": "f_assigns", "descr": "Untried status",
- "file": "tests/report/classify.c", "line": 24 }
+ "file": "tests/report/classify.c", "line": 25 }
]
diff --git a/src/plugins/report/tests/report/oracle/classify.0.res.oracle b/src/plugins/report/tests/report/oracle/classify.0.res.oracle
index e19a301288f31daaee5a84de423e34be38e9a539..5484bb541213ea2e6bb40e362b4f5c95d164a9e3 100644
--- a/src/plugins/report/tests/report/oracle/classify.0.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.0.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
-[kernel:annot-error] tests/report/classify.c:27: Warning:
+[kernel:annot-error] tests/report/classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/report/tests/report/oracle/classify.1.res.oracle b/src/plugins/report/tests/report/oracle/classify.1.res.oracle
index 442bb8d3b8ce3649bef6678accea16e983d104d3..ab8672ef1b4e893489351d33b45e5b17d67b0e11 100644
--- a/src/plugins/report/tests/report/oracle/classify.1.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.1.res.oracle
@@ -1,7 +1,7 @@
[report] Monitoring events
# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
-[kernel:annot-error] tests/report/classify.c:27: Warning:
+[kernel:annot-error] tests/report/classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/report/tests/report/oracle/classify.2.res.oracle b/src/plugins/report/tests/report/oracle/classify.2.res.oracle
index 974d340981d9d583ddecf5a335ebfbe03c3002a9..a9cd75caa362e75d69326006fab6658fa50e8482 100644
--- a/src/plugins/report/tests/report/oracle/classify.2.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.2.res.oracle
@@ -1,7 +1,7 @@
[report] Monitoring events
# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
-[kernel:annot-error] tests/report/classify.c:27: Warning:
+[kernel:annot-error] tests/report/classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/report/tests/report/oracle/classify.3.res.oracle b/src/plugins/report/tests/report/oracle/classify.3.res.oracle
index 91bb8b30a52c6ab24b75cf1c04a53d3cc15534d7..b9a1a38184fe8c745b10cefea6581e135ef82b5e 100644
--- a/src/plugins/report/tests/report/oracle/classify.3.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.3.res.oracle
@@ -2,7 +2,7 @@
[report] Loading 'tests/report/classify.json'
# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
-[kernel:annot-error] tests/report/classify.c:27: Warning:
+[kernel:annot-error] tests/report/classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/report/tests/report/oracle/classify.4.res.oracle b/src/plugins/report/tests/report/oracle/classify.4.res.oracle
index ab13ead4ecb87d3507d41418ee453bf3a16f4fde..abe3dd32f57024301fe09b7dfc63c2a3793c60d9 100644
--- a/src/plugins/report/tests/report/oracle/classify.4.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.4.res.oracle
@@ -2,7 +2,7 @@
[report] Loading 'tests/report/classify.json'
# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
-[kernel:annot-error] tests/report/classify.c:27: Warning:
+[kernel:annot-error] tests/report/classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/report/tests/report/oracle/classify.5.res.oracle b/src/plugins/report/tests/report/oracle/classify.5.res.oracle
index bab75d5f591e203476328215f076bf5d0ad61a7a..3cbe2f38f0621b4b9ee1a5221efe94ee299d2ace 100644
--- a/src/plugins/report/tests/report/oracle/classify.5.res.oracle
+++ b/src/plugins/report/tests/report/oracle/classify.5.res.oracle
@@ -2,7 +2,7 @@
[report] Loading 'tests/report/classify.json'
# frama-c -wp [...]
[kernel] Parsing tests/report/classify.c (with preprocessing)
-[kernel:annot-error] tests/report/classify.c:27: Warning:
+[kernel:annot-error] tests/report/classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json
index b9bbb5e7c626ca31ccbd1c122cc1385072b40f89..7546c88e6c0dcaf39fd1b126cf4eb9a2f394d995 100644
--- a/src/plugins/server/tests/batch/oracle/ast_services.out.json
+++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json
@@ -12,7 +12,7 @@
"dir": "tests/batch",
"base": "ast_services.i",
"file": "tests/batch/ast_services.i",
- "line": 2
+ "line": 8
}
},
{
@@ -24,7 +24,7 @@
"dir": "tests/batch",
"base": "ast_services.i",
"file": "tests/batch/ast_services.i",
- "line": 1
+ "line": 7
}
}
],
diff --git a/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
index c05a4ba9b29af3af3f01dcbf46d240984404e5b4..6583645e23e6e02434401ad134f582841fe8247d 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
@@ -1,4 +1,4 @@
-[kernel] tests/erroneous/not-enough-par.i:4: User Error:
+[kernel] tests/erroneous/not-enough-par.i:8: User Error:
Too few arguments in call to f.
[kernel] User Error: stopping on file "tests/erroneous/not-enough-par.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
index bf189af5926715a5665d71211f84b792dbffd641..7b54306d9847d14b9f3386ddc37d1999a1c76738 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
@@ -1,9 +1,9 @@
-[variadic] tests/erroneous/variadic-builtin.i:1:
+[variadic] tests/erroneous/variadic-builtin.i:5:
Declaration of variadic function Frama_C_show_each_warning.
-[variadic] tests/erroneous/variadic-builtin.i:1:
- Variadic builtin Frama_C_show_each_warning left untransformed.
[variadic] tests/erroneous/variadic-builtin.i:5:
+ Variadic builtin Frama_C_show_each_warning left untransformed.
+[variadic] tests/erroneous/variadic-builtin.i:9:
Call to variadic builtin Frama_C_show_each_warning left untransformed.
-[kernel] tests/erroneous/variadic-builtin.i:6: Plug-in variadic aborted: unimplemented feature.
+[kernel] tests/erroneous/variadic-builtin.i:10: Plug-in variadic aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in variadic] The variadic plugin doesn't handle calls to a pointer to the variadic builtin Frama_C_show_each_warning.'.
diff --git a/tests/builtins/oracle/watch.res.oracle b/tests/builtins/oracle/watch.res.oracle
index 59019484ae98a15510c1d4b2d77bb66d104eb208..28fc5ca752290093449dfdb06b399008642ff8c5 100644
--- a/tests/builtins/oracle/watch.res.oracle
+++ b/tests/builtins/oracle/watch.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing tests/builtins/watch.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/builtins/watch.c:5: Warning:
+[kernel:typing:implicit-function-declaration] tests/builtins/watch.c:10: Warning:
Calling undeclared function Frama_C_watch_value. Old style K&R code?
-[kernel:typing:implicit-function-declaration] tests/builtins/watch.c:11: Warning:
+[kernel:typing:implicit-function-declaration] tests/builtins/watch.c:16: Warning:
Calling undeclared function u. Old style K&R code?
-[kernel:annot:missing-spec] tests/builtins/watch.c:3: Warning:
+[kernel:annot:missing-spec] tests/builtins/watch.c:8: Warning:
Neither code nor specification for function Frama_C_watch_value, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -12,18 +12,18 @@
x ∈ {0}
y ∈ {0}
z ∈ {0}
-[eva] tests/builtins/watch.c:5: Call to builtin Frama_C_watch_value
-[eva] tests/builtins/watch.c:8: Watchpoint: & c [--..--]
-[eva] tests/builtins/watch.c:9: Watchpoint: & c [--..--]
+[eva] tests/builtins/watch.c:10: Call to builtin Frama_C_watch_value
+[eva] tests/builtins/watch.c:13: Watchpoint: & c [--..--]
+[eva] tests/builtins/watch.c:14: Watchpoint: & c [--..--]
[eva] computing for function u <- main.
- Called from tests/builtins/watch.c:11.
-[kernel:annot:missing-spec] tests/builtins/watch.c:11: Warning:
+ Called from tests/builtins/watch.c:16.
+[kernel:annot:missing-spec] tests/builtins/watch.c:16: Warning:
Neither code nor specification for function u, generating default assigns from the prototype
[eva] using specification for function u
[eva] Done for function u
-[eva] tests/builtins/watch.c:12: Watchpoint: & c [--..--]
-[eva] tests/builtins/watch.c:13: Watchpoint: & c [--..--]
-[eva] tests/builtins/watch.c:14: Watchpoint: & c [--..--]
+[eva] tests/builtins/watch.c:17: Watchpoint: & c [--..--]
+[eva] tests/builtins/watch.c:18: Watchpoint: & c [--..--]
+[eva] tests/builtins/watch.c:19: Watchpoint: & c [--..--]
[eva] User Error: Degeneration occurred:
results are not correct for lines of code that can be reached from the degeneration point.
[from] Computing for function main
diff --git a/tests/cil/oracle/acsl-comments.res.oracle b/tests/cil/oracle/acsl-comments.res.oracle
index 605a2d7b753d8a769cba70e603bd2cb54ed60a82..ce4dd692b429f04a6028c23770c778cdbe5dbed4 100644
--- a/tests/cil/oracle/acsl-comments.res.oracle
+++ b/tests/cil/oracle/acsl-comments.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/cil/acsl-comments.i (no preprocessing)
-[kernel:annot-error] tests/cil/acsl-comments.i:1: Warning:
+[kernel:annot-error] tests/cil/acsl-comments.i:6: Warning:
lexical error, unexpected block-comment opening
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "tests/cil/acsl-comments.i" that has errors.
diff --git a/tests/cil/oracle/bts892.res.oracle b/tests/cil/oracle/bts892.res.oracle
index dd2a50f79542e3a8939f8e8086e82473ace5a81d..ac7ac95ae66a836a0b2d1a10dfb98fcf5eb89c0e 100644
--- a/tests/cil/oracle/bts892.res.oracle
+++ b/tests/cil/oracle/bts892.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/cil/bts892.i (no preprocessing)
-[kernel] tests/cil/bts892.i:11: User Error:
+[kernel] tests/cil/bts892.i:17: User Error:
Forbidden access to local variable i in static initializer
[kernel] User Error: stopping on file "tests/cil/bts892.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle
index 9b833655a031c17620a11961d2a2d036d30bad01..d006b7d3b427b888d6215fc3e4a2cacc35240f50 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -1,41 +1,41 @@
[kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:9: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:10: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto X; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:26: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:27: Warning:
Ghost code breaks CFG starting at:
/*@ ghost if (i == 0) break; */
i ++;
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:34: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:35: Warning:
Ghost code breaks CFG starting at:
/*@ ghost if (i == 0) continue; */
i ++;
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:60: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:61: Warning:
Ghost code breaks CFG starting at:
/*@ ghost case 1: g = 3; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:79: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:80: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto X; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:89: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:90: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto X; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:100: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:101: Warning:
Ghost code breaks CFG starting at:
/*@ ghost case 1: x ++; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:108: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:109: Warning:
Ghost code breaks CFG starting at:
/*@ ghost __retres = 1; */
/*@ ghost goto return_label; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:114: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:115: Warning:
Ghost code breaks CFG starting at:
/*@ ghost case 3: ; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:142: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:143: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto return_label; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:132: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:133: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto X; */
-[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:108: Warning:
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:109: Warning:
'__retres' is a non-ghost lvalue, it cannot be assigned in ghost code
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/cil/oracle/ghost_cfg.1.res.oracle b/tests/cil/oracle/ghost_cfg.1.res.oracle
index 494260f7dfe4e335e5735ed4258d7a94afbbbfb1..68a94840387fdfdd1b5ef1a5ba3147f11fa6b7d8 100644
--- a/tests/cil/oracle/ghost_cfg.1.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel] tests/cil/ghost_cfg.c:153: User Error:
+[kernel] tests/cil/ghost_cfg.c:154: User Error:
'goto X;' would jump from normal statement to ghost code
[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/misc/oracle/bts0451.res.oracle b/tests/misc/oracle/bts0451.res.oracle
index feb299b32acd882e5508f6f436b1b772375f1d27..473b9fd4f165b99bddc3b43c237985f18f736c99 100644
--- a/tests/misc/oracle/bts0451.res.oracle
+++ b/tests/misc/oracle/bts0451.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/misc/bts0451.i (no preprocessing)
-[kernel] tests/misc/bts0451.i:26: User Error:
+[kernel] tests/misc/bts0451.i:27: User Error:
break outside of a loop or switch
- 24 /* should abort with an error at type-checking */
- 25 int main (void) {
- 26 break;
+ 25 /* should abort with an error at type-checking */
+ 26 int main (void) {
+ 27 break;
^^^^^^^^
- 27 return 0;
- 28 }
+ 28 return 0;
+ 29 }
[kernel] User Error: stopping on file "tests/misc/bts0451.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_alignof.res.oracle b/tests/misc/oracle/function_ptr_alignof.res.oracle
index 3a83624e3444f3b2ca8bd89373a97023cf34fb46..b7d7520c167f71b7acb3867d646ea49253ae84a3 100644
--- a/tests/misc/oracle/function_ptr_alignof.res.oracle
+++ b/tests/misc/oracle/function_ptr_alignof.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/function_ptr_alignof.i (no preprocessing)
-[kernel] tests/misc/function_ptr_alignof.i:10: User Error:
+[kernel] tests/misc/function_ptr_alignof.i:13: User Error:
alignof() called on a function.
[kernel] User Error: stopping on file "tests/misc/function_ptr_alignof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_lvalue_1.res.oracle b/tests/misc/oracle/function_ptr_lvalue_1.res.oracle
index 34164dbea515cb8a682704949347ffefd9cf5517..17925b5b8e35fb2c11ce03e0a400ca7c17b1cb03 100644
--- a/tests/misc/oracle/function_ptr_lvalue_1.res.oracle
+++ b/tests/misc/oracle/function_ptr_lvalue_1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/function_ptr_lvalue_1.i (no preprocessing)
-[kernel] tests/misc/function_ptr_lvalue_1.i:7: User Error:
+[kernel] tests/misc/function_ptr_lvalue_1.i:13: User Error:
Cannot assign to non-modifiable lval *p
[kernel] User Error: stopping on file "tests/misc/function_ptr_lvalue_1.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_lvalue_2.res.oracle b/tests/misc/oracle/function_ptr_lvalue_2.res.oracle
index 30a6df5ceef884d4f5b89d5f898ce3b6a104553a..c2c0cf02b8a48b729c5b41d5164dd37be21468d0 100644
--- a/tests/misc/oracle/function_ptr_lvalue_2.res.oracle
+++ b/tests/misc/oracle/function_ptr_lvalue_2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/function_ptr_lvalue_2.i (no preprocessing)
-[kernel] tests/misc/function_ptr_lvalue_2.i:7: User Error:
+[kernel] tests/misc/function_ptr_lvalue_2.i:12: User Error:
Cannot assign to non-modifiable lval *p
[kernel] User Error: stopping on file "tests/misc/function_ptr_lvalue_2.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_sizeof.res.oracle b/tests/misc/oracle/function_ptr_sizeof.res.oracle
index 0a31265b9f6a3851e84d09ad2d222318772c9a78..bc70a4785cb896cff2b3bae69cb194831acdcab9 100644
--- a/tests/misc/oracle/function_ptr_sizeof.res.oracle
+++ b/tests/misc/oracle/function_ptr_sizeof.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/function_ptr_sizeof.i (no preprocessing)
-[kernel] tests/misc/function_ptr_sizeof.i:10: User Error:
+[kernel] tests/misc/function_ptr_sizeof.i:13: User Error:
sizeof() called on function
[kernel] User Error: stopping on file "tests/misc/function_ptr_sizeof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/widen_hints.0.res.oracle b/tests/misc/oracle/widen_hints.0.res.oracle
index d86de98015d8cfbf1598e8941ee3591b24b3ef37..582badd66f55e69c4929f48ca8051a9533ecf31c 100644
--- a/tests/misc/oracle/widen_hints.0.res.oracle
+++ b/tests/misc/oracle/widen_hints.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
-[kernel:annot-error] tests/misc/widen_hints.c:14: Warning:
+[kernel:annot-error] tests/misc/widen_hints.c:16: Warning:
invalid widen_hints annotation: no hints. Ignoring code annotation
-[kernel:annot-error] tests/misc/widen_hints.c:19: Warning:
+[kernel:annot-error] tests/misc/widen_hints.c:21: Warning:
invalid widen_hints annotation: no hints. Ignoring code annotation
-[kernel:annot-error] tests/misc/widen_hints.c:24: Warning:
+[kernel:annot-error] tests/misc/widen_hints.c:26: Warning:
unbound logic variable b. Ignoring code annotation
-[eva] tests/misc/widen_hints.c:29: User Error:
+[eva] tests/misc/widen_hints.c:31: User Error:
could not parse widening hint: not_const
If it contains variables, they must be global const integers.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/misc/oracle/widen_hints.1.res.oracle b/tests/misc/oracle/widen_hints.1.res.oracle
index a6a3f7e9b775729381f4ecc5c5c0233858dbdbbe..7d63e13e27d9a28984b039985679f55bbb5373bb 100644
--- a/tests/misc/oracle/widen_hints.1.res.oracle
+++ b/tests/misc/oracle/widen_hints.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
-[eva] tests/misc/widen_hints.c:65: User Error:
+[eva] tests/misc/widen_hints.c:67: User Error:
could not parse widening hint: local_const
If it contains variables, they must be global const integers.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/misc/oracle/widen_hints.2.res.oracle b/tests/misc/oracle/widen_hints.2.res.oracle
index 065a307ea653ab80fbd03769c998038549f079b9..89d5bd4b3937d98113688b8c58f58b3901d6c535 100644
--- a/tests/misc/oracle/widen_hints.2.res.oracle
+++ b/tests/misc/oracle/widen_hints.2.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
[eva:widen-hints] computing global widen hints
-[eva:widen-hints] tests/misc/widen_hints.c:71:
+[eva:widen-hints] tests/misc/widen_hints.c:73:
adding hint from annotation: a, { 87 } (for all statements)
-[eva:widen-hints] tests/misc/widen_hints.c:87:
+[eva:widen-hints] tests/misc/widen_hints.c:89:
adding hint from annotation: ss, { 87 } (for all statements)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -10,56 +10,56 @@
[eva:initial-state] Values of globals at initialization
x ∈ {9}
not_const ∈ {42}
-[eva:widen-hints] tests/misc/widen_hints.c:72:
+[eva:widen-hints] tests/misc/widen_hints.c:74:
computing dynamic hints for statement 16
-[eva] tests/misc/widen_hints.c:73: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:72: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:88:
+[eva] tests/misc/widen_hints.c:75: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:74: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:90:
computing dynamic hints for statement 30
-[eva] tests/misc/widen_hints.c:89: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:88: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:97:
+[eva] tests/misc/widen_hints.c:91: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:90: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:99:
computing dynamic hints for statement 48
-[eva:widen-hints] tests/misc/widen_hints.c:97:
+[eva:widen-hints] tests/misc/widen_hints.c:99:
adding new base due to dynamic widen hint: ip, { 87 }
-[eva] tests/misc/widen_hints.c:98: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:97: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:107:
+[eva] tests/misc/widen_hints.c:100: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:99: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:109:
computing dynamic hints for statement 67
-[eva:widen-hints] tests/misc/widen_hints.c:107:
+[eva:widen-hints] tests/misc/widen_hints.c:109:
adding new base due to dynamic widen hint: ip2, { 87 }
-[eva] tests/misc/widen_hints.c:108: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:107: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:118:
+[eva] tests/misc/widen_hints.c:110: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:109: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:120:
computing dynamic hints for statement 91
-[eva:widen-hints] tests/misc/widen_hints.c:118:
+[eva:widen-hints] tests/misc/widen_hints.c:120:
adding new base due to dynamic widen hint: iarray, { 87 }
+[eva] tests/misc/widen_hints.c:120: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:118: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:116: starting to merge loop iterations
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
-[eva:widen-hints] tests/misc/widen_hints.c:58:
+ Called from tests/misc/widen_hints.c:126.
+[eva:widen-hints] tests/misc/widen_hints.c:60:
computing dynamic hints for statement 2
-[eva:widen-hints] tests/misc/widen_hints.c:58:
+[eva:widen-hints] tests/misc/widen_hints.c:60:
adding new base due to dynamic widen hint: outer_i, { 87 }
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
+ Called from tests/misc/widen_hints.c:126.
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
-[eva] tests/misc/widen_hints.c:123: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:125: starting to merge loop iterations
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
-[eva] tests/misc/widen_hints.c:58: starting to merge loop iterations
+ Called from tests/misc/widen_hints.c:126.
+[eva] tests/misc/widen_hints.c:60: starting to merge loop iterations
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
+ Called from tests/misc/widen_hints.c:126.
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
+ Called from tests/misc/widen_hints.c:126.
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] Recording results for main
diff --git a/tests/misc/oracle/widen_hints.3.res.oracle b/tests/misc/oracle/widen_hints.3.res.oracle
index 0d957fb92d935e14ab7e855ce4f3d4652bf16eef..0d403fde663d2aac035a7f1edd2a804cec646183 100644
--- a/tests/misc/oracle/widen_hints.3.res.oracle
+++ b/tests/misc/oracle/widen_hints.3.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
[eva:widen-hints] computing global widen hints
-[eva:widen-hints] tests/misc/widen_hints.c:79:
+[eva:widen-hints] tests/misc/widen_hints.c:81:
adding global hint from annotation: for all variables, { 88 } (for all statements)
-[eva:widen-hints] tests/misc/widen_hints.c:71:
+[eva:widen-hints] tests/misc/widen_hints.c:73:
adding hint from annotation: a, { 87 } (for all statements)
-[eva:widen-hints] tests/misc/widen_hints.c:87:
+[eva:widen-hints] tests/misc/widen_hints.c:89:
adding hint from annotation: ss, { 87 } (for all statements)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -12,60 +12,60 @@
[eva:initial-state] Values of globals at initialization
x ∈ {9}
not_const ∈ {42}
-[eva:widen-hints] tests/misc/widen_hints.c:72:
+[eva:widen-hints] tests/misc/widen_hints.c:74:
computing dynamic hints for statement 36
-[eva] tests/misc/widen_hints.c:72: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:73: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:80:
+[eva] tests/misc/widen_hints.c:74: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:75: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:82:
computing dynamic hints for statement 50
[eva] computing for function f <- main.
- Called from tests/misc/widen_hints.c:80.
-[eva] tests/misc/widen_hints.c:41: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:42: starting to merge loop iterations
+ Called from tests/misc/widen_hints.c:82.
+[eva] tests/misc/widen_hints.c:43: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:44: starting to merge loop iterations
[eva] Recording results for f
[eva] Done for function f
-[eva:widen-hints] tests/misc/widen_hints.c:88:
+[eva:widen-hints] tests/misc/widen_hints.c:90:
computing dynamic hints for statement 52
-[eva] tests/misc/widen_hints.c:88: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:89: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:97:
+[eva] tests/misc/widen_hints.c:90: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:91: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:99:
computing dynamic hints for statement 70
-[eva:widen-hints] tests/misc/widen_hints.c:97:
+[eva:widen-hints] tests/misc/widen_hints.c:99:
adding new base due to dynamic widen hint: ip, { 87 }
-[eva] tests/misc/widen_hints.c:97: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:98: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:107:
+[eva] tests/misc/widen_hints.c:99: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:100: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:109:
computing dynamic hints for statement 89
-[eva:widen-hints] tests/misc/widen_hints.c:107:
+[eva:widen-hints] tests/misc/widen_hints.c:109:
adding new base due to dynamic widen hint: ip2, { 87 }
-[eva] tests/misc/widen_hints.c:107: starting to merge loop iterations
-[eva] tests/misc/widen_hints.c:108: starting to merge loop iterations
-[eva:widen-hints] tests/misc/widen_hints.c:118:
+[eva] tests/misc/widen_hints.c:109: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:110: starting to merge loop iterations
+[eva:widen-hints] tests/misc/widen_hints.c:120:
computing dynamic hints for statement 113
-[eva:widen-hints] tests/misc/widen_hints.c:118:
+[eva:widen-hints] tests/misc/widen_hints.c:120:
adding new base due to dynamic widen hint: iarray, { 87 }
-[eva] tests/misc/widen_hints.c:116: starting to merge loop iterations
[eva] tests/misc/widen_hints.c:118: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:120: starting to merge loop iterations
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
-[eva:widen-hints] tests/misc/widen_hints.c:58:
+ Called from tests/misc/widen_hints.c:126.
+[eva:widen-hints] tests/misc/widen_hints.c:60:
computing dynamic hints for statement 22
-[eva:widen-hints] tests/misc/widen_hints.c:58:
+[eva:widen-hints] tests/misc/widen_hints.c:60:
adding new base due to dynamic widen hint: outer_i, { 87 }
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
-[eva] tests/misc/widen_hints.c:123: starting to merge loop iterations
+[eva] tests/misc/widen_hints.c:125: starting to merge loop iterations
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
-[eva] tests/misc/widen_hints.c:58: starting to merge loop iterations
+ Called from tests/misc/widen_hints.c:126.
+[eva] tests/misc/widen_hints.c:60: starting to merge loop iterations
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
+ Called from tests/misc/widen_hints.c:126.
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] computing for function using_dynamic_global <- main.
- Called from tests/misc/widen_hints.c:124.
+ Called from tests/misc/widen_hints.c:126.
[eva] Recording results for using_dynamic_global
[eva] Done for function using_dynamic_global
[eva] Recording results for main
diff --git a/tests/syntax/oracle/alloc_order.res.oracle b/tests/syntax/oracle/alloc_order.res.oracle
index 173bd5cb869ad8b1702c444344ed0be2eef73e91..59aebb036c3b4be1d4705dc54c4b050e1a66121e 100644
--- a/tests/syntax/oracle/alloc_order.res.oracle
+++ b/tests/syntax/oracle/alloc_order.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/alloc_order.i (no preprocessing)
-[kernel:annot-error] tests/syntax/alloc_order.i:3: Warning:
+[kernel:annot-error] tests/syntax/alloc_order.i:8: Warning:
wrong order of clause in contract: requires after post-condition, assigns or allocates.
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "tests/syntax/alloc_order.i" that has errors.
diff --git a/tests/syntax/oracle/array_cast_bts1099.res.oracle b/tests/syntax/oracle/array_cast_bts1099.res.oracle
index 3ffc08e781dc03aa74057fdadaa70e25c2a532b6..d1d6270e09fd6f2c43391ed6dcd3a6bdaaf3e354 100644
--- a/tests/syntax/oracle/array_cast_bts1099.res.oracle
+++ b/tests/syntax/oracle/array_cast_bts1099.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/syntax/array_cast_bts1099.i (no preprocessing)
-[kernel] tests/syntax/array_cast_bts1099.i:7: User Error:
+[kernel] tests/syntax/array_cast_bts1099.i:12: User Error:
Cast over a non-scalar type int [10]
- 5 int tab1[4];
- 6 u* p = &tab1;
- 7 t* p2 = (t) p;
+ 10 int tab1[4];
+ 11 u* p = &tab1;
+ 12 t* p2 = (t) p;
^^^^^^^^^^^^^^^^
- 8 }
+ 13 }
[kernel] User Error: stopping on file "tests/syntax/array_cast_bts1099.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_size.res.oracle b/tests/syntax/oracle/array_size.res.oracle
index ec2486e5181ba4a029dc69d0d451180ae504612b..de7738eb5114683a6c340766053fceaa9395f02e 100644
--- a/tests/syntax/oracle/array_size.res.oracle
+++ b/tests/syntax/oracle/array_size.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/syntax/array_size.i (no preprocessing)
-[kernel] tests/syntax/array_size.i:1: User Error: Array length is negative.
+[kernel] tests/syntax/array_size.i:7: User Error: Array length is negative.
[kernel] User Error: stopping on file "tests/syntax/array_size.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/axiomatic_nested.res.oracle b/tests/syntax/oracle/axiomatic_nested.res.oracle
index d3bdcc55f5071d1bfe4ef4c98f29f605fc591745..3fbfd43b9c4870d3110175283772cb50b7b11eda 100644
--- a/tests/syntax/oracle/axiomatic_nested.res.oracle
+++ b/tests/syntax/oracle/axiomatic_nested.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/axiomatic_nested.i (no preprocessing)
-[kernel:annot-error] tests/syntax/axiomatic_nested.i:4: Warning:
+[kernel:annot-error] tests/syntax/axiomatic_nested.i:8: Warning:
Nested axiomatic. Ignoring body of bla2. Ignoring global annotation
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "tests/syntax/axiomatic_nested.i" that has errors.
diff --git a/tests/syntax/oracle/bad_return_bts_599.res.oracle b/tests/syntax/oracle/bad_return_bts_599.res.oracle
index 547da73ae039c6839eb2a5a261b8fbe3e591b498..d497519859d77d74ab944ded30b382d1f03ebcb2 100644
--- a/tests/syntax/oracle/bad_return_bts_599.res.oracle
+++ b/tests/syntax/oracle/bad_return_bts_599.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/bad_return_bts_599.i (no preprocessing)
-[kernel] tests/syntax/bad_return_bts_599.i:4: User Error:
+[kernel] tests/syntax/bad_return_bts_599.i:7: User Error:
Return statement without a value in function returning int
-[kernel] tests/syntax/bad_return_bts_599.i:9: User Error:
+[kernel] tests/syntax/bad_return_bts_599.i:12: User Error:
Return statement without a value in function returning int
[kernel] User Error: stopping on file "tests/syntax/bad_return_bts_599.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/bts0519.1.res.oracle b/tests/syntax/oracle/bts0519.1.res.oracle
index 569bc14d16ed150c732eea7095eed1ac511cf9d5..e7405b10ba795d9cc21051f3351c848af9c182d5 100644
--- a/tests/syntax/oracle/bts0519.1.res.oracle
+++ b/tests/syntax/oracle/bts0519.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/bts0519.c (with preprocessing)
-[kernel] tests/syntax/bts0519.c:9: User Error:
+[kernel] tests/syntax/bts0519.c:10: User Error:
static specifier inside array argument is allowed only in function argument
[kernel] User Error: stopping on file "tests/syntax/bts0519.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/cert-dcl-36.res.oracle b/tests/syntax/oracle/cert-dcl-36.res.oracle
index 847b9b1daf4de01140c7d03e3147b99a84a7194a..b1c09cfdec30ff4124c89ea50544288a5014e94e 100644
--- a/tests/syntax/oracle/cert-dcl-36.res.oracle
+++ b/tests/syntax/oracle/cert-dcl-36.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/cert-dcl-36.c (with preprocessing)
-[kernel] tests/syntax/cert-dcl-36.c:7: User Error:
- Inconsistent storage specification for i2. Previous declaration: tests/syntax/cert-dcl-36.c:2
-[kernel] tests/syntax/cert-dcl-36.c:10: User Error:
- Inconsistent storage specification for i5. Previous declaration: tests/syntax/cert-dcl-36.c:5
+[kernel] tests/syntax/cert-dcl-36.c:12: User Error:
+ Inconsistent storage specification for i2. Previous declaration: tests/syntax/cert-dcl-36.c:7
+[kernel] tests/syntax/cert-dcl-36.c:15: User Error:
+ Inconsistent storage specification for i5. Previous declaration: tests/syntax/cert-dcl-36.c:10
[kernel] User Error: stopping on file "tests/syntax/cert-dcl-36.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.0.res.oracle b/tests/syntax/oracle/cert_msc_38.0.res.oracle
index 436be5934df83f34a38c349268bc1cc44c678eca..04ff74b2370c01075635c950d12d486cb2ce8a9c 100644
--- a/tests/syntax/oracle/cert_msc_38.0.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:25: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:26: Warning:
assert is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] tests/syntax/cert_msc_38.c:25: User Error:
+[kernel] tests/syntax/cert_msc_38.c:26: User Error:
Cannot resolve variable assert
[kernel] User Error: stopping on file "tests/syntax/cert_msc_38.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/cert_msc_38.1.res.oracle b/tests/syntax/oracle/cert_msc_38.1.res.oracle
index 912e7c39eda85a2aca5b384ba7c66a19a7cc5ae3..eb28de05e6ccd14529eb0f194f929194af767bd1 100644
--- a/tests/syntax/oracle/cert_msc_38.1.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:32: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:33: Warning:
Attempt to declare errno as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C
[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.2.res.oracle b/tests/syntax/oracle/cert_msc_38.2.res.oracle
index 9f32d3600137b87eec1c8173f9c25065724ced79..abc74174dda62c557908b513cd781e03e62a5f29 100644
--- a/tests/syntax/oracle/cert_msc_38.2.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:37: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:38: Warning:
Attempt to declare math_errhandling as external identifier outside of the stdlib. It is supposed to be a macro name and cannot be declared. See CERT C coding rule MSC38-C
[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.3.res.oracle b/tests/syntax/oracle/cert_msc_38.3.res.oracle
index 1d21e57a88d24c9b96be04b54e6a2cc7ae571c1d..14676195dd4eae5ed1171034ca44b30f1b74d441 100644
--- a/tests/syntax/oracle/cert_msc_38.3.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.3.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:42: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:43: Warning:
va_start is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] tests/syntax/cert_msc_38.c:42: User Error:
+[kernel] tests/syntax/cert_msc_38.c:43: User Error:
Cannot resolve variable va_start
[kernel] User Error: stopping on file "tests/syntax/cert_msc_38.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/cert_msc_38.4.res.oracle b/tests/syntax/oracle/cert_msc_38.4.res.oracle
index a65e4b430e8d16990b62fde88248bc2595dab725..f867e2dca1a32b845de6d3dfe84e234a66de9e21 100644
--- a/tests/syntax/oracle/cert_msc_38.4.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.4.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:46: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:47: Warning:
va_copy is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] tests/syntax/cert_msc_38.c:46: User Error:
+[kernel] tests/syntax/cert_msc_38.c:47: User Error:
Cannot resolve variable va_copy
[kernel] User Error: stopping on file "tests/syntax/cert_msc_38.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/cert_msc_38.5.res.oracle b/tests/syntax/oracle/cert_msc_38.5.res.oracle
index 38293bc7042745d1f53f4b7b07f04c991d7b871b..15a1c6c5ec34746a35112dfec92bc76c861cce7d 100644
--- a/tests/syntax/oracle/cert_msc_38.5.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.5.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:50: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:51: Warning:
va_arg is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] tests/syntax/cert_msc_38.c:50: User Error:
+[kernel] tests/syntax/cert_msc_38.c:51: User Error:
Cannot resolve variable va_arg
[kernel] User Error: stopping on file "tests/syntax/cert_msc_38.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/cert_msc_38.6.res.oracle b/tests/syntax/oracle/cert_msc_38.6.res.oracle
index 5aad28f718a5497c62d4ea5465bb4abe26a7b0b8..467a8bc0b1a0c4c3a1e67c858736955aca2e314c 100644
--- a/tests/syntax/oracle/cert_msc_38.6.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.6.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:54: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:55: Warning:
va_end is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
-[kernel] tests/syntax/cert_msc_38.c:54: User Error:
+[kernel] tests/syntax/cert_msc_38.c:55: User Error:
Cannot resolve variable va_end
[kernel] User Error: stopping on file "tests/syntax/cert_msc_38.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/cert_msc_38.7.res.oracle b/tests/syntax/oracle/cert_msc_38.7.res.oracle
index a13d4f25031321d636b4bd57ad8ff9ca9c89e66f..f32737dfff88f02c4e8c09ccde67b5d0d3484656 100644
--- a/tests/syntax/oracle/cert_msc_38.7.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.7.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/cert_msc_38.c (with preprocessing)
-[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:59: Warning:
+[kernel:CERT:MSC:38] tests/syntax/cert_msc_38.c:60: Warning:
setjmp is a standard macro. Its definition cannot be suppressed, see CERT C coding rules MSC38-C
[kernel] Warning: warning CERT:MSC:38 treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/composite-tags.res.oracle b/tests/syntax/oracle/composite-tags.res.oracle
index 4bffd45b6e6122b339e7770cfc8aada85d1a3c75..a48143d07d80ec5eed131ac8631df8d43ca43117 100644
--- a/tests/syntax/oracle/composite-tags.res.oracle
+++ b/tests/syntax/oracle/composite-tags.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/composite-tags.i (no preprocessing)
-[kernel] tests/syntax/composite-tags.i:5: User Error:
- Declaration of f does not match previous declaration from tests/syntax/composite-tags.i:4 (structs with different tags).
-[kernel] tests/syntax/composite-tags.i:11: User Error:
- Declaration of g does not match previous declaration from tests/syntax/composite-tags.i:10 (unions with different tags).
+[kernel] tests/syntax/composite-tags.i:10: User Error:
+ Declaration of f does not match previous declaration from tests/syntax/composite-tags.i:9 (structs with different tags).
+[kernel] tests/syntax/composite-tags.i:16: User Error:
+ Declaration of g does not match previous declaration from tests/syntax/composite-tags.i:15 (unions with different tags).
[kernel] User Error: stopping on file "tests/syntax/composite-tags.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/duplicate_field.res.oracle b/tests/syntax/oracle/duplicate_field.res.oracle
index 1535831390d805fc0dc1ee5d05f8d1bdc43fe451..158feb74eaf514db805002c0630d203b7e721c59 100644
--- a/tests/syntax/oracle/duplicate_field.res.oracle
+++ b/tests/syntax/oracle/duplicate_field.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/duplicate_field.i (no preprocessing)
-[kernel] tests/syntax/duplicate_field.i:3: User Error:
- field x occurs multiple times in aggregate struct test. Previous occurrence is at line 2.
+[kernel] tests/syntax/duplicate_field.i:8: User Error:
+ field x occurs multiple times in aggregate struct test. Previous occurrence is at line 7.
[kernel] User Error: stopping on file "tests/syntax/duplicate_field.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/fam.res.oracle b/tests/syntax/oracle/fam.res.oracle
index 950231170bb236c3b469691bf90fff7e7e252eac..8ccf9f18f6f5ea030a3ff85f5e597a43aa74de04 100644
--- a/tests/syntax/oracle/fam.res.oracle
+++ b/tests/syntax/oracle/fam.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing tests/syntax/fam.i (no preprocessing)
-[kernel] tests/syntax/fam.i:10: User Error:
+[kernel] tests/syntax/fam.i:16: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] tests/syntax/fam.i:22: User Error:
+[kernel] tests/syntax/fam.i:28: User Error:
field `b' is declared with incomplete type char []
-[kernel] tests/syntax/fam.i:22: User Error:
+[kernel] tests/syntax/fam.i:28: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] tests/syntax/fam.i:43: User Error:
+[kernel] tests/syntax/fam.i:49: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] tests/syntax/fam.i:57: User Error:
+[kernel] tests/syntax/fam.i:63: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] tests/syntax/fam.i:71: User Error:
+[kernel] tests/syntax/fam.i:77: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] User Error: stopping on file "tests/syntax/fam.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle
index 890a48ecd862d9470b308cf965ff2cc6eb8c8dae..1747cd9c2c39144829c5697e1846f8828161ae67 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid1.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid1.i:2: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid1.i:7: User Error:
flexible array member 'data' (type char []) not allowed in otherwise empty struct
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid1.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle
index 9c14914576b0d4d2d23a3a463d1c19e8c8a89766..08b2bbe1285519910ffd0194603ecffc25ea179d 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid2.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid2.i:2: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid2.i:7: User Error:
field `data' is declared with incomplete type char []
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid2.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle
index 738f4dd85865879c0b2aed1b12e163c3ebdb8486..c7e88ab06296193f8a930b30f4ac9686c457763b 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid3.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid3.i:2: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid3.i:8: User Error:
field `data' is declared with incomplete type char []
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid3.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle
index 5ebb2f663bee3a6eea0e0badae1c837cacbe0f0c..238b92acd43a45da575a026a1ed434bdc0f90033 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid4.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid4.i:2: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid4.i:7: User Error:
field `data' is declared with incomplete type char []
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid4.i" that has
errors.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
index b72d52714a53559377d9fb88a5548899a3a9855a..8e1dca203f55c5b1536d845e7f3cb4826cac798d 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid5.i (no preprocessing)
-[kernel] tests/syntax/flexible_array_member_invalid5.i:7: User Error:
+[kernel] tests/syntax/flexible_array_member_invalid5.i:13: User Error:
field `f' declared with a type containing a flexible array member.
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid5.i" that has
errors.
diff --git a/tests/syntax/oracle/ghost_cv_incompat.res.oracle b/tests/syntax/oracle/ghost_cv_incompat.res.oracle
index 83f13fa55732a3b6f24a9e8db2be97083bd4e6e0..5f5a16766c2e9ca23359aedf9cd10be0ff3cb1db 100644
--- a/tests/syntax/oracle/ghost_cv_incompat.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_incompat.res.oracle
@@ -1,97 +1,97 @@
[kernel] Parsing tests/syntax/ghost_cv_incompat.i (no preprocessing)
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:22: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:27: Warning:
Invalid cast of '& ng' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:23: Warning:
- Invalid cast of 'gl_gp' from 'int *' to 'int \ghost *'
[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:28: Warning:
+ Invalid cast of 'gl_gp' from 'int *' to 'int \ghost *'
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:33: Warning:
Invalid cast of 'gl_p00' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:28: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:33: Warning:
Invalid cast of 'gl_p00' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:28: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:33: Warning:
Invalid cast of 'gl_p01' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:38: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:43: Warning:
Invalid cast of '& i' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:39: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:44: Warning:
Invalid cast of 'p' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:40: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:45: Warning:
Invalid cast of 'a' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:46: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:51: Warning:
Invalid cast of 'nga' from 'int (*)[10]' to 'int \ghost (*)[10]'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:53: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:58: Warning:
Invalid cast of 'p2' from 'int * \ghost *' to 'int \ghost * \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:54: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:59: Warning:
Invalid cast of 'array' from 'int * \ghost *' to 'int \ghost * \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:56: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:61: Warning:
Invalid cast of '*p2' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:57: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:62: Warning:
Invalid cast of 'array[0]' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:61: Warning:
- Invalid cast of 'p4' from 'int * \ghost (*)[10]' to 'int \ghost * \ghost * \ghost *'
[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:66: Warning:
+ Invalid cast of 'p4' from 'int * \ghost (*)[10]' to 'int \ghost * \ghost * \ghost *'
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:71: Warning:
Invalid cast of '& ng_var.field' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:74: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:79: Warning:
Invalid cast of '& i' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:75: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:80: Warning:
Invalid cast of 'p' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:76: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:81: Warning:
Invalid cast of 'a' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:78: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:83: Warning:
Cannot cast return of 'function' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:81: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:86: Warning:
Invalid cast of 'p00' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:81: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:86: Warning:
Invalid cast of 'p00' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:81: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:86: Warning:
Invalid cast of 'p01' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:89: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:94: Warning:
Invalid cast of '& i' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:90: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:95: Warning:
Invalid cast of '& i' from 'int *' to 'int \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:99: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:104: Warning:
Invalid cast of '& g' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:100: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:105: Warning:
Invalid cast of 'gl_gpg' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:115: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:120: Warning:
Invalid cast of '& i' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:116: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:121: Warning:
Invalid cast of 'p' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:117: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:122: Warning:
Invalid cast of 'a' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:123: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:128: Warning:
Invalid cast of 'gpai' from 'int (*)[10]' to 'int \ghost (*)[10]'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:130: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:135: Warning:
Invalid cast of 'p2' from 'int \ghost * \ghost *' to 'int * \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:131: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:136: Warning:
Invalid cast of 'array' from 'int \ghost * \ghost *' to 'int * \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:133: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:138: Warning:
Invalid cast of '*p2' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:134: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:139: Warning:
Invalid cast of 'array[0]' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:138: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:143: Warning:
Invalid cast of 'p4' from 'int \ghost * \ghost (*)[10]' to 'int * \ghost * \ghost *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:144: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:149: Warning:
Invalid cast of '& g_var.field' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:158: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:163: Warning:
Invalid cast of '& i' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:159: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:164: Warning:
Invalid cast of 'p' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:160: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:165: Warning:
Invalid cast of 'a' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:162: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:167: Warning:
Cannot cast return of 'function_g' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:165: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:170: Warning:
Invalid cast of 'p00' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:165: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:170: Warning:
Invalid cast of 'p00' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:165: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:170: Warning:
Invalid cast of 'p01' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:173: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:178: Warning:
Invalid cast of '& b' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:174: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:179: Warning:
Invalid cast of '& b' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:188: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:193: Warning:
Invalid cast of '& g_0' from 'int \ghost *' to 'int *'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:189: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_incompat.i:194: Warning:
Invalid cast of '& g_0' from 'int \ghost *' to 'int *'
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
index 16d262f30bb320f70beb9ba5de043807f9ff7357..0c09108e57d8f9a7f699139082b20552d9cf3937 100644
--- a/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_invalid_use.res.oracle
@@ -1,61 +1,61 @@
[kernel] Parsing tests/syntax/ghost_cv_invalid_use.i (no preprocessing)
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:10: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:14: Warning:
'ng' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:16: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:20: Warning:
'*ptr' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:21: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:25: Warning:
'ng_var.field' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:33: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:37: Warning:
'*ptrp' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:34: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:38: Warning:
'*(*ptrp)' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:35: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:39: Warning:
'*(*ptrpg)' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:36: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:40: Warning:
'*(arrp[0])' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:37: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:41: Warning:
'(*ptra)[0]' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:42: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:46: Warning:
'*a' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:50: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:54: Warning:
'*a' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:60: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:64: Warning:
'p' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:65: Warning:
- '*p' is a non-ghost lvalue, it cannot be assigned in ghost code
[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:69: Warning:
'*p' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:79: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:73: Warning:
+ '*p' is a non-ghost lvalue, it cannot be assigned in ghost code
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:83: Warning:
'*p' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:84: Warning:
- '*(p + (0 .. max))' is a non-ghost lvalue, it cannot be assigned in ghost code
[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:88: Warning:
'*(p + (0 .. max))' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:99: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:92: Warning:
'*(p + (0 .. max))' is a non-ghost lvalue, it cannot be assigned in ghost code
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:123: Warning:
- Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:124: Warning:
- Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:125: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:103: Warning:
+ '*(p + (0 .. max))' is a non-ghost lvalue, it cannot be assigned in ghost code
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:127: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:128: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:129: Warning:
Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:130: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:132: Warning:
Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:151: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:133: Warning:
Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:152: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:134: Warning:
Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:153: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:155: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:156: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:157: Warning:
Call to non-ghost function from ghost code is not allowed
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:158: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:160: Warning:
+ Call to non-ghost function from ghost code is not allowed
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:161: Warning:
+ Call to non-ghost function from ghost code is not allowed
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_invalid_use.i:162: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
index 11e0f79f7ac8199f0d10116325a2dfb06f0b267f..6a919917f2b276988d936cca115367b2fe07e7a3 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] tests/syntax/ghost_cv_parsing_errors.c:11:
+[kernel] tests/syntax/ghost_cv_parsing_errors.c:12:
Use of \ghost out of ghost code:
- Location: between lines 11 and 13, before or at token: \ghost
- 9 #ifdef IN_TYPE
- 10
+ Location: between lines 12 and 14, before or at token: \ghost
+ 10 #ifdef IN_TYPE
+ 11
- 11 struct S {
- 12 int a ;
- 13 } \ghost ;
+ 12 struct S {
+ 13 int a ;
+ 14 } \ghost ;
- 14
- 15 #endif
+ 15
+ 16 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
index 79a1e05ec98cfb5e45d89f7936d79fcabc1dbd21..fbf1db47255e1c8dbb1e37d680f7071d211b7a73 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] tests/syntax/ghost_cv_parsing_errors.c:19:
+[kernel] tests/syntax/ghost_cv_parsing_errors.c:20:
Use of \ghost out of ghost code:
- Location: line 19, between columns 0 and 4, before or at token: \ghost
- 17 #ifdef IN_DECL
- 18
- 19 int \ghost global ;
+ Location: line 20, between columns 0 and 4, before or at token: \ghost
+ 18 #ifdef IN_DECL
+ 19
+ 20 int \ghost global ;
^^^^^^^^^^^^^^^^^^^
- 20
- 21 #endif
+ 21
+ 22 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
index 221217ee8deff4d92b722f17e10e341859edccb3..1ab8175cb4e50711ffcb0d50a9e5510183c9b5f7 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] tests/syntax/ghost_cv_parsing_errors.c:25:
+[kernel] tests/syntax/ghost_cv_parsing_errors.c:26:
Use of \ghost out of ghost code:
- Location: line 25, between columns 14 and 14
- 23 #ifdef IN_GHOST_ATTR
- 24
- 25 int /*@ \ghost */ global ;
+ Location: line 26, between columns 14 and 14
+ 24 #ifdef IN_GHOST_ATTR
+ 25
+ 26 int /*@ \ghost */ global ;
^^^^^^^^^^^^^^^^^^^^^^^^^^
- 26
- 27 #endif
+ 27
+ 28 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle b/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle
index 19e4440c2c82f5bc39a032aa56eae8402042c268..dd8e3e9e2fbd50d002b9ec1d22e7f2c520bfcf58 100644
--- a/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_var_decl.0.res.oracle
@@ -1,39 +1,39 @@
[kernel] Parsing tests/syntax/ghost_cv_var_decl.c (with preprocessing)
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:12:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:15:
'g1' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:22:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:25:
'g1' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:23:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:26:
'g2' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:32:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:35:
'g0' elements are already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:45:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:48:
'g0' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:175:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:178:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:184:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:187:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:191:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:194:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:200:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:203:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:207:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:210:
'b' elements are already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:216:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:219:
'b' elements are already ghost
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:149: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:152: Warning:
No definition, nor assigns specification for ghost function 'decl_bad_return_type'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:149: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:152: Warning:
Invalid return type: indirection from non-ghost to ghost
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:150: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:153: Warning:
No definition, nor assigns specification for ghost function 'decl_bad_parameter_type'
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:150: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:153: Warning:
Invalid type for 'param': indirection from non-ghost to ghost
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:151: Warning:
- Invalid return type: indirection from non-ghost to ghost
[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:154: Warning:
+ Invalid return type: indirection from non-ghost to ghost
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:157: Warning:
Invalid type for 'param': indirection from non-ghost to ghost
-[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:163: Warning:
+[kernel:ghost:bad-use] tests/syntax/ghost_cv_var_decl.c:166: Warning:
Invalid type for 'pptrg': indirection from non-ghost to ghost
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
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 abe9b55416e548f97930b91e953498421d74f81c..47cd7ced61ba42f93890221e9f20e48b40c2eee3 100644
--- a/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_var_decl.1.res.oracle
@@ -1,195 +1,195 @@
[kernel] Parsing tests/syntax/ghost_cv_var_decl.c (with preprocessing)
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:12:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:15:
'g1' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:22:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:25:
'g1' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:23:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:26:
'g2' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:32:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:35:
'g0' elements are already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:45:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:48:
'g0' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:175:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:178:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:184:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:187:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:191:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:194:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:200:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:203:
'b' is already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:207:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:210:
'b' elements are already ghost
-[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:216:
+[kernel:ghost:already-ghost] tests/syntax/ghost_cv_var_decl.c:219:
'b' elements are already ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:8
+[kernel] tests/syntax/ghost_cv_var_decl.c:11
f_ints: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:9
+[kernel] tests/syntax/ghost_cv_var_decl.c:12
ng: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:11
+[kernel] tests/syntax/ghost_cv_var_decl.c:14
g0: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:12
- g1: ghost
[kernel] tests/syntax/ghost_cv_var_decl.c:15
+ g1: ghost
+[kernel] tests/syntax/ghost_cv_var_decl.c:18
f_ptrs: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:16
- ng: normal -> normal
[kernel] tests/syntax/ghost_cv_var_decl.c:19
+ ng: normal -> normal
+[kernel] tests/syntax/ghost_cv_var_decl.c:22
g: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:20
+[kernel] tests/syntax/ghost_cv_var_decl.c:23
g0: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:22
+[kernel] tests/syntax/ghost_cv_var_decl.c:25
g1: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:23
+[kernel] tests/syntax/ghost_cv_var_decl.c:26
g2: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:27
+[kernel] tests/syntax/ghost_cv_var_decl.c:30
f_arrays: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:28
- ng: normal -> normal
[kernel] tests/syntax/ghost_cv_var_decl.c:31
+ ng: normal -> normal
+[kernel] tests/syntax/ghost_cv_var_decl.c:34
g: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:32
+[kernel] tests/syntax/ghost_cv_var_decl.c:35
g0: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:40
+[kernel] tests/syntax/ghost_cv_var_decl.c:43
f_structs: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:41
- ng: normal -> { field: normal }
[kernel] tests/syntax/ghost_cv_var_decl.c:44
+ ng: normal -> { field: normal }
+[kernel] tests/syntax/ghost_cv_var_decl.c:47
g: ghost -> { field: ghost }
-[kernel] tests/syntax/ghost_cv_var_decl.c:45
+[kernel] tests/syntax/ghost_cv_var_decl.c:48
g0: ghost -> { field: ghost }
-[kernel] tests/syntax/ghost_cv_var_decl.c:52
+[kernel] tests/syntax/ghost_cv_var_decl.c:55
named: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:53
+[kernel] tests/syntax/ghost_cv_var_decl.c:56
a: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:54
+[kernel] tests/syntax/ghost_cv_var_decl.c:57
ptr: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:73
+[kernel] tests/syntax/ghost_cv_var_decl.c:76
nesting_non_ghost: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:74
+[kernel] tests/syntax/ghost_cv_var_decl.c:77
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:75
+[kernel] tests/syntax/ghost_cv_var_decl.c:78
ptr: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:76
+[kernel] tests/syntax/ghost_cv_var_decl.c:79
array: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:78
+[kernel] tests/syntax/ghost_cv_var_decl.c:81
pptr: normal -> normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:79
+[kernel] tests/syntax/ghost_cv_var_decl.c:82
parray: normal -> normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:80
+[kernel] tests/syntax/ghost_cv_var_decl.c:83
aptr: normal -> normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:81
+[kernel] tests/syntax/ghost_cv_var_decl.c:84
aarray: normal -> normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:83
+[kernel] tests/syntax/ghost_cv_var_decl.c:86
sp: normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:84
+[kernel] tests/syntax/ghost_cv_var_decl.c:87
sa: normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:85
+[kernel] tests/syntax/ghost_cv_var_decl.c:88
spa: normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:86
+[kernel] tests/syntax/ghost_cv_var_decl.c:89
sap: normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:88
+[kernel] tests/syntax/ghost_cv_var_decl.c:91
psp: normal -> normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:89
+[kernel] tests/syntax/ghost_cv_var_decl.c:92
psa: normal -> normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:90
+[kernel] tests/syntax/ghost_cv_var_decl.c:93
pspa: normal -> normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:91
+[kernel] tests/syntax/ghost_cv_var_decl.c:94
psap: normal -> normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:93
+[kernel] tests/syntax/ghost_cv_var_decl.c:96
asp: normal -> normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:94
+[kernel] tests/syntax/ghost_cv_var_decl.c:97
asa: normal -> normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:95
+[kernel] tests/syntax/ghost_cv_var_decl.c:98
aspa: normal -> normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:96
+[kernel] tests/syntax/ghost_cv_var_decl.c:99
asap: normal -> normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:101
+[kernel] tests/syntax/ghost_cv_var_decl.c:104
nesting_ghost: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:103
+[kernel] tests/syntax/ghost_cv_var_decl.c:106
a: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:104
+[kernel] tests/syntax/ghost_cv_var_decl.c:107
ptr: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:105
+[kernel] tests/syntax/ghost_cv_var_decl.c:108
ptrg: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:107
+[kernel] tests/syntax/ghost_cv_var_decl.c:110
array: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:109
+[kernel] tests/syntax/ghost_cv_var_decl.c:112
pptr: ghost -> normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:110
+[kernel] tests/syntax/ghost_cv_var_decl.c:113
pptrg: ghost -> ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:111
+[kernel] tests/syntax/ghost_cv_var_decl.c:114
pptrgg: ghost -> ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:113
+[kernel] tests/syntax/ghost_cv_var_decl.c:116
parray: ghost -> normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:114
+[kernel] tests/syntax/ghost_cv_var_decl.c:117
parrayg: ghost -> ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:116
+[kernel] tests/syntax/ghost_cv_var_decl.c:119
aptr: ghost -> ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:117
+[kernel] tests/syntax/ghost_cv_var_decl.c:120
aptrg: ghost -> ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:119
+[kernel] tests/syntax/ghost_cv_var_decl.c:122
aarray: ghost -> ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:121
+[kernel] tests/syntax/ghost_cv_var_decl.c:124
sp: ghost -> { field: ghost -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:122
+[kernel] tests/syntax/ghost_cv_var_decl.c:125
sa: ghost -> { field: ghost -> ghost }
-[kernel] tests/syntax/ghost_cv_var_decl.c:123
+[kernel] tests/syntax/ghost_cv_var_decl.c:126
spa: ghost -> { field: ghost -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:124
+[kernel] tests/syntax/ghost_cv_var_decl.c:127
sap: ghost -> { field: ghost -> ghost -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:126
+[kernel] tests/syntax/ghost_cv_var_decl.c:129
psp: ghost -> normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:127
+[kernel] tests/syntax/ghost_cv_var_decl.c:130
pspg: ghost -> ghost -> { field: ghost -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:129
+[kernel] tests/syntax/ghost_cv_var_decl.c:132
psa: ghost -> normal -> { field: normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:130
+[kernel] tests/syntax/ghost_cv_var_decl.c:133
psag: ghost -> ghost -> { field: ghost -> ghost }
-[kernel] tests/syntax/ghost_cv_var_decl.c:132
+[kernel] tests/syntax/ghost_cv_var_decl.c:135
pspa: ghost -> normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:133
+[kernel] tests/syntax/ghost_cv_var_decl.c:136
pspag: ghost -> ghost -> { field: ghost -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:135
+[kernel] tests/syntax/ghost_cv_var_decl.c:138
psap: ghost -> normal -> { field: normal -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:136
+[kernel] tests/syntax/ghost_cv_var_decl.c:139
psapg: ghost -> ghost -> { field: ghost -> ghost -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:138
+[kernel] tests/syntax/ghost_cv_var_decl.c:141
asp: ghost -> ghost -> { field: ghost -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:139
+[kernel] tests/syntax/ghost_cv_var_decl.c:142
asa: ghost -> ghost -> { field: ghost -> ghost }
-[kernel] tests/syntax/ghost_cv_var_decl.c:140
+[kernel] tests/syntax/ghost_cv_var_decl.c:143
aspa: ghost -> ghost -> { field: ghost -> normal -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:141
+[kernel] tests/syntax/ghost_cv_var_decl.c:144
asap: ghost -> ghost -> { field: ghost -> ghost -> normal }
-[kernel] tests/syntax/ghost_cv_var_decl.c:171
+[kernel] tests/syntax/ghost_cv_var_decl.c:174
foo_1: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:171
+[kernel] tests/syntax/ghost_cv_var_decl.c:174
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:175
+[kernel] tests/syntax/ghost_cv_var_decl.c:178
foo_2: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:175
+[kernel] tests/syntax/ghost_cv_var_decl.c:178
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:175
+[kernel] tests/syntax/ghost_cv_var_decl.c:178
b: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:179
+[kernel] tests/syntax/ghost_cv_var_decl.c:182
foo_3: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:179
+[kernel] tests/syntax/ghost_cv_var_decl.c:182
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:179
+[kernel] tests/syntax/ghost_cv_var_decl.c:182
b: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:179
+[kernel] tests/syntax/ghost_cv_var_decl.c:182
c: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:183
+[kernel] tests/syntax/ghost_cv_var_decl.c:186
bar_1: normal
[kernel] :0
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:184
+[kernel] tests/syntax/ghost_cv_var_decl.c:187
bar_2: normal
[kernel] :0
a: normal
[kernel] :0
b: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:185
+[kernel] tests/syntax/ghost_cv_var_decl.c:188
bar_3: normal
[kernel] :0
a: normal
@@ -197,35 +197,35 @@
b: ghost
[kernel] :0
c: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:187
+[kernel] tests/syntax/ghost_cv_var_decl.c:190
pfoo_1: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:187
+[kernel] tests/syntax/ghost_cv_var_decl.c:190
a: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:191
+[kernel] tests/syntax/ghost_cv_var_decl.c:194
pfoo_2: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:191
+[kernel] tests/syntax/ghost_cv_var_decl.c:194
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:191
+[kernel] tests/syntax/ghost_cv_var_decl.c:194
b: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:195
+[kernel] tests/syntax/ghost_cv_var_decl.c:198
pfoo_3: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:195
+[kernel] tests/syntax/ghost_cv_var_decl.c:198
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:195
+[kernel] tests/syntax/ghost_cv_var_decl.c:198
b: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:195
+[kernel] tests/syntax/ghost_cv_var_decl.c:198
c: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:199
+[kernel] tests/syntax/ghost_cv_var_decl.c:202
pbar_1: normal
[kernel] :0
a: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:200
+[kernel] tests/syntax/ghost_cv_var_decl.c:203
pbar_2: normal
[kernel] :0
a: normal
[kernel] :0
b: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:201
+[kernel] tests/syntax/ghost_cv_var_decl.c:204
pbar_3: normal
[kernel] :0
a: normal
@@ -233,63 +233,63 @@
b: ghost -> ghost
[kernel] :0
c: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:203
+[kernel] tests/syntax/ghost_cv_var_decl.c:206
afoo_1: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:203
+[kernel] tests/syntax/ghost_cv_var_decl.c:206
a: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:207
+[kernel] tests/syntax/ghost_cv_var_decl.c:210
afoo_2: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:207
+[kernel] tests/syntax/ghost_cv_var_decl.c:210
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:207
+[kernel] tests/syntax/ghost_cv_var_decl.c:210
b: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:211
+[kernel] tests/syntax/ghost_cv_var_decl.c:214
afoo_3: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:211
+[kernel] tests/syntax/ghost_cv_var_decl.c:214
a: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:211
+[kernel] tests/syntax/ghost_cv_var_decl.c:214
b: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:215
+[kernel] tests/syntax/ghost_cv_var_decl.c:218
abar_1: normal
[kernel] :0
a: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:216
+[kernel] tests/syntax/ghost_cv_var_decl.c:219
abar_2: normal
[kernel] :0
a: normal
[kernel] :0
b: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:217
+[kernel] tests/syntax/ghost_cv_var_decl.c:220
abar_3: normal
[kernel] :0
a: normal
[kernel] :0
b: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:220
+[kernel] tests/syntax/ghost_cv_var_decl.c:223
reference_functions: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:225
+[kernel] tests/syntax/ghost_cv_var_decl.c:228
v: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:226
+[kernel] tests/syntax/ghost_cv_var_decl.c:229
gp: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:231
+[kernel] tests/syntax/ghost_cv_var_decl.c:234
ng: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:232
+[kernel] tests/syntax/ghost_cv_var_decl.c:235
ga: ghost -> ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:245
+[kernel] tests/syntax/ghost_cv_var_decl.c:248
x: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:239
+[kernel] tests/syntax/ghost_cv_var_decl.c:242
i: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:240
+[kernel] tests/syntax/ghost_cv_var_decl.c:243
p: normal -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:242
+[kernel] tests/syntax/ghost_cv_var_decl.c:245
gp1: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:243
+[kernel] tests/syntax/ghost_cv_var_decl.c:246
gp2: ghost -> normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:245
+[kernel] tests/syntax/ghost_cv_var_decl.c:248
x: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:247
+[kernel] tests/syntax/ghost_cv_var_decl.c:250
main: normal
-[kernel] tests/syntax/ghost_cv_var_decl.c:248
+[kernel] tests/syntax/ghost_cv_var_decl.c:251
value: ghost
-[kernel] tests/syntax/ghost_cv_var_decl.c:249
+[kernel] tests/syntax/ghost_cv_var_decl.c:252
__retres: normal
diff --git a/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle b/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
index ded857214d7df397ddd4536ad0c1e3202448c04c..7d11d6d80c426f9d896ea6bb7dd4317a364d8e2e 100644
--- a/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
@@ -3,7 +3,7 @@
syntax error:
Location: between lines 6 and 8, before or at token:
- 4
+ 4 */
5 void if_ghost_else_one_line_bad(int x, int y) {
6 if (x) {
diff --git a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
index f1017ea0fd6d2995e921f0f11b879852e02a5d53..57ace82adf4d748cc114423a10da8bd639362cb2 100644
--- a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
+++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/ghost_local_ill_formed.i (no preprocessing)
-[kernel] tests/syntax/ghost_local_ill_formed.i:5: User Error:
+[kernel] tests/syntax/ghost_local_ill_formed.i:9: User Error:
redefinition of 'c' in the same scope.
- Previous declaration was at tests/syntax/ghost_local_ill_formed.i:2
-[kernel] tests/syntax/ghost_local_ill_formed.i:17: User Error:
+ Previous declaration was at tests/syntax/ghost_local_ill_formed.i:6
+[kernel] tests/syntax/ghost_local_ill_formed.i:21: User Error:
Variable c is a ghost symbol. It cannot be used in non-ghost context. Did you forget a /*@ ghost ... /?
[kernel] User Error: stopping on file "tests/syntax/ghost_local_ill_formed.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.0.res.oracle b/tests/syntax/oracle/ghost_parameters.0.res.oracle
index 926c68c1c6b88ab5190ce6d4e0fc0db055e8652e..4fb237c265e78b5b17f2c644b71be992e0e5d451 100644
--- a/tests/syntax/oracle/ghost_parameters.0.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.0.res.oracle
@@ -1,23 +1,23 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:29: User Error:
+[kernel] tests/syntax/ghost_parameters.c:32: User Error:
Too few ghost arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:30: User Error:
+[kernel] tests/syntax/ghost_parameters.c:33: User Error:
Too few ghost arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:31: User Error:
+[kernel] tests/syntax/ghost_parameters.c:34: User Error:
Too few arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:32: User Error:
+[kernel] tests/syntax/ghost_parameters.c:35: User Error:
Too few ghost arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:32: User Error:
+[kernel] tests/syntax/ghost_parameters.c:35: User Error:
Too many arguments in call to function
-[kernel] tests/syntax/ghost_parameters.c:33: User Error:
+[kernel] tests/syntax/ghost_parameters.c:36: User Error:
Too many ghost arguments in call to function
-[kernel] tests/syntax/ghost_parameters.c:33: User Error:
+[kernel] tests/syntax/ghost_parameters.c:36: User Error:
Too few arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:35: User Error:
+[kernel] tests/syntax/ghost_parameters.c:38: User Error:
Too few arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:36: User Error:
+[kernel] tests/syntax/ghost_parameters.c:39: User Error:
Too few arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:37: User Error:
+[kernel] tests/syntax/ghost_parameters.c:40: User Error:
Too few arguments in call to function.
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/ghost_parameters.1.res.oracle b/tests/syntax/oracle/ghost_parameters.1.res.oracle
index 614c8ad74c075c9e1eb74b8277c9cb1dd90ff432..73c87461ca1c48b79a3b102cb33ef57b08d1ce98 100644
--- a/tests/syntax/oracle/ghost_parameters.1.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.1.res.oracle
@@ -1,21 +1,21 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:54: User Error:
+[kernel] tests/syntax/ghost_parameters.c:57: User Error:
Too few ghost arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:55: User Error:
+[kernel] tests/syntax/ghost_parameters.c:58: User Error:
Too few ghost arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:56: User Error:
+[kernel] tests/syntax/ghost_parameters.c:59: User Error:
Too many arguments in call to function
-[kernel] tests/syntax/ghost_parameters.c:57: User Error:
+[kernel] tests/syntax/ghost_parameters.c:60: User Error:
Too few ghost arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:57: User Error:
+[kernel] tests/syntax/ghost_parameters.c:60: User Error:
Too many arguments in call to function
-[kernel] tests/syntax/ghost_parameters.c:58: User Error:
+[kernel] tests/syntax/ghost_parameters.c:61: User Error:
Too many ghost arguments in call to function
-[kernel] tests/syntax/ghost_parameters.c:60: User Error:
+[kernel] tests/syntax/ghost_parameters.c:63: User Error:
Too few arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:61: User Error:
+[kernel] tests/syntax/ghost_parameters.c:64: User Error:
Too few arguments in call to function.
-[kernel] tests/syntax/ghost_parameters.c:62: User Error:
+[kernel] tests/syntax/ghost_parameters.c:65: User Error:
Too many arguments in call to function
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/ghost_parameters.10.res.oracle b/tests/syntax/oracle/ghost_parameters.10.res.oracle
index 477b266404d4270969128b8295e5957a8ffb1083..a98fcc2d2869de77d0a0ab390b9cdb8c86ba95a8 100644
--- a/tests/syntax/oracle/ghost_parameters.10.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.10.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:184: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:178 (different number of arguments).
-[kernel] tests/syntax/ghost_parameters.c:184: User Error:
+[kernel] tests/syntax/ghost_parameters.c:187: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:181 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:187: User Error:
Inconsistent formals
- 182 }
- 183
- 184 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 185 }
+ 186
+ 187 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 185
- 186 }
+ 188
+ 189 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.11.res.oracle b/tests/syntax/oracle/ghost_parameters.11.res.oracle
index 1d8c5da2c6f63a8b566ed678f910648131c852eb..0651a7a4fb06805d45583a09798076d9f49b0c72 100644
--- a/tests/syntax/oracle/ghost_parameters.11.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.11.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:192:
+[kernel] tests/syntax/ghost_parameters.c:195:
syntax error:
- Location: line 192, between columns 35 and 36, before or at token: )
- 190 #ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
- 191
- 192 void function_void(void) /*@ ghost () */ {
+ Location: line 195, between columns 35 and 36, before or at token: )
+ 193 #ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
+ 194
+ 195 void function_void(void) /*@ ghost () */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 193
- 194 }
+ 196
+ 197 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.12.res.oracle b/tests/syntax/oracle/ghost_parameters.12.res.oracle
index 8bc53156a937624d69449742be9e9d452f89dedf..e2ccb5f8899c698dcf41b46d5338fb7ebe41ace1 100644
--- a/tests/syntax/oracle/ghost_parameters.12.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.12.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:200: User Error:
+[kernel] tests/syntax/ghost_parameters.c:203: User Error:
ghost parameters list cannot be void
-[kernel] tests/syntax/ghost_parameters.c:204: User Error:
+[kernel] tests/syntax/ghost_parameters.c:207: User Error:
ghost parameters list cannot be void
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/ghost_parameters.3.res.oracle b/tests/syntax/oracle/ghost_parameters.3.res.oracle
index c621d5748d1d6aa8f095a4cb262df1322c86d17d..a6fcb41b2ae94d9e62eeb0563cf1c7c04fc3cce7 100644
--- a/tests/syntax/oracle/ghost_parameters.3.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.3.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:89: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:85 (different number of arguments).
-[kernel] tests/syntax/ghost_parameters.c:89: User Error:
+[kernel] tests/syntax/ghost_parameters.c:92: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:88 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:92: User Error:
Inconsistent formals
- 87 }
- 88
- 89 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 90 }
+ 91
+ 92 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 90
- 91 }
+ 93
+ 94 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.4.res.oracle b/tests/syntax/oracle/ghost_parameters.4.res.oracle
index d6b376ee2b1e3a910608069d60980a8f0f23dde8..1c0dd17504194b4ce87e1f80caaf68835f21f952 100644
--- a/tests/syntax/oracle/ghost_parameters.4.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.4.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:103: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:97 (different number of arguments).
-[kernel] tests/syntax/ghost_parameters.c:103: User Error:
+[kernel] tests/syntax/ghost_parameters.c:106: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:100 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:106: User Error:
Inconsistent formals
- 101 }
- 102
- 103 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 104 }
+ 105
+ 106 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 104
- 105 }
+ 107
+ 108 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.5.res.oracle b/tests/syntax/oracle/ghost_parameters.5.res.oracle
index 138709d0a9bdc0236cd4021f28304fb0a23c312a..4b4cafeba689033db21f4171a41081ac55619d8d 100644
--- a/tests/syntax/oracle/ghost_parameters.5.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.5.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:116: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:112 (different number of ghost arguments).
-[kernel] tests/syntax/ghost_parameters.c:116: User Error:
+[kernel] tests/syntax/ghost_parameters.c:119: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:115 (different number of ghost arguments).
+[kernel] tests/syntax/ghost_parameters.c:119: User Error:
Inconsistent formals
- 114 }
- 115
- 116 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 117 }
+ 118
+ 119 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 117
- 118 }
+ 120
+ 121 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.6.res.oracle b/tests/syntax/oracle/ghost_parameters.6.res.oracle
index 5807a9726441f905b6ffed9dd250f8ce4ec425d4..35d3d52f66099892f79e46267b1c6a92b43a667c 100644
--- a/tests/syntax/oracle/ghost_parameters.6.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.6.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:130: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:124 (different number of ghost arguments).
-[kernel] tests/syntax/ghost_parameters.c:130: User Error:
+[kernel] tests/syntax/ghost_parameters.c:133: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:127 (different number of ghost arguments).
+[kernel] tests/syntax/ghost_parameters.c:133: User Error:
Inconsistent formals
- 128 }
- 129
- 130 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 131 }
+ 132
+ 133 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 131
- 132 }
+ 134
+ 135 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.7.res.oracle b/tests/syntax/oracle/ghost_parameters.7.res.oracle
index e5de27561f6b32bb38613b5762dbd2632e2999b4..5c437cf03fc9619c4bfc458f652858be834d4bf6 100644
--- a/tests/syntax/oracle/ghost_parameters.7.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.7.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:143: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:139 (different number of arguments).
-[kernel] tests/syntax/ghost_parameters.c:143: User Error:
+[kernel] tests/syntax/ghost_parameters.c:146: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:142 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:146: User Error:
Inconsistent formals
- 141 }
- 142
- 143 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 144 }
+ 145
+ 146 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 144
- 145 }
+ 147
+ 148 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.8.res.oracle b/tests/syntax/oracle/ghost_parameters.8.res.oracle
index bb6ac89e90999848f2a97340e24f02d246491450..0327e4ab2986e625e3e22a1517cc391b09e35df2 100644
--- a/tests/syntax/oracle/ghost_parameters.8.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.8.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:157: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:151 (different number of arguments).
-[kernel] tests/syntax/ghost_parameters.c:157: User Error:
+[kernel] tests/syntax/ghost_parameters.c:160: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:154 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:160: User Error:
Inconsistent formals
- 155 }
- 156
- 157 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 158 }
+ 159
+ 160 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 158
- 159 }
+ 161
+ 162 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.9.res.oracle b/tests/syntax/oracle/ghost_parameters.9.res.oracle
index 53080c4e6f3f5a60ba9ad30cd6a8621da29d5a5d..a75c5519836c379430a3e5c9060eecccbd4914ff 100644
--- a/tests/syntax/oracle/ghost_parameters.9.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.9.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
-[kernel] tests/syntax/ghost_parameters.c:170: User Error:
- Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:166 (different number of arguments).
-[kernel] tests/syntax/ghost_parameters.c:170: User Error:
+[kernel] tests/syntax/ghost_parameters.c:173: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:169 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:173: User Error:
Inconsistent formals
- 168 }
- 169
- 170 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ 171 }
+ 172
+ 173 void function(int a, int b) /*@ ghost(int c, int d) */ {
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 171
- 172 }
+ 174
+ 175 }
[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/incompatible_qualifiers.0.res.oracle b/tests/syntax/oracle/incompatible_qualifiers.0.res.oracle
index 7acff04489b2fdb56a9248e581427dbb33def21c..89200b976aee9b260720a68718b3c19e0bc4652a 100644
--- a/tests/syntax/oracle/incompatible_qualifiers.0.res.oracle
+++ b/tests/syntax/oracle/incompatible_qualifiers.0.res.oracle
@@ -1,22 +1,18 @@
[kernel] Parsing tests/syntax/incompatible_qualifiers.c (with preprocessing)
-[kernel] tests/syntax/incompatible_qualifiers.c:11: User Error:
- Declaration of f does not match previous declaration from tests/syntax/incompatible_qualifiers.c:9 (different qualifiers).
-[kernel] tests/syntax/incompatible_qualifiers.c:19: User Error:
- Declaration of h does not match previous declaration from tests/syntax/incompatible_qualifiers.c:17 (different qualifiers).
-[kernel] tests/syntax/incompatible_qualifiers.c:27: User Error:
- Declaration of j does not match previous declaration from tests/syntax/incompatible_qualifiers.c:25 (different qualifiers).
-[kernel] tests/syntax/incompatible_qualifiers.c:38: User Error:
- Declaration of l does not match previous declaration from tests/syntax/incompatible_qualifiers.c:36 (different qualifiers).
-[kernel] tests/syntax/incompatible_qualifiers.c:46: User Error:
- Declaration of n does not match previous declaration from tests/syntax/incompatible_qualifiers.c:44 (different qualifiers).
-[kernel] tests/syntax/incompatible_qualifiers.c:51: User Error:
+[kernel] tests/syntax/incompatible_qualifiers.c:13: User Error:
+ Declaration of f does not match previous declaration from tests/syntax/incompatible_qualifiers.c:11 (different qualifiers).
+[kernel] tests/syntax/incompatible_qualifiers.c:21: User Error:
+ Declaration of h does not match previous declaration from tests/syntax/incompatible_qualifiers.c:19 (different qualifiers).
+[kernel] tests/syntax/incompatible_qualifiers.c:29: User Error:
+ Declaration of j does not match previous declaration from tests/syntax/incompatible_qualifiers.c:27 (different qualifiers).
+[kernel] tests/syntax/incompatible_qualifiers.c:40: User Error:
+ Declaration of l does not match previous declaration from tests/syntax/incompatible_qualifiers.c:38 (different qualifiers).
+[kernel] tests/syntax/incompatible_qualifiers.c:48: User Error:
+ Declaration of n does not match previous declaration from tests/syntax/incompatible_qualifiers.c:46 (different qualifiers).
+[kernel] tests/syntax/incompatible_qualifiers.c:53: User Error:
invalid usage of 'restrict' qualifier
-[kernel] tests/syntax/incompatible_qualifiers.c:65: User Error:
+[kernel] tests/syntax/incompatible_qualifiers.c:67: User Error:
function pointer type does not allow 'restrict' qualifier
-[kernel] tests/syntax/incompatible_qualifiers.c:72: User Error:
- invalid usage of 'restrict' qualifier
-[kernel] tests/syntax/incompatible_qualifiers.c:73: User Error:
- invalid usage of 'restrict' qualifier
[kernel] tests/syntax/incompatible_qualifiers.c:74: User Error:
invalid usage of 'restrict' qualifier
[kernel] tests/syntax/incompatible_qualifiers.c:75: User Error:
@@ -24,6 +20,10 @@
[kernel] tests/syntax/incompatible_qualifiers.c:76: User Error:
invalid usage of 'restrict' qualifier
[kernel] tests/syntax/incompatible_qualifiers.c:77: User Error:
+ invalid usage of 'restrict' qualifier
+[kernel] tests/syntax/incompatible_qualifiers.c:78: User Error:
+ invalid usage of 'restrict' qualifier
+[kernel] tests/syntax/incompatible_qualifiers.c:79: User Error:
function pointer type does not allow 'restrict' qualifier
[kernel] User Error: stopping on file "tests/syntax/incompatible_qualifiers.c" that has errors.
Add '-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/incomplete_array.res.oracle b/tests/syntax/oracle/incomplete_array.res.oracle
index b00e464eb824b298be4ec4cf57fe4705e4c6d82d..ac5c2714b71df9b1c1460513ed0fe189b952cf00 100644
--- a/tests/syntax/oracle/incomplete_array.res.oracle
+++ b/tests/syntax/oracle/incomplete_array.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/incomplete_array.i (no preprocessing)
-[kernel] tests/syntax/incomplete_array.i:7: User Error:
+[kernel] tests/syntax/incomplete_array.i:11: User Error:
declaration of array of incomplete type 'struct S`
[kernel] User Error: stopping on file "tests/syntax/incomplete_array.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/incomplete_struct_field.res.oracle b/tests/syntax/oracle/incomplete_struct_field.res.oracle
index 1da6f42644dd16360b1ebdbd454d298ccbd0d4ab..1fd54ec0cfd8ceb5a376b144f885cb2f48cc6043 100644
--- a/tests/syntax/oracle/incomplete_struct_field.res.oracle
+++ b/tests/syntax/oracle/incomplete_struct_field.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing tests/syntax/incomplete_struct_field.i (no preprocessing)
-[kernel] tests/syntax/incomplete_struct_field.i:1: User Error:
+[kernel] tests/syntax/incomplete_struct_field.i:5: User Error:
declaration of array of incomplete type 'struct _s`
-[kernel] tests/syntax/incomplete_struct_field.i:1: User Error:
+[kernel] tests/syntax/incomplete_struct_field.i:5: User Error:
field `v' is declared with incomplete type struct _s [12]
-[kernel] tests/syntax/incomplete_struct_field.i:1: User Error:
+[kernel] tests/syntax/incomplete_struct_field.i:5: User Error:
type struct _s is circular
[kernel] User Error: stopping on file "tests/syntax/incomplete_struct_field.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_decl.0.res.oracle b/tests/syntax/oracle/inconsistent_decl.0.res.oracle
index 0533b81aa66297b03a1edf90abcb01ed7e0d7d4b..c61779854906d5d6bd9d795a146816f6b35d3f89 100644
--- a/tests/syntax/oracle/inconsistent_decl.0.res.oracle
+++ b/tests/syntax/oracle/inconsistent_decl.0.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing tests/syntax/inconsistent_decl.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/syntax/inconsistent_decl.c:11: Warning:
+[kernel:typing:implicit-function-declaration] tests/syntax/inconsistent_decl.c:12: Warning:
Calling undeclared function f. Old style K&R code?
[kernel] Parsing tests/syntax/inconsistent_decl_2.i (no preprocessing)
[kernel] User Error: Incompatible declaration for f:
different type constructors: int vs. double
- First declaration was at tests/syntax/inconsistent_decl.c:11
+ First declaration was at tests/syntax/inconsistent_decl.c:12
Current declaration is at tests/syntax/inconsistent_decl_2.i:5
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_decl.1.res.oracle b/tests/syntax/oracle/inconsistent_decl.1.res.oracle
index 20264c218aafa8fa9b1e077d4a4ff778a20b08a0..351743abc10e75821b85ac3441a8ff476fa9573c 100644
--- a/tests/syntax/oracle/inconsistent_decl.1.res.oracle
+++ b/tests/syntax/oracle/inconsistent_decl.1.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/syntax/inconsistent_decl.c (with preprocessing)
-[kernel:typing:no-proto] tests/syntax/inconsistent_decl.c:11: Warning:
+[kernel:typing:no-proto] tests/syntax/inconsistent_decl.c:12: Warning:
Calling function f that is declared without prototype.
Its formals will be inferred from actual arguments
[kernel] Parsing tests/syntax/inconsistent_decl_2.i (no preprocessing)
[kernel] User Error: Incompatible declaration for f:
different type constructors: int vs. double
- First declaration was at tests/syntax/inconsistent_decl.c:7
+ First declaration was at tests/syntax/inconsistent_decl.c:8
Current declaration is at tests/syntax/inconsistent_decl_2.i:5
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/init_bts1352.res.oracle b/tests/syntax/oracle/init_bts1352.res.oracle
index 1f56fffc94ca2a804e9578d192f5ac6b6b68ac37..9070651b18ee79f3817a84dec96b259fe9932325 100644
--- a/tests/syntax/oracle/init_bts1352.res.oracle
+++ b/tests/syntax/oracle/init_bts1352.res.oracle
@@ -1,9 +1,10 @@
[kernel] Parsing tests/syntax/init_bts1352.i (no preprocessing)
-[kernel] tests/syntax/init_bts1352.i:2: User Error:
+[kernel] tests/syntax/init_bts1352.i:8: User Error:
scalar value (of type int) initialized by compound initializer
- 1 int main(void) {
- 2 int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
+ 6
+ 7 int main(void) {
+ 8 int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 3 }
+ 9 }
[kernel] User Error: stopping on file "tests/syntax/init_bts1352.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/invalid_constant.res.oracle b/tests/syntax/oracle/invalid_constant.res.oracle
index ea07d5fbb326453e5406634bfda1b8458bd0248b..b4b0da647d4313161e9561d38aa1b02bb4c8dfff 100644
--- a/tests/syntax/oracle/invalid_constant.res.oracle
+++ b/tests/syntax/oracle/invalid_constant.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/invalid_constant.i (no preprocessing)
-[kernel] tests/syntax/invalid_constant.i:2: Failure:
+[kernel] tests/syntax/invalid_constant.i:6: Failure:
Invalid digit 8 in integer constant '0123456789' in base 8.
[kernel] User Error: stopping on file "tests/syntax/invalid_constant.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/line_number.res.oracle b/tests/syntax/oracle/line_number.res.oracle
index 31ecbc78f906c2563141cad799311d5eda8286fa..a1c31a18635a515a610b3c172e735e014f147d8b 100644
--- a/tests/syntax/oracle/line_number.res.oracle
+++ b/tests/syntax/oracle/line_number.res.oracle
@@ -1,8 +1,10 @@
[kernel] Parsing tests/syntax/line_number.c (with preprocessing)
-[kernel] tests/syntax/line_number.c:1:
+[kernel] tests/syntax/line_number.c:6:
syntax error:
- 1 //@ assert \result == 0;
+ 4 */
+ 5
+ 6 //@ assert \result == 0;
^^^^^^^^^^^^^^^^^^^^^^^^
- 2 extern int p(void void);
+ 7 extern int p(void void);
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/lvalvoid.res.oracle b/tests/syntax/oracle/lvalvoid.res.oracle
index f84b2e3041b25539a45b3a2c42676ac9e0f7e8f4..4d18770bdb646c110b57c5d5ba30d82f3312513e 100644
--- a/tests/syntax/oracle/lvalvoid.res.oracle
+++ b/tests/syntax/oracle/lvalvoid.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/syntax/lvalvoid.i (no preprocessing)
-[kernel] tests/syntax/lvalvoid.i:4: Failure: lvalue of type void: *(src + i)
+[kernel] tests/syntax/lvalvoid.i:8: Failure: lvalue of type void: *(src + i)
[kernel] User Error: stopping on file "tests/syntax/lvalvoid.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/merge_unused.res.oracle b/tests/syntax/oracle/merge_unused.res.oracle
index 70f368124fe046ac15e316f1a3b5c9c82b3519ad..89e2f903de59e9bf367c2a941447d3648748be4a 100644
--- a/tests/syntax/oracle/merge_unused.res.oracle
+++ b/tests/syntax/oracle/merge_unused.res.oracle
@@ -13,7 +13,7 @@
int i ;
};
- First declaration was at tests/syntax/merge_unused.c:11
+ First declaration was at tests/syntax/merge_unused.c:12
Current declaration is at tests/syntax/merge_unused.h:7
Current declaration is unused, silently removing it
[kernel] User Error: Incompatible declaration for G3:
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
index b90f4dc55f6e2c31b6f7656f8f8cc0ecfa6cf03d..c434bbfc224f4aebda78bbc2c97c6403f6aebc84 100644
--- a/tests/syntax/oracle/multiple_froms.res.oracle
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/multiple_froms.i (no preprocessing)
[kernel:annot:multi-from] Warning:
- Drop 'b' \from at tests/syntax/multiple_froms.i:9 for more precise one at tests/syntax/multiple_froms.i:10
+ Drop 'b' \from at tests/syntax/multiple_froms.i:15 for more precise one at tests/syntax/multiple_froms.i:16
[kernel:annot:multi-from] Warning:
- Drop 'a' \from at tests/syntax/multiple_froms.i:7 for more precise one at tests/syntax/multiple_froms.i:6
+ Drop 'a' \from at tests/syntax/multiple_froms.i:13 for more precise one at tests/syntax/multiple_froms.i:12
/* Generated by Frama-C */
int a;
int b;
diff --git a/tests/syntax/oracle/mutually_recursive_struct.res.oracle b/tests/syntax/oracle/mutually_recursive_struct.res.oracle
index 74ebf746db91b9e965360d7c32544edc1075bf5e..cdcbc56b85cb8a17ea24d453f2c232ff8a05f9b2 100644
--- a/tests/syntax/oracle/mutually_recursive_struct.res.oracle
+++ b/tests/syntax/oracle/mutually_recursive_struct.res.oracle
@@ -1,13 +1,13 @@
[kernel] Parsing tests/syntax/mutually_recursive_struct.i (no preprocessing)
-[kernel] tests/syntax/mutually_recursive_struct.i:4: User Error:
+[kernel] tests/syntax/mutually_recursive_struct.i:9: User Error:
declaration of array of incomplete type 'struct S2`
-[kernel] tests/syntax/mutually_recursive_struct.i:4: User Error:
+[kernel] tests/syntax/mutually_recursive_struct.i:9: User Error:
field `s2' is declared with incomplete type struct S2 [2]
-[kernel] tests/syntax/mutually_recursive_struct.i:6: User Error:
+[kernel] tests/syntax/mutually_recursive_struct.i:11: User Error:
declaration of array of incomplete type 'struct S1`
-[kernel] tests/syntax/mutually_recursive_struct.i:6: User Error:
+[kernel] tests/syntax/mutually_recursive_struct.i:11: User Error:
field `s1' is declared with incomplete type struct S1 [2]
-[kernel] tests/syntax/mutually_recursive_struct.i:6: User Error:
+[kernel] tests/syntax/mutually_recursive_struct.i:11: User Error:
type struct S2 is circular
[kernel] User Error: stopping on file "tests/syntax/mutually_recursive_struct.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/no_prototype.res.oracle b/tests/syntax/oracle/no_prototype.res.oracle
index b0064d8723ea85a6a45fcc5a4040da540487485c..9bb1885d269161234d68e0f2c13438ebe1311804 100644
--- a/tests/syntax/oracle/no_prototype.res.oracle
+++ b/tests/syntax/oracle/no_prototype.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/no_prototype.i (no preprocessing)
-[kernel:typing:no-proto] tests/syntax/no_prototype.i:4: Warning:
+[kernel:typing:no-proto] tests/syntax/no_prototype.i:9: Warning:
Calling function foo that is declared without prototype.
Its formals will be inferred from actual arguments
-[kernel] tests/syntax/no_prototype.i:6: User Error:
- Declaration of foo does not match previous declaration from tests/syntax/no_prototype.i:1 (different number of arguments).
+[kernel] tests/syntax/no_prototype.i:11: User Error:
+ Declaration of foo does not match previous declaration from tests/syntax/no_prototype.i:6 (different number of arguments).
[kernel] User Error: stopping on file "tests/syntax/no_prototype.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/rettype.res.oracle b/tests/syntax/oracle/rettype.res.oracle
index 0b3783f28964f90407a67e0aca5c947569388b7d..85dda4b5756e386d116d358c76f9c68f3ca596f3 100644
--- a/tests/syntax/oracle/rettype.res.oracle
+++ b/tests/syntax/oracle/rettype.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/syntax/rettype.i (no preprocessing)
-[kernel] tests/syntax/rettype.i:8: User Error:
- Declaration of foo does not match previous declaration from tests/syntax/rettype.i:5 (different integer types:
+[kernel] tests/syntax/rettype.i:12: User Error:
+ Declaration of foo does not match previous declaration from tests/syntax/rettype.i:9 (different integer types:
'int' and 'unsigned short').
-[kernel] tests/syntax/rettype.i:7: Warning:
- found two contracts (old location: tests/syntax/rettype.i:4). Merging them
+[kernel] tests/syntax/rettype.i:11: Warning:
+ found two contracts (old location: tests/syntax/rettype.i:8). Merging them
[kernel] User Error: stopping on file "tests/syntax/rettype.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/sizeof_incomplete_type.res.oracle b/tests/syntax/oracle/sizeof_incomplete_type.res.oracle
index 37dab603578cf0871a5a4db6574b22f76161a385..2388b58b2c57db3e0a8640bb2b58d4f72882d4b7 100644
--- a/tests/syntax/oracle/sizeof_incomplete_type.res.oracle
+++ b/tests/syntax/oracle/sizeof_incomplete_type.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/sizeof_incomplete_type.c (with preprocessing)
-[kernel] tests/syntax/sizeof_incomplete_type.c:21: User Error:
+[kernel] tests/syntax/sizeof_incomplete_type.c:26: User Error:
sizeof on incomplete type 'struct inexistent'
[kernel] User Error: stopping on file "tests/syntax/sizeof_incomplete_type.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle b/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
index 84a6987f04d2ca7793c48046d7d166f1323aaaef..92f8b8d02b28340680cdcc04ada03fc045c83138 100644
--- a/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
+++ b/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
@@ -1,12 +1,14 @@
[kernel] Parsing tests/syntax/spurious_brace_bts_1273.i (no preprocessing)
-[kernel] tests/syntax/spurious_brace_bts_1273.i:1:
+[kernel] tests/syntax/spurious_brace_bts_1273.i:6:
syntax error:
- Location: between lines 1 and 3, before or at token: }
+ Location: between lines 6 and 8, before or at token: }
+ 4 */
+ 5
- 1 void foo() {
- 2 }
- 3 }
+ 6 void foo() {
+ 7 }
+ 8 }
- 4
- 5 void main () {
+ 9
+ 10 void main () {
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle b/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
index 45747b51b22f2fbb51563aafc724f25cdea89791..b54f3ab0368599cabc43276115e2a317bae3dfa8 100644
--- a/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
+++ b/tests/syntax/oracle/struct_with_function_field_invalid.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/struct_with_function_field_invalid.i (no preprocessing)
-[kernel] tests/syntax/struct_with_function_field_invalid.i:2: User Error:
+[kernel] tests/syntax/struct_with_function_field_invalid.i:7: User Error:
field `f' declared as a function
[kernel] User Error: stopping on file "tests/syntax/struct_with_function_field_invalid.i" that has
errors.
diff --git a/tests/syntax/oracle/syntactic_hook.res.oracle b/tests/syntax/oracle/syntactic_hook.res.oracle
index 4d15d03a3ad3423d6b318c306cfbdfe997c2aee2..33146264125abe9ef723828e8d8ca38012c6aa91 100644
--- a/tests/syntax/oracle/syntactic_hook.res.oracle
+++ b/tests/syntax/oracle/syntactic_hook.res.oracle
@@ -1,54 +1,54 @@
[kernel] Parsing tests/syntax/syntactic_hook.i (no preprocessing)
-[kernel] tests/syntax/syntactic_hook.i:5:
+[kernel] tests/syntax/syntactic_hook.i:8:
New global node introducing identifier f(22)
[kernel] First occurrence of f
-[kernel] tests/syntax/syntactic_hook.i:7:
+[kernel] tests/syntax/syntactic_hook.i:10:
New global node introducing identifier k(25)
[kernel] First occurrence of k
-[kernel] tests/syntax/syntactic_hook.i:9:
+[kernel] tests/syntax/syntactic_hook.i:12:
New global node introducing identifier k(25)
[kernel] New occurrence of existing identifier k
-[kernel] tests/syntax/syntactic_hook.i:11:
+[kernel] tests/syntax/syntactic_hook.i:14:
New global node introducing identifier main(31)
[kernel] First occurrence of main
-[kernel] tests/syntax/syntactic_hook.i:13:
+[kernel] tests/syntax/syntactic_hook.i:16:
New global node introducing identifier t(35)
[kernel] First occurrence of t
-[kernel] tests/syntax/syntactic_hook.i:13: Warning:
+[kernel] tests/syntax/syntactic_hook.i:16: Warning:
[SH]: definition of local function t
[kernel] :0: New global node introducing identifier g(37)
[kernel] First occurrence of g
-[kernel:typing:implicit-function-declaration] tests/syntax/syntactic_hook.i:17: Warning:
+[kernel:typing:implicit-function-declaration] tests/syntax/syntactic_hook.i:20: Warning:
Calling undeclared function g. Old style K&R code?
-[kernel] tests/syntax/syntactic_hook.i:17: Warning:
+[kernel] tests/syntax/syntactic_hook.i:20: Warning:
[SH]: implicit declaration for prototype g
-[kernel] tests/syntax/syntactic_hook.i:18: Dropping side-effect in sizeof.
-[kernel] tests/syntax/syntactic_hook.i:18: Warning:
+[kernel] tests/syntax/syntactic_hook.i:21: Dropping side-effect in sizeof.
+[kernel] tests/syntax/syntactic_hook.i:21: Warning:
[SH]: dropping side effect in sizeof: (x++) is converted to tmp
-[kernel] tests/syntax/syntactic_hook.i:20: Warning:
+[kernel] tests/syntax/syntactic_hook.i:23: Warning:
[SH]: side effect of expression x++ occurs in conditional part of
expression x && x++. It is not always executed.
-[kernel] tests/syntax/syntactic_hook.i:21: Warning:
+[kernel] tests/syntax/syntactic_hook.i:24: Warning:
[SH]: side effect of expression x++ occurs in conditional part of
expression x && (x++ || x). It is not always executed.
-[kernel] tests/syntax/syntactic_hook.i:22: Warning:
+[kernel] tests/syntax/syntactic_hook.i:25: Warning:
[SH]: side effect of expression x++ occurs in conditional part of
expression x || x++. It is not always executed.
-[kernel] tests/syntax/syntactic_hook.i:23: Warning:
+[kernel] tests/syntax/syntactic_hook.i:26: Warning:
[SH]: side effect of expression x++ occurs in conditional part of
expression x ? x++ : x++. It is not always executed.
-[kernel] tests/syntax/syntactic_hook.i:23: Warning:
+[kernel] tests/syntax/syntactic_hook.i:26: Warning:
[SH]: side effect of expression x++ occurs in conditional part of
expression x ? x++ : x++. It is not always executed.
-[kernel] tests/syntax/syntactic_hook.i:27: User Error:
- Declaration of f does not match previous declaration from tests/syntax/syntactic_hook.i:5 (different number of arguments).
-[kernel] tests/syntax/syntactic_hook.i:27: Warning:
- [SH]: conflict with declaration of f at line 5: different number of arguments
-[kernel] tests/syntax/syntactic_hook.i:27: User Error:
+[kernel] tests/syntax/syntactic_hook.i:30: User Error:
+ Declaration of f does not match previous declaration from tests/syntax/syntactic_hook.i:8 (different number of arguments).
+[kernel] tests/syntax/syntactic_hook.i:30: Warning:
+ [SH]: conflict with declaration of f at line 8: different number of arguments
+[kernel] tests/syntax/syntactic_hook.i:30: User Error:
Inconsistent formals
- 25 }
- 26
- 27 int f(int); //error: conflicting decls
+ 28 }
+ 29
+ 30 int f(int); //error: conflicting decls
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[kernel] User Error: stopping on file "tests/syntax/syntactic_hook.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/type_branch_bts_1081.res.oracle b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
index 2f186ca6fcbcfc1010dffbaef7e98fde6916e3a8..1b52b8d786f3342d9edefa1abb0eb58c661f0abd 100644
--- a/tests/syntax/oracle/type_branch_bts_1081.res.oracle
+++ b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/type_branch_bts_1081.i (no preprocessing)
-[kernel] tests/syntax/type_branch_bts_1081.i:5: Failure:
+[kernel] tests/syntax/type_branch_bts_1081.i:10: Failure:
invalid implicit conversion from void to signed char
[kernel] User Error: stopping on file "tests/syntax/type_branch_bts_1081.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
index 39a0d601cd9097018aba4b5ed75ec2b0008b84f2..98fbeb9c9f407970000a9fd9beb78f50fe2deb5b 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing tests/syntax/typedef_namespace_bts1500.c (with preprocessing)
-[kernel] tests/syntax/typedef_namespace_bts1500.c:20:
+[kernel] tests/syntax/typedef_namespace_bts1500.c:21:
syntax error:
- Location: between lines 20 and 23, before or at token: y
- 18 int main () {
- 19 digit x = 4;
+ Location: between lines 21 and 24, before or at token: y
+ 19 int main () {
+ 20 digit x = 4;
- 20 int digit = 3;
- 21 // error: digit is now a variable
- 22 #ifdef HIDING_TYPEDEF
- 23 digit y = 5;
+ 21 int digit = 3;
+ 22 // error: digit is now a variable
+ 23 #ifdef HIDING_TYPEDEF
+ 24 digit y = 5;
- 24 #endif
- 25 return x + digit+A;
+ 25 #endif
+ 26 return x + digit+A;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.2.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.2.res.oracle
index 165029eae5b0b9ec0cfff7cd0b8b4c7ffff3f542..ef5b7cf9747509d6e389dbbb0c7e09c1660821e4 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.2.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.2.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/syntax/typedef_namespace_bts1500.c (with preprocessing)
-[kernel] tests/syntax/typedef_namespace_bts1500.c:31: User Error:
+[kernel] tests/syntax/typedef_namespace_bts1500.c:32: User Error:
redefinition of 'digit' with different kind in the same scope.
- Previous declaration was at tests/syntax/typedef_namespace_bts1500.c:6
+ Previous declaration was at tests/syntax/typedef_namespace_bts1500.c:7
[kernel] User Error: stopping on file "tests/syntax/typedef_namespace_bts1500.c" that has errors.
Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/va.res.oracle b/tests/syntax/oracle/va.res.oracle
index 0e57ec19d38c2459048b01a4ced3f6cf69bcdd27..0504b7e85dafee5c7d08a9dc623d71c009654126 100644
--- a/tests/syntax/oracle/va.res.oracle
+++ b/tests/syntax/oracle/va.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/syntax/va.c (with preprocessing)
-[kernel] tests/syntax/va.c:7: User Error:
+[kernel] tests/syntax/va.c:12: User Error:
redefinition of 'x' in the same scope.
- Previous declaration was at tests/syntax/va.c:6
-[kernel] tests/syntax/va.c:13: User Error:
+ Previous declaration was at tests/syntax/va.c:11
+[kernel] tests/syntax/va.c:18: User Error:
redefinition of 'x' in the same scope.
- Previous declaration was at tests/syntax/va.c:12
-[kernel] tests/syntax/va.c:21: User Error:
+ Previous declaration was at tests/syntax/va.c:17
+[kernel] tests/syntax/va.c:26: User Error:
The last argument in call to __builtin_va_start should be the last formal argument of f
[kernel] User Error: stopping on file "tests/syntax/va.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/vla_goto.res.oracle b/tests/syntax/oracle/vla_goto.res.oracle
index d09ee0e49dd873b84d25b672820586cc28b84bff..8cd64384ecc914fba273c137912cff692b33c7d5 100644
--- a/tests/syntax/oracle/vla_goto.res.oracle
+++ b/tests/syntax/oracle/vla_goto.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/syntax/vla_goto.i (no preprocessing)
-[kernel] User Error: tests/syntax/vla_goto.i:5, cannot jump from goto statement bypassing initialization of variable b2, declared at tests/syntax/vla_goto.i:9
+[kernel] User Error: tests/syntax/vla_goto.i:11, cannot jump from goto statement bypassing initialization of variable b2, declared at tests/syntax/vla_goto.i:15
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/vla_goto3.res.oracle b/tests/syntax/oracle/vla_goto3.res.oracle
index 6278462c8d29811a497f44fe505f53fb69ae7b1e..6b562dc695fc57448ef64f7abe73375efb68e936 100644
--- a/tests/syntax/oracle/vla_goto3.res.oracle
+++ b/tests/syntax/oracle/vla_goto3.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/syntax/vla_goto3.i (no preprocessing)
-[kernel] User Error: tests/syntax/vla_goto3.i:5, cannot jump from goto statement bypassing initialization of variable vla, declared at tests/syntax/vla_goto3.i:6
+[kernel] User Error: tests/syntax/vla_goto3.i:9, cannot jump from goto statement bypassing initialization of variable vla, declared at tests/syntax/vla_goto3.i:10
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/vla_goto_same_block_below.res.oracle b/tests/syntax/oracle/vla_goto_same_block_below.res.oracle
index b61b6e96000ef532c750da0b271ca5ad84ddcfd8..c9f452a6a375af94f30e7289869525f62e220fad 100644
--- a/tests/syntax/oracle/vla_goto_same_block_below.res.oracle
+++ b/tests/syntax/oracle/vla_goto_same_block_below.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing tests/syntax/vla_goto_same_block_below.i (no preprocessing)
-[kernel] User Error: tests/syntax/vla_goto_same_block_below.i:6, cannot jump from goto statement bypassing initialization of variable vla, declared at tests/syntax/vla_goto_same_block_below.i:9
+[kernel] User Error: tests/syntax/vla_goto_same_block_below.i:11, cannot jump from goto statement bypassing initialization of variable vla, declared at tests/syntax/vla_goto_same_block_below.i:14
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/vla_switch.res.oracle b/tests/syntax/oracle/vla_switch.res.oracle
index 003cf921a9f29f2b73f828c55c1adc79217e6c5a..55afc254bf0c44d5f760af4fe96de5936a0d7d28 100644
--- a/tests/syntax/oracle/vla_switch.res.oracle
+++ b/tests/syntax/oracle/vla_switch.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/vla_switch.i (no preprocessing)
-[kernel] tests/syntax/vla_switch.i:11: Warning:
+[kernel] tests/syntax/vla_switch.i:16: Warning:
Body of function case3 falls-through. Adding a return statement
-[kernel] User Error: tests/syntax/vla_switch.i:2, cannot jump from switch statement bypassing initialization of variable b, declared at tests/syntax/vla_switch.i:4
+[kernel] User Error: tests/syntax/vla_switch.i:7, cannot jump from switch statement bypassing initialization of variable b, declared at tests/syntax/vla_switch.i:9
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle
index aba1a2ecee9a40e229449d6158e269eae7c2061f..68e9058081fb6f8c9d54e94abac71b0edd18f9d4 100644
--- a/tests/syntax/oracle/wrong-assignment.res.oracle
+++ b/tests/syntax/oracle/wrong-assignment.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/syntax/wrong-assignment.i (no preprocessing)
-[kernel] tests/syntax/wrong-assignment.i:7: Failure: castTo ebool -> _Bool
+[kernel] tests/syntax/wrong-assignment.i:13: Failure: castTo ebool -> _Bool
[kernel] User Error: stopping on file "tests/syntax/wrong-assignment.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong_label.res.oracle b/tests/syntax/oracle/wrong_label.res.oracle
index b95ec14c2063a28ceb6331afc1d8f28408e29c3e..7223664bee838bf3bbfad6358917169ee5c05d5b 100644
--- a/tests/syntax/oracle/wrong_label.res.oracle
+++ b/tests/syntax/oracle/wrong_label.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing tests/syntax/wrong_label.i (no preprocessing)
-[kernel] tests/syntax/wrong_label.i:6:
+[kernel] tests/syntax/wrong_label.i:11:
syntax error:
- Location: line 6, between columns 3 and 8, before or at token: }
- 4
- 5 void main() {
- 6 {_LOR:} // KO: labels can't be at the end of a block.
+ Location: line 11, between columns 3 and 8, before or at token: }
+ 9
+ 10 void main() {
+ 11 {_LOR:} // KO: labels can't be at the end of a block.
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 7 }
+ 12 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/array_zero_length.0.res.oracle b/tests/value/oracle/array_zero_length.0.res.oracle
index 6fdacf5f712ee03db803d2beb51af3d8158ce397..e74e0ef0bd84ccb3d91adb66ba28a5cd81aa5937 100644
--- a/tests/value/oracle/array_zero_length.0.res.oracle
+++ b/tests/value/oracle/array_zero_length.0.res.oracle
@@ -1,19 +1,19 @@
[kernel] Parsing tests/value/array_zero_length.i (no preprocessing)
-[kernel] tests/value/array_zero_length.i:10: Warning:
+[kernel] tests/value/array_zero_length.i:11: Warning:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are a compiler extension
-[kernel] tests/value/array_zero_length.i:15: Warning:
+[kernel] tests/value/array_zero_length.i:16: Warning:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are a compiler extension
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
-[eva] tests/value/array_zero_length.i:7: Warning:
+[eva] tests/value/array_zero_length.i:8: Warning:
during initialization of variable 'T', size of type 'char []' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:9: Warning:
+[eva] tests/value/array_zero_length.i:10: Warning:
during initialization of variable 'V', size of type 'char [][2]' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:10: Warning:
+[eva] tests/value/array_zero_length.i:11: Warning:
during initialization of variable 'W', size of type 'char [][0]' cannot be
computed (Size of array without number of elements.)
[eva] Initial state computed
@@ -23,34 +23,34 @@
W[bits 0 to ..] ∈ {0} or UNINITIALIZED
W2[0..1][0] ∈ {0}
pW ∈ {0}
-[eva] tests/value/array_zero_length.i:24: assertion got status valid.
-[eva] tests/value/array_zero_length.i:28: assertion got status valid.
-[eva] tests/value/array_zero_length.i:30: assertion got status valid.
-[eva] tests/value/array_zero_length.i:32: assertion got status valid.
-[eva] tests/value/array_zero_length.i:34: assertion got status valid.
-[eva:alarm] tests/value/array_zero_length.i:36: Warning:
- out of bounds write. assert \valid(&T[2]);
+[eva] tests/value/array_zero_length.i:25: assertion got status valid.
+[eva] tests/value/array_zero_length.i:29: assertion got status valid.
+[eva] tests/value/array_zero_length.i:31: assertion got status valid.
+[eva] tests/value/array_zero_length.i:33: assertion got status valid.
+[eva] tests/value/array_zero_length.i:35: assertion got status valid.
[eva:alarm] tests/value/array_zero_length.i:37: Warning:
+ out of bounds write. assert \valid(&T[2]);
+[eva:alarm] tests/value/array_zero_length.i:38: Warning:
out of bounds write. assert \valid(&T[1]);
-[eva:alarm] tests/value/array_zero_length.i:37: Warning:
+[eva:alarm] tests/value/array_zero_length.i:38: Warning:
accessing uninitialized left-value. assert \initialized(&T[3]);
-[eva:alarm] tests/value/array_zero_length.i:37: Warning:
+[eva:alarm] tests/value/array_zero_length.i:38: Warning:
out of bounds read. assert \valid_read(&T[3]);
-[eva:alarm] tests/value/array_zero_length.i:39: Warning:
- out of bounds write. assert \valid(&V[2][1]);
[eva:alarm] tests/value/array_zero_length.i:40: Warning:
+ out of bounds write. assert \valid(&V[2][1]);
+[eva:alarm] tests/value/array_zero_length.i:41: Warning:
out of bounds write. assert \valid(&V[1][1]);
-[eva:alarm] tests/value/array_zero_length.i:40: Warning:
+[eva:alarm] tests/value/array_zero_length.i:41: Warning:
accessing uninitialized left-value. assert \initialized(&V[3][1]);
-[eva:alarm] tests/value/array_zero_length.i:40: Warning:
+[eva:alarm] tests/value/array_zero_length.i:41: Warning:
out of bounds read. assert \valid_read(&V[3][1]);
-[eva:alarm] tests/value/array_zero_length.i:42: Warning:
- out of bounds write. assert \valid(&W[2][1]);
[eva:alarm] tests/value/array_zero_length.i:43: Warning:
+ out of bounds write. assert \valid(&W[2][1]);
+[eva:alarm] tests/value/array_zero_length.i:44: Warning:
out of bounds write. assert \valid(&W[1][1]);
-[eva:alarm] tests/value/array_zero_length.i:43: Warning:
+[eva:alarm] tests/value/array_zero_length.i:44: Warning:
accessing uninitialized left-value. assert \initialized(&W[3][1]);
-[eva:alarm] tests/value/array_zero_length.i:43: Warning:
+[eva:alarm] tests/value/array_zero_length.i:44: Warning:
out of bounds read. assert \valid_read(&W[3][1]);
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/value/oracle/array_zero_length.1.res.oracle b/tests/value/oracle/array_zero_length.1.res.oracle
index 70dc88689546fef2e4ee22528325bf1da0cfb6b8..1b90339b79a210f4bd4e74a18cfc5d44d1e68180 100644
--- a/tests/value/oracle/array_zero_length.1.res.oracle
+++ b/tests/value/oracle/array_zero_length.1.res.oracle
@@ -1,19 +1,19 @@
[kernel] Parsing tests/value/array_zero_length.i (no preprocessing)
-[kernel] tests/value/array_zero_length.i:10: Warning:
+[kernel] tests/value/array_zero_length.i:11: Warning:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are a compiler extension
-[kernel] tests/value/array_zero_length.i:15: Warning:
+[kernel] tests/value/array_zero_length.i:16: Warning:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are a compiler extension
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
-[eva] tests/value/array_zero_length.i:7: Warning:
+[eva] tests/value/array_zero_length.i:8: Warning:
during initialization of variable 'T', size of type 'char []' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:9: Warning:
+[eva] tests/value/array_zero_length.i:10: Warning:
during initialization of variable 'V', size of type 'char [][2]' cannot be
computed (Size of array without number of elements.)
-[eva] tests/value/array_zero_length.i:10: Warning:
+[eva] tests/value/array_zero_length.i:11: Warning:
during initialization of variable 'W', size of type 'char [][0]' cannot be
computed (Size of array without number of elements.)
[eva] Initial state computed
@@ -24,34 +24,34 @@
W2[0..1][0] ∈ [--..--]
pW ∈ {{ NULL ; &S_pW[0] }}
S_pW[0..1] ∈ [--..--]
-[eva] tests/value/array_zero_length.i:24: assertion got status valid.
-[eva] tests/value/array_zero_length.i:28: assertion got status valid.
-[eva] tests/value/array_zero_length.i:30: assertion got status valid.
-[eva] tests/value/array_zero_length.i:32: assertion got status valid.
-[eva] tests/value/array_zero_length.i:34: assertion got status valid.
-[eva:alarm] tests/value/array_zero_length.i:36: Warning:
- out of bounds write. assert \valid(&T[2]);
+[eva] tests/value/array_zero_length.i:25: assertion got status valid.
+[eva] tests/value/array_zero_length.i:29: assertion got status valid.
+[eva] tests/value/array_zero_length.i:31: assertion got status valid.
+[eva] tests/value/array_zero_length.i:33: assertion got status valid.
+[eva] tests/value/array_zero_length.i:35: assertion got status valid.
[eva:alarm] tests/value/array_zero_length.i:37: Warning:
+ out of bounds write. assert \valid(&T[2]);
+[eva:alarm] tests/value/array_zero_length.i:38: Warning:
out of bounds write. assert \valid(&T[1]);
-[eva:alarm] tests/value/array_zero_length.i:37: Warning:
+[eva:alarm] tests/value/array_zero_length.i:38: Warning:
accessing uninitialized left-value. assert \initialized(&T[3]);
-[eva:alarm] tests/value/array_zero_length.i:37: Warning:
+[eva:alarm] tests/value/array_zero_length.i:38: Warning:
out of bounds read. assert \valid_read(&T[3]);
-[eva:alarm] tests/value/array_zero_length.i:39: Warning:
- out of bounds write. assert \valid(&V[2][1]);
[eva:alarm] tests/value/array_zero_length.i:40: Warning:
+ out of bounds write. assert \valid(&V[2][1]);
+[eva:alarm] tests/value/array_zero_length.i:41: Warning:
out of bounds write. assert \valid(&V[1][1]);
-[eva:alarm] tests/value/array_zero_length.i:40: Warning:
+[eva:alarm] tests/value/array_zero_length.i:41: Warning:
accessing uninitialized left-value. assert \initialized(&V[3][1]);
-[eva:alarm] tests/value/array_zero_length.i:40: Warning:
+[eva:alarm] tests/value/array_zero_length.i:41: Warning:
out of bounds read. assert \valid_read(&V[3][1]);
-[eva:alarm] tests/value/array_zero_length.i:42: Warning:
- out of bounds write. assert \valid(&W[2][1]);
[eva:alarm] tests/value/array_zero_length.i:43: Warning:
+ out of bounds write. assert \valid(&W[2][1]);
+[eva:alarm] tests/value/array_zero_length.i:44: Warning:
out of bounds write. assert \valid(&W[1][1]);
-[eva:alarm] tests/value/array_zero_length.i:43: Warning:
+[eva:alarm] tests/value/array_zero_length.i:44: Warning:
accessing uninitialized left-value. assert \initialized(&W[3][1]);
-[eva:alarm] tests/value/array_zero_length.i:43: Warning:
+[eva:alarm] tests/value/array_zero_length.i:44: Warning:
out of bounds read. assert \valid_read(&W[3][1]);
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index 20b7cf8335339ce1a11fedfeb396eb5f69949087..d5eb6f33988efe8fe86ec90a88f5012364e1e7c6 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -1,18 +1,18 @@
[kernel] Parsing tests/value/array_zero_length.i (no preprocessing)
-[kernel] tests/value/array_zero_length.i:8: User Error:
+[kernel] tests/value/array_zero_length.i:9: User Error:
zero-length arrays only allowed for GCC/MSVC
-[kernel] tests/value/array_zero_length.i:10: User Error:
+[kernel] tests/value/array_zero_length.i:11: User Error:
zero-length arrays only allowed for GCC/MSVC
-[kernel] tests/value/array_zero_length.i:10: User Error:
+[kernel] tests/value/array_zero_length.i:11: User Error:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are not allowed in C99
-[kernel] tests/value/array_zero_length.i:12: User Error:
+[kernel] tests/value/array_zero_length.i:13: User Error:
empty initializers only allowed for GCC/MSVC
- 10 char W[][0];
- 11
- 12 char T1[] = {};
+ 11 char W[][0];
+ 12
+ 13 char T1[] = {};
^^^^^^^^^^^^^^^
- 13 char U1[0] = {};
- 14 char V1[][2] = {};
+ 14 char U1[0] = {};
+ 15 char V1[][2] = {};
[kernel] User Error: stopping on file "tests/value/array_zero_length.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/empty_base.0.res.oracle b/tests/value/oracle/empty_base.0.res.oracle
index aeae7116f43d7078810a20537b31366e3fdf4c96..0af48095560b9c93b62c891c7466ad21314f60a8 100644
--- a/tests/value/oracle/empty_base.0.res.oracle
+++ b/tests/value/oracle/empty_base.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/value/empty_base.c (with preprocessing)
-[kernel] tests/value/empty_base.c:62: User Error:
+[kernel] tests/value/empty_base.c:63: User Error:
variable `c' has initializer but incomplete type
-[kernel] tests/value/empty_base.c:66: Warning:
+[kernel] tests/value/empty_base.c:67: Warning:
Too many initializers for structure
-[kernel] tests/value/empty_base.c:74: User Error:
+[kernel] tests/value/empty_base.c:75: User Error:
field `z' declared with a type containing a flexible array member.
-[kernel] tests/value/empty_base.c:79: User Error:
+[kernel] tests/value/empty_base.c:80: User Error:
field `f1' declared with a type containing a flexible array member.
[kernel] User Error: stopping on file "tests/value/empty_base.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index 462f654cb30d09c1897b7cb830aca984f4e0686b..d20639084b8ef275e8ff05de7e5179670ad8a54a 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,16 +1,16 @@
[kernel] Parsing tests/value/empty_base.c (with preprocessing)
-[kernel] tests/value/empty_base.c:12: User Error:
+[kernel] tests/value/empty_base.c:13: User Error:
empty structs only allowed for GCC/MSVC
-[kernel] tests/value/empty_base.c:47: User Error:
+[kernel] tests/value/empty_base.c:48: User Error:
zero-length arrays only allowed for GCC/MSVC
-[kernel] tests/value/empty_base.c:49: User Error:
+[kernel] tests/value/empty_base.c:50: User Error:
empty initializers only allowed for GCC/MSVC
- 47 struct empty empty_array_of_empty[0];
- 48 struct empty array_of_empty[1];
- 49 struct empty many_empty[3] = {{}};
+ 48 struct empty empty_array_of_empty[0];
+ 49 struct empty array_of_empty[1];
+ 50 struct empty many_empty[3] = {{}};
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 50
- 51 comp array_of_comp[1] = {{.a = 17, .b = 45, .e = {}}};
+ 51
+ 52 comp array_of_comp[1] = {{.a = 17, .b = 45, .e = {}}};
[kernel] User Error: stopping on file "tests/value/empty_base.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/recursion.0.res.oracle b/tests/value/oracle/recursion.0.res.oracle
index ce5542a5e4b49993e223f8c370341f1e032a698c..11c074e5b372b9701116afdea0737dc70dd5e8d4 100644
--- a/tests/value/oracle/recursion.0.res.oracle
+++ b/tests/value/oracle/recursion.0.res.oracle
@@ -10,9 +10,9 @@
pg ∈ {{ NULL ; &S_pg[0] }}
S_pg[0..1] ∈ [--..--]
[eva] computing for function ff <- main.
- Called from tests/value/recursion.i:67.
-[eva] tests/value/recursion.i:8: User Error:
- detected recursive call (ff <- ff :: tests/value/recursion.i:67 <- main)
+ Called from tests/value/recursion.i:68.
+[eva] tests/value/recursion.i:9: User Error:
+ detected recursive call (ff <- ff :: tests/value/recursion.i:68 <- main)
Use -eva-ignore-recursive-calls to ignore (beware this will make the analysis
unsound)
[eva] User Error: Degeneration occurred:
diff --git a/tests/value/oracle/recursion.1.res.oracle b/tests/value/oracle/recursion.1.res.oracle
index f191d35fb500de8a27cc0bbfdd9a065427be64f2..4738d12e1cca4cee88dc7dad81f2718b31e1b7ea 100644
--- a/tests/value/oracle/recursion.1.res.oracle
+++ b/tests/value/oracle/recursion.1.res.oracle
@@ -10,79 +10,79 @@
pg ∈ {{ NULL ; &S_pg[0] }}
S_pg[0..1] ∈ [--..--]
[eva] computing for function ff <- main.
- Called from tests/value/recursion.i:67.
-[eva] tests/value/recursion.i:8: Warning:
+ Called from tests/value/recursion.i:68.
+[eva] tests/value/recursion.i:9: Warning:
recursive call during value analysis
- of ff (ff <- ff :: tests/value/recursion.i:67 <- main). Assuming the call has
+ of ff (ff <- ff :: tests/value/recursion.i:68 <- main). Assuming the call has
no effect. The analysis will be unsound.
[eva] computing for function ff <- ff <- main.
- Called from tests/value/recursion.i:8.
+ Called from tests/value/recursion.i:9.
[eva] using specification for function ff
[eva] Done for function ff
[eva] Recording results for ff
[eva] Done for function ff
[eva] computing for function g <- main.
- Called from tests/value/recursion.i:68.
-[eva] tests/value/recursion.i:39: Warning:
+ Called from tests/value/recursion.i:69.
+[eva] tests/value/recursion.i:40: Warning:
recursive call during value analysis
- of g (g <- g :: tests/value/recursion.i:68 <- main). Assuming the call has
+ of g (g <- g :: tests/value/recursion.i:69 <- main). Assuming the call has
no effect. The analysis will be unsound.
[eva] computing for function g <- g <- main.
- Called from tests/value/recursion.i:39.
+ Called from tests/value/recursion.i:40.
[eva] using specification for function g
[eva] Done for function g
[eva] Recording results for g
[eva] Done for function g
[eva] computing for function h <- main.
- Called from tests/value/recursion.i:70.
-[eva] tests/value/recursion.i:44: Warning:
+ Called from tests/value/recursion.i:71.
+[eva] tests/value/recursion.i:45: Warning:
recursive call during value analysis
- of h (h <- h :: tests/value/recursion.i:70 <- main). Assuming the call has
+ of h (h <- h :: tests/value/recursion.i:71 <- main). Assuming the call has
no effect. The analysis will be unsound.
[eva] computing for function h <- h <- main.
- Called from tests/value/recursion.i:44.
+ Called from tests/value/recursion.i:45.
[eva] using specification for function h
[eva] Done for function h
[eva] Recording results for h
[eva] Done for function h
-[eva] tests/value/recursion.i:71: Frama_C_show_each: Bottom, Bottom
+[eva] tests/value/recursion.i:72: Frama_C_show_each: Bottom, Bottom
[eva] computing for function escaping_formal <- main.
- Called from tests/value/recursion.i:72.
-[eva] tests/value/recursion.i:72:
+ Called from tests/value/recursion.i:73.
+[eva] tests/value/recursion.i:73:
function escaping_formal: precondition got status valid.
-[eva] tests/value/recursion.i:58: Frama_C_show_each: {{ &i }}, {10}, {0}, {10}
-[eva] tests/value/recursion.i:59: Warning:
+[eva] tests/value/recursion.i:59: Frama_C_show_each: {{ &i }}, {10}, {0}, {10}
+[eva] tests/value/recursion.i:60: Warning:
recursive call during value analysis
- of escaping_formal (escaping_formal <- escaping_formal :: tests/value/recursion.i:72 <-
+ of escaping_formal (escaping_formal <- escaping_formal :: tests/value/recursion.i:73 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/value/recursion.i:59: User Error:
+[eva] tests/value/recursion.i:60: User Error:
function 'escaping_formal' (involved in a recursive call) has a formal parameter whose address is taken. Analysis may be unsound.
[eva] computing for function escaping_formal <- escaping_formal <- main.
- Called from tests/value/recursion.i:59.
+ Called from tests/value/recursion.i:60.
[eva] using specification for function escaping_formal
[eva] Done for function escaping_formal
-[eva] tests/value/recursion.i:62: Frama_C_show_each: {{ &i }}, {10}, {0}, {10}
-[eva] tests/value/recursion.i:54:
+[eva] tests/value/recursion.i:63: Frama_C_show_each: {{ &i }}, {10}, {0}, {10}
+[eva] tests/value/recursion.i:55:
function escaping_formal: postcondition got status valid.
[eva] Recording results for escaping_formal
[eva] Done for function escaping_formal
[eva] computing for function f <- main.
- Called from tests/value/recursion.i:73.
-[eva] tests/value/recursion.i:28: Frama_C_show_each: {2}, {0}
-[eva] tests/value/recursion.i:30: Warning:
+ Called from tests/value/recursion.i:74.
+[eva] tests/value/recursion.i:29: Frama_C_show_each: {2}, {0}
+[eva] tests/value/recursion.i:31: Warning:
recursive call during value analysis
- of f (f <- f :: tests/value/recursion.i:73 <- main). Assuming the call has
+ of f (f <- f :: tests/value/recursion.i:74 <- main). Assuming the call has
no effect. The analysis will be unsound.
[eva] computing for function f <- f <- main.
- Called from tests/value/recursion.i:30.
+ Called from tests/value/recursion.i:31.
[eva] using specification for function f
[eva] Done for function f
-[eva] tests/value/recursion.i:31: Frama_C_show_each: {2}, {0}
+[eva] tests/value/recursion.i:32: Frama_C_show_each: {2}, {0}
[eva] Recording results for f
[eva] Done for function f
-[eva] tests/value/recursion.i:74: Frama_C_show_each: {2}
-[eva:alarm] tests/value/recursion.i:75: Warning:
+[eva] tests/value/recursion.i:75: Frama_C_show_each: {2}
+[eva:alarm] tests/value/recursion.i:76: Warning:
signed overflow. assert r.f1 + 1 ≤ 2147483647;
[eva] Recording results for main
[eva] done for function main
diff --git a/tests/value/oracle/split_return.0.res.oracle b/tests/value/oracle/split_return.0.res.oracle
index 91a2153418a268c08e37b36b945cf667389b2575..3c39daac7720985d50738ccf8f1157084f82ae0b 100644
--- a/tests/value/oracle/split_return.0.res.oracle
+++ b/tests/value/oracle/split_return.0.res.oracle
@@ -19,109 +19,109 @@
v7 ∈ {0}
rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:204.
+ Called from tests/value/split_return.i:207.
[eva] computing for function init <- main1 <- main.
- Called from tests/value/split_return.i:17.
+ Called from tests/value/split_return.i:20.
[eva] using specification for function init
[eva] Done for function init
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:205.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f2 <- main2 <- main.
- Called from tests/value/split_return.i:48.
+ Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5; 7}, {5}
-[eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
[eva] tests/value/split_return.i:54: assertion got status valid.
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:57: assertion got status valid.
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
-[eva] tests/value/split_return.i:69: cannot properly split on \result == -2
+ Called from tests/value/split_return.i:76.
+[eva] tests/value/split_return.i:72: cannot properly split on \result == -2
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2; 7}, {0; 5}
-[eva:alarm] tests/value/split_return.i:76: Warning:
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2; 7}, {0; 5}
+[eva:alarm] tests/value/split_return.i:79: Warning:
assertion got status unknown.
-[eva:alarm] tests/value/split_return.i:78: Warning:
+[eva:alarm] tests/value/split_return.i:81: Warning:
assertion got status unknown.
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4; 7}, {0; 5}
-[eva:alarm] tests/value/split_return.i:97: Warning:
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4; 7}, {0; 5}
+[eva:alarm] tests/value/split_return.i:100: Warning:
assertion got status unknown.
-[eva:alarm] tests/value/split_return.i:99: Warning:
+[eva:alarm] tests/value/split_return.i:102: Warning:
assertion got status unknown.
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:208.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f5 <- main5 <- main.
- Called from tests/value/split_return.i:117.
+ Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:120: assertion got status valid.
-[eva] tests/value/split_return.i:122: assertion got status valid.
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:125: assertion got status valid.
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
-[eva:alarm] tests/value/split_return.i:130: Warning:
+ Called from tests/value/split_return.i:138.
+[eva:alarm] tests/value/split_return.i:133: Warning:
assertion got status unknown.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153:
+[eva] tests/value/split_return.i:156:
Frama_C_show_each_NULL: {{ NULL ; &v }}, {0; 1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172:
+[eva] tests/value/split_return.i:175:
Frama_C_show_each_then8: {-1; 4}, {{ NULL ; &x }}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
- Called from tests/value/split_return.i:212.
+ Called from tests/value/split_return.i:215.
[eva] computing for function uninit <- main9 <- main.
- Called from tests/value/split_return.i:199.
+ Called from tests/value/split_return.i:202.
[eva] Recording results for uninit
[eva] Done for function uninit
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
-[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ Called from tests/value/split_return.i:203.
+[eva:locals-escaping] tests/value/split_return.i:195: Warning:
locals {x} escaping the scope of a block of escaping through p
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
+ Called from tests/value/split_return.i:203.
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] Recording results for main9
@@ -363,13 +363,13 @@
--- Properties of Function 'init'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file tests/value/split_return.i, line 12)
+[ Extern ] Post-condition (file tests/value/split_return.i, line 15)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file tests/value/split_return.i, line 10)
+[ Extern ] Assigns (file tests/value/split_return.i, line 13)
Unverifiable but considered Valid.
-[ Extern ] Froms (file tests/value/split_return.i, line 10)
+[ Extern ] Froms (file tests/value/split_return.i, line 13)
Unverifiable but considered Valid.
-[ Extern ] Froms (file tests/value/split_return.i, line 11)
+[ Extern ] Froms (file tests/value/split_return.i, line 14)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -378,54 +378,54 @@
--- Properties of Function 'main1'
--------------------------------------------------------------------------------
-[ Dead ] Assertion (file tests/value/split_return.i, line 27)
+[ Dead ] Assertion (file tests/value/split_return.i, line 30)
Locally valid, but unreachable.
By Eva because:
- - Unreachable program point (file tests/value/split_return.i, line 27)
-[Unreachable] Unreachable program point (file tests/value/split_return.i, line 27)
+ - Unreachable program point (file tests/value/split_return.i, line 30)
+[Unreachable] Unreachable program point (file tests/value/split_return.i, line 30)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main2'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/value/split_return.i, line 51)
- by Eva.
[ Valid ] Assertion (file tests/value/split_return.i, line 54)
by Eva.
+[ Valid ] Assertion (file tests/value/split_return.i, line 57)
+ by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main3'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/value/split_return.i, line 76)
+[ - ] Assertion (file tests/value/split_return.i, line 79)
tried with Eva.
-[ - ] Assertion (file tests/value/split_return.i, line 78)
+[ - ] Assertion (file tests/value/split_return.i, line 81)
tried with Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main4'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/value/split_return.i, line 97)
+[ - ] Assertion (file tests/value/split_return.i, line 100)
tried with Eva.
-[ - ] Assertion (file tests/value/split_return.i, line 99)
+[ - ] Assertion (file tests/value/split_return.i, line 102)
tried with Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main5'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/value/split_return.i, line 120)
+[ Valid ] Assertion (file tests/value/split_return.i, line 123)
by Eva.
-[ Valid ] Assertion (file tests/value/split_return.i, line 122)
+[ Valid ] Assertion (file tests/value/split_return.i, line 125)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'f6'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/value/split_return.i, line 130)
+[ - ] Assertion (file tests/value/split_return.i, line 133)
tried with Eva.
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/split_return.1.res.oracle b/tests/value/oracle/split_return.1.res.oracle
index 31917f8388259ed060c5ff08e9b6289bf35effbc..e161e8a21148dd6de625f47fd1cd8b0935903ee8 100644
--- a/tests/value/oracle/split_return.1.res.oracle
+++ b/tests/value/oracle/split_return.1.res.oracle
@@ -21,102 +21,102 @@
v7 ∈ {0}
rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:204.
+ Called from tests/value/split_return.i:207.
[eva] computing for function init <- main1 <- main.
- Called from tests/value/split_return.i:17.
+ Called from tests/value/split_return.i:20.
[eva] using specification for function init
[eva] Done for function init
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:205.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f2 <- main2 <- main.
- Called from tests/value/split_return.i:48.
+ Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5; 7}, {5}
-[eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
[eva] tests/value/split_return.i:54: assertion got status valid.
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:57: assertion got status valid.
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:76: assertion got status valid.
-[eva] tests/value/split_return.i:78: assertion got status valid.
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:79: assertion got status valid.
+[eva] tests/value/split_return.i:81: assertion got status valid.
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
-[eva] tests/value/split_return.i:97: assertion got status valid.
-[eva] tests/value/split_return.i:99: assertion got status valid.
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: assertion got status valid.
+[eva] tests/value/split_return.i:102: assertion got status valid.
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:208.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f5 <- main5 <- main.
- Called from tests/value/split_return.i:117.
+ Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:120: assertion got status valid.
-[eva] tests/value/split_return.i:122: assertion got status valid.
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:125: assertion got status valid.
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
-[eva:alarm] tests/value/split_return.i:130: Warning:
+ Called from tests/value/split_return.i:138.
+[eva:alarm] tests/value/split_return.i:133: Warning:
assertion got status unknown.
-[eva] tests/value/split_return.i:131: cannot properly split on \result == 0
+[eva] tests/value/split_return.i:134: cannot properly split on \result == 0
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
- Called from tests/value/split_return.i:212.
+ Called from tests/value/split_return.i:215.
[eva] computing for function uninit <- main9 <- main.
- Called from tests/value/split_return.i:199.
+ Called from tests/value/split_return.i:202.
[eva] Recording results for uninit
[eva] Done for function uninit
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
-[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ Called from tests/value/split_return.i:203.
+[eva:locals-escaping] tests/value/split_return.i:195: Warning:
locals {x} escaping the scope of a block of escaping through p
[eva] Recording results for escaping
[eva] Done for function escaping
@@ -359,13 +359,13 @@
--- Properties of Function 'init'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition (file tests/value/split_return.i, line 12)
+[ Extern ] Post-condition (file tests/value/split_return.i, line 15)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file tests/value/split_return.i, line 10)
+[ Extern ] Assigns (file tests/value/split_return.i, line 13)
Unverifiable but considered Valid.
-[ Extern ] Froms (file tests/value/split_return.i, line 10)
+[ Extern ] Froms (file tests/value/split_return.i, line 13)
Unverifiable but considered Valid.
-[ Extern ] Froms (file tests/value/split_return.i, line 11)
+[ Extern ] Froms (file tests/value/split_return.i, line 14)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -374,54 +374,54 @@
--- Properties of Function 'main1'
--------------------------------------------------------------------------------
-[ Dead ] Assertion (file tests/value/split_return.i, line 27)
+[ Dead ] Assertion (file tests/value/split_return.i, line 30)
Locally valid, but unreachable.
By Eva because:
- - Unreachable program point (file tests/value/split_return.i, line 27)
-[Unreachable] Unreachable program point (file tests/value/split_return.i, line 27)
+ - Unreachable program point (file tests/value/split_return.i, line 30)
+[Unreachable] Unreachable program point (file tests/value/split_return.i, line 30)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main2'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/value/split_return.i, line 51)
- by Eva.
[ Valid ] Assertion (file tests/value/split_return.i, line 54)
by Eva.
+[ Valid ] Assertion (file tests/value/split_return.i, line 57)
+ by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main3'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/value/split_return.i, line 76)
+[ Valid ] Assertion (file tests/value/split_return.i, line 79)
by Eva.
-[ Valid ] Assertion (file tests/value/split_return.i, line 78)
+[ Valid ] Assertion (file tests/value/split_return.i, line 81)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main4'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/value/split_return.i, line 97)
+[ Valid ] Assertion (file tests/value/split_return.i, line 100)
by Eva.
-[ Valid ] Assertion (file tests/value/split_return.i, line 99)
+[ Valid ] Assertion (file tests/value/split_return.i, line 102)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'main5'
--------------------------------------------------------------------------------
-[ Valid ] Assertion (file tests/value/split_return.i, line 120)
+[ Valid ] Assertion (file tests/value/split_return.i, line 123)
by Eva.
-[ Valid ] Assertion (file tests/value/split_return.i, line 122)
+[ Valid ] Assertion (file tests/value/split_return.i, line 125)
by Eva.
--------------------------------------------------------------------------------
--- Properties of Function 'f6'
--------------------------------------------------------------------------------
-[ - ] Assertion (file tests/value/split_return.i, line 130)
+[ - ] Assertion (file tests/value/split_return.i, line 133)
tried with Eva.
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/split_return.3.res.oracle b/tests/value/oracle/split_return.3.res.oracle
index 1ad5a6b949801e802041412d0870ce55b97cb0da..0efcd2430ce9e8239d2ac44023a3a3c42f36a4b1 100644
--- a/tests/value/oracle/split_return.3.res.oracle
+++ b/tests/value/oracle/split_return.3.res.oracle
@@ -13,196 +13,196 @@
v7 ∈ {0}
rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:204.
+ Called from tests/value/split_return.i:207.
[eva] computing for function init <- main1 <- main.
- Called from tests/value/split_return.i:17.
+ Called from tests/value/split_return.i:20.
[eva] using specification for function init
[eva] Done for function init
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:205.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f2 <- main2 <- main.
- Called from tests/value/split_return.i:48.
+ Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
-[eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {7}, {5}
[eva] tests/value/split_return.i:54: assertion got status valid.
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5}, {5}
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:57: assertion got status valid.
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
-[eva] tests/value/split_return.i:76: assertion got status valid.
-[eva] tests/value/split_return.i:78: assertion got status valid.
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: assertion got status valid.
+[eva] tests/value/split_return.i:81: assertion got status valid.
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
-[eva] tests/value/split_return.i:97: assertion got status valid.
-[eva] tests/value/split_return.i:99: assertion got status valid.
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: assertion got status valid.
+[eva] tests/value/split_return.i:102: assertion got status valid.
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:208.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f5 <- main5 <- main.
- Called from tests/value/split_return.i:117.
+ Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:120: assertion got status valid.
-[eva] tests/value/split_return.i:122: assertion got status valid.
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:125: assertion got status valid.
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
-[eva:alarm] tests/value/split_return.i:130: Warning:
+ Called from tests/value/split_return.i:138.
+[eva:alarm] tests/value/split_return.i:133: Warning:
assertion got status unknown.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
+ Called from tests/value/split_return.i:138.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
- Called from tests/value/split_return.i:212.
+ Called from tests/value/split_return.i:215.
[eva] computing for function uninit <- main9 <- main.
- Called from tests/value/split_return.i:199.
+ Called from tests/value/split_return.i:202.
[eva] Recording results for uninit
[eva] Done for function uninit
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
-[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ Called from tests/value/split_return.i:203.
+[eva:locals-escaping] tests/value/split_return.i:195: Warning:
locals {x} escaping the scope of a block of escaping through p
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
+ Called from tests/value/split_return.i:203.
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] Recording results for main9
diff --git a/tests/value/oracle/split_return.4.res.oracle b/tests/value/oracle/split_return.4.res.oracle
index 08cbe3aca4477cb95925fcb4f6d6365c1f5e4ec7..9751f1d714782c4f4f5c41324c7050e3690dd387 100644
--- a/tests/value/oracle/split_return.4.res.oracle
+++ b/tests/value/oracle/split_return.4.res.oracle
@@ -16,196 +16,196 @@
v7 ∈ {0}
rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:204.
+ Called from tests/value/split_return.i:207.
[eva] computing for function init <- main1 <- main.
- Called from tests/value/split_return.i:17.
+ Called from tests/value/split_return.i:20.
[eva] using specification for function init
[eva] Done for function init
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:205.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f2 <- main2 <- main.
- Called from tests/value/split_return.i:48.
+ Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5}, {5}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {7}, {5}
-[eva] tests/value/split_return.i:51: assertion got status valid.
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5}, {5}
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {7}, {5}
[eva] tests/value/split_return.i:54: assertion got status valid.
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5}, {5}
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {7}, {5}
+[eva] tests/value/split_return.i:57: assertion got status valid.
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
-[eva] tests/value/split_return.i:76: assertion got status valid.
-[eva] tests/value/split_return.i:78: assertion got status valid.
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:79: assertion got status valid.
+[eva] tests/value/split_return.i:81: assertion got status valid.
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
-[eva] tests/value/split_return.i:97: assertion got status valid.
-[eva] tests/value/split_return.i:99: assertion got status valid.
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:100: assertion got status valid.
+[eva] tests/value/split_return.i:102: assertion got status valid.
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:208.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f5 <- main5 <- main.
- Called from tests/value/split_return.i:117.
+ Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
-[eva] tests/value/split_return.i:120: assertion got status valid.
-[eva] tests/value/split_return.i:122: assertion got status valid.
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:123: assertion got status valid.
+[eva] tests/value/split_return.i:125: assertion got status valid.
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
-[eva:alarm] tests/value/split_return.i:130: Warning:
+ Called from tests/value/split_return.i:138.
+[eva:alarm] tests/value/split_return.i:133: Warning:
assertion got status unknown.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
+ Called from tests/value/split_return.i:138.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
- Called from tests/value/split_return.i:212.
+ Called from tests/value/split_return.i:215.
[eva] computing for function uninit <- main9 <- main.
- Called from tests/value/split_return.i:199.
+ Called from tests/value/split_return.i:202.
[eva] Recording results for uninit
[eva] Done for function uninit
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
-[eva:locals-escaping] tests/value/split_return.i:192: Warning:
+ Called from tests/value/split_return.i:203.
+[eva:locals-escaping] tests/value/split_return.i:195: Warning:
locals {x} escaping the scope of a block of escaping through p
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
+ Called from tests/value/split_return.i:203.
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] Recording results for main9
@@ -460,181 +460,181 @@
v7 ∈ {0}
rand ∈ [--..--]
[eva] computing for function main1 <- main.
- Called from tests/value/split_return.i:204.
+ Called from tests/value/split_return.i:207.
[eva] computing for function init <- main1 <- main.
- Called from tests/value/split_return.i:17.
+ Called from tests/value/split_return.i:20.
[eva] Done for function init
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
- Called from tests/value/split_return.i:205.
+ Called from tests/value/split_return.i:208.
[eva] computing for function f2 <- main2 <- main.
- Called from tests/value/split_return.i:48.
+ Called from tests/value/split_return.i:51.
[eva] Recording results for f2
[eva] Done for function f2
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {0}, {0}
-[eva] tests/value/split_return.i:49: Frama_C_show_each_f2: {5; 7}, {5}
-[eva] tests/value/split_return.i:53: Frama_C_show_each_f2_2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main3 <- main.
- Called from tests/value/split_return.i:206.
+ Called from tests/value/split_return.i:209.
[eva] computing for function f3 <- main3 <- main.
- Called from tests/value/split_return.i:73.
+ Called from tests/value/split_return.i:76.
[eva] Recording results for f3
[eva] Done for function f3
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {7}, {5}
-[eva] tests/value/split_return.i:74: Frama_C_show_each_f3: {-2}, {0}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
[eva] Recording results for main3
[eva] Done for function main3
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main4 <- main.
- Called from tests/value/split_return.i:207.
+ Called from tests/value/split_return.i:210.
[eva] computing for function f4 <- main4 <- main.
- Called from tests/value/split_return.i:94.
+ Called from tests/value/split_return.i:97.
[eva] Recording results for f4
[eva] Done for function f4
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {4}, {0}
-[eva] tests/value/split_return.i:95: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
[eva] Recording results for main4
[eva] Done for function main4
[eva] computing for function main5 <- main.
- Called from tests/value/split_return.i:208.
+ Called from tests/value/split_return.i:211.
[eva] computing for function f5 <- main5 <- main.
- Called from tests/value/split_return.i:117.
+ Called from tests/value/split_return.i:120.
[eva] Recording results for f5
[eva] Done for function f5
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {7}, {5}
-[eva] tests/value/split_return.i:118: Frama_C_show_each_f5: {-2}, {0}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
[eva] Recording results for main5
[eva] Done for function main5
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
+ Called from tests/value/split_return.i:138.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main6 <- main.
- Called from tests/value/split_return.i:209.
+ Called from tests/value/split_return.i:212.
[eva] computing for function f6 <- main6 <- main.
- Called from tests/value/split_return.i:135.
+ Called from tests/value/split_return.i:138.
[eva] Recording results for f6
[eva] Done for function f6
[eva] Recording results for main6
[eva] Done for function main6
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main7 <- main.
- Called from tests/value/split_return.i:210.
+ Called from tests/value/split_return.i:213.
[eva] computing for function f7 <- main7 <- main.
- Called from tests/value/split_return.i:148.
+ Called from tests/value/split_return.i:151.
[eva] Recording results for f7
[eva] Done for function f7
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {0}, {0}
-[eva] tests/value/split_return.i:153: Frama_C_show_each_NULL: {{ &v }}, {1}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {0}, {0}
+[eva] tests/value/split_return.i:156: Frama_C_show_each_NULL: {{ &v }}, {1}
[eva] Recording results for main7
[eva] Done for function main7
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main8 <- main.
- Called from tests/value/split_return.i:211.
+ Called from tests/value/split_return.i:214.
[eva] computing for function f8 <- main8 <- main.
- Called from tests/value/split_return.i:171.
+ Called from tests/value/split_return.i:174.
[eva] Recording results for f8
[eva] Done for function f8
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {4}, {{ &x }}
-[eva] tests/value/split_return.i:172: Frama_C_show_each_then8: {-1}, {0}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
[eva] Recording results for main8
[eva] Done for function main8
[eva] computing for function main9 <- main.
- Called from tests/value/split_return.i:212.
+ Called from tests/value/split_return.i:215.
[eva] computing for function uninit <- main9 <- main.
- Called from tests/value/split_return.i:199.
+ Called from tests/value/split_return.i:202.
[eva] Recording results for uninit
[eva] Done for function uninit
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
+ Called from tests/value/split_return.i:203.
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] computing for function escaping <- main9 <- main.
- Called from tests/value/split_return.i:200.
+ Called from tests/value/split_return.i:203.
[eva] Recording results for escaping
[eva] Done for function escaping
[eva] Recording results for main9
diff --git a/tests/value/oracle/va_list.0.res.oracle b/tests/value/oracle/va_list.0.res.oracle
index dd7d28e7c730028ddea8ae1c1f259d29818a6085..ab51d92efd04854b39bf5a77d5812ea908c7a4dc 100644
--- a/tests/value/oracle/va_list.0.res.oracle
+++ b/tests/value/oracle/va_list.0.res.oracle
@@ -9,8 +9,8 @@
[eva:initial-state]
creating variable S_1_S___va_params with imprecise size (type void)
[eva] computing for function __builtin_next_arg <- main.
- Called from tests/value/va_list.c:13.
-[kernel:annot:missing-spec] tests/value/va_list.c:13: Warning:
+ Called from tests/value/va_list.c:14.
+[kernel:annot:missing-spec] tests/value/va_list.c:14: Warning:
Neither code nor specification for function __builtin_next_arg, generating default assigns from the prototype
[eva] using specification for function __builtin_next_arg
[eva] Done for function __builtin_next_arg
diff --git a/tests/value/oracle/va_list.1.res.oracle b/tests/value/oracle/va_list.1.res.oracle
index e5c9853fe1164c594a07cf8da34a21ebb3aa6df3..54aa90f97b95cdbeb41756dbbb9bd98e1de282fb 100644
--- a/tests/value/oracle/va_list.1.res.oracle
+++ b/tests/value/oracle/va_list.1.res.oracle
@@ -5,11 +5,11 @@
[eva:initial-state] Values of globals at initialization
[eva] computing for function __builtin_next_arg <- main.
- Called from tests/value/va_list.c:13.
-[kernel:annot:missing-spec] tests/value/va_list.c:13: Warning:
+ Called from tests/value/va_list.c:14.
+[kernel:annot:missing-spec] tests/value/va_list.c:14: Warning:
Neither code nor specification for function __builtin_next_arg, generating default assigns from the prototype
[eva] using specification for function __builtin_next_arg
-[eva] tests/value/va_list.c:13: User Error:
+[eva] tests/value/va_list.c:14: User Error:
functions returning variadic arguments must be stubbed
[eva] Done for function __builtin_next_arg
[eva] Recording results for main
diff --git a/tests/value/traces/test5.i b/tests/value/traces/test5.i
index d3f122845da8990429ab62d1f98d30ebd81bfb4b..8f21952cadf7e80687dc60f6a6e274cee2e14b8d 100644
--- a/tests/value/traces/test5.i
+++ b/tests/value/traces/test5.i
@@ -1,8 +1,8 @@
/* run.config
+ EXIT: 1
STDOPT: #"-eva-domains traces -eva-msg-key d-traces -eva-slevel 10" +"-then-last -eva -eva-slevel 10 -print -no-eva-traces-domain"
*/
-
/* Check the fix for the creation of expression by dataflows2 for
switch (conversion to list of if) */