Skip to content
Snippets Groups Projects
Commit 40d7c451 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[libc] fix postcondition in strto* functions 

Thanks to Mark Dascher for the fix.
parent b43febc8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
share/libc/stdlib.h
+ 7
− 7
View file @ 40d7c451
......@@ -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;
......
src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+ 28
− 28
View file @ 40d7c451
......@@ -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
}
}
}
......
tests/libc/oracle/fc_libc.1.res.oracle
+ 7
− 7
View file @ 40d7c451
......@@ -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
......
tests/libc/oracle/stdlib_h.0.res.oracle
+ 28
− 28
View file @ 40d7c451
......@@ -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
......
tests/libc/oracle/stdlib_h.1.res.oracle
+ 28
− 28
View file @ 40d7c451
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment