diff --git a/tests/syntax/const-assignments.c b/tests/syntax/const-assignments.c index caa00564dc0548a83057048cafe084a1d51d0e8e..fbe73e72e7bf26d24cdedecda4f746e0a7fc88f9 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 8e1f025840a55596efdf118439d9065a193710a9..de3d0783c7c8bdccc47d733735a199338ff9816e 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 195e9432c3555aca11aa92de91a32b05d21cf62e..038ab482208c4f531c62dc10d5e6c86f1d9c1e49 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 0000000000000000000000000000000000000000..aaee700de3e0333d391e2524439b518ab3b5d152 --- /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 e253406148ecb9fe1f8e77d7a0fb8e4bd88414a6..67303a701fca626253759917c6a8d7ef31be47fa 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 33c4bad33a33015d727a3c3a3f5dae7fbca66b67..79768f7799b608b775963b5a3463710cdcb47635 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 8c9c93e9c82c5e04902d4a665fb2d152e612fcb8..0ae872708907a5410141a74efc231c127126d7e8 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 b7aa22f538e9eae22eea1cab7b0bfc7fa9dfe983..395f59284a48ac86eca556a12c95f23a5078c816 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 f05bcf02955448caf41e171a2b5bc9a506be37ae..349d3259223c8124771466cdf8c806797e50d91a 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 28fb4fda51942323ab613869ae6b9fff453bbeee..f397d365bcaad40d3e5369fe61c74f07918b368c 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 ee37293dbcb604246197f3309fd0e31ace6a5be5..281cae543fca4f7190a43e578eced91b459f2ba8 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 ec0fc31a9236c7dba702341a780aba577ec3237d..7d532fb832d1b38c4f5eba24de67bdaf9429055c 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.