From 406cc7f2043e91352a629984522b539bb9fd6bff Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 16 Dec 2022 19:32:59 +0100
Subject: [PATCH] [tests] refactor const-assignments.c to ensure first run does
not have warnings
also make real errors for KO instructions
---
tests/syntax/const-assignments.c | 3 +++
tests/syntax/oracle/const-assignments.0.res.oracle | 3 ---
tests/syntax/oracle/const-assignments.1.res.oracle | 2 +-
tests/syntax/oracle/const-assignments.10.res.oracle | 7 +++++++
tests/syntax/oracle/const-assignments.2.res.oracle | 2 +-
tests/syntax/oracle/const-assignments.3.res.oracle | 2 +-
tests/syntax/oracle/const-assignments.4.res.oracle | 2 +-
tests/syntax/oracle/const-assignments.5.res.oracle | 2 +-
tests/syntax/oracle/const-assignments.6.res.oracle | 2 +-
tests/syntax/oracle/const-assignments.7.res.oracle | 5 +----
tests/syntax/oracle/const-assignments.8.res.oracle | 5 +----
tests/syntax/oracle/const-assignments.9.res.oracle | 4 +---
12 files changed, 19 insertions(+), 20 deletions(-)
create mode 100644 tests/syntax/oracle/const-assignments.10.res.oracle
diff --git a/tests/syntax/const-assignments.c b/tests/syntax/const-assignments.c
index caa00564dc0..fbe73e72e7b 100644
--- a/tests/syntax/const-assignments.c
+++ b/tests/syntax/const-assignments.c
@@ -12,6 +12,7 @@
STDOPT: +" -cpp-extra-args=-DT7"
EXIT:1
STDOPT: +" -cpp-extra-args=-DT8"
+ STDOPT: +" -cpp-extra-args=-DT9" +"-kernel-warn-key typing:incompatible-types-call=abort"
*/
/* The first run is correct. The others should fail, as they include invalid
assignments to const lvalues. */
@@ -103,9 +104,11 @@ void mutable_test_call(__attribute__((__fc_initialized_object)) const S* s) {
int a = 1;
k1(a + (s + 2));
k2(&(s + 2)->y);
+#ifdef T9
/* KO: although s has the __fc_initialized_object attribute, z[0] has not (and
cannot) and y is const. */
k2(&s->z[0]->y);
+#endif
}
#ifdef T8
diff --git a/tests/syntax/oracle/const-assignments.0.res.oracle b/tests/syntax/oracle/const-assignments.0.res.oracle
index 8e1f025840a..de3d0783c7c 100644
--- a/tests/syntax/oracle/const-assignments.0.res.oracle
+++ b/tests/syntax/oracle/const-assignments.0.res.oracle
@@ -1,6 +1,4 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
- expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
struct S {
int x ;
@@ -45,7 +43,6 @@ void mutable_test_call(S const *s)
int a = 1;
k1((S *)((s + 2) + a));
k2((int *)(& (s + 2)->y));
- k2((int *)(& (s->z[0])->y));
return;
}
diff --git a/tests/syntax/oracle/const-assignments.1.res.oracle b/tests/syntax/oracle/const-assignments.1.res.oracle
index 195e9432c35..038ab482208 100644
--- a/tests/syntax/oracle/const-assignments.1.res.oracle
+++ b/tests/syntax/oracle/const-assignments.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:21: User Error:
+[kernel] const-assignments.c:22: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.10.res.oracle b/tests/syntax/oracle/const-assignments.10.res.oracle
new file mode 100644
index 00000000000..aaee700de3e
--- /dev/null
+++ b/tests/syntax/oracle/const-assignments.10.res.oracle
@@ -0,0 +1,7 @@
+[kernel] Parsing const-assignments.c (with preprocessing)
+[kernel:typing:incompatible-types-call] const-assignments.c:110: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
+[kernel] User Error: warning typing:incompatible-types-call treated as fatal error.
+[kernel] User Error: stopping on file "const-assignments.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/const-assignments.2.res.oracle b/tests/syntax/oracle/const-assignments.2.res.oracle
index e253406148e..67303a701fc 100644
--- a/tests/syntax/oracle/const-assignments.2.res.oracle
+++ b/tests/syntax/oracle/const-assignments.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:27: User Error:
+[kernel] const-assignments.c:28: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.3.res.oracle b/tests/syntax/oracle/const-assignments.3.res.oracle
index 33c4bad33a3..79768f7799b 100644
--- a/tests/syntax/oracle/const-assignments.3.res.oracle
+++ b/tests/syntax/oracle/const-assignments.3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:33: User Error:
+[kernel] const-assignments.c:34: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.4.res.oracle b/tests/syntax/oracle/const-assignments.4.res.oracle
index 8c9c93e9c82..0ae87270890 100644
--- a/tests/syntax/oracle/const-assignments.4.res.oracle
+++ b/tests/syntax/oracle/const-assignments.4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:39: User Error:
+[kernel] const-assignments.c:40: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.5.res.oracle b/tests/syntax/oracle/const-assignments.5.res.oracle
index b7aa22f538e..395f59284a4 100644
--- a/tests/syntax/oracle/const-assignments.5.res.oracle
+++ b/tests/syntax/oracle/const-assignments.5.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:46: User Error:
+[kernel] const-assignments.c:47: User Error:
Cannot assign to non-modifiable lval x_0
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.6.res.oracle b/tests/syntax/oracle/const-assignments.6.res.oracle
index f05bcf02955..349d3259223 100644
--- a/tests/syntax/oracle/const-assignments.6.res.oracle
+++ b/tests/syntax/oracle/const-assignments.6.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:52: User Error:
+[kernel] const-assignments.c:53: User Error:
Cannot assign to non-modifiable lval *x_0
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.7.res.oracle b/tests/syntax/oracle/const-assignments.7.res.oracle
index 28fb4fda519..f397d365bca 100644
--- a/tests/syntax/oracle/const-assignments.7.res.oracle
+++ b/tests/syntax/oracle/const-assignments.7.res.oracle
@@ -1,8 +1,6 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel:typing:incompatible-types-call] const-assignments.c:60: Warning:
+[kernel:typing:incompatible-types-call] const-assignments.c:61: Warning:
expected 'int *' but got argument of type 'int const *': & x
-[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
- expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
struct S {
int x ;
@@ -53,7 +51,6 @@ void mutable_test_call(S const *s)
int a = 1;
k1((S *)((s + 2) + a));
k2((int *)(& (s + 2)->y));
- k2((int *)(& (s->z[0])->y));
return;
}
diff --git a/tests/syntax/oracle/const-assignments.8.res.oracle b/tests/syntax/oracle/const-assignments.8.res.oracle
index ee37293dbcb..281cae543fc 100644
--- a/tests/syntax/oracle/const-assignments.8.res.oracle
+++ b/tests/syntax/oracle/const-assignments.8.res.oracle
@@ -1,8 +1,6 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel:typing:incompatible-types-call] const-assignments.c:66: Warning:
+[kernel:typing:incompatible-types-call] const-assignments.c:67: Warning:
expected 'int *' but got argument of type 'int const *': x_0
-[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
- expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
struct S {
int x ;
@@ -53,7 +51,6 @@ void mutable_test_call(S const *s)
int a = 1;
k1((S *)((s + 2) + a));
k2((int *)(& (s + 2)->y));
- k2((int *)(& (s->z[0])->y));
return;
}
diff --git a/tests/syntax/oracle/const-assignments.9.res.oracle b/tests/syntax/oracle/const-assignments.9.res.oracle
index ec0fc31a923..7d532fb832d 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -1,7 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
- expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
-[kernel] const-assignments.c:118: User Error:
+[kernel] const-assignments.c:121: User Error:
Cannot assign to non-modifiable lval t->s.y
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
--
GitLab