From 97d687c8cbca9f3f6aa4632a9a3ab4f3b54f0b53 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 3 Jan 2022 18:45:08 +0100
Subject: [PATCH] [Libc] add stdnoreturn.h and add/improve some specs
---
headers/header_spec.txt | 1 +
share/compliance/glibc_functions.json | 1 +
share/libc/__fc_libc.h | 1 +
share/libc/stdlib.h | 14 ++
share/libc/stdnoreturn.h | 31 +++
share/libc/time.h | 11 +
.../tests/sarif/oracle/std_string.sarif | 232 +++++++++++++++++-
tests/libc/fc_libc.c | 1 +
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.0.res.oracle | 27 +-
tests/libc/oracle/fc_libc.1.res.oracle | 30 +++
tests/libc/oracle/fc_libc.2.res.oracle | 1 +
tests/libc/oracle/stdlib_h.res.oracle | 2 +
tests/libc/oracle/stdnoreturn_h.res.oracle | 23 ++
tests/libc/oracle/time_h.res.oracle | 21 ++
tests/libc/stdnoreturn_h.c | 20 ++
tests/libc/time_h.c | 5 +
17 files changed, 399 insertions(+), 24 deletions(-)
create mode 100644 share/libc/stdnoreturn.h
create mode 100644 tests/libc/oracle/stdnoreturn_h.res.oracle
create mode 100644 tests/libc/stdnoreturn_h.c
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4e8f0d8ddef..31a54d668dd 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -294,6 +294,7 @@ share/libc/stdio.c: CEA_LGPL
share/libc/stdio.h: CEA_LGPL
share/libc/stdlib.c: CEA_LGPL
share/libc/stdlib.h: CEA_LGPL
+share/libc/stdnoreturn.h: CEA_LGPL
share/libc/string.c: CEA_LGPL
share/libc/string.h: CEA_LGPL
share/libc/strings.h: CEA_LGPL
diff --git a/share/compliance/glibc_functions.json b/share/compliance/glibc_functions.json
index 90906ec100e..78d75c93756 100644
--- a/share/compliance/glibc_functions.json
+++ b/share/compliance/glibc_functions.json
@@ -929,6 +929,7 @@
"mkfifo",
"mknod",
"mkstemp",
+ "mkstemps",
"mktemp",
"mktime",
"mlock",
diff --git a/share/libc/__fc_libc.h b/share/libc/__fc_libc.h
index 3e710e9cec5..2f78bbc8bb1 100644
--- a/share/libc/__fc_libc.h
+++ b/share/libc/__fc_libc.h
@@ -80,6 +80,7 @@
#include "stdint.h"
#include "stdio.h"
#include "stdlib.h"
+#include "stdnoreturn.h"
#include "string.h"
#include "strings.h"
#include "stropts.h"
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index dcb1f408493..c40adfa3b82 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -692,6 +692,7 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
// missing: requires 'last 6 characters of template must be XXXXXX'
// missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) >= 6;
assigns templat[0..] \from \nothing;
assigns \result \from \nothing;
ensures result_error_or_valid_fd: \result == -1 ||
@@ -699,6 +700,19 @@ extern int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
extern int mkstemp(char *templat);
+/*@
+ // missing: requires 'last (6+suffixlen) characters of template must be X's'
+ // missing: assigns \result, templat[0..] \from 'filesystem', 'RNG';
+ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) >= 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen >= 0;
+ assigns templat[0..] \from \nothing;
+ assigns \result \from \nothing;
+ ensures result_error_or_valid_fd: \result == -1 ||
+ 0 <= \result < __FC_FOPEN_MAX;
+ */
+extern int mkstemps(char *templat, int suffixlen);
+
// This function may allocate memory for the result, which is not supported by
// some plugins such as Eva. In such cases, it is preferable to use the stub
// provided in stdlib.c.
diff --git a/share/libc/stdnoreturn.h b/share/libc/stdnoreturn.h
new file mode 100644
index 00000000000..866c6b74aea
--- /dev/null
+++ b/share/libc/stdnoreturn.h
@@ -0,0 +1,31 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2021 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+// This file is not in the C standard; it exists for compatibility purposes
+
+// 'noreturn' is an attribute in C++
+#ifndef __cpluscplus
+// Note that Frama-C still requires the '-c11' command-line option to parse
+// the _Noreturn keyword. Mere inclusion of this header without the option
+// will not work.
+#define noreturn _Noreturn
+#endif
diff --git a/share/libc/time.h b/share/libc/time.h
index fe6304ce88d..1ac6af43c3f 100644
--- a/share/libc/time.h
+++ b/share/libc/time.h
@@ -148,6 +148,7 @@ extern struct tm *gmtime(const time_t *timer);
assigns __fc_time_tm \from *timer;
ensures result_null_or_internal_tm:
\result == &__fc_time_tm || \result == \null;
+ ensures maybe_error: errno == \old(errno) || errno == EOVERFLOW;
*/
extern struct tm *localtime(const time_t *timer);
@@ -277,6 +278,16 @@ extern struct tm *getdate(const char *string);
extern struct tm *gmtime_r(const time_t *restrict timer,
struct tm *restrict result);
+/*@
+ requires valid_timer: \valid_read(timep);
+ requires valid_result: \valid(result);
+ assigns \result \from indirect:*timep, result;
+ assigns *result \from indirect:*timep;
+ assigns errno \from indirect:*timep;
+ ensures result_null_or_initialized:initialization:
+ (\result == result && \initialized(result)) || \result == \null;
+ ensures maybe_error: errno == \old(errno) || errno == EOVERFLOW;
+*/
extern struct tm *localtime_r(const time_t *restrict timep,
struct tm *restrict result);
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 368f8a6a14c..082afbda187 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -11276,9 +11276,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 700,
+ "startLine": 701,
"startColumn": 11,
- "endLine": 700,
+ "endLine": 701,
"endColumn": 18,
"byteLength": 7
}
@@ -11309,6 +11309,29 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "template_len." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 695,
+ "startColumn": 25,
+ "endLine": 695,
+ "endColumn": 45,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
@@ -11322,9 +11345,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 697,
+ "startLine": 698,
"startColumn": 36,
- "endLine": 698,
+ "endLine": 699,
"endColumn": 53,
"byteLength": 70
}
@@ -11345,9 +11368,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 695,
+ "startLine": 696,
"startColumn": 10,
- "endLine": 695,
+ "endLine": 696,
"endColumn": 22,
"byteLength": 12
}
@@ -11371,9 +11394,9 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 695,
+ "startLine": 696,
"startColumn": 10,
- "endLine": 695,
+ "endLine": 696,
"endColumn": 22,
"byteLength": 12
}
@@ -11396,9 +11419,198 @@
"uriBaseId": "FRAMAC_SHARE"
},
"region": {
- "startLine": 696,
+ "startLine": 697,
"startColumn": 10,
- "endLine": 696,
+ "endLine": 697,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function mkstemps." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 714,
+ "startColumn": 11,
+ "endLine": 714,
+ "endColumn": 19,
+ "byteLength": 8
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_template." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 706,
+ "startColumn": 27,
+ "endLine": 706,
+ "endColumn": 48,
+ "byteLength": 21
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "template_len." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 707,
+ "startColumn": 25,
+ "endLine": 707,
+ "endColumn": 57,
+ "byteLength": 32
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "non_negative_suffixlen." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 708,
+ "startColumn": 35,
+ "endLine": 708,
+ "endColumn": 49,
+ "byteLength": 14
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "result_error_or_valid_fd." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 711,
+ "startColumn": 36,
+ "endLine": 712,
+ "endColumn": 53,
+ "byteLength": 70
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function mkstemps." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 709,
+ "startColumn": 10,
+ "endLine": 709,
+ "endColumn": 22,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text":
+ "from clause of term *(templat + (0 ..)) in function mkstemps."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 709,
+ "startColumn": 10,
+ "endLine": 709,
+ "endColumn": 22,
+ "byteLength": 12
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function mkstemps."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 710,
+ "startColumn": 10,
+ "endLine": 710,
"endColumn": 17,
"byteLength": 7
}
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 89e599df66e..7c5a799d86a 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -127,6 +127,7 @@
#include "stdint.h"
#include "stdio.h"
#include "stdlib.h"
+#include "stdnoreturn.h"
#include "string.h"
#include "strings.h"
#include "stropts.h"
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 65435f28136..8f5441c585c 100644
--- a/tests/libc/oracle/coverage.res.oracle
+++ b/tests/libc/oracle/coverage.res.oracle
@@ -28,7 +28,7 @@
main: 4 stmts out of 4 (100.0%)
[metrics] Eva coverage statistics
=======================
- Syntactically reachable functions = 2 (out of 114)
+ Syntactically reachable functions = 2 (out of 115)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 3e6a3b4a237..47563bc9e75 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -4,10 +4,10 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] fc_libc.c:169: assertion got status valid.
[eva] fc_libc.c:170: assertion got status valid.
[eva] fc_libc.c:171: assertion got status valid.
[eva] fc_libc.c:172: assertion got status valid.
+[eva] fc_libc.c:173: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -64,7 +64,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (427)
+ Specified-only functions (429)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -138,16 +138,17 @@
jrand48 (0 call); kill (0 call); killpg (0 call); labs (0 call);
lcong48 (0 call); ldexp (0 call); ldexpf (0 call); ldiv (0 call);
listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
- log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
- log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
- longjmp (0 call); lrand48 (0 call); lseek (0 call); lstat (0 call);
- malloc (13 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
- mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
- mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
- nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
- ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
- openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
- pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+ localtime_r (0 call); log (0 call); log10 (0 call); log10f (0 call);
+ log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
+ logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
+ lseek (0 call); lstat (0 call); malloc (13 calls); mblen (0 call);
+ mbstowcs (0 call); mbtowc (0 call); mkdir (0 call); mkfifo (0 call);
+ mknod (0 call); mkstemp (0 call); mkstemps (0 call); mktime (0 call);
+ mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
+ nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
+ open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
+ pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
+ poll (0 call); popen (0 call); pow (0 call); powf (0 call);
pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
pthread_cond_init (0 call); pthread_cond_wait (0 call);
pthread_create (0 call); pthread_getname_np (0 call); pthread_join (0 call);
@@ -221,7 +222,7 @@
Goto = 118
Assignment = 718
Exit point = 129
- Function = 557
+ Function = 559
Function call = 166
Pointer dereferencing = 350
Cyclomatic complexity = 436
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 880d36bf6a6..566c5af75a0 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -1620,6 +1620,7 @@ extern size_t wcstombs(char * restrict s, wchar_t const * restrict pwcs,
int posix_memalign(void **memptr, size_t alignment, size_t size);
/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6;
ensures
result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
assigns *(templat + (0 ..)), \result;
@@ -1628,6 +1629,17 @@ int posix_memalign(void **memptr, size_t alignment, size_t size);
*/
extern int mkstemp(char *templat);
+/*@ requires valid_template: valid_string(templat);
+ requires template_len: strlen(templat) ≥ 6 + suffixlen;
+ requires non_negative_suffixlen: suffixlen ≥ 0;
+ ensures
+ result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16);
+ assigns *(templat + (0 ..)), \result;
+ assigns *(templat + (0 ..)) \from \nothing;
+ assigns \result \from \nothing;
+ */
+extern int mkstemps(char *templat, int suffixlen);
+
char *realpath(char const * restrict file_name, char * restrict resolved_name);
char *canonicalize_file_name(char const *path);
@@ -5286,6 +5298,8 @@ extern struct tm *gmtime(time_t const *timer);
ensures
result_null_or_internal_tm:
\result ≡ &__fc_time_tm ∨ \result ≡ \null;
+ ensures
+ maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 75;
assigns \result, __fc_time_tm;
assigns \result \from __fc_p_time_tm;
assigns __fc_time_tm \from *timer;
@@ -5440,6 +5454,22 @@ extern int clock_nanosleep(clockid_t clock_id, int flags,
extern struct tm *gmtime_r(time_t const * restrict timer,
struct tm * restrict result);
+/*@ requires valid_timer: \valid_read(timep);
+ requires valid_result: \valid(result);
+ ensures
+ result_null_or_initialized: initialization:
+ (\result ≡ \old(result) ∧ \initialized(\old(result))) ∨
+ \result ≡ \null;
+ ensures
+ maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 75;
+ assigns \result, *result, __fc_errno;
+ assigns \result \from (indirect: *timep), result;
+ assigns *result \from (indirect: *timep);
+ assigns __fc_errno \from (indirect: *timep);
+ */
+extern struct tm *localtime_r(time_t const * restrict timep,
+ struct tm * restrict result);
+
/*@ requires valid_request: \valid_read(rqtp);
requires
initialization: initialized_request:
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 19a092a2d83..9e97d67741a 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -100,6 +100,7 @@ skipping FRAMAC_SHARE/libc/complex.h
[kernel] Parsing FRAMAC_SHARE/libc/stdint.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdio.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stdlib.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/libc/stdnoreturn.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/string.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/strings.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/libc/stropts.h (with preprocessing)
diff --git a/tests/libc/oracle/stdlib_h.res.oracle b/tests/libc/oracle/stdlib_h.res.oracle
index 76a413c1aad..158e8ba4bdc 100644
--- a/tests/libc/oracle/stdlib_h.res.oracle
+++ b/tests/libc/oracle/stdlib_h.res.oracle
@@ -237,6 +237,8 @@
[eva] using specification for function mkstemp
[eva] stdlib_h.c:82:
function mkstemp: precondition 'valid_template' got status valid.
+[eva] stdlib_h.c:82:
+ function mkstemp: precondition 'template_len' got status valid.
[eva] Done for function mkstemp
[eva] computing for function drand48 <- main.
Called from stdlib_h.c:86.
diff --git a/tests/libc/oracle/stdnoreturn_h.res.oracle b/tests/libc/oracle/stdnoreturn_h.res.oracle
new file mode 100644
index 00000000000..f5fbba713d5
--- /dev/null
+++ b/tests/libc/oracle/stdnoreturn_h.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing stdnoreturn_h.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva] computing for function f <- main.
+ Called from stdnoreturn_h.c:18.
+[eva] Recording results for f
+[eva] Done for function f
+[eva] computing for function g <- main.
+ Called from stdnoreturn_h.c:19.
+[eva] Recording results for g
+[eva] Done for function g
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function f:
+ NON TERMINATING FUNCTION
+[eva:final-states] Values at end of function g:
+ NON TERMINATING FUNCTION
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/time_h.res.oracle b/tests/libc/oracle/time_h.res.oracle
index 8ca10a9c75b..1700a2d16a4 100644
--- a/tests/libc/oracle/time_h.res.oracle
+++ b/tests/libc/oracle/time_h.res.oracle
@@ -233,10 +233,29 @@
function asctime: precondition 'initialization,init_timeptr' got status valid.
[eva] Done for function asctime
[eva:alarm] time_h.c:65: Warning: assertion got status unknown.
+[eva] computing for function localtime <- main.
+ Called from time_h.c:67.
+[eva] using specification for function localtime
+[eva] time_h.c:67:
+ function localtime: precondition 'valid_timer' got status valid.
+[eva] Done for function localtime
+[eva] computing for function localtime_r <- main.
+ Called from time_h.c:69.
+[eva] using specification for function localtime_r
+[eva] time_h.c:69:
+ function localtime_r: precondition 'valid_timer' got status valid.
+[eva] time_h.c:69:
+ function localtime_r: precondition 'valid_result' got status valid.
+[eva] Done for function localtime_r
+[eva] computing for function localtime_r <- main.
+ Called from time_h.c:69.
+[eva] Done for function localtime_r
+[eva] time_h.c:70: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
__fc_ctime[0..25] ∈ [--..--]
__fc_time_tm ∈ [--..--]
Frama_C_entropy_source ∈ [--..--]
@@ -252,4 +271,6 @@
t ∈ [--..--]
res_time ∈ {{ NULL ; &mytime2 }} or UNINITIALIZED
mytime2 ∈ [--..--] or UNINITIALIZED
+ localp ∈ {{ NULL ; &localr }}
+ localr ∈ [--..--] or UNINITIALIZED
__retres ∈ {0; 1; 2}
diff --git a/tests/libc/stdnoreturn_h.c b/tests/libc/stdnoreturn_h.c
new file mode 100644
index 00000000000..8b234faea6a
--- /dev/null
+++ b/tests/libc/stdnoreturn_h.c
@@ -0,0 +1,20 @@
+/*run.config
+ STDOPT: #"-c11"
+*/
+
+#include <stdnoreturn.h>
+
+noreturn void f(void) {
+ while (1);
+}
+
+_Noreturn void g(void) {
+ while (2);
+}
+
+volatile int v;
+
+int main() {
+ if (v) f();
+ if (v) g();
+}
diff --git a/tests/libc/time_h.c b/tests/libc/time_h.c
index 52a14290535..28d599ddb65 100644
--- a/tests/libc/time_h.c
+++ b/tests/libc/time_h.c
@@ -64,5 +64,10 @@ int main() {
time_str = asctime(&mytime);
//@ assert valid_string(time_str);
+ struct tm *localp = localtime(&t);
+ struct tm localr;
+ localp = localtime_r(&t, &localr);
+ //@ assert localp == \null || localp == &localr;
+
return 0;
}
--
GitLab