diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 55783f8ac05109755785389af04ffbe841e83e26..dc22e5eeb1468dce1851b15f660d35019be5d647 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -95,7 +95,7 @@ extern long long int atoll(const char *nptr);
/* See ISO C: 7.20.1.3 to complete these specifications */
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
assigns \result \from indirect:nptr, indirect:nptr[0 ..];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
@@ -117,7 +117,7 @@ extern double strtod(const char * restrict nptr,
char ** restrict endptr);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
assigns \result \from indirect:nptr, indirect:nptr[0 ..];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
@@ -139,7 +139,7 @@ extern float strtof(const char * restrict nptr,
char ** restrict endptr);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
assigns \result \from indirect:nptr, indirect:nptr[0 ..];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
@@ -162,7 +162,7 @@ extern long double strtold(const char * restrict nptr,
/* TODO: See ISO C 7.20.1.4 to complete these specifications */
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
@@ -187,7 +187,7 @@ extern long int strtol(
int base);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
@@ -212,7 +212,7 @@ extern long long int strtoll(
int base);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
@@ -237,7 +237,7 @@ extern unsigned long int strtoul(
int base);
/*@
- requires valid_nptr: \valid_read(nptr); // cannot be precise, valid_read_string too strong
+ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base == 0 || 2 <= base <= 36;
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index e499e1e35008e4a11b45db79ffe85612b898482d..d5f67f7b13cc9f0205bc7ba7d27029f9e93dec28 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -20940,7 +20940,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -20950,10 +20950,10 @@
},
"region": {
"startLine": 98,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 98,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
@@ -21435,7 +21435,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -21445,10 +21445,10 @@
},
"region": {
"startLine": 120,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 120,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
@@ -23281,7 +23281,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -23291,10 +23291,10 @@
},
"region": {
"startLine": 165,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 165,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
@@ -23799,7 +23799,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -23809,10 +23809,10 @@
},
"region": {
"startLine": 142,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 142,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
@@ -24294,7 +24294,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -24304,10 +24304,10 @@
},
"region": {
"startLine": 190,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 190,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
@@ -24812,7 +24812,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -24822,10 +24822,10 @@
},
"region": {
"startLine": 215,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 215,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
@@ -25330,7 +25330,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_nptr." },
+ "message": { "text": "valid_string_nptr." },
"locations": [
{
"physicalLocation": {
@@ -25340,10 +25340,10 @@
},
"region": {
"startLine": 240,
- "startColumn": 23,
+ "startColumn": 30,
"endLine": 240,
- "endColumn": 40,
- "byteLength": 17
+ "endColumn": 53,
+ "byteLength": 23
}
}
}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 23a36e77700e65a967504abf760ccd37298f00ea..f54c0e53e9ef9e9077a8f8d192babb74943146b3 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -927,7 +927,7 @@ extern long atol(char const *nptr);
*/
extern long long atoll(char const *nptr);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
assigns \result, *endptr;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -955,7 +955,7 @@ extern long long atoll(char const *nptr);
*/
extern double strtod(char const * restrict nptr, char ** restrict endptr);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
assigns \result, *endptr;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -983,7 +983,7 @@ extern double strtod(char const * restrict nptr, char ** restrict endptr);
*/
extern float strtof(char const * restrict nptr, char ** restrict endptr);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
assigns \result, *endptr;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -1012,7 +1012,7 @@ extern float strtof(char const * restrict nptr, char ** restrict endptr);
extern long double strtold(char const * restrict nptr,
char ** restrict endptr);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
assigns \result, *endptr;
@@ -1049,7 +1049,7 @@ extern long double strtold(char const * restrict nptr,
extern long strtol(char const * restrict nptr, char ** restrict endptr,
int base);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
assigns \result, *endptr;
@@ -1086,7 +1086,7 @@ extern long strtol(char const * restrict nptr, char ** restrict endptr,
extern long long strtoll(char const * restrict nptr, char ** restrict endptr,
int base);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
assigns \result, *endptr;
@@ -1123,7 +1123,7 @@ extern long long strtoll(char const * restrict nptr, char ** restrict endptr,
extern unsigned long strtoul(char const * restrict nptr,
char ** restrict endptr, int base);
-/*@ requires valid_nptr: \valid_read(nptr);
+/*@ requires valid_string_nptr: valid_read_string(nptr);
requires separation: \separated(nptr, endptr);
requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36);
assigns \result, *endptr;
diff --git a/tests/libc/oracle/stdlib_h.0.res.oracle b/tests/libc/oracle/stdlib_h.0.res.oracle
index 7ed7accc254f0e7afb3ba7ec52f6513fdc441475..f3c34ab3d7b20fc92706f5c64290e6cff09f0e05 100644
--- a/tests/libc/oracle/stdlib_h.0.res.oracle
+++ b/tests/libc/oracle/stdlib_h.0.res.oracle
@@ -8,7 +8,7 @@
Called from stdlib_h.c:21.
[eva] using specification for function strtol
[eva] stdlib_h.c:21:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:21:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:21:
@@ -19,7 +19,7 @@
[eva] computing for function strtol <- main.
Called from stdlib_h.c:22.
[eva] stdlib_h.c:22:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:22:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:22:
@@ -30,7 +30,7 @@
[eva] computing for function strtol <- main.
Called from stdlib_h.c:23.
[eva] stdlib_h.c:23:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:23:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:23:
@@ -39,7 +39,7 @@
[eva] computing for function strtol <- main.
Called from stdlib_h.c:24.
[eva] stdlib_h.c:24:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:24:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:24:
@@ -49,7 +49,7 @@
Called from stdlib_h.c:28.
[eva] using specification for function strtoll
[eva] stdlib_h.c:28:
- function strtoll: precondition 'valid_nptr' got status valid.
+ function strtoll: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:28:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:28:
@@ -60,7 +60,7 @@
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:29.
[eva] stdlib_h.c:29:
- function strtoll: precondition 'valid_nptr' got status valid.
+ function strtoll: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:29:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:29:
@@ -71,7 +71,7 @@
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:30.
[eva] stdlib_h.c:30:
- function strtoll: precondition 'valid_nptr' got status valid.
+ function strtoll: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:30:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:30:
@@ -81,7 +81,7 @@
Called from stdlib_h.c:34.
[eva] using specification for function strtoul
[eva] stdlib_h.c:34:
- function strtoul: precondition 'valid_nptr' got status valid.
+ function strtoul: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:34:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:34:
@@ -92,7 +92,7 @@
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:35.
[eva] stdlib_h.c:35:
- function strtoul: precondition 'valid_nptr' got status valid.
+ function strtoul: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:35:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:35:
@@ -103,7 +103,7 @@
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:36.
[eva] stdlib_h.c:36:
- function strtoul: precondition 'valid_nptr' got status valid.
+ function strtoul: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:36:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:36:
@@ -113,7 +113,7 @@
Called from stdlib_h.c:40.
[eva] using specification for function strtoull
[eva] stdlib_h.c:40:
- function strtoull: precondition 'valid_nptr' got status valid.
+ function strtoull: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:40:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:40:
@@ -124,7 +124,7 @@
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:41.
[eva] stdlib_h.c:41:
- function strtoull: precondition 'valid_nptr' got status valid.
+ function strtoull: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:41:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:41:
@@ -135,7 +135,7 @@
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:42.
[eva] stdlib_h.c:42:
- function strtoull: precondition 'valid_nptr' got status valid.
+ function strtoull: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:42:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:42:
@@ -145,7 +145,7 @@
Called from stdlib_h.c:47.
[eva] using specification for function strtod
[eva] stdlib_h.c:47:
- function strtod: precondition 'valid_nptr' got status valid.
+ function strtod: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:47:
function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:47:
@@ -154,7 +154,7 @@
[eva] computing for function strtod <- main.
Called from stdlib_h.c:48.
[eva] stdlib_h.c:48:
- function strtod: precondition 'valid_nptr' got status valid.
+ function strtod: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:48:
function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:48:
@@ -163,7 +163,7 @@
[eva] computing for function strtod <- main.
Called from stdlib_h.c:49.
[eva] stdlib_h.c:49:
- function strtod: precondition 'valid_nptr' got status valid.
+ function strtod: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:49:
function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
@@ -171,7 +171,7 @@
Called from stdlib_h.c:53.
[eva] using specification for function strtold
[eva] stdlib_h.c:53:
- function strtold: precondition 'valid_nptr' got status valid.
+ function strtold: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:53:
function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:53:
@@ -180,7 +180,7 @@
[eva] computing for function strtold <- main.
Called from stdlib_h.c:54.
[eva] stdlib_h.c:54:
- function strtold: precondition 'valid_nptr' got status valid.
+ function strtold: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:54:
function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:54:
@@ -189,7 +189,7 @@
[eva] computing for function strtold <- main.
Called from stdlib_h.c:55.
[eva] stdlib_h.c:55:
- function strtold: precondition 'valid_nptr' got status valid.
+ function strtold: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:55:
function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
@@ -197,7 +197,7 @@
Called from stdlib_h.c:59.
[eva] using specification for function strtof
[eva] stdlib_h.c:59:
- function strtof: precondition 'valid_nptr' got status valid.
+ function strtof: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:59:
function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:59:
@@ -206,7 +206,7 @@
[eva] computing for function strtof <- main.
Called from stdlib_h.c:60.
[eva] stdlib_h.c:60:
- function strtof: precondition 'valid_nptr' got status valid.
+ function strtof: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:60:
function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:60:
@@ -215,7 +215,7 @@
[eva] computing for function strtof <- main.
Called from stdlib_h.c:61.
[eva] stdlib_h.c:61:
- function strtof: precondition 'valid_nptr' got status valid.
+ function strtof: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:61:
function strtof: precondition 'separation' got status valid.
[eva] Done for function strtof
diff --git a/tests/libc/oracle/stdlib_h.1.res.oracle b/tests/libc/oracle/stdlib_h.1.res.oracle
index 03146ea7ad797f9cdafb3c52ebc15c4ff5ffeff6..ae6a5de51506dd6f6c779a0f8b45098644817988 100644
--- a/tests/libc/oracle/stdlib_h.1.res.oracle
+++ b/tests/libc/oracle/stdlib_h.1.res.oracle
@@ -8,7 +8,7 @@
Called from stdlib_h.c:21.
[eva] using specification for function strtol
[eva] stdlib_h.c:21:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:21:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:21:
@@ -19,7 +19,7 @@
[eva] computing for function strtol <- main.
Called from stdlib_h.c:22.
[eva] stdlib_h.c:22:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:22:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:22:
@@ -30,7 +30,7 @@
[eva] computing for function strtol <- main.
Called from stdlib_h.c:23.
[eva] stdlib_h.c:23:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:23:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:23:
@@ -39,7 +39,7 @@
[eva] computing for function strtol <- main.
Called from stdlib_h.c:24.
[eva] stdlib_h.c:24:
- function strtol: precondition 'valid_nptr' got status valid.
+ function strtol: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:24:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:24:
@@ -49,7 +49,7 @@
Called from stdlib_h.c:28.
[eva] using specification for function strtoll
[eva] stdlib_h.c:28:
- function strtoll: precondition 'valid_nptr' got status valid.
+ function strtoll: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:28:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:28:
@@ -60,7 +60,7 @@
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:29.
[eva] stdlib_h.c:29:
- function strtoll: precondition 'valid_nptr' got status valid.
+ function strtoll: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:29:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:29:
@@ -71,7 +71,7 @@
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:30.
[eva] stdlib_h.c:30:
- function strtoll: precondition 'valid_nptr' got status valid.
+ function strtoll: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:30:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:30:
@@ -81,7 +81,7 @@
Called from stdlib_h.c:34.
[eva] using specification for function strtoul
[eva] stdlib_h.c:34:
- function strtoul: precondition 'valid_nptr' got status valid.
+ function strtoul: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:34:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:34:
@@ -92,7 +92,7 @@
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:35.
[eva] stdlib_h.c:35:
- function strtoul: precondition 'valid_nptr' got status valid.
+ function strtoul: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:35:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:35:
@@ -103,7 +103,7 @@
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:36.
[eva] stdlib_h.c:36:
- function strtoul: precondition 'valid_nptr' got status valid.
+ function strtoul: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:36:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:36:
@@ -113,7 +113,7 @@
Called from stdlib_h.c:40.
[eva] using specification for function strtoull
[eva] stdlib_h.c:40:
- function strtoull: precondition 'valid_nptr' got status valid.
+ function strtoull: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:40:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:40:
@@ -124,7 +124,7 @@
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:41.
[eva] stdlib_h.c:41:
- function strtoull: precondition 'valid_nptr' got status valid.
+ function strtoull: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:41:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:41:
@@ -135,7 +135,7 @@
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:42.
[eva] stdlib_h.c:42:
- function strtoull: precondition 'valid_nptr' got status valid.
+ function strtoull: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:42:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:42:
@@ -145,7 +145,7 @@
Called from stdlib_h.c:47.
[eva] using specification for function strtod
[eva] stdlib_h.c:47:
- function strtod: precondition 'valid_nptr' got status valid.
+ function strtod: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:47:
function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:47:
@@ -154,7 +154,7 @@
[eva] computing for function strtod <- main.
Called from stdlib_h.c:48.
[eva] stdlib_h.c:48:
- function strtod: precondition 'valid_nptr' got status valid.
+ function strtod: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:48:
function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:48:
@@ -163,7 +163,7 @@
[eva] computing for function strtod <- main.
Called from stdlib_h.c:49.
[eva] stdlib_h.c:49:
- function strtod: precondition 'valid_nptr' got status valid.
+ function strtod: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:49:
function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
@@ -171,7 +171,7 @@
Called from stdlib_h.c:53.
[eva] using specification for function strtold
[eva] stdlib_h.c:53:
- function strtold: precondition 'valid_nptr' got status valid.
+ function strtold: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:53:
function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:53:
@@ -180,7 +180,7 @@
[eva] computing for function strtold <- main.
Called from stdlib_h.c:54.
[eva] stdlib_h.c:54:
- function strtold: precondition 'valid_nptr' got status valid.
+ function strtold: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:54:
function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:54:
@@ -189,7 +189,7 @@
[eva] computing for function strtold <- main.
Called from stdlib_h.c:55.
[eva] stdlib_h.c:55:
- function strtold: precondition 'valid_nptr' got status valid.
+ function strtold: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:55:
function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
@@ -197,7 +197,7 @@
Called from stdlib_h.c:59.
[eva] using specification for function strtof
[eva] stdlib_h.c:59:
- function strtof: precondition 'valid_nptr' got status valid.
+ function strtof: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:59:
function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:59:
@@ -206,7 +206,7 @@
[eva] computing for function strtof <- main.
Called from stdlib_h.c:60.
[eva] stdlib_h.c:60:
- function strtof: precondition 'valid_nptr' got status valid.
+ function strtof: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:60:
function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:60:
@@ -215,7 +215,7 @@
[eva] computing for function strtof <- main.
Called from stdlib_h.c:61.
[eva] stdlib_h.c:61:
- function strtof: precondition 'valid_nptr' got status valid.
+ function strtof: precondition 'valid_string_nptr' got status valid.
[eva] stdlib_h.c:61:
function strtof: precondition 'separation' got status valid.
[eva] Done for function strtof