From 40d7c4518670a326c5492439b5ae207ca7bb3a5b Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 24 Feb 2023 09:25:46 +0100
Subject: [PATCH] [libc] fix postcondition in strto* functions
Thanks to Mark Dascher for the fix.
---
share/libc/stdlib.h | 14 ++---
.../tests/sarif/oracle/std_string.sarif | 56 +++++++++----------
tests/libc/oracle/fc_libc.1.res.oracle | 14 ++---
tests/libc/oracle/stdlib_h.0.res.oracle | 56 +++++++++----------
tests/libc/oracle/stdlib_h.1.res.oracle | 56 +++++++++----------
5 files changed, 98 insertions(+), 98 deletions(-)
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 0b8dbb19a68..55783f8ac05 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -108,7 +108,7 @@ extern long long int atoll(const char *nptr);
assigns \result \from indirect:nptr, indirect:nptr[0 ..];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
@@ -130,7 +130,7 @@ extern double strtod(const char * restrict nptr,
assigns \result \from indirect:nptr, indirect:nptr[0 ..];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
@@ -152,7 +152,7 @@ extern float strtof(const char * restrict nptr,
assigns \result \from indirect:nptr, indirect:nptr[0 ..];
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
@@ -176,7 +176,7 @@ extern long double strtold(const char * restrict nptr,
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
@@ -201,7 +201,7 @@ extern long int strtol(
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
@@ -226,7 +226,7 @@ extern long long int strtoll(
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
@@ -251,7 +251,7 @@ extern unsigned long int strtoul(
assigns \result \from indirect:nptr, indirect:nptr[0 ..], indirect:base;
assigns *endptr \from nptr, indirect:nptr[0 ..], indirect:endptr, indirect:base;
ensures initialization: \initialized(endptr);
- ensures valid_endptr: \valid_read(endptr);
+ ensures valid_endptr_content: \valid_read(*endptr);
ensures position_subset: \subset(*endptr, nptr + (0 ..));
complete behaviors;
disjoint behaviors;
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 1e15a794fc4..e499e1e3500 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -21078,7 +21078,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -21088,10 +21088,10 @@
},
"region": {
"startLine": 111,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 111,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
@@ -21573,7 +21573,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -21583,10 +21583,10 @@
},
"region": {
"startLine": 133,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 133,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
@@ -23442,7 +23442,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -23452,10 +23452,10 @@
},
"region": {
"startLine": 179,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 179,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
@@ -23937,7 +23937,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -23947,10 +23947,10 @@
},
"region": {
"startLine": 155,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 155,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
@@ -24455,7 +24455,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -24465,10 +24465,10 @@
},
"region": {
"startLine": 204,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 204,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
@@ -24973,7 +24973,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -24983,10 +24983,10 @@
},
"region": {
"startLine": 229,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 229,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
@@ -25491,7 +25491,7 @@
"ruleId": "user-spec",
"kind": "pass",
"level": "none",
- "message": { "text": "valid_endptr." },
+ "message": { "text": "valid_endptr_content." },
"locations": [
{
"physicalLocation": {
@@ -25501,10 +25501,10 @@
},
"region": {
"startLine": 254,
- "startColumn": 26,
+ "startColumn": 34,
"endLine": 254,
- "endColumn": 45,
- "byteLength": 19
+ "endColumn": 54,
+ "byteLength": 20
}
}
}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index af69919cfaa..23a36e77700 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -943,7 +943,7 @@ extern long long atoll(char const *nptr);
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -971,7 +971,7 @@ extern double strtod(char const * restrict nptr, char ** restrict endptr);
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -999,7 +999,7 @@ extern float strtof(char const * restrict nptr, char ** restrict endptr);
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -1033,7 +1033,7 @@ extern long double strtold(char const * restrict nptr,
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result
@@ -1070,7 +1070,7 @@ extern long strtol(char const * restrict nptr, char ** restrict endptr,
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result
@@ -1107,7 +1107,7 @@ extern long long strtoll(char const * restrict nptr, char ** restrict endptr,
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result
@@ -1144,7 +1144,7 @@ extern unsigned long strtoul(char const * restrict nptr,
assumes nonnull_endptr: endptr ≢ \null;
requires valid_endptr: \valid(endptr);
ensures initialization: \initialized(\old(endptr));
- ensures valid_endptr: \valid_read(\old(endptr));
+ ensures valid_endptr_content: \valid_read(*\old(endptr));
ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..));
assigns \result, *endptr;
assigns \result
diff --git a/tests/libc/oracle/stdlib_h.0.res.oracle b/tests/libc/oracle/stdlib_h.0.res.oracle
index cc7c4632797..7ed7accc254 100644
--- a/tests/libc/oracle/stdlib_h.0.res.oracle
+++ b/tests/libc/oracle/stdlib_h.0.res.oracle
@@ -18,8 +18,8 @@
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from stdlib_h.c:22.
-[eva:alarm] stdlib_h.c:22: Warning:
- function strtol: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:22:
+ function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:22:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:22:
@@ -29,8 +29,8 @@
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from stdlib_h.c:23.
-[eva:alarm] stdlib_h.c:23: Warning:
- function strtol: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:23:
+ function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:23:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:23:
@@ -59,8 +59,8 @@
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:29.
-[eva:alarm] stdlib_h.c:29: Warning:
- function strtoll: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:29:
+ function strtoll: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:29:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:29:
@@ -70,8 +70,8 @@
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:30.
-[eva:alarm] stdlib_h.c:30: Warning:
- function strtoll: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:30:
+ function strtoll: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:30:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:30:
@@ -91,8 +91,8 @@
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:35.
-[eva:alarm] stdlib_h.c:35: Warning:
- function strtoul: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:35:
+ function strtoul: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:35:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:35:
@@ -102,8 +102,8 @@
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:36.
-[eva:alarm] stdlib_h.c:36: Warning:
- function strtoul: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:36:
+ function strtoul: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:36:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:36:
@@ -123,8 +123,8 @@
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:41.
-[eva:alarm] stdlib_h.c:41: Warning:
- function strtoull: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:41:
+ function strtoull: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:41:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:41:
@@ -134,8 +134,8 @@
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:42.
-[eva:alarm] stdlib_h.c:42: Warning:
- function strtoull: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:42:
+ function strtoull: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:42:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:42:
@@ -153,8 +153,8 @@
[eva] Done for function strtod
[eva] computing for function strtod <- main.
Called from stdlib_h.c:48.
-[eva:alarm] stdlib_h.c:48: Warning:
- function strtod: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:48:
+ function strtod: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:48:
function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:48:
@@ -162,8 +162,8 @@
[eva] Done for function strtod
[eva] computing for function strtod <- main.
Called from stdlib_h.c:49.
-[eva:alarm] stdlib_h.c:49: Warning:
- function strtod: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:49:
+ function strtod: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:49:
function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
@@ -179,8 +179,8 @@
[eva] Done for function strtold
[eva] computing for function strtold <- main.
Called from stdlib_h.c:54.
-[eva:alarm] stdlib_h.c:54: Warning:
- function strtold: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:54:
+ function strtold: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:54:
function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:54:
@@ -188,8 +188,8 @@
[eva] Done for function strtold
[eva] computing for function strtold <- main.
Called from stdlib_h.c:55.
-[eva:alarm] stdlib_h.c:55: Warning:
- function strtold: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:55:
+ function strtold: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:55:
function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
@@ -205,8 +205,8 @@
[eva] Done for function strtof
[eva] computing for function strtof <- main.
Called from stdlib_h.c:60.
-[eva:alarm] stdlib_h.c:60: Warning:
- function strtof: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:60:
+ function strtof: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:60:
function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:60:
@@ -214,8 +214,8 @@
[eva] Done for function strtof
[eva] computing for function strtof <- main.
Called from stdlib_h.c:61.
-[eva:alarm] stdlib_h.c:61: Warning:
- function strtof: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:61:
+ function strtof: precondition 'valid_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 e2727df8a18..03146ea7ad7 100644
--- a/tests/libc/oracle/stdlib_h.1.res.oracle
+++ b/tests/libc/oracle/stdlib_h.1.res.oracle
@@ -18,8 +18,8 @@
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from stdlib_h.c:22.
-[eva:alarm] stdlib_h.c:22: Warning:
- function strtol: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:22:
+ function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:22:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:22:
@@ -29,8 +29,8 @@
[eva] Done for function strtol
[eva] computing for function strtol <- main.
Called from stdlib_h.c:23.
-[eva:alarm] stdlib_h.c:23: Warning:
- function strtol: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:23:
+ function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:23:
function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:23:
@@ -59,8 +59,8 @@
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:29.
-[eva:alarm] stdlib_h.c:29: Warning:
- function strtoll: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:29:
+ function strtoll: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:29:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:29:
@@ -70,8 +70,8 @@
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
Called from stdlib_h.c:30.
-[eva:alarm] stdlib_h.c:30: Warning:
- function strtoll: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:30:
+ function strtoll: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:30:
function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:30:
@@ -91,8 +91,8 @@
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:35.
-[eva:alarm] stdlib_h.c:35: Warning:
- function strtoul: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:35:
+ function strtoul: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:35:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:35:
@@ -102,8 +102,8 @@
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
Called from stdlib_h.c:36.
-[eva:alarm] stdlib_h.c:36: Warning:
- function strtoul: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:36:
+ function strtoul: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:36:
function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:36:
@@ -123,8 +123,8 @@
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:41.
-[eva:alarm] stdlib_h.c:41: Warning:
- function strtoull: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:41:
+ function strtoull: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:41:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:41:
@@ -134,8 +134,8 @@
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
Called from stdlib_h.c:42.
-[eva:alarm] stdlib_h.c:42: Warning:
- function strtoull: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:42:
+ function strtoull: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:42:
function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:42:
@@ -153,8 +153,8 @@
[eva] Done for function strtod
[eva] computing for function strtod <- main.
Called from stdlib_h.c:48.
-[eva:alarm] stdlib_h.c:48: Warning:
- function strtod: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:48:
+ function strtod: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:48:
function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:48:
@@ -162,8 +162,8 @@
[eva] Done for function strtod
[eva] computing for function strtod <- main.
Called from stdlib_h.c:49.
-[eva:alarm] stdlib_h.c:49: Warning:
- function strtod: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:49:
+ function strtod: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:49:
function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
@@ -179,8 +179,8 @@
[eva] Done for function strtold
[eva] computing for function strtold <- main.
Called from stdlib_h.c:54.
-[eva:alarm] stdlib_h.c:54: Warning:
- function strtold: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:54:
+ function strtold: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:54:
function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:54:
@@ -188,8 +188,8 @@
[eva] Done for function strtold
[eva] computing for function strtold <- main.
Called from stdlib_h.c:55.
-[eva:alarm] stdlib_h.c:55: Warning:
- function strtold: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:55:
+ function strtold: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:55:
function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
@@ -205,8 +205,8 @@
[eva] Done for function strtof
[eva] computing for function strtof <- main.
Called from stdlib_h.c:60.
-[eva:alarm] stdlib_h.c:60: Warning:
- function strtof: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:60:
+ function strtof: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:60:
function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:60:
@@ -214,8 +214,8 @@
[eva] Done for function strtof
[eva] computing for function strtof <- main.
Called from stdlib_h.c:61.
-[eva:alarm] stdlib_h.c:61: Warning:
- function strtof: precondition 'valid_nptr' got status unknown.
+[eva] stdlib_h.c:61:
+ function strtof: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:61:
function strtof: precondition 'separation' got status valid.
[eva] Done for function strtof
--
GitLab