From bff33984024e642dba9abe358614f36f026b372a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 2 Aug 2019 15:26:39 +0200
Subject: [PATCH] [Libc] add requires to strdup
---
share/libc/string.h | 3 ++-
tests/builtins/oracle/memcpy.res.oracle | 26 ++++++++++++-------------
tests/libc/oracle/fc_libc.1.res.oracle | 3 ++-
tests/libc/oracle/string_h.res.oracle | 2 ++
4 files changed, 19 insertions(+), 15 deletions(-)
diff --git a/share/libc/string.h b/share/libc/string.h
index 566b296162c..6f265a44d01 100644
--- a/share/libc/string.h
+++ b/share/libc/string.h
@@ -457,7 +457,8 @@ extern size_t strxfrm (char *restrict dest,
// Allocate strings
-/*@ allocates \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ @ allocates \result;
@ assigns \result \from indirect:s[0..strlen(s)], indirect:__fc_heap_status;
@ behavior allocation:
@ assumes can_allocate: is_allocable(strlen(s));
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index fffd2495d1d..630d2219ba4 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -1691,19 +1691,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 464)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 465)
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 464)
- Unverifiable but considered Valid.
[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 465)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 461)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 466)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 462)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 471)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 472)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1711,7 +1711,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 460)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 461)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -1726,19 +1726,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 482)
+[ Extern ] Assigns for 'allocation' (file share/libc/string.h, line 483)
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 482)
- Unverifiable but considered Valid.
[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 483)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 478)
+[ Extern ] Froms for 'allocation' (file share/libc/string.h, line 484)
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/string.h, line 479)
Unverifiable but considered Valid.
-[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 492)
+[ Extern ] Froms for 'no_allocation' (file share/libc/string.h, line 493)
Unverifiable but considered Valid.
[ Valid ] Behavior 'allocation'
by Frama-C kernel.
@@ -1746,7 +1746,7 @@
by Frama-C kernel.
[ Valid ] Behavior 'no_allocation'
by Frama-C kernel.
-[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 477)
+[ Extern ] Frees/Allocates nothing/(file share/libc/string.h, line 478)
Unverifiable but considered Valid.
[ Extern ] Frees/Allocates for 'no_allocation' nothing/nothing
Unverifiable but considered Valid.
@@ -1763,7 +1763,7 @@
Unverifiable but considered Valid.
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/string.h, line 508)
+[ Extern ] Froms (file share/libc/string.h, line 509)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 97573852495..062a50bfd13 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -5557,7 +5557,8 @@ char *strerror(int errnum)
return __retres;
}
-/*@ assigns \result;
+/*@ requires valid_string_s: valid_read_string(s);
+ assigns \result;
assigns \result
\from (indirect: *(s + (0 .. strlen{Old}(s)))),
(indirect: __fc_heap_status);
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index 66a8414bd90..75780c1ba4a 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -247,6 +247,8 @@
The specification of function 'strdup' is currently not supported by Eva.
Consider adding ./share/libc/string.c to the analyzed source files.
[eva] tests/libc/string_h.c:119: Warning: ignoring unsupported \allocates clause
+[eva] tests/libc/string_h.c:119:
+ function strdup: precondition 'valid_string_s' got status valid.
[eva] Done for function strdup
[eva] computing for function strndup <- main.
Called from tests/libc/string_h.c:120.
--
GitLab