From 6b44067235aa81fbb2b52f461c32e36e4418e517 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 22 Mar 2021 15:56:04 +0100
Subject: [PATCH] [Tests] adds EXIT directives (updated oracles)
---
.../tests/report/oracle/classified.0.json | 2 +-
.../tests/report/oracle/classified.1.json | 2 +-
.../tests/report/oracle/classified.2.json | 2 +-
.../tests/report/oracle/classified.3.json | 4 +-
.../tests/report/oracle/classified.4.json | 4 +-
.../tests/report/oracle/classified.5.json | 8 +-
.../tests/report/oracle/classify.0.res.oracle | 2 +-
.../tests/report/oracle/classify.1.res.oracle | 2 +-
.../tests/report/oracle/classify.2.res.oracle | 2 +-
.../tests/report/oracle/classify.3.res.oracle | 2 +-
.../tests/report/oracle/classify.4.res.oracle | 2 +-
.../tests/report/oracle/classify.5.res.oracle | 2 +-
.../tests/batch/oracle/ast_services.out.json | 4 +-
.../oracle/not-enough-par.res.oracle | 2 +-
.../oracle/variadic-builtin.res.oracle | 8 +-
tests/builtins/oracle/watch.res.oracle | 22 +-
tests/cil/oracle/acsl-comments.res.oracle | 2 +-
tests/cil/oracle/bts892.res.oracle | 2 +-
tests/cil/oracle/ghost_cfg.0.res.oracle | 24 +-
tests/cil/oracle/ghost_cfg.1.res.oracle | 2 +-
tests/misc/oracle/bts0451.res.oracle | 12 +-
.../oracle/function_ptr_alignof.res.oracle | 2 +-
.../oracle/function_ptr_lvalue_1.res.oracle | 2 +-
.../oracle/function_ptr_lvalue_2.res.oracle | 2 +-
.../oracle/function_ptr_sizeof.res.oracle | 2 +-
tests/misc/oracle/widen_hints.0.res.oracle | 8 +-
tests/misc/oracle/widen_hints.1.res.oracle | 2 +-
tests/misc/oracle/widen_hints.2.res.oracle | 56 ++--
tests/misc/oracle/widen_hints.3.res.oracle | 64 ++--
tests/syntax/oracle/alloc_order.res.oracle | 2 +-
.../oracle/array_cast_bts1099.res.oracle | 10 +-
tests/syntax/oracle/array_size.res.oracle | 2 +-
.../syntax/oracle/axiomatic_nested.res.oracle | 2 +-
.../oracle/bad_return_bts_599.res.oracle | 4 +-
tests/syntax/oracle/bts0519.1.res.oracle | 2 +-
tests/syntax/oracle/cert-dcl-36.res.oracle | 8 +-
tests/syntax/oracle/cert_msc_38.0.res.oracle | 4 +-
tests/syntax/oracle/cert_msc_38.1.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.2.res.oracle | 2 +-
tests/syntax/oracle/cert_msc_38.3.res.oracle | 4 +-
tests/syntax/oracle/cert_msc_38.4.res.oracle | 4 +-
tests/syntax/oracle/cert_msc_38.5.res.oracle | 4 +-
tests/syntax/oracle/cert_msc_38.6.res.oracle | 4 +-
tests/syntax/oracle/cert_msc_38.7.res.oracle | 2 +-
tests/syntax/oracle/composite-tags.res.oracle | 8 +-
.../syntax/oracle/duplicate_field.res.oracle | 4 +-
tests/syntax/oracle/fam.res.oracle | 12 +-
.../flexible_array_member_invalid1.res.oracle | 2 +-
.../flexible_array_member_invalid2.res.oracle | 2 +-
.../flexible_array_member_invalid3.res.oracle | 2 +-
.../flexible_array_member_invalid4.res.oracle | 2 +-
.../flexible_array_member_invalid5.res.oracle | 2 +-
.../oracle/ghost_cv_incompat.res.oracle | 94 +++---
.../oracle/ghost_cv_invalid_use.res.oracle | 54 ++--
.../ghost_cv_parsing_errors.0.res.oracle | 18 +-
.../ghost_cv_parsing_errors.1.res.oracle | 14 +-
.../ghost_cv_parsing_errors.2.res.oracle | 14 +-
.../oracle/ghost_cv_var_decl.0.res.oracle | 36 +--
.../oracle/ghost_cv_var_decl.1.res.oracle | 260 ++++++++--------
.../oracle/ghost_else_bad_oneline.res.oracle | 2 +-
.../oracle/ghost_local_ill_formed.res.oracle | 6 +-
.../oracle/ghost_parameters.0.res.oracle | 20 +-
.../oracle/ghost_parameters.1.res.oracle | 18 +-
.../oracle/ghost_parameters.10.res.oracle | 16 +-
.../oracle/ghost_parameters.11.res.oracle | 14 +-
.../oracle/ghost_parameters.12.res.oracle | 4 +-
.../oracle/ghost_parameters.3.res.oracle | 16 +-
.../oracle/ghost_parameters.4.res.oracle | 16 +-
.../oracle/ghost_parameters.5.res.oracle | 16 +-
.../oracle/ghost_parameters.6.res.oracle | 16 +-
.../oracle/ghost_parameters.7.res.oracle | 16 +-
.../oracle/ghost_parameters.8.res.oracle | 16 +-
.../oracle/ghost_parameters.9.res.oracle | 16 +-
.../incompatible_qualifiers.0.res.oracle | 32 +-
.../syntax/oracle/incomplete_array.res.oracle | 2 +-
.../oracle/incomplete_struct_field.res.oracle | 6 +-
.../oracle/inconsistent_decl.0.res.oracle | 4 +-
.../oracle/inconsistent_decl.1.res.oracle | 4 +-
tests/syntax/oracle/init_bts1352.res.oracle | 9 +-
.../syntax/oracle/invalid_constant.res.oracle | 2 +-
tests/syntax/oracle/line_number.res.oracle | 8 +-
tests/syntax/oracle/lvalvoid.res.oracle | 2 +-
tests/syntax/oracle/merge_unused.res.oracle | 2 +-
tests/syntax/oracle/multiple_froms.res.oracle | 4 +-
.../mutually_recursive_struct.res.oracle | 10 +-
tests/syntax/oracle/no_prototype.res.oracle | 6 +-
tests/syntax/oracle/rettype.res.oracle | 8 +-
.../oracle/sizeof_incomplete_type.res.oracle | 2 +-
.../oracle/spurious_brace_bts_1273.res.oracle | 16 +-
...uct_with_function_field_invalid.res.oracle | 2 +-
tests/syntax/oracle/syntactic_hook.res.oracle | 46 +--
.../oracle/type_branch_bts_1081.res.oracle | 2 +-
.../typedef_namespace_bts1500.1.res.oracle | 20 +-
.../typedef_namespace_bts1500.2.res.oracle | 4 +-
tests/syntax/oracle/va.res.oracle | 10 +-
tests/syntax/oracle/vla_goto.res.oracle | 2 +-
tests/syntax/oracle/vla_goto3.res.oracle | 2 +-
.../vla_goto_same_block_below.res.oracle | 2 +-
tests/syntax/oracle/vla_switch.res.oracle | 4 +-
.../syntax/oracle/wrong-assignment.res.oracle | 2 +-
tests/syntax/oracle/wrong_label.res.oracle | 12 +-
.../oracle/array_zero_length.0.res.oracle | 44 +--
.../oracle/array_zero_length.1.res.oracle | 44 +--
.../oracle/array_zero_length.2.res.oracle | 18 +-
tests/value/oracle/empty_base.0.res.oracle | 8 +-
tests/value/oracle/empty_base.1.res.oracle | 16 +-
tests/value/oracle/recursion.0.res.oracle | 6 +-
tests/value/oracle/recursion.1.res.oracle | 60 ++--
tests/value/oracle/split_return.0.res.oracle | 110 +++----
tests/value/oracle/split_return.1.res.oracle | 116 +++----
tests/value/oracle/split_return.3.res.oracle | 156 +++++-----
tests/value/oracle/split_return.4.res.oracle | 290 +++++++++---------
tests/value/oracle/va_list.0.res.oracle | 4 +-
tests/value/oracle/va_list.1.res.oracle | 6 +-
tests/value/traces/test5.i | 2 +-
115 files changed, 1066 insertions(+), 1061 deletions(-)
diff --git a/src/plugins/report/tests/report/oracle/classified.0.json b/src/plugins/report/tests/report/oracle/classified.0.json
index e9c382db69c..f25ccd19078 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 27e60abed79..c8821c7ebaf 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 27e60abed79..c8821c7ebaf 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 8af0cb6a445..aed33faf82e 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 8af0cb6a445..aed33faf82e 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 81e4ec8552e..e55c70dfe28 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 e19a301288f..5484bb54121 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 442bb8d3b8c..ab8672ef1b4 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 974d340981d..a9cd75caa36 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 91bb8b30a52..b9a1a38184f 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 ab13ead4ecb..abe3dd32f57 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 bab75d5f591..3cbe2f38f06 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 b9bbb5e7c62..7546c88e6c0 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 c05a4ba9b29..6583645e23e 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 bf189af5926..7b54306d984 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 59019484ae9..28fc5ca7522 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 605a2d7b753..ce4dd692b42 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 dd2a50f7954..ac7ac95ae66 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 9b833655a03..d006b7d3b42 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 494260f7dfe..68a94840387 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 feb299b32ac..473b9fd4f16 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 3a83624e344..b7d7520c167 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 34164dbea51..17925b5b8e3 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 30a6df5ceef..c2c0cf02b8a 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 0a31265b9f6..bc70a4785cb 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 d86de98015d..582badd66f5 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 a6a3f7e9b77..7d63e13e27d 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 065a307ea65..89d5bd4b393 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 0d957fb92d9..0d403fde663 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 173bd5cb869..59aebb036c3 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 3ffc08e781d..d1d6270e09f 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 ec2486e5181..de7738eb511 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 d3bdcc55f50..3fbfd43b9c4 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 547da73ae03..d497519859d 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 569bc14d16e..e7405b10ba7 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 847b9b1daf4..b1c09cfdec3 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 436be5934df..04ff74b2370 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 912e7c39eda..eb28de05e6c 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 9f32d360013..abc74174dda 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 1d21e57a88d..14676195dd4 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 a65e4b430e8..f867e2dca1a 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 38293bc7042..15a1c6c5ec3 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 5aad28f718a..467a8bc0b1a 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 a13d4f25031..f32737dfff8 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 4bffd45b6e6..a48143d07d8 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 1535831390d..158feb74eaf 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 950231170bb..8ccf9f18f6f 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 890a48ecd86..1747cd9c2c3 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 9c14914576b..08b2bbe1285 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 738f4dd8586..c7e88ab0629 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 5ebb2f663be..238b92acd43 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 b72d52714a5..8e1dca203f5 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 83f13fa5573..5f5a16766c2 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 16d262f30bb..0c09108e57d 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 11e0f79f7ac..6a919917f2b 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 79a1e05ec98..fbf1db47255 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 221217ee8de..1ab8175cb4e 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 19e4440c2c8..dd8e3e9e2fb 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 abe9b55416e..47cd7ced61b 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 ded857214d7..7d11d6d80c4 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 f1017ea0fd6..57ace82adf4 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 926c68c1c6b..4fb237c265e 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 614c8ad74c0..73c87461ca1 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 477b266404d..a98fcc2d286 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 1d8c5da2c6f..0651a7a4fb0 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 8bc53156a93..e2ccb5f8899 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 c621d5748d1..a6fcb41b2ae 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 d6b376ee2b1..1c0dd175041 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 138709d0a9b..4b4cafeba68 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 5807a972644..35d3d52f660 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 e5de27561f6..5c437cf03fc 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 bb6ac89e909..0327e4ab298 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 53080c4e6f3..a75c5519836 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 7acff04489b..89200b976ae 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 b00e464eb82..ac5c2714b71 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 1da6f42644d..1fd54ec0cfd 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 0533b81aa66..c6177985490 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 20264c218aa..351743abc10 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 1f56fffc94c..9070651b18e 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 ea07d5fbb32..b4b0da647d4 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 31ecbc78f90..a1c31a18635 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 f84b2e3041b..4d18770bdb6 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 70f368124fe..89e2f903de5 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 b90f4dc55f6..c434bbfc224 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 74ebf746db9..cdcbc56b85c 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 b0064d8723e..9bb1885d269 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 0b3783f2896..85dda4b5756 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 37dab603578..2388b58b2c5 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 84a6987f04d..92f8b8d02b2 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 45747b51b22..b54f3ab0368 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 4d15d03a3ad..33146264125 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 2f186ca6fcb..1b52b8d786f 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 39a0d601cd9..98fbeb9c9f4 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 165029eae5b..ef5b7cf9747 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 0e57ec19d38..0504b7e85da 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 d09ee0e49dd..8cd64384ecc 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 6278462c8d2..6b562dc695f 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 b61b6e96000..c9f452a6a37 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 003cf921a9f..55afc254bf0 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 aba1a2ecee9..68e9058081f 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 b95ec14c206..7223664bee8 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 6fdacf5f712..e74e0ef0bd8 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 70dc8868954..1b90339b79a 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 20b7cf83353..d5eb6f33988 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 aeae7116f43..0af48095560 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 462f654cb30..d20639084b8 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 ce5542a5e4b..11c074e5b37 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 f191d35fb50..4738d12e1cc 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 91a2153418a..3c39daac772 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 31917f83882..e161e8a2114 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 1ad5a6b9498..0efcd2430ce 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 08cbe3aca44..9751f1d7147 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 dd7d28e7c73..ab51d92efd0 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 e5c9853fe11..54aa90f97b9 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 d3f122845da..8f21952cadf 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) */
--
GitLab