From ffffa4fec4be188386879797602a91100c91be47 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 26 Apr 2024 17:20:02 +0200
Subject: [PATCH] [libc] minor fixes
---
share/libc/netdb.h | 2 +-
share/libc/stdlib.h | 2 +-
share/libc/wchar.h | 2 ++
.../tests/sarif/oracle/std_string.sarif | 25 +++++++++++++++++++
.../tests/known/oracle/printf.res.oracle | 12 ++++-----
.../tests/known/oracle/swprintf.res.oracle | 14 +++++------
.../tests/known/oracle/wchar.res.oracle | 12 ++++-----
tests/libc/oracle/fc_libc.1.res.oracle | 13 +++++++---
tests/libc/oracle/stdlib_h.0.res.oracle | 3 +++
tests/libc/oracle/stdlib_h.1.res.oracle | 3 +++
tests/libc/oracle/wchar_h.res.oracle | 1 +
11 files changed, 64 insertions(+), 25 deletions(-)
diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index 0b09f4b9d9c..6e1c2515915 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -181,7 +181,7 @@ extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
/*@
allocates \result;
- assigns \result, *\result \from name[0 .. strlen(name)];
+ assigns *\result \from name[0 .. strlen(name)];
*/
extern struct hostent *gethostbyname(const char *name);
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 9042a4ca36c..e4c4ca549f1 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -570,7 +570,7 @@ extern int putenv(char *string);
requires valid_name: valid_read_string(name);
requires valid_value: valid_read_string(value);
allocates __fc_env[0..];
- assigns \result, __fc_env[0..]
+ assigns \result, __fc_env[0..], __fc_errno
\from __fc_env[0..], indirect:name[0 .. strlen(name)],
indirect:value[0 .. strlen(value)], indirect:overwrite;
assigns __fc_env[0..][0..] \from name[0 .. strlen(name)],
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 38bcc2d98cc..89bbba4df2e 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -271,6 +271,8 @@ extern int wcscasecmp(const wchar_t *ws1, const wchar_t *ws2);
requires valid_wstring: valid_read_wstring(ws);
allocates \result;
assigns \result \from indirect:ws[0..wcslen(ws)], indirect:__fc_heap_status;
+ assigns __fc_heap_status \from indirect:ws[0 .. wcslen(ws)],
+ __fc_heap_status;
behavior allocation:
assumes can_allocate: is_allocable(wcslen(ws));
assigns __fc_heap_status \from indirect:ws[0 .. wcslen(ws)],
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 8cd873462f2..6c7da9d8629 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -18247,6 +18247,31 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term __fc_errno in function setenv."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 573,
+ "startColumn": 34,
+ "endLine": 573,
+ "endColumn": 44,
+ "byteLength": 10
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 2dc413e1c2b..00a916d66f0 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:292:
- Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:294:
- Declaration of variadic function swprintf.
+ Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:296:
+ Declaration of variadic function swprintf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:298:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:299:
- Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:301:
- Declaration of variadic function fwscanf.
+ Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:303:
+ Declaration of variadic function fwscanf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:305:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index a7437bfcd7c..dc5aa4bc442 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:292:
- Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:294:
- Declaration of variadic function swprintf.
+ Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:296:
+ Declaration of variadic function swprintf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:298:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:299:
- Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:301:
- Declaration of variadic function fwscanf.
+ Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:303:
+ Declaration of variadic function fwscanf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:305:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
@@ -35,7 +35,7 @@
[eva] Analyzing a complete application starting at main
[eva] using specification for function wmemset
[eva] using specification for function swprintf_va_1
-[eva] FRAMAC_SHARE/libc/wchar.h:294:
+[eva] FRAMAC_SHARE/libc/wchar.h:296:
Cannot evaluate range bound wformat_length(format) - 1
(unsupported ACSL construct: logic function wformat_length). Approximating
[eva:alarm] swprintf.c:12: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index e0192389ab0..e845bbf02f0 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:292:
- Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:294:
- Declaration of variadic function swprintf.
+ Declaration of variadic function fwprintf.
[variadic] FRAMAC_SHARE/libc/wchar.h:296:
+ Declaration of variadic function swprintf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:298:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:299:
- Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:301:
- Declaration of variadic function fwscanf.
+ Declaration of variadic function wscanf.
[variadic] FRAMAC_SHARE/libc/wchar.h:303:
+ Declaration of variadic function fwscanf.
+[variadic] FRAMAC_SHARE/libc/wchar.h:305:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6f3dc88e2df..bb27675e27a 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5254,8 +5254,7 @@ static int res_search(char const *dname, int rec_class, int type,
return tmp;
}
-/*@ assigns \result, *\result;
- assigns \result \from *(name + (0 .. strlen{Old}(name)));
+/*@ assigns *\result;
assigns *\result \from *(name + (0 .. strlen{Old}(name)));
allocates \result;
*/
@@ -8346,7 +8345,7 @@ int putenv(char *string)
/*@ requires valid_name: valid_read_string(name);
requires valid_value: valid_read_string(value);
ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
- assigns \result, __fc_env[0 ..], *(__fc_env[0 ..] + (0 ..));
+ assigns \result, __fc_env[0 ..], __fc_errno, *(__fc_env[0 ..] + (0 ..));
assigns \result
\from __fc_env[0 ..], (indirect: *(name + (0 .. strlen{Old}(name)))),
(indirect: *(value + (0 .. strlen{Old}(value)))),
@@ -8355,6 +8354,10 @@ int putenv(char *string)
\from __fc_env[0 ..], (indirect: *(name + (0 .. strlen{Old}(name)))),
(indirect: *(value + (0 .. strlen{Old}(value)))),
(indirect: overwrite);
+ assigns __fc_errno
+ \from __fc_env[0 ..], (indirect: *(name + (0 .. strlen{Old}(name)))),
+ (indirect: *(value + (0 .. strlen{Old}(value)))),
+ (indirect: overwrite);
assigns *(__fc_env[0 ..] + (0 ..))
\from *(name + (0 .. strlen{Old}(name))),
*(value + (0 .. strlen{Old}(value))), (indirect: __fc_env[0 ..]),
@@ -10245,10 +10248,12 @@ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n)
}
/*@ requires valid_wstring: valid_read_wstring(ws);
- assigns \result;
+ assigns \result, __fc_heap_status;
assigns \result
\from (indirect: *(ws + (0 .. wcslen{Old}(ws)))),
(indirect: __fc_heap_status);
+ assigns __fc_heap_status
+ \from (indirect: *(ws + (0 .. wcslen{Old}(ws)))), __fc_heap_status;
allocates \result;
behavior allocation:
diff --git a/tests/libc/oracle/stdlib_h.0.res.oracle b/tests/libc/oracle/stdlib_h.0.res.oracle
index 4c93198f826..1cc7c46da27 100644
--- a/tests/libc/oracle/stdlib_h.0.res.oracle
+++ b/tests/libc/oracle/stdlib_h.0.res.oracle
@@ -424,6 +424,9 @@
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_errno ∈
+ {{ garbled mix of &{S_0___fc_env; S_1___fc_env}
+ (origin: Library function {stdlib_h.c:131}) }}
__fc_random48_init ∈ {1}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_env[0..4095] ∈
diff --git a/tests/libc/oracle/stdlib_h.1.res.oracle b/tests/libc/oracle/stdlib_h.1.res.oracle
index 9f36d6f4d13..51a15bb613a 100644
--- a/tests/libc/oracle/stdlib_h.1.res.oracle
+++ b/tests/libc/oracle/stdlib_h.1.res.oracle
@@ -424,6 +424,9 @@
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_errno ∈
+ {{ garbled mix of &{S_0___fc_env; S_1___fc_env}
+ (origin: Library function {stdlib_h.c:131}) }}
__fc_random48_init ∈ {1}
__fc_random48_counter[0..2] ∈ [--..--]
__fc_env[0..4095] ∈
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index b11bedc26e3..8abb7517100 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -209,6 +209,7 @@
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
fd ∈ {{ NULL ; &__fc_fopen + [0..120],0%8 }}
buf[0..28] ∈ [--..--] or UNINITIALIZED
[29] ∈ UNINITIALIZED
--
GitLab