From 8be52d82bfcaac30e309aeabba978b483b91f7ff Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 12 Sep 2023 16:29:17 +0200
Subject: [PATCH] [libc] add spec to realpath
---
share/libc/stdlib.h | 31 +-
.../tests/memory/oracle/gen_hidden_malloc.c | 200 +++++-
.../memory/oracle/hidden_malloc.res.oracle | 38 +-
.../tests/temporal/oracle/gen_t_fun_lib.c | 214 +++++-
.../temporal/oracle/t_fun_lib.res.oracle | 52 +-
.../tests/sarif/oracle/std_string.sarif | 670 ++++++++++++++++++
tests/libc/oracle/argz_c.res.oracle | 1 +
tests/libc/oracle/coverage.res.oracle | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 41 ++
tests/libc/oracle/netdb_c.res.oracle | 1 +
10 files changed, 1223 insertions(+), 27 deletions(-)
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index dc22e5eeb14..8e21ad8b05f 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -748,9 +748,38 @@ extern int mkstemp(char *templat);
*/
extern int mkstemps(char *templat, int suffixlen);
-// This function may allocate memory for the result, which is not supported by
+// 'realpath' 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.
+/*@
+ requires valid_file_name: valid_read_string(file_name);
+ requires resolved_name_null_or_allocated:
+ resolved_name == \null || \valid(resolved_name+(0 .. PATH_MAX-1));
+ assigns __fc_heap_status \from indirect:resolved_name, __fc_heap_status;
+ assigns \result, resolved_name[0 .. PATH_MAX-1] \from
+ indirect:__fc_heap_status, indirect:resolved_name, indirect:file_name[0..];
+ behavior allocate_resolved_name:
+ assumes resolved_name_null: resolved_name == \null;
+ assumes can_allocate: is_allocable(PATH_MAX);
+ assigns __fc_heap_status \from __fc_heap_status;
+ assigns \result \from indirect:__fc_heap_status;
+ ensures allocation: \fresh(\result,PATH_MAX);
+ behavior not_enough_memory:
+ assumes resolved_name_null: resolved_name == \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+ ensures null_result: \result == \null;
+ behavior resolved_name_buffer:
+ assumes allocated_resolved_name_or_fail:
+ \valid(resolved_name+(0 .. PATH_MAX-1));
+ assigns \result \from \nothing;
+ assigns resolved_name[0 .. PATH_MAX-1] \from indirect:file_name[0..];
+ ensures valid_string_resolved_name: valid_string(resolved_name);
+ // missing: assigns \result,
+ // resolved_name[0 .. PATH_MAX-1] \from 'filesystem';
+ ensures resolved_result: \result == resolved_name;
+ allocates \nothing;
+ */
extern char *realpath(const char *restrict file_name,
char *restrict resolved_name);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
index f264c45b599..e38b61a985d 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
@@ -10,6 +10,204 @@
char *__gen_e_acsl_literal_string;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+/*@ requires valid_file_name: 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, *(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns \result
+ \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 ..)));
+
+ behavior allocate_resolved_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 resolved_name_null: resolved_name == \null;
+ ensures null_result: \result == \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures valid_string_resolved_name: valid_string(\old(resolved_name));
+ ensures resolved_result: \result == \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from \nothing;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+ */
+char *__gen_e_acsl_realpath(char const * restrict file_name,
+ char * restrict resolved_name);
+
+/*@ requires valid_file_name: 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, *(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns \result
+ \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 ..)));
+
+ behavior allocate_resolved_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 resolved_name_null: resolved_name == \null;
+ ensures null_result: \result == \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures valid_string_resolved_name: valid_string(\old(resolved_name));
+ ensures resolved_result: \result == \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from \nothing;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+ */
+char *__gen_e_acsl_realpath(char const * restrict file_name,
+ char * restrict resolved_name)
+{
+ __e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at;
+ char *__retres;
+ {
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_2;
+ __e_acsl_store_block((void *)(& resolved_name),8UL);
+ __gen_e_acsl_at = resolved_name;
+ __gen_e_acsl_contract = __e_acsl_contract_init(3UL);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
+ "resolved_name",(void *)resolved_name);
+ if (resolved_name == (char *)0) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_size = 1 * (((4096 - 1) - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(resolved_name + 1 * 0),
+ (size_t)__gen_e_acsl_if,
+ (void *)resolved_name,
+ (void *)(& resolved_name));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
+ "resolved_name",(void *)resolved_name);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "sizeof(char)",0,1);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "sizeof(char)",0,1);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"size",0,
+ __gen_e_acsl_size);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"size",0,
+ __gen_e_acsl_size);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "\\valid(resolved_name + (0 .. 4096 - 1))",
+ 0,__gen_e_acsl_valid);
+ __gen_e_acsl_or = __gen_e_acsl_valid;
+ }
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Precondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "resolved_name == \\null || \\valid(resolved_name + (0 .. 4096 - 1))";
+ __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h";
+ __gen_e_acsl_assert_data_2.fct = "realpath";
+ __gen_e_acsl_assert_data_2.line = 757;
+ __gen_e_acsl_assert_data_2.name = "resolved_name_null_or_allocated";
+ __e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,1UL,
+ resolved_name == (char *)0);
+ __gen_e_acsl_size_2 = 1 * (((4096 - 1) - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(resolved_name + 1 * 0),
+ (size_t)__gen_e_acsl_if_2,
+ (void *)resolved_name,
+ (void *)(& resolved_name));
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,2UL,
+ __gen_e_acsl_valid_2);
+ }
+ __retres = realpath(file_name,resolved_name);
+ {
+ int __gen_e_acsl_assumes_value;
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,1UL);
+ if (__gen_e_acsl_assumes_value) {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"\\result",
+ (void *)__retres);
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "Postcondition";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\result == \\null";
+ __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h";
+ __gen_e_acsl_assert_data_4.fct = "realpath";
+ __gen_e_acsl_assert_data_4.line = 771;
+ __gen_e_acsl_assert_data_4.name = "not_enough_memory/null_result";
+ __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
+ }
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,2UL);
+ if (__gen_e_acsl_assumes_value) {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result",
+ (void *)__retres);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
+ "\\old(resolved_name)",
+ (void *)__gen_e_acsl_at);
+ __gen_e_acsl_assert_data_6.blocking = 1;
+ __gen_e_acsl_assert_data_6.kind = "Postcondition";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(resolved_name)";
+ __gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdlib.h";
+ __gen_e_acsl_assert_data_6.fct = "realpath";
+ __gen_e_acsl_assert_data_6.line = 780;
+ __gen_e_acsl_assert_data_6.name = "resolved_name_buffer/resolved_result";
+ __e_acsl_assert(__retres == __gen_e_acsl_at,
+ & __gen_e_acsl_assert_data_6);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
+ }
+ __e_acsl_contract_clean(__gen_e_acsl_contract);
+ __e_acsl_delete_block((void *)(& resolved_name));
+ return __retres;
+ }
+}
+
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -28,7 +226,7 @@ int main(int argc, char const **argv)
int __retres;
__e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
__e_acsl_globals_init();
- char *cwd = realpath(__gen_e_acsl_literal_string,(char *)0);
+ char *cwd = __gen_e_acsl_realpath(__gen_e_acsl_literal_string,(char *)0);
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index aa890a27d2e..526a044a539 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
@@ -1,5 +1,37 @@
[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `realpath':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning:
+ no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:763: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+ Some assumes clauses could not be translated.
+ Ignoring complete and disjoint behaviors annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:771: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning:
+ no assigns clause generated for function valid_string because pointers as arguments is not yet supported
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] hidden_malloc.c:11: Warning:
- Neither code nor specification for function realpath,
- generating default assigns. See -generated-spec-* options for more info
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
index 354f67ce51f..acadb73bba2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
@@ -10,6 +10,212 @@
char *__gen_e_acsl_literal_string;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+/*@ requires valid_file_name: 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, *(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns \result
+ \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 ..)));
+
+ behavior allocate_resolved_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 resolved_name_null: resolved_name == \null;
+ ensures null_result: \result == \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures valid_string_resolved_name: valid_string(\old(resolved_name));
+ ensures resolved_result: \result == \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from \nothing;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+ */
+char *__gen_e_acsl_realpath(char const * restrict file_name,
+ char * restrict resolved_name);
+
+/*@ requires valid_file_name: 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, *(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns \result
+ \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 ..)));
+
+ behavior allocate_resolved_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 resolved_name_null: resolved_name == \null;
+ ensures null_result: \result == \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures valid_string_resolved_name: valid_string(\old(resolved_name));
+ ensures resolved_result: \result == \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from \nothing;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+ */
+char *__gen_e_acsl_realpath(char const * restrict file_name,
+ char * restrict resolved_name)
+{
+ __e_acsl_contract_t *__gen_e_acsl_contract;
+ char *__gen_e_acsl_at;
+ char *__retres;
+ __e_acsl_store_block((void *)(& __retres),8UL);
+ {
+ int __gen_e_acsl_or;
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_valid_2;
+ __e_acsl_store_block((void *)(& resolved_name),8UL);
+ __e_acsl_temporal_pull_parameter((void *)(& resolved_name),1U,8UL);
+ __gen_e_acsl_at = resolved_name;
+ __gen_e_acsl_contract = __e_acsl_contract_init(3UL);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
+ "resolved_name",(void *)resolved_name);
+ if (resolved_name == (char *)0) __gen_e_acsl_or = 1;
+ else {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_size = 1 * (((4096 - 1) - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)(resolved_name + 1 * 0),
+ (size_t)__gen_e_acsl_if,
+ (void *)resolved_name,
+ (void *)(& resolved_name));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
+ "resolved_name",(void *)resolved_name);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "sizeof(char)",0,1);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "sizeof(char)",0,1);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"size",0,
+ __gen_e_acsl_size);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"size",0,
+ __gen_e_acsl_size);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+ "\\valid(resolved_name + (0 .. 4096 - 1))",
+ 0,__gen_e_acsl_valid);
+ __gen_e_acsl_or = __gen_e_acsl_valid;
+ }
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Precondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "resolved_name == \\null || \\valid(resolved_name + (0 .. 4096 - 1))";
+ __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdlib.h";
+ __gen_e_acsl_assert_data_2.fct = "realpath";
+ __gen_e_acsl_assert_data_2.line = 757;
+ __gen_e_acsl_assert_data_2.name = "resolved_name_null_or_allocated";
+ __e_acsl_assert(__gen_e_acsl_or,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,1UL,
+ resolved_name == (char *)0);
+ __gen_e_acsl_size_2 = 1 * (((4096 - 1) - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(resolved_name + 1 * 0),
+ (size_t)__gen_e_acsl_if_2,
+ (void *)resolved_name,
+ (void *)(& resolved_name));
+ __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,2UL,
+ __gen_e_acsl_valid_2);
+ __e_acsl_temporal_reset_parameters();
+ __e_acsl_temporal_reset_return();
+ __e_acsl_temporal_save_nreferent_parameter((void *)(& resolved_name),1U);
+ }
+ __retres = realpath(file_name,resolved_name);
+ __e_acsl_temporal_store_nblock((void *)(& __retres),(void *)*(& __retres));
+ {
+ int __gen_e_acsl_assumes_value;
+ __e_acsl_temporal_save_return((void *)(& __retres));
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,1UL);
+ if (__gen_e_acsl_assumes_value) {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,"\\result",
+ (void *)__retres);
+ __gen_e_acsl_assert_data_4.blocking = 1;
+ __gen_e_acsl_assert_data_4.kind = "Postcondition";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\result == \\null";
+ __gen_e_acsl_assert_data_4.file = "FRAMAC_SHARE/libc/stdlib.h";
+ __gen_e_acsl_assert_data_4.fct = "realpath";
+ __gen_e_acsl_assert_data_4.line = 771;
+ __gen_e_acsl_assert_data_4.name = "not_enough_memory/null_result";
+ __e_acsl_assert(__retres == (char *)0,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
+ }
+ __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes
+ ((__e_acsl_contract_t const *)__gen_e_acsl_contract,2UL);
+ if (__gen_e_acsl_assumes_value) {
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,"\\result",
+ (void *)__retres);
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_6,
+ "\\old(resolved_name)",
+ (void *)__gen_e_acsl_at);
+ __gen_e_acsl_assert_data_6.blocking = 1;
+ __gen_e_acsl_assert_data_6.kind = "Postcondition";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\result == \\old(resolved_name)";
+ __gen_e_acsl_assert_data_6.file = "FRAMAC_SHARE/libc/stdlib.h";
+ __gen_e_acsl_assert_data_6.fct = "realpath";
+ __gen_e_acsl_assert_data_6.line = 780;
+ __gen_e_acsl_assert_data_6.name = "resolved_name_buffer/resolved_result";
+ __e_acsl_assert(__retres == __gen_e_acsl_at,
+ & __gen_e_acsl_assert_data_6);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
+ }
+ __e_acsl_contract_clean(__gen_e_acsl_contract);
+ __e_acsl_delete_block((void *)(& resolved_name));
+ __e_acsl_delete_block((void *)(& __retres));
+ return __retres;
+ }
+}
+
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -111,16 +317,16 @@ int main(void)
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& q),1U);
- char *path = realpath((char const *)c,q);
- __e_acsl_temporal_store_nblock((void *)(& path),(void *)*(& path));
+ char *path = __gen_e_acsl_realpath((char const *)c,q);
+ __e_acsl_temporal_pull_return((void *)(& path));
__e_acsl_store_block((void *)(& path),8UL);
__e_acsl_full_init((void *)(& path));
__e_acsl_full_init((void *)(& path));
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& q),1U);
- path = realpath((char const *)c,q);
- __e_acsl_temporal_store_nblock((void *)(& path),(void *)*(& path));
+ path = __gen_e_acsl_realpath((char const *)c,q);
+ __e_acsl_temporal_pull_return((void *)(& path));
{
int __gen_e_acsl_initialized_3;
int __gen_e_acsl_and_4;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
index f6c71b561f1..fec515bf845 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
@@ -1,4 +1,39 @@
[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `realpath':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:755: Warning:
+ no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:763: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+ Some assumes clauses could not be translated.
+ Ignoring complete and disjoint behaviors annotations.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:766: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:771: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:777: Warning:
+ no assigns clause generated for function valid_string because pointers as arguments is not yet supported
+[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] t_fun_lib.c:15: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
@@ -27,20 +62,3 @@
[eva:alarm] t_fun_lib.c:15: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[kernel:annot:missing-spec] t_fun_lib.c:19: Warning:
- Neither code nor specification for function realpath,
- generating default assigns. See -generated-spec-* options for more info
-[eva:alarm] t_fun_lib.c:22: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] t_fun_lib.c:22: Warning:
- function __e_acsl_assert_register_int: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] t_fun_lib.c:22: Warning:
- function __e_acsl_assert_register_ptr: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] t_fun_lib.c:22: Warning:
- function __e_acsl_assert_register_ulong: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] t_fun_lib.c:22: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status invalid.
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 d5f67f7b13c..c09cffbaa62 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -14182,6 +14182,676 @@
}
]
},
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "behavior allocate_resolved_name in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "behavior default! in function realpath." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "behavior not_enough_memory in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "behavior resolved_name_buffer in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_file_name." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 755,
+ "startColumn": 28,
+ "endLine": 755,
+ "endColumn": 56,
+ "byteLength": 28
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "resolved_name_null_or_allocated." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 757,
+ "startColumn": 4,
+ "endLine": 757,
+ "endColumn": 66,
+ "byteLength": 62
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "resolved_name_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 762,
+ "startColumn": 32,
+ "endLine": 762,
+ "endColumn": 54,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "can_allocate." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 763,
+ "startColumn": 26,
+ "endLine": 763,
+ "endColumn": 44,
+ "byteLength": 18
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "resolved_name_null." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 768,
+ "startColumn": 32,
+ "endLine": 768,
+ "endColumn": 54,
+ "byteLength": 22
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocated_resolved_name_or_fail." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 774,
+ "startColumn": 6,
+ "endLine": 774,
+ "endColumn": 42,
+ "byteLength": 36
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "allocation." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 766,
+ "startColumn": 24,
+ "endLine": 766,
+ "endColumn": 44,
+ "byteLength": 20
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "null_result." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 771,
+ "startColumn": 25,
+ "endLine": 771,
+ "endColumn": 41,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "valid_string_resolved_name." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 777,
+ "startColumn": 40,
+ "endLine": 777,
+ "endColumn": 67,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "resolved_result." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 780,
+ "startColumn": 29,
+ "endLine": 780,
+ "endColumn": 53,
+ "byteLength": 24
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realpath." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 764,
+ "startColumn": 12,
+ "endLine": 764,
+ "endColumn": 28,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realpath." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 758,
+ "startColumn": 10,
+ "endLine": 758,
+ "endColumn": 26,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realpath." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": { "text": "assigns clause in function realpath." },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 775,
+ "startColumn": 12,
+ "endLine": 775,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term __fc_heap_status in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 764,
+ "startColumn": 12,
+ "endLine": 764,
+ "endColumn": 28,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 765,
+ "startColumn": 12,
+ "endLine": 765,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term __fc_heap_status in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 758,
+ "startColumn": 10,
+ "endLine": 758,
+ "endColumn": 26,
+ "byteLength": 16
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 759,
+ "startColumn": 10,
+ "endLine": 759,
+ "endColumn": 17,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *(resolved_name + (0 .. 4096 - 1)) in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 759,
+ "startColumn": 19,
+ "endLine": 759,
+ "endColumn": 46,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 769,
+ "startColumn": 12,
+ "endLine": 769,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term \\result in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 775,
+ "startColumn": 12,
+ "endLine": 775,
+ "endColumn": 19,
+ "byteLength": 7
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "from clause of term *(resolved_name + (0 .. 4096 - 1)) in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 776,
+ "startColumn": 12,
+ "endLine": 776,
+ "endColumn": 39,
+ "byteLength": 27
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
+ {
+ "ruleId": "user-spec",
+ "kind": "pass",
+ "level": "none",
+ "message": {
+ "text": "allocates/frees clause in function realpath."
+ },
+ "locations": [
+ {
+ "physicalLocation": {
+ "artifactLocation": {
+ "uri": "libc/stdlib.h",
+ "uriBaseId": "FRAMAC_SHARE"
+ },
+ "region": {
+ "startLine": 783,
+ "startColumn": 12,
+ "endLine": 783,
+ "endColumn": 13,
+ "byteLength": 1
+ }
+ }
+ }
+ ]
+ },
{
"ruleId": "user-spec",
"kind": "pass",
diff --git a/tests/libc/oracle/argz_c.res.oracle b/tests/libc/oracle/argz_c.res.oracle
index f1c6521d1fb..38884838a6f 100644
--- a/tests/libc/oracle/argz_c.res.oracle
+++ b/tests/libc/oracle/argz_c.res.oracle
@@ -21,6 +21,7 @@
\return(reallocarray) == 0 (auto)
\return(getenv) == 0 (auto)
\return(bsearch) == 0 (auto)
+ \return(realpath) == 0 (auto)
\return(memchr) == 0 (auto)
\return(memrchr) == 0 (auto)
\return(memcpy) == 0 (auto)
diff --git a/tests/libc/oracle/coverage.res.oracle b/tests/libc/oracle/coverage.res.oracle
index fc23e8f6baa..b53e4177747 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 98)
+ Syntactically reachable functions = 2 (out of 99)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 06f9fb802ba..d08401adb21 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7194,6 +7194,47 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
return_label: return __retres;
}
+/*@ requires valid_file_name: 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, *(resolved_name + (0 .. 4096 - 1));
+ assigns __fc_heap_status
+ \from (indirect: resolved_name), __fc_heap_status;
+ assigns \result
+ \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 ..)));
+
+ behavior allocate_resolved_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 resolved_name_null: resolved_name ≡ \null;
+ ensures null_result: \result ≡ \null;
+ assigns \result;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ behavior resolved_name_buffer:
+ assumes
+ allocated_resolved_name_or_fail:
+ \valid(resolved_name + (0 .. 4096 - 1));
+ ensures valid_string_resolved_name: valid_string(\old(resolved_name));
+ ensures resolved_result: \result ≡ \old(resolved_name);
+ assigns \result, *(resolved_name + (0 .. 4096 - 1));
+ assigns \result \from \nothing;
+ assigns *(resolved_name + (0 .. 4096 - 1))
+ \from (indirect: *(file_name + (0 ..)));
+ allocates \nothing;
+ */
char *realpath(char const * restrict file_name, char * restrict resolved_name)
{
char *__retres;
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 860879bc5e5..55cc38194e3 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -16,6 +16,7 @@
\return(reallocarray) == 0 (auto)
\return(getenv) == 0 (auto)
\return(bsearch) == 0 (auto)
+ \return(realpath) == 0 (auto)
\return(getcwd) == 0 (auto)
\return(ttyname) == 0 (auto)
\return(memchr) == 0 (auto)
--
GitLab