diff --git a/share/libc/strings.h b/share/libc/strings.h index ee25b389858070303825fba1dd7ff3f5b3d41c6b..24ff2e7cfcd60834227c735a7ea716002e1c90cf 100644 --- a/share/libc/strings.h +++ b/share/libc/strings.h @@ -52,6 +52,9 @@ extern void bzero(void *s, size_t n); */ extern int ffs(int i); +#if _POSIX_C_SOURCE < 200809L +// index and rindex were removed in POSIX-1.2008 + /*@ assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c; */ @@ -61,6 +64,7 @@ extern char *index(const char *s, int c); assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c; */ extern char *rindex(const char *s, int c); +#endif /*@ requires valid_string_s1: valid_read_string(s1); diff --git a/tests/builtins/oracle/memcpy.0.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle index 4f0cb38f1d5dd9ab9abf9ac38dffdd1891f5c825..3f3237a3c0ece4ee4083e7fb5452934b9cf3ebe2 100644 --- a/tests/builtins/oracle/memcpy.0.res.oracle +++ b/tests/builtins/oracle/memcpy.0.res.oracle @@ -1814,7 +1814,7 @@ [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 56) +[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 59) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1825,7 +1825,7 @@ [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 61) +[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 64) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1836,7 +1836,7 @@ [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 68) +[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 72) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. @@ -1847,7 +1847,7 @@ [ Extern ] Assigns nothing Unverifiable but considered Valid. -[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 75) +[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 79) Unverifiable but considered Valid. [ Valid ] Default behavior by Frama-C kernel. diff --git a/tests/libc/oracle/strings_h.res.oracle b/tests/libc/oracle/strings_h.0.res.oracle similarity index 83% rename from tests/libc/oracle/strings_h.res.oracle rename to tests/libc/oracle/strings_h.0.res.oracle index 291159bf7a42e6e13c65d9aa8cfd8035cf98d4f1..4683c96f6407734372f1061dcc1726136bf00534 100644 --- a/tests/libc/oracle/strings_h.res.oracle +++ b/tests/libc/oracle/strings_h.0.res.oracle @@ -5,63 +5,63 @@ [eva:initial-state] Values of globals at initialization nondet ∈ [--..--] [eva] computing for function strcasecmp <- main. - Called from strings_h.c:9. + Called from strings_h.c:15. [eva] using specification for function strcasecmp -[eva] strings_h.c:9: +[eva] strings_h.c:15: function strcasecmp: precondition 'valid_string_s1' got status valid. -[eva] strings_h.c:9: +[eva] strings_h.c:15: function strcasecmp: precondition 'valid_string_s2' got status valid. [eva] Done for function strcasecmp [eva] computing for function strcasecmp <- main. - Called from strings_h.c:10. -[eva] strings_h.c:10: + Called from strings_h.c:16. +[eva] strings_h.c:16: function strcasecmp: precondition 'valid_string_s1' got status valid. -[eva] strings_h.c:10: +[eva] strings_h.c:16: function strcasecmp: precondition 'valid_string_s2' got status valid. [eva] Done for function strcasecmp [eva] computing for function strcasecmp <- main. - Called from strings_h.c:11. -[eva] strings_h.c:11: + Called from strings_h.c:17. +[eva] strings_h.c:17: function strcasecmp: precondition 'valid_string_s1' got status valid. -[eva] strings_h.c:11: +[eva] strings_h.c:17: function strcasecmp: precondition 'valid_string_s2' got status valid. [eva] Done for function strcasecmp [eva] computing for function strcasecmp <- main. - Called from strings_h.c:12. -[eva] strings_h.c:12: + Called from strings_h.c:18. +[eva] strings_h.c:18: function strcasecmp: precondition 'valid_string_s1' got status valid. -[eva:alarm] strings_h.c:12: Warning: +[eva:alarm] strings_h.c:18: Warning: function strcasecmp: precondition 'valid_string_s2' got status invalid. [eva] Done for function strcasecmp [eva] computing for function strncasecmp <- main. - Called from strings_h.c:13. + Called from strings_h.c:19. [eva] using specification for function strncasecmp -[eva] strings_h.c:13: +[eva] strings_h.c:19: function strncasecmp: precondition 'valid_string_s1' got status valid. -[eva] strings_h.c:13: +[eva] strings_h.c:19: function strncasecmp: precondition 'valid_string_s2' got status valid. [eva] Done for function strncasecmp [eva] computing for function strncasecmp <- main. - Called from strings_h.c:14. -[eva] strings_h.c:14: + Called from strings_h.c:20. +[eva] strings_h.c:20: function strncasecmp: precondition 'valid_string_s1' got status valid. -[eva:alarm] strings_h.c:14: Warning: +[eva:alarm] strings_h.c:20: Warning: function strncasecmp: precondition 'valid_string_s2' got status invalid. [eva] Done for function strncasecmp [eva] computing for function strncasecmp <- main. - Called from strings_h.c:15. -[eva] strings_h.c:15: + Called from strings_h.c:21. +[eva] strings_h.c:21: function strncasecmp: precondition 'valid_string_s1' got status valid. -[eva] strings_h.c:15: +[eva] strings_h.c:21: function strncasecmp: precondition 'valid_string_s2' got status valid. [eva] Done for function strncasecmp [eva] computing for function bzero <- main. - Called from strings_h.c:18. + Called from strings_h.c:24. [eva] using specification for function bzero -[eva] strings_h.c:18: +[eva] strings_h.c:24: function bzero: precondition 'valid_memory_area' got status valid. [eva] Done for function bzero -[eva] strings_h.c:19: assertion got status valid. +[eva] strings_h.c:25: assertion got status valid. [eva] Recording results for main [eva] Done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/tests/libc/oracle/strings_h.1.res.oracle b/tests/libc/oracle/strings_h.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..714fee2dc3e800f3d7b7a55f6f422e4e11d92b0d --- /dev/null +++ b/tests/libc/oracle/strings_h.1.res.oracle @@ -0,0 +1,11 @@ +[kernel] Parsing strings_h.c (with preprocessing) +[kernel] strings_h.c:29: User Error: + Inconsistent storage specification for index. Previous declaration: FRAMAC_SHARE/libc/strings.h:61 +[kernel] strings_h.c:29: User Error: + Declaration of index does not match previous declaration from FRAMAC_SHARE/libc/strings.h:61 (different type constructors: + char *(char const *s, int c) and int). + 27 + 28 // Check that 'index' is not defined when _POSIX_C_SOURCE >= 200809L + 29 static int index = 42; + ^^^^^ +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/libc/strings_h.c b/tests/libc/strings_h.c index 587b961e6ef5517cf3ec3b2fd254d10c6e9dd243..7b0d60d8542ba28a3c216bf11be5d03e3dec60e4 100644 --- a/tests/libc/strings_h.c +++ b/tests/libc/strings_h.c @@ -1,3 +1,9 @@ +/* run.config + STDOPT: #"-cpp-extra-args=\"-D_POSIX_C_SOURCE=200809L\"" + EXIT: 1 + STDOPT: +*/ + #include <strings.h> volatile int nondet; @@ -18,3 +24,6 @@ void main() { bzero(s4, 10); //@ assert s4[9] == s4[8] == 0; } + +// Check that 'index' is not defined when _POSIX_C_SOURCE >= 200809L +static int index = 42;