From acfb70a1491c327f50cdd9d7269107476cac4eac Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 6 Mar 2024 16:06:50 +0100
Subject: [PATCH] sync with frama-c/frama-c!4310
---
tests/basic/oracle/placement_new.err.oracle | 1 +
tests/basic/oracle/placement_new.res.oracle | 75 +++++++++++++++++++
tests/basic/oracle/placement_newb.err.oracle | 1 +
tests/basic/oracle/placement_newb.res.oracle | 75 +++++++++++++++++++
.../stl_shared_ptr_mistake10.err.oracle | 1 +
.../stl_shared_ptr_mistake10.res.oracle | 75 +++++++++++++++++++
.../oracle/stl_shared_ptr_mistake5.err.oracle | 1 +
.../oracle/stl_shared_ptr_mistake5.res.oracle | 75 +++++++++++++++++++
.../oracle/stl_shared_ptr_mistake6.err.oracle | 1 +
.../oracle/stl_shared_ptr_mistake6.res.oracle | 75 +++++++++++++++++++
10 files changed, 380 insertions(+)
create mode 100644 tests/basic/oracle/placement_new.err.oracle
create mode 100644 tests/basic/oracle/placement_newb.err.oracle
create mode 100644 tests/stl/oracle/stl_shared_ptr_mistake10.err.oracle
create mode 100644 tests/stl/oracle/stl_shared_ptr_mistake5.err.oracle
create mode 100644 tests/stl/oracle/stl_shared_ptr_mistake6.err.oracle
diff --git a/tests/basic/oracle/placement_new.err.oracle b/tests/basic/oracle/placement_new.err.oracle
new file mode 100644
index 00000000..0a7cae45
--- /dev/null
+++ b/tests/basic/oracle/placement_new.err.oracle
@@ -0,0 +1 @@
+FRAMAC_SHARE/libc/stdlib.h:804:19: the body of the post-condition is not a predicate
diff --git a/tests/basic/oracle/placement_new.res.oracle b/tests/basic/oracle/placement_new.res.oracle
index 7e1a1b55..f1b04d62 100644
--- a/tests/basic/oracle/placement_new.res.oracle
+++ b/tests/basic/oracle/placement_new.res.oracle
@@ -412,6 +412,9 @@ predicate valid_read_nwstring{L}(wchar_t *s, ℤ n) =
predicate valid_wstring_or_null{L}(wchar_t *s) =
s ≡ \null ∨ valid_wstring(s);
*/
+int __fc_errno;
+char *program_invocation_name;
+char *program_invocation_short_name;
/*@ requires valid_nptr: \valid_read(nptr);
assigns \result;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -1157,6 +1160,78 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires
+ valid_file_name_or_null:
+ file_name ≡ \null ∨ valid_read_string(file_name);
+ requires
+ resolved_name_null_or_allocated:
+ resolved_name ≡ \null ∨ \valid(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)),
+ *(resolved_name + (0 .. 4096 - 1)), __fc_errno;
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns *(\result + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno
+ \from (indirect: file_name), (indirect: *(file_name + (0 ..))),
+ (indirect: resolved_name), (indirect: __fc_heap_status);
+
+ behavior null_file_name:
+ assumes null_file_name: file_name ≡ \null;
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 22;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: file_name);
+ assigns __fc_errno \from (indirect: file_name);
+
+ behavior allocate_resolved_name:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes can_allocate: is_allocable(4096);
+ ensures allocation: \fresh{Old, Here}(\result,4096);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from (indirect: __fc_heap_status);
+
+ behavior not_enough_memory:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes cannot_allocate: ¬is_allocable(4096);
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 12;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures
+ valid_string_resolved_name:
+ valid_string(\old(resolved_name)) ∧
+ strlen(\old(resolved_name)) < 4096;
+ ensures resolved_result: \result ≡ \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from resolved_name;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+
+ behavior filesystem_error:
+ assumes valid_file_name: valid_read_string(file_name);
+ ensures null_result: \result ≡ \null;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno \from (indirect: *(file_name + (0 ..)));
+ */
+char *realpath(char const * restrict file_name, char * restrict resolved_name);
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid_read(this); */
diff --git a/tests/basic/oracle/placement_newb.err.oracle b/tests/basic/oracle/placement_newb.err.oracle
new file mode 100644
index 00000000..0a7cae45
--- /dev/null
+++ b/tests/basic/oracle/placement_newb.err.oracle
@@ -0,0 +1 @@
+FRAMAC_SHARE/libc/stdlib.h:804:19: the body of the post-condition is not a predicate
diff --git a/tests/basic/oracle/placement_newb.res.oracle b/tests/basic/oracle/placement_newb.res.oracle
index 9a45df60..39905324 100644
--- a/tests/basic/oracle/placement_newb.res.oracle
+++ b/tests/basic/oracle/placement_newb.res.oracle
@@ -381,6 +381,9 @@ predicate valid_read_nwstring{L}(wchar_t *s, ℤ n) =
predicate valid_wstring_or_null{L}(wchar_t *s) =
s ≡ \null ∨ valid_wstring(s);
*/
+int __fc_errno;
+char *program_invocation_name;
+char *program_invocation_short_name;
/*@ requires valid_nptr: \valid_read(nptr);
assigns \result;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -1126,4 +1129,76 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires
+ valid_file_name_or_null:
+ file_name ≡ \null ∨ valid_read_string(file_name);
+ requires
+ resolved_name_null_or_allocated:
+ resolved_name ≡ \null ∨ \valid(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)),
+ *(resolved_name + (0 .. 4096 - 1)), __fc_errno;
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns *(\result + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno
+ \from (indirect: file_name), (indirect: *(file_name + (0 ..))),
+ (indirect: resolved_name), (indirect: __fc_heap_status);
+
+ behavior null_file_name:
+ assumes null_file_name: file_name ≡ \null;
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 22;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: file_name);
+ assigns __fc_errno \from (indirect: file_name);
+
+ behavior allocate_resolved_name:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes can_allocate: is_allocable(4096);
+ ensures allocation: \fresh{Old, Here}(\result,4096);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from (indirect: __fc_heap_status);
+
+ behavior not_enough_memory:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes cannot_allocate: ¬is_allocable(4096);
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 12;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures
+ valid_string_resolved_name:
+ valid_string(\old(resolved_name)) ∧
+ strlen(\old(resolved_name)) < 4096;
+ ensures resolved_result: \result ≡ \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from resolved_name;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+
+ behavior filesystem_error:
+ assumes valid_file_name: valid_read_string(file_name);
+ ensures null_result: \result ≡ \null;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno \from (indirect: *(file_name + (0 ..)));
+ */
+char *realpath(char const * restrict file_name, char * restrict resolved_name);
+
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.err.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.err.oracle
new file mode 100644
index 00000000..0a7cae45
--- /dev/null
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.err.oracle
@@ -0,0 +1 @@
+FRAMAC_SHARE/libc/stdlib.h:804:19: the body of the post-condition is not a predicate
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
index 769ed4ab..a98a8a7e 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake10.res.oracle
@@ -2508,6 +2508,9 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
+int __fc_errno;
+char *program_invocation_name;
+char *program_invocation_short_name;
/*@ requires valid_nptr: \valid_read(nptr);
assigns \result;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -3253,6 +3256,78 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires
+ valid_file_name_or_null:
+ file_name ≡ \null ∨ valid_read_string(file_name);
+ requires
+ resolved_name_null_or_allocated:
+ resolved_name ≡ \null ∨ \valid(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)),
+ *(resolved_name + (0 .. 4096 - 1)), __fc_errno;
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns *(\result + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno
+ \from (indirect: file_name), (indirect: *(file_name + (0 ..))),
+ (indirect: resolved_name), (indirect: __fc_heap_status);
+
+ behavior null_file_name:
+ assumes null_file_name: file_name ≡ \null;
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 22;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: file_name);
+ assigns __fc_errno \from (indirect: file_name);
+
+ behavior allocate_resolved_name:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes can_allocate: is_allocable(4096);
+ ensures allocation: \fresh{Old, Here}(\result,4096);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from (indirect: __fc_heap_status);
+
+ behavior not_enough_memory:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes cannot_allocate: ¬is_allocable(4096);
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 12;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures
+ valid_string_resolved_name:
+ valid_string(\old(resolved_name)) ∧
+ strlen(\old(resolved_name)) < 4096;
+ ensures resolved_result: \result ≡ \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from resolved_name;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+
+ behavior filesystem_error:
+ assumes valid_file_name: valid_read_string(file_name);
+ ensures null_result: \result ≡ \null;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno \from (indirect: *(file_name + (0 ..)));
+ */
+char *realpath(char const * restrict file_name, char * restrict resolved_name);
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.err.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.err.oracle
new file mode 100644
index 00000000..0a7cae45
--- /dev/null
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.err.oracle
@@ -0,0 +1 @@
+FRAMAC_SHARE/libc/stdlib.h:804:19: the body of the post-condition is not a predicate
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
index 7787be6b..540339c4 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake5.res.oracle
@@ -2287,6 +2287,9 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
+int __fc_errno;
+char *program_invocation_name;
+char *program_invocation_short_name;
/*@ requires valid_nptr: \valid_read(nptr);
assigns \result;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -3032,6 +3035,78 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires
+ valid_file_name_or_null:
+ file_name ≡ \null ∨ valid_read_string(file_name);
+ requires
+ resolved_name_null_or_allocated:
+ resolved_name ≡ \null ∨ \valid(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)),
+ *(resolved_name + (0 .. 4096 - 1)), __fc_errno;
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns *(\result + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno
+ \from (indirect: file_name), (indirect: *(file_name + (0 ..))),
+ (indirect: resolved_name), (indirect: __fc_heap_status);
+
+ behavior null_file_name:
+ assumes null_file_name: file_name ≡ \null;
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 22;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: file_name);
+ assigns __fc_errno \from (indirect: file_name);
+
+ behavior allocate_resolved_name:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes can_allocate: is_allocable(4096);
+ ensures allocation: \fresh{Old, Here}(\result,4096);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from (indirect: __fc_heap_status);
+
+ behavior not_enough_memory:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes cannot_allocate: ¬is_allocable(4096);
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 12;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures
+ valid_string_resolved_name:
+ valid_string(\old(resolved_name)) ∧
+ strlen(\old(resolved_name)) < 4096;
+ ensures resolved_result: \result ≡ \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from resolved_name;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+
+ behavior filesystem_error:
+ assumes valid_file_name: valid_read_string(file_name);
+ ensures null_result: \result ≡ \null;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno \from (indirect: *(file_name + (0 ..)));
+ */
+char *realpath(char const * restrict file_name, char * restrict resolved_name);
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.err.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.err.oracle
new file mode 100644
index 00000000..0a7cae45
--- /dev/null
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.err.oracle
@@ -0,0 +1 @@
+FRAMAC_SHARE/libc/stdlib.h:804:19: the body of the post-condition is not a predicate
diff --git a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
index e86ef322..474773e2 100644
--- a/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
+++ b/tests/stl/oracle/stl_shared_ptr_mistake6.res.oracle
@@ -2293,6 +2293,9 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
+int __fc_errno;
+char *program_invocation_name;
+char *program_invocation_short_name;
/*@ requires valid_nptr: \valid_read(nptr);
assigns \result;
assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..)));
@@ -3038,6 +3041,78 @@ int mkstemp(char *templat);
*/
int mkstemps(char *templat, int suffixlen);
+/*@ requires
+ valid_file_name_or_null:
+ file_name ≡ \null ∨ valid_read_string(file_name);
+ requires
+ resolved_name_null_or_allocated:
+ resolved_name ≡ \null ∨ \valid(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status, *(\result + (0 .. 4096 - 1)),
+ *(resolved_name + (0 .. 4096 - 1)), __fc_errno;
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns *(\result + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: __fc_heap_status), (indirect: resolved_name),
+ (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno
+ \from (indirect: file_name), (indirect: *(file_name + (0 ..))),
+ (indirect: resolved_name), (indirect: __fc_heap_status);
+
+ behavior null_file_name:
+ assumes null_file_name: file_name ≡ \null;
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 22;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: file_name);
+ assigns __fc_errno \from (indirect: file_name);
+
+ behavior allocate_resolved_name:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes can_allocate: is_allocable(4096);
+ ensures allocation: \fresh{Old, Here}(\result,4096);
+ assigns __fc_heap_status, \result;
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from (indirect: __fc_heap_status);
+
+ behavior not_enough_memory:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes resolved_name_null: resolved_name ≡ \null;
+ assumes cannot_allocate: ¬is_allocable(4096);
+ ensures null_result: \result ≡ \null;
+ ensures errno_set: __fc_errno ≡ 12;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes valid_file_name: valid_read_string(file_name);
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures
+ valid_string_resolved_name:
+ valid_string(\old(resolved_name)) ∧
+ strlen(\old(resolved_name)) < 4096;
+ ensures resolved_result: \result ≡ \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from resolved_name;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+
+ behavior filesystem_error:
+ assumes valid_file_name: valid_read_string(file_name);
+ ensures null_result: \result ≡ \null;
+ assigns \result, __fc_errno;
+ assigns \result \from (indirect: *(file_name + (0 ..)));
+ assigns __fc_errno \from (indirect: *(file_name + (0 ..)));
+ */
+char *realpath(char const * restrict file_name, char * restrict resolved_name);
+
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid(this); */
--
GitLab