diff --git a/tests/basic/oracle/placement_new.err.oracle b/tests/basic/oracle/placement_new.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0a7cae45d12ab222537daff8e31eb5653cce4750
--- /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 7e1a1b5555b633a20a637213b53ad36e2e995df5..f1b04d623fa5c7f00e8f7210ae4d1eca0840fd43 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 0000000000000000000000000000000000000000..0a7cae45d12ab222537daff8e31eb5653cce4750
--- /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 9a45df60bf414465446e3b3f8936b0cc0f519fdb..39905324945b67e7a479d3a95f3402e34b818e47 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 0000000000000000000000000000000000000000..0a7cae45d12ab222537daff8e31eb5653cce4750
--- /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 769ed4ab3a1da2b8bc8a5cac2e56d358ff028386..a98a8a7ee933cf7004e23ca2d8ffffd77c740ac6 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 0000000000000000000000000000000000000000..0a7cae45d12ab222537daff8e31eb5653cce4750
--- /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 7787be6ba39f85775f88784540c6d6a84729b522..540339c4f0a55df8fe56f23c5f13015f186b4f66 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 0000000000000000000000000000000000000000..0a7cae45d12ab222537daff8e31eb5653cce4750
--- /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 e86ef322294f9b0b67701a27aec44f440580f4f2..474773e28a369a709cfe378de0e8b785feba86f0 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); */