From 6f2c7ee21b993f56695c8951a291333a83c1be4b Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 29 Jan 2025 15:14:04 +0100
Subject: [PATCH] [kernel] Add test for `-commands-file`
---
.gitattributes | 1 +
.../commands_file.t/comments_and_newlines.txt | 34 ++
tests/misc/commands_file.t/eva.txt | 4 +
tests/misc/commands_file.t/full.txt | 10 +
tests/misc/commands_file.t/kernel.txt | 2 +
tests/misc/commands_file.t/ll_load.txt | 5 +
tests/misc/commands_file.t/ll_save.txt | 3 +
tests/misc/commands_file.t/prepro.txt | 6 +
tests/misc/commands_file.t/print.txt | 1 +
tests/misc/commands_file.t/run.t | 338 ++++++++++++++++++
tests/misc/commands_file.t/src.c | 42 +++
tests/misc/commands_file.t/src_empty.c | 1 +
tests/misc/commands_file.t/with_error.txt | 1 +
13 files changed, 448 insertions(+)
create mode 100644 tests/misc/commands_file.t/comments_and_newlines.txt
create mode 100644 tests/misc/commands_file.t/eva.txt
create mode 100644 tests/misc/commands_file.t/full.txt
create mode 100644 tests/misc/commands_file.t/kernel.txt
create mode 100644 tests/misc/commands_file.t/ll_load.txt
create mode 100644 tests/misc/commands_file.t/ll_save.txt
create mode 100644 tests/misc/commands_file.t/prepro.txt
create mode 100644 tests/misc/commands_file.t/print.txt
create mode 100644 tests/misc/commands_file.t/run.t
create mode 100644 tests/misc/commands_file.t/src.c
create mode 100644 tests/misc/commands_file.t/src_empty.c
create mode 100644 tests/misc/commands_file.t/with_error.txt
diff --git a/.gitattributes b/.gitattributes
index 29ae5719c9..dcba03f1e0 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -82,6 +82,7 @@ src/plugins/e-acsl/examples/ensuresec/**/*.py -check-indent
*.dot -check-eoleof
+/tests/misc/commands_file.t/comments_and_newlines.txt -check-eoleof
/tests/spec/unfinished-oneline-acsl-comment.i -check-eoleof
/doc/developer/check_api/run.oracle -check-eoleof
diff --git a/tests/misc/commands_file.t/comments_and_newlines.txt b/tests/misc/commands_file.t/comments_and_newlines.txt
new file mode 100644
index 0000000000..d7cba91479
--- /dev/null
+++ b/tests/misc/commands_file.t/comments_and_newlines.txt
@@ -0,0 +1,34 @@
+# The config file supports comments starting with #
+
+src_empty.c
+
+# If a line ends with \ then the next line is merged with it.
+-eva-precision \
+ 5
+
+# Several \ can be chained
+-eva-domains \
+ equality, \
+ gauges
+
+ # Comments can be indented with spaces
+ # or tabs
+
+# The spaces are preserved when merging lines so they can be put on the
+# first or second one independently. And the spaces around the value are
+# trimmed.
+-eva-slevel\
+ 200
+-eva-ilevel \
+32
+-eva-plevel=\
+100
+
+# If a line ends with \ and the next line contains only spaces, the option is
+# considered without value
+-eva \
+ \
+
+# No crash if the last line ends with a backslash (no new line at the end of the
+# config file on purpose for the test)
+-eva-partition-history 2 \
\ No newline at end of file
diff --git a/tests/misc/commands_file.t/eva.txt b/tests/misc/commands_file.t/eva.txt
new file mode 100644
index 0000000000..8b10a19654
--- /dev/null
+++ b/tests/misc/commands_file.t/eva.txt
@@ -0,0 +1,4 @@
+-eva
+-eva-slevel 50
+-eva-precision=5
+-eva-slevel 200
diff --git a/tests/misc/commands_file.t/full.txt b/tests/misc/commands_file.t/full.txt
new file mode 100644
index 0000000000..97595d032c
--- /dev/null
+++ b/tests/misc/commands_file.t/full.txt
@@ -0,0 +1,10 @@
+src.c
+-commands-file prepro.txt
+-keep-unused-types
+-then
+-eva
+-eva-slevel 50
+-eva-precision=5
+-eva-slevel 200
+-then
+-print
diff --git a/tests/misc/commands_file.t/kernel.txt b/tests/misc/commands_file.t/kernel.txt
new file mode 100644
index 0000000000..19fd104754
--- /dev/null
+++ b/tests/misc/commands_file.t/kernel.txt
@@ -0,0 +1,2 @@
+src.c
+-keep-unused-types
diff --git a/tests/misc/commands_file.t/ll_load.txt b/tests/misc/commands_file.t/ll_load.txt
new file mode 100644
index 0000000000..219f71b6fc
--- /dev/null
+++ b/tests/misc/commands_file.t/ll_load.txt
@@ -0,0 +1,5 @@
+-no-autoload-plugins
+-load saved_in_commands_file.sav
+-then
+-load-plugin eva,inout
+-eva
diff --git a/tests/misc/commands_file.t/ll_save.txt b/tests/misc/commands_file.t/ll_save.txt
new file mode 100644
index 0000000000..8c4bb81a98
--- /dev/null
+++ b/tests/misc/commands_file.t/ll_save.txt
@@ -0,0 +1,3 @@
+-no-autoload-plugins
+src_empty.c
+-save saved_in_commands_file.sav
diff --git a/tests/misc/commands_file.t/prepro.txt b/tests/misc/commands_file.t/prepro.txt
new file mode 100644
index 0000000000..2727981bb9
--- /dev/null
+++ b/tests/misc/commands_file.t/prepro.txt
@@ -0,0 +1,6 @@
+-cpp-extra-args="-DTEST_QUOTED_1 -DTEST_QUOTED_2=2"
+-cpp-extra-args -DTEST_UNQUOTED_1 -DTEST_UNQUOTED_2=4
+-cpp-extra-args "-DTEST_QUOTED_STRING_1=\"test_quoted_string_1\""
+-cpp-extra-args -DTEST_QUOTED_STRING_2=\"test_quoted_string_2\"
+-cpp-extra-args=-DTEST_UNQUOTED_STRING_1="test_unquoted_string_1"
+-cpp-extra-args="-DTEST_UNQUOTED_STRING_2=test_unquoted_string_2"
diff --git a/tests/misc/commands_file.t/print.txt b/tests/misc/commands_file.t/print.txt
new file mode 100644
index 0000000000..d2444ba432
--- /dev/null
+++ b/tests/misc/commands_file.t/print.txt
@@ -0,0 +1 @@
+-print
diff --git a/tests/misc/commands_file.t/run.t b/tests/misc/commands_file.t/run.t
new file mode 100644
index 0000000000..d6d75be41a
--- /dev/null
+++ b/tests/misc/commands_file.t/run.t
@@ -0,0 +1,338 @@
+Everything in a commands file
+ $ dune exec --cache=disabled -- frama-c -commands-file full.txt
+ [kernel] Expanding arguments from full.txt
+ [kernel] Expanding arguments from prepro.txt
+ [kernel] Parsing src.c (with preprocessing)
+ [eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 128.
+ option -eva-widening-delay set to 3 (default value).
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel already set to 200 (not modified).
+ option -eva-ilevel set to 48.
+ option -eva-plevel set to 150.
+ option -eva-subdivide-non-linear set to 100.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
+ option -eva-split-return set to 'auto'.
+ option -eva-equality-through-calls set to 'formals' (default value).
+ option -eva-octagon-through-calls set to false (default value).
+ [eva] Splitting return states on:
+ [eva] Analyzing a complete application starting at main
+ [eva:initial-state] Values of globals at initialization
+
+ [eva] ====== VALUES COMPUTED ======
+ [eva:final-states] Values at end of function main:
+ __retres ∈ {0; 5; 6; 7; 8; 9; 10; 11; 12}
+ [eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 2): 50% coverage.
+ In this function, 11 statements reached (out of 11): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+ /* Generated by Frama-C */
+ struct t {
+ int a ;
+ };
+ #pragma message("Quoted test strings are \'test_quoted_string_1\' and \'test_quoted_string_2\'")
+ #pragma message("Unquoted test strings are \'test_unquoted_string_1\' and \'test_unquoted_string_2\'")
+ int incr(int a)
+ {
+ int __retres;
+ __retres = a + 1;
+ return __retres;
+ }
+
+ int main(int argc, char const **argv)
+ {
+ int __retres;
+ if (argc > 1) {
+ if (argc < 10) {
+ __retres = argc + 3;
+ goto return_label;
+ }
+ else goto _LAND;
+ }
+ else {
+ _LAND: {
+ __retres = 0;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+ }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Commands split around -then
+ $ dune exec --cache=disabled -- frama-c -commands-file prepro.txt -commands-file kernel.txt -then -commands-file eva.txt -then -commands-file="print.txt"
+ [kernel] Expanding arguments from prepro.txt
+ [kernel] Expanding arguments from kernel.txt
+ [kernel] Expanding arguments from eva.txt
+ [kernel] Expanding arguments from print.txt
+ [kernel] Parsing src.c (with preprocessing)
+ [eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 128.
+ option -eva-widening-delay set to 3 (default value).
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel already set to 200 (not modified).
+ option -eva-ilevel set to 48.
+ option -eva-plevel set to 150.
+ option -eva-subdivide-non-linear set to 100.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
+ option -eva-split-return set to 'auto'.
+ option -eva-equality-through-calls set to 'formals' (default value).
+ option -eva-octagon-through-calls set to false (default value).
+ [eva] Splitting return states on:
+ [eva] Analyzing a complete application starting at main
+ [eva:initial-state] Values of globals at initialization
+
+ [eva] ====== VALUES COMPUTED ======
+ [eva:final-states] Values at end of function main:
+ __retres ∈ {0; 5; 6; 7; 8; 9; 10; 11; 12}
+ [eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 2): 50% coverage.
+ In this function, 11 statements reached (out of 11): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+ /* Generated by Frama-C */
+ struct t {
+ int a ;
+ };
+ #pragma message("Quoted test strings are \'test_quoted_string_1\' and \'test_quoted_string_2\'")
+ #pragma message("Unquoted test strings are \'test_unquoted_string_1\' and \'test_unquoted_string_2\'")
+ int incr(int a)
+ {
+ int __retres;
+ __retres = a + 1;
+ return __retres;
+ }
+
+ int main(int argc, char const **argv)
+ {
+ int __retres;
+ if (argc > 1) {
+ if (argc < 10) {
+ __retres = argc + 3;
+ goto return_label;
+ }
+ else goto _LAND;
+ }
+ else {
+ _LAND: {
+ __retres = 0;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+ }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Mix of commands file and command line
+ $ dune exec --cache=disabled -- frama-c -commands-file prepro.txt src.c -keep-unused-types -then -commands-file="eva.txt" -then -print
+ [kernel] Expanding arguments from prepro.txt
+ [kernel] Expanding arguments from eva.txt
+ [kernel] Parsing src.c (with preprocessing)
+ [eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 128.
+ option -eva-widening-delay set to 3 (default value).
+ option -eva-partition-history set to 0 (default value).
+ option -eva-slevel already set to 200 (not modified).
+ option -eva-ilevel set to 48.
+ option -eva-plevel set to 150.
+ option -eva-subdivide-non-linear set to 100.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
+ option -eva-split-return set to 'auto'.
+ option -eva-equality-through-calls set to 'formals' (default value).
+ option -eva-octagon-through-calls set to false (default value).
+ [eva] Splitting return states on:
+ [eva] Analyzing a complete application starting at main
+ [eva:initial-state] Values of globals at initialization
+
+ [eva] ====== VALUES COMPUTED ======
+ [eva:final-states] Values at end of function main:
+ __retres ∈ {0; 5; 6; 7; 8; 9; 10; 11; 12}
+ [eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 2): 50% coverage.
+ In this function, 11 statements reached (out of 11): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+ /* Generated by Frama-C */
+ struct t {
+ int a ;
+ };
+ #pragma message("Quoted test strings are \'test_quoted_string_1\' and \'test_quoted_string_2\'")
+ #pragma message("Unquoted test strings are \'test_unquoted_string_1\' and \'test_unquoted_string_2\'")
+ int incr(int a)
+ {
+ int __retres;
+ __retres = a + 1;
+ return __retres;
+ }
+
+ int main(int argc, char const **argv)
+ {
+ int __retres;
+ if (argc > 1) {
+ if (argc < 10) {
+ __retres = argc + 3;
+ goto return_label;
+ }
+ else goto _LAND;
+ }
+ else {
+ _LAND: {
+ __retres = 0;
+ goto return_label;
+ }
+ }
+ return_label: return __retres;
+ }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+Error while parsing something in the commands file
+(set -o pipefail is used so that the exit status of the whole pipe fails if one
+ of the command fails. Moreover a sub-shell `(set -o pipefail && ...)` is used
+ so that we do not need to restore the pipefail setting).
+ $ (set -o pipefail && dune exec --cache=disabled -- frama-c -commands-file with_error.txt src_empty.c -then -print | sed 's/^\(\s*use `\).*\(frama-c -help.*\)$/\1\2/g')
+ [kernel] Expanding arguments from with_error.txt
+ [kernel] User Error: option `-cache-size' requires an integer as argument.
+ use `frama-c -help' for more information.
+ [kernel] Frama-C aborted: invalid user input.
+ [1]
+
+Low-level options in the commands file (save)
+ $ dune exec --cache=disabled -- frama-c -commands-file ll_save.txt
+ [kernel] Expanding arguments from ll_save.txt
+ [kernel] Parsing src_empty.c (with preprocessing)
+
+Low-level options in the commands file (load)
+ $ dune exec --cache=disabled -- frama-c -commands-file ll_load.txt
+ [kernel] Expanding arguments from ll_load.txt
+ [eva] Analyzing a complete application starting at main
+ [eva:initial-state] Values of globals at initialization
+
+ [eva] Warning: The scope plugin is missing: cannot remove redundant alarms.
+ [eva] ====== VALUES COMPUTED ======
+ [eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+ [eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 100% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+
+Config file with \ and comments
+ $ dune exec --cache=disabled -- frama-c -commands-file comments_and_newlines.txt
+ [kernel] Expanding arguments from comments_and_newlines.txt
+ [kernel] Parsing src_empty.c (with preprocessing)
+ [eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
+ option -eva-min-loop-unroll set to 0 (default value).
+ option -eva-auto-loop-unroll set to 128.
+ option -eva-widening-delay set to 3 (default value).
+ option -eva-partition-history already set to 2 (not modified).
+ option -eva-slevel already set to 200 (not modified).
+ option -eva-ilevel already set to 32 (not modified).
+ option -eva-plevel already set to 100 (not modified).
+ option -eva-subdivide-non-linear set to 100.
+ option -eva-remove-redundant-alarms set to true (default value).
+ option -eva-domains already set to '@default,equality, gauges' (not modified).
+ option -eva-split-return set to 'auto'.
+ option -eva-equality-through-calls set to 'formals' (default value).
+ option -eva-octagon-through-calls set to false (default value).
+ [eva] Splitting return states on:
+ [eva] Analyzing a complete application starting at main
+ [eva:initial-state] Values of globals at initialization
+
+ [eva] ====== VALUES COMPUTED ======
+ [eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+ [eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 2 statements reached (out of 2): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/tests/misc/commands_file.t/src.c b/tests/misc/commands_file.t/src.c
new file mode 100644
index 0000000000..a48c97a14f
--- /dev/null
+++ b/tests/misc/commands_file.t/src.c
@@ -0,0 +1,42 @@
+#if defined(TEST_QUOTED_1) && defined(TEST_QUOTED_2) && TEST_QUOTED_2 == 2
+ // ok
+#else
+ #warning "Unable to parse TEST_QUOTED_1 and TEST_QUOTED_2"
+#endif
+
+#if defined(TEST_UNQUOTED_1) && defined(TEST_UNQUOTED_2) && TEST_UNQUOTED_2 == 4
+ // ok
+#else
+ #warning "Unable to parse TEST_UNQUOTED_1 and TEST_UNQUOTED2"
+#endif
+
+#if defined(TEST_QUOTED_STRING_1) && defined(TEST_QUOTED_STRING_2)
+ #pragma message("Quoted test strings are '" TEST_QUOTED_STRING_1 \
+ "' and '" TEST_QUOTED_STRING_2 "'")
+#else
+ #warning "Unable to parse TEST_QUOTED_STRING"
+#endif
+
+#if defined(TEST_UNQUOTED_STRING_1) && defined(TEST_UNQUOTED_STRING_2)
+ #define _STRINGIFY(str) #str
+ #define STRINGIFY(str) _STRINGIFY(str)
+ #pragma message("Unquoted test strings are '" \
+ STRINGIFY(TEST_UNQUOTED_STRING_1) "' and '" \
+ STRINGIFY(TEST_UNQUOTED_STRING_2) "'")
+#else
+ #warning "Unable to parse TEST_UNQUOTED_STRING"
+#endif
+
+struct t {
+ int a;
+};
+
+int incr(int a) { return a + 1; }
+
+int main(int argc, const char **argv) {
+ if (argc > 1 && argc < 10) {
+ return argc + 3;
+ } else {
+ return 0;
+ }
+}
diff --git a/tests/misc/commands_file.t/src_empty.c b/tests/misc/commands_file.t/src_empty.c
new file mode 100644
index 0000000000..76e8197013
--- /dev/null
+++ b/tests/misc/commands_file.t/src_empty.c
@@ -0,0 +1 @@
+int main() { return 0; }
diff --git a/tests/misc/commands_file.t/with_error.txt b/tests/misc/commands_file.t/with_error.txt
new file mode 100644
index 0000000000..7daf194603
--- /dev/null
+++ b/tests/misc/commands_file.t/with_error.txt
@@ -0,0 +1 @@
+-cache-size=="much big so number"
--
GitLab