Skip to content
Snippets Groups Projects
Commit 406cc7f2 authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Michele Alberti
Browse files

[tests] refactor const-assignments.c to ensure first run does not have warnings

also make real errors for KO instructions
parent ae7067ee
No related branches found
No related tags found
No related merge requests found
Showing
with 19 additions and 20 deletions
...@@ -12,6 +12,7 @@ ...@@ -12,6 +12,7 @@
STDOPT: +" -cpp-extra-args=-DT7" STDOPT: +" -cpp-extra-args=-DT7"
EXIT:1 EXIT:1
STDOPT: +" -cpp-extra-args=-DT8" 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 /* The first run is correct. The others should fail, as they include invalid
assignments to const lvalues. */ assignments to const lvalues. */
...@@ -103,9 +104,11 @@ void mutable_test_call(__attribute__((__fc_initialized_object)) const S* s) { ...@@ -103,9 +104,11 @@ void mutable_test_call(__attribute__((__fc_initialized_object)) const S* s) {
int a = 1; int a = 1;
k1(a + (s + 2)); k1(a + (s + 2));
k2(&(s + 2)->y); k2(&(s + 2)->y);
#ifdef T9
/* KO: although s has the __fc_initialized_object attribute, z[0] has not (and /* KO: although s has the __fc_initialized_object attribute, z[0] has not (and
cannot) and y is const. */ cannot) and y is const. */
k2(&s->z[0]->y); k2(&s->z[0]->y);
#endif
} }
#ifdef T8 #ifdef T8
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 */ /* Generated by Frama-C */
struct S { struct S {
int x ; int x ;
...@@ -45,7 +43,6 @@ void mutable_test_call(S const *s) ...@@ -45,7 +43,6 @@ void mutable_test_call(S const *s)
int a = 1; int a = 1;
k1((S *)((s + 2) + a)); k1((S *)((s + 2) + a));
k2((int *)(& (s + 2)->y)); k2((int *)(& (s + 2)->y));
k2((int *)(& (s->z[0])->y));
return; return;
} }
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
[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.
[kernel] Parsing const-assignments.c (with preprocessing) [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 Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 Cannot assign to non-modifiable lval x_0
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 Cannot assign to non-modifiable lval *x_0
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 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 */ /* Generated by Frama-C */
struct S { struct S {
int x ; int x ;
...@@ -53,7 +51,6 @@ void mutable_test_call(S const *s) ...@@ -53,7 +51,6 @@ void mutable_test_call(S const *s)
int a = 1; int a = 1;
k1((S *)((s + 2) + a)); k1((S *)((s + 2) + a));
k2((int *)(& (s + 2)->y)); k2((int *)(& (s + 2)->y));
k2((int *)(& (s->z[0])->y));
return; return;
} }
......
[kernel] Parsing const-assignments.c (with preprocessing) [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 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 */ /* Generated by Frama-C */
struct S { struct S {
int x ; int x ;
...@@ -53,7 +51,6 @@ void mutable_test_call(S const *s) ...@@ -53,7 +51,6 @@ void mutable_test_call(S const *s)
int a = 1; int a = 1;
k1((S *)((s + 2) + a)); k1((S *)((s + 2) + a));
k2((int *)(& (s + 2)->y)); k2((int *)(& (s + 2)->y));
k2((int *)(& (s->z[0])->y));
return; return;
} }
......
[kernel] Parsing const-assignments.c (with preprocessing) [kernel] Parsing const-assignments.c (with preprocessing)
[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning: [kernel] const-assignments.c:121: User Error:
expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
[kernel] const-assignments.c:118: User Error:
Cannot assign to non-modifiable lval t->s.y Cannot assign to non-modifiable lval t->s.y
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add [kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command. '-kernel-msg-key pp' for preprocessing command.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment