From 618f21ce4fabed0a990e2661c4a6e9470da4a544 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 30 Aug 2019 16:12:39 +0200
Subject: [PATCH] [Libc] add spec for GNU function strchrnul; improve spec for
strchr
---
share/libc/string.h | 8 +-
tests/builtins/oracle/memcpy.res.oracle | 181 ++++++++++--------
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.0.res.oracle | 38 ++--
tests/libc/oracle/fc_libc.1.res.oracle | 12 +-
tests/libc/oracle/netdb_c.res.oracle | 3 +-
tests/libc/oracle/stdlib_c_env.res.oracle | 2 +-
tests/libc/oracle/string_c.res.oracle | 42 ++--
tests/libc/oracle/string_c_generic.res.oracle | 32 ++--
tests/libc/oracle/string_c_strstr.res.oracle | 6 +-
tests/libc/oracle/string_h.res.oracle | 25 ++-
tests/libc/string_h.c | 7 +
12 files changed, 209 insertions(+), 149 deletions(-)
diff --git a/share/libc/string.h b/share/libc/string.h
index 097225f94e8..a2b62c15e8d 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -155,7 +155,7 @@ extern int strncmp (const char *s1, const char *s2, size_t n);
extern int strcoll (const char *s1, const char *s2);
/*@ requires valid_string_s: valid_read_string(s);
- @ assigns \result \from s, s[0..],c;
+ @ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
@ behavior found:
@ assumes char_found: strchr(s,c);
@ ensures result_char: *\result == (char)c;
@@ -172,6 +172,12 @@ extern int strcoll (const char *s1, const char *s2);
@*/
extern char *strchr(const char *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ @ assigns \result \from s, indirect:s[0..strlen(s)], indirect:c;
+ @ ensures result_same_base: \subset(\result, s+(0..strlen(s)));
+ @*/
+extern char *strchrnul(const char *s, int c);
+
/*@ requires valid_string_s: valid_read_string(s);
@ assigns \result \from s, s[0..],c;
@ behavior found:
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 68da1692272..dd7e4c0161b 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1318,6 +1318,19 @@
[ Valid ] Behavior 'not_found'
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'strchrnul'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'result_same_base'
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 176)
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'strrchr'
--------------------------------------------------------------------------------
@@ -1334,7 +1347,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 176)
+[ Extern ] Froms (file share/libc/string.h, line 182)
Unverifiable but considered Valid.
[ Valid ] Behavior 'default'
by Frama-C kernel.
@@ -1353,7 +1366,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 193)
+[ Extern ] Froms (file share/libc/string.h, line 199)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1364,11 +1377,11 @@
[ Extern ] Post-condition 'result_bounded'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 200)
+[ Extern ] Assigns (file share/libc/string.h, line 206)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 200)
+[ Extern ] Froms (file share/libc/string.h, line 206)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 201)
+[ Extern ] Froms (file share/libc/string.h, line 207)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1381,7 +1394,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 208)
+[ Extern ] Froms (file share/libc/string.h, line 214)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1394,7 +1407,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 216)
+[ Extern ] Froms (file share/libc/string.h, line 222)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1407,7 +1420,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 227)
+[ Extern ] Froms (file share/libc/string.h, line 233)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1424,31 +1437,31 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'resume_str' 'ptr_subset'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 240)
+[ Extern ] Assigns (file share/libc/string.h, line 246)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 255)
+[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 261)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 263)
+[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 269)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 240)
+[ Extern ] Froms (file share/libc/string.h, line 246)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 242)
+[ Extern ] Froms (file share/libc/string.h, line 248)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 244)
+[ Extern ] Froms (file share/libc/string.h, line 250)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 246)
+[ Extern ] Froms (file share/libc/string.h, line 252)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 255)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 261)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 256)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 262)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 257)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 263)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 263)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 269)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 266)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 272)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 269)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 275)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1471,31 +1484,31 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'resume_str' 'saveptr_subset'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 282)
+[ Extern ] Assigns (file share/libc/string.h, line 288)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 297)
+[ Extern ] Assigns for 'new_str' (file share/libc/string.h, line 303)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 307)
+[ Extern ] Assigns for 'resume_str' (file share/libc/string.h, line 313)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 282)
+[ Extern ] Froms (file share/libc/string.h, line 288)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 284)
+[ Extern ] Froms (file share/libc/string.h, line 290)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 286)
+[ Extern ] Froms (file share/libc/string.h, line 292)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 288)
+[ Extern ] Froms (file share/libc/string.h, line 294)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 297)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 303)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 298)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 304)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 299)
+[ Extern ] Froms for 'new_str' (file share/libc/string.h, line 305)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 307)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 313)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 310)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 316)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 313)
+[ Extern ] Froms for 'resume_str' (file share/libc/string.h, line 319)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1508,11 +1521,11 @@
--- Properties of Function 'strsep'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/string.h, line 325)
+[ Extern ] Assigns (file share/libc/string.h, line 331)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 325)
+[ Extern ] Froms (file share/libc/string.h, line 331)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 326)
+[ Extern ] Froms (file share/libc/string.h, line 332)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1529,7 +1542,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 336)
+[ Extern ] Froms (file share/libc/string.h, line 342)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1542,11 +1555,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 349)
+[ Extern ] Assigns (file share/libc/string.h, line 355)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 349)
+[ Extern ] Froms (file share/libc/string.h, line 355)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 350)
+[ Extern ] Froms (file share/libc/string.h, line 356)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1563,11 +1576,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'partial' 'equal_prefix'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 361)
+[ Extern ] Assigns (file share/libc/string.h, line 367)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 361)
+[ Extern ] Froms (file share/libc/string.h, line 367)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 362)
+[ Extern ] Froms (file share/libc/string.h, line 368)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete'
by Frama-C kernel.
@@ -1584,11 +1597,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'bounded_result'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 382)
+[ Extern ] Assigns (file share/libc/string.h, line 388)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 382)
+[ Extern ] Froms (file share/libc/string.h, line 388)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 383)
+[ Extern ] Froms (file share/libc/string.h, line 389)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1601,11 +1614,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'points_to_end'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 394)
+[ Extern ] Assigns (file share/libc/string.h, line 400)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 394)
+[ Extern ] Froms (file share/libc/string.h, line 400)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 395)
+[ Extern ] Froms (file share/libc/string.h, line 401)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1622,11 +1635,11 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition 'result_ptr'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 405)
+[ Extern ] Assigns (file share/libc/string.h, line 411)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 405)
+[ Extern ] Froms (file share/libc/string.h, line 411)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 408)
+[ Extern ] Froms (file share/libc/string.h, line 414)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1641,23 +1654,23 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'partial' 'sum_of_bounded_lengths'
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 425)
+[ Extern ] Assigns for 'complete' (file share/libc/string.h, line 431)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 419)
+[ Extern ] Assigns (file share/libc/string.h, line 425)
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 433)
+[ Extern ] Assigns for 'partial' (file share/libc/string.h, line 439)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'complete' (file share/libc/string.h, line 425)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 431)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'complete' (file share/libc/string.h, line 427)
+[ Extern ] Froms for 'complete' (file share/libc/string.h, line 433)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 419)
+[ Extern ] Froms (file share/libc/string.h, line 425)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 420)
+[ Extern ] Froms (file share/libc/string.h, line 426)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'partial' (file share/libc/string.h, line 433)
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 439)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'partial' (file share/libc/string.h, line 435)
+[ Extern ] Froms for 'partial' (file share/libc/string.h, line 441)
Unverifiable but considered Valid.
[ Valid ] Behavior 'complete'
by Frama-C kernel.
@@ -1672,11 +1685,11 @@
[ Extern ] Post-condition 'bounded_result'
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/string.h, line 445)
+[ Extern ] Assigns (file share/libc/string.h, line 451)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 445)
+[ Extern ] Froms (file share/libc/string.h, line 451)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 446)
+[ Extern ] Froms (file share/libc/string.h, line 452)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1685,11 +1698,11 @@
--- Properties of Function 'strxfrm'
--------------------------------------------------------------------------------
-[ Extern ] Assigns (file share/libc/string.h, line 454)
+[ Extern ] Assigns (file share/libc/string.h, line 460)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 454)
+[ Extern ] Froms (file share/libc/string.h, line 460)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 455)
+[ Extern ] Froms (file share/libc/string.h, line 461)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1704,19 +1717,19 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null'
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 467)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 473)
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 467)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 473)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 468)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 474)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 464)
+[ Extern ] Froms (file share/libc/string.h, line 470)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 474)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 480)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1724,7 +1737,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 463)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 469)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -1739,19 +1752,19 @@
Unverifiable but considered Valid.
[ Extern ] Post-condition for 'no_allocation' 'result_null'
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 486)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 492)
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
[ Extern ] Assigns for 'no_allocation' nothing
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 486)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 492)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 487)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 493)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 482)
+[ Extern ] Froms (file share/libc/string.h, line 488)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 496)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 502)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1759,7 +1772,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 481)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 487)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -1776,7 +1789,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 512)
+[ Extern ] Froms (file share/libc/string.h, line 518)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -2238,10 +2251,10 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 162 Completely validated
+ 163 Completely validated
1 Locally validated
- 239 Considered valid
+ 242 Considered valid
32 To be validated
4 Alarms emitted
- 438 Total
+ 442 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index 420792611b3..f0696a6f2d1 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 112)
+ Syntactically reachable functions = 2 (out of 113)
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 02529fbe95f..413b1aee0f0 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (394)
+ Undefined functions (395)
=========================
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);
@@ -142,23 +142,23 @@
sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
srand48 (0 call); srandom (0 call); stat (0 call); stpcpy (0 call);
- strcasestr (0 call); strcoll (0 call); strcspn (0 call); strftime (0 call);
- strlcat (0 call); strlcpy (0 call); strncasecmp (0 call); strpbrk (0 call);
- strsep (0 call); strspn (0 call); strtod (0 call); strtof (0 call);
- strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
- strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
- strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
- system (0 call); tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call);
- time (0 call); times (0 call); tmpfile (0 call); tmpnam (0 call);
- trunc (0 call); truncf (0 call); truncl (0 call); ttyname (0 call);
- tzset (0 call); umask (0 call); ungetc (0 call); unlink (0 call);
- usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
- vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
- vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
- wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
- wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
- wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
- wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ strcasestr (0 call); strchrnul (0 call); strcoll (0 call); strcspn (0 call);
+ strftime (0 call); strlcat (0 call); strlcpy (0 call); strncasecmp (0 call);
+ strpbrk (0 call); strsep (0 call); strspn (0 call); strtod (0 call);
+ strtof (0 call); strtoimax (0 call); strtok (0 call); strtok_r (0 call);
+ strtol (0 call); strtold (0 call); strtoll (0 call); strtoul (0 call);
+ strtoull (0 call); strxfrm (0 call); sync (0 call); sysconf (0 call);
+ syslog (0 call); system (0 call); tcflush (0 call); tcgetattr (0 call);
+ tcsetattr (0 call); time (0 call); times (0 call); tmpfile (0 call);
+ tmpnam (0 call); trunc (0 call); truncf (0 call); truncl (0 call);
+ ttyname (0 call); tzset (0 call); umask (0 call); ungetc (0 call);
+ unlink (0 call); usleep (0 call); utimes (0 call); vfprintf (0 call);
+ vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call);
+ vsprintf (0 call); vsyslog (0 call); wait (0 call); waitpid (0 call);
+ wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
+ wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
+ wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
+ wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call);
'Extern' global variables (16)
==============================
@@ -181,7 +181,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 476
+ Function = 477
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 3ac0899086f..34abdcbb6ed 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3999,6 +3999,15 @@ extern int strcoll(char const *s1, char const *s2);
char *strchr(char const *s, int c);
+/*@ requires valid_string_s: valid_read_string(s);
+ ensures
+ result_same_base: \subset(\result, \old(s) + (0 .. strlen(\old(s))));
+ assigns \result;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
+ */
+extern char *strchrnul(char const *s, int c);
+
char *strrchr(char const *s, int c);
/*@ requires valid_string_s: valid_read_string(s);
@@ -5919,7 +5928,8 @@ char *strncpy(char *dest, char const *src, size_t n)
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
- assigns \result \from s, *(s + (0 ..)), c;
+ assigns \result
+ \from s, (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: c);
behavior found:
assumes char_found: strchr(s, c) ≡ \true;
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 7245bc0aa8f..d3a9ddf8739 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -21,6 +21,7 @@
\return(memmove) == 0 (auto)
\return(memset) == 0 (auto)
\return(strchr) == 0 (auto)
+ \return(strchrnul) == 0 (auto)
\return(strrchr) == 0 (auto)
\return(strpbrk) == 0 (auto)
\return(strstr) == 0 (auto)
@@ -248,7 +249,7 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] share/libc/netdb.c:147:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:367:
+[eva] share/libc/string.h:373:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strncpy
[eva] Recording results for gethostbyname
diff --git a/tests/libc/oracle/stdlib_c_env.res.oracle b/tests/libc/oracle/stdlib_c_env.res.oracle
index 5322b2985d4..fc9107a8102 100644
--- a/tests/libc/oracle/stdlib_c_env.res.oracle
+++ b/tests/libc/oracle/stdlib_c_env.res.oracle
@@ -105,7 +105,7 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/stdlib_c_env.c:15:
function strcpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:351:
+[eva] share/libc/string.h:357:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
[eva] Done for function strcpy
[eva] computing for function getenv <- main.
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index 65a4843c64b..033c83c6b47 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -494,13 +494,13 @@
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
-[eva] share/libc/string.h:407:
+[eva] share/libc/string.h:413:
function strcat: postcondition 'sum_of_lengths' got status valid.
-[eva] share/libc/string.h:410:
+[eva] share/libc/string.h:416:
function strcat: postcondition 'initialization,dest' got status valid.
-[eva] share/libc/string.h:411:
+[eva] share/libc/string.h:417:
function strcat: postcondition 'dest_null_terminated' got status valid.
-[eva] share/libc/string.h:412:
+[eva] share/libc/string.h:418:
function strcat: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcat
[eva] Done for function strcat
@@ -559,11 +559,11 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/string_c.c:142:
function strcpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:351:
+[eva] share/libc/string.h:357:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:351: Warning:
+[eva:alarm] share/libc/string.h:357: Warning:
function strcpy: postcondition 'equal_contents' got status unknown.
-[eva] share/libc/string.h:352:
+[eva] share/libc/string.h:358:
function strcpy: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcpy
[eva] Done for function strcpy
@@ -603,13 +603,13 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:154:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:363:
+[eva] share/libc/string.h:369:
function strncpy: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:364:
+[eva] share/libc/string.h:370:
function strncpy: postcondition 'initialization' got status valid.
-[eva] share/libc/string.h:367:
+[eva] share/libc/string.h:373:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:367: Warning:
+[eva:alarm] share/libc/string.h:373: Warning:
function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -623,9 +623,9 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c.c:157:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:370:
+[eva] share/libc/string.h:376:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva:alarm] share/libc/string.h:370: Warning:
+[eva:alarm] share/libc/string.h:376: Warning:
function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -712,13 +712,13 @@
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
-[eva] share/libc/string.h:179:
+[eva] share/libc/string.h:185:
function strrchr, behavior found: postcondition 'result_char' got status valid.
-[eva] share/libc/string.h:180:
+[eva] share/libc/string.h:186:
function strrchr, behavior found: postcondition 'result_same_base' got status valid.
-[eva] share/libc/string.h:181:
- function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva] share/libc/string.h:187:
+ function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:193:
function strrchr, behavior default: postcondition 'result_null_or_same_base' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
@@ -728,7 +728,7 @@
[eva] tests/libc/string_c.c:216:
function strrchr: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.c:237: Reusing old results for call to strlen
-[eva] share/libc/string.h:184:
+[eva] share/libc/string.h:190:
function strrchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
@@ -883,9 +883,9 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c.c:261:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] share/libc/string.h:221:
+[eva] share/libc/string.h:227:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva:alarm] share/libc/string.h:219: Warning:
+[eva:alarm] share/libc/string.h:225: Warning:
function strstr: postcondition 'result_null_or_in_haystack' got status unknown.
[eva] Recording results for strstr
[eva] Done for function strstr
@@ -905,7 +905,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c.c:265:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] share/libc/string.h:219:
+[eva] share/libc/string.h:225:
function strstr: postcondition 'result_null_or_in_haystack' got status valid.
[eva] Recording results for strstr
[eva] Done for function strstr
diff --git a/tests/libc/oracle/string_c_generic.res.oracle b/tests/libc/oracle/string_c_generic.res.oracle
index 41ee7f4cbff..d2f546a60ac 100644
--- a/tests/libc/oracle/string_c_generic.res.oracle
+++ b/tests/libc/oracle/string_c_generic.res.oracle
@@ -12,11 +12,11 @@
function strcpy: precondition 'room_string' got status valid.
[eva] tests/libc/string_c_generic.c:56:
function strcpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:351:
+[eva] share/libc/string.h:357:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:351: Warning:
+[eva:alarm] share/libc/string.h:357: Warning:
function strcpy: postcondition 'equal_contents' got status unknown.
-[eva] share/libc/string.h:352:
+[eva] share/libc/string.h:358:
function strcpy: postcondition 'result_ptr' got status valid.
[eva] Recording results for strcpy
[eva] Done for function strcpy
@@ -161,13 +161,13 @@
[eva] tests/libc/string_c_generic.c:73:
function strncpy: precondition 'separation' got status valid.
[eva] share/libc/string.c:220: starting to merge loop iterations
-[eva] share/libc/string.h:363:
+[eva] share/libc/string.h:369:
function strncpy: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:364:
+[eva] share/libc/string.h:370:
function strncpy: postcondition 'initialization' got status valid.
-[eva] share/libc/string.h:367:
+[eva] share/libc/string.h:373:
cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
-[eva:alarm] share/libc/string.h:367: Warning:
+[eva:alarm] share/libc/string.h:373: Warning:
function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -199,9 +199,9 @@
function strncpy: precondition 'room_nstring' got status valid.
[eva] tests/libc/string_c_generic.c:78:
function strncpy: precondition 'separation' got status valid.
-[eva] share/libc/string.h:370:
+[eva] share/libc/string.h:376:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva:alarm] share/libc/string.h:370: Warning:
+[eva:alarm] share/libc/string.h:376: Warning:
function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
[eva] Recording results for strncpy
[eva] Done for function strncpy
@@ -252,9 +252,9 @@
function strlen: postcondition 'acsl_c_equiv' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
-[eva] share/libc/string.h:421:
+[eva] share/libc/string.h:427:
function strncat: postcondition 'result_ptr' got status valid.
-[eva] share/libc/string.h:436:
+[eva] share/libc/string.h:442:
function strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status valid.
[eva] Recording results for strncat
[eva] Done for function strncat
@@ -312,13 +312,13 @@
function strlen: precondition 'valid_string_s' got status valid.
[eva] Recording results for strlen
[eva] Done for function strlen
-[eva] share/libc/string.h:179:
+[eva] share/libc/string.h:185:
function strrchr, behavior found: postcondition 'result_char' got status valid.
-[eva] share/libc/string.h:180:
+[eva] share/libc/string.h:186:
function strrchr, behavior found: postcondition 'result_same_base' got status valid.
-[eva] share/libc/string.h:181:
- function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
[eva] share/libc/string.h:187:
+ function strrchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] share/libc/string.h:193:
function strrchr, behavior default: postcondition 'result_null_or_same_base' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
@@ -328,7 +328,7 @@
function strrchr: precondition 'valid_string_s' got status valid.
[eva] share/libc/string.c:237: Reusing old results for call to strlen
[eva] share/libc/string.c:237: starting to merge loop iterations
-[eva] share/libc/string.h:184:
+[eva] share/libc/string.h:190:
function strrchr, behavior not_found: postcondition 'result_null' got status valid.
[eva] Recording results for strrchr
[eva] Done for function strrchr
diff --git a/tests/libc/oracle/string_c_strstr.res.oracle b/tests/libc/oracle/string_c_strstr.res.oracle
index 6009523b883..ab662fa0802 100644
--- a/tests/libc/oracle/string_c_strstr.res.oracle
+++ b/tests/libc/oracle/string_c_strstr.res.oracle
@@ -10,7 +10,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c_strstr.c:52:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] share/libc/string.h:219:
+[eva] share/libc/string.h:225:
function strstr: postcondition 'result_null_or_in_haystack' got status valid.
[eva] Recording results for strstr
[eva] Done for function strstr
@@ -101,9 +101,9 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_c_strstr.c:64:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] share/libc/string.h:221:
+[eva] share/libc/string.h:227:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
-[eva:alarm] share/libc/string.h:219: Warning:
+[eva:alarm] share/libc/string.h:225: Warning:
function strstr: postcondition 'result_null_or_in_haystack' got status unknown.
[eva] Recording results for strstr
[eva] Done for function strstr
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 89300398e63..5e1e94a0719 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -51,7 +51,7 @@
function strstr: precondition 'valid_string_haystack' got status valid.
[eva] tests/libc/string_h.c:24:
function strstr: precondition 'valid_string_needle' got status valid.
-[eva] share/libc/string.h:221:
+[eva] share/libc/string.h:227:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
[eva] Done for function strstr
[eva:alarm] tests/libc/string_h.c:25: Warning: assertion got status unknown.
@@ -330,6 +330,23 @@
[eva] Done for function strlcpy
[eva] Recording results for test_strlcpy
[eva] Done for function test_strlcpy
+[eva] tests/libc/string_h.c:154: Call to builtin strchr
+[eva] tests/libc/string_h.c:154:
+ function strchr: precondition 'valid_string_s' got status valid.
+[eva] computing for function strchrnul <- main.
+ Called from tests/libc/string_h.c:155.
+[eva] using specification for function strchrnul
+[eva] tests/libc/string_h.c:155:
+ function strchrnul: precondition 'valid_string_s' got status valid.
+[eva] Done for function strchrnul
+[eva] tests/libc/string_h.c:157: Call to builtin strchr
+[eva] tests/libc/string_h.c:157:
+ function strchr: precondition 'valid_string_s' got status valid.
+[eva] computing for function strchrnul <- main.
+ Called from tests/libc/string_h.c:158.
+[eva] tests/libc/string_h.c:158:
+ function strchrnul: precondition 'valid_string_s' got status valid.
+[eva] Done for function strchrnul
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -395,4 +412,10 @@
a ∈ [--..--]
b ∈ [--..--]
strsig ∈ {{ &__fc_strsignal[0] }}
+ c ∈ {{ "haystack" }}
+ d ∈ {97; 110}
+ chr1 ∈ {{ "haystack" + {2; 7} }}
+ nul1 ∈ {{ "haystack" + [0..8] }}
+ chr2 ∈ {{ NULL ; "haystack" + {1} }}
+ nul2 ∈ {{ "haystack" + [0..8] }}
__retres ∈ {0}
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index 0b264a61566..cf18b8e5463 100644
--- a/tests/libc/string_h.c
+++ b/tests/libc/string_h.c
@@ -149,5 +149,12 @@ int main(int argc, char **argv)
//@ assert valid_read_string(strsig);
test_strncpy();
test_strlcpy();
+ char *c = "haystack";
+ char d = nondet ? 'y' : 'k';
+ char *chr1 = strchr(c, d);
+ char *nul1 = strchrnul(c, d);
+ d = nondet ? 'a' : 'n';
+ char *chr2 = strchr(c, d);
+ char *nul2 = strchrnul(c, d);
return 0;
}
--
GitLab