From 283eb24c263cd483665b5cc7ee3374ccebea3adb Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 28 Sep 2022 10:38:30 +0200
Subject: [PATCH] [E-ACSL] restore libc test suite
---
src/plugins/e-acsl/tests/libc/file.c | 1 +
.../e-acsl/tests/libc/oracle/file.res.oracle | 19 ++++++
.../e-acsl/tests/libc/oracle/gen_file.c | 65 +++++++++++++++++++
src/plugins/e-acsl/tests/ptests_config | 4 +-
4 files changed, 87 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/tests/libc/file.c b/src/plugins/e-acsl/tests/libc/file.c
index eeb01ad1781..7e72a73f8f0 100644
--- a/src/plugins/e-acsl/tests/libc/file.c
+++ b/src/plugins/e-acsl/tests/libc/file.c
@@ -36,5 +36,6 @@ int main() {
//@ assert !\initialized(&buf2[0]);
//@ assert \initialized(&buf2[1..4]);
//@ assert !\initialized(&buf2[5]);
+ fclose(f);
return 0;
}
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
index dcd42b67a10..96af9661135 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -1,4 +1,7 @@
[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `fclose':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
@@ -19,6 +22,9 @@
`logic functions or predicates with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:118: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] file.c:12: Warning:
function __gen_e_acsl_fread: precondition 'valid_stream' got status unknown.
@@ -145,3 +151,16 @@
[eva:alarm] file.c:38: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
+[eva:alarm] file.c:39: Warning:
+ function __gen_e_acsl_fclose: precondition 'valid_stream' got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
+ function __e_acsl_assert_register_ulong: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:122: Warning:
+ function __e_acsl_assert_register_int: precondition data->values == \null ||
+ \valid(data->values) got status unknown.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
index aaa3f356135..7f8b5b42d2c 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -10,6 +10,13 @@ char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+/*@ requires valid_stream: \valid(stream);
+ ensures result_zero_or_EOF: \result == 0 || \result == -1;
+ assigns \result;
+ assigns \result \from (indirect: stream), (indirect: *stream);
+ */
+int __gen_e_acsl_fclose(FILE *stream);
+
/*@ requires valid_filename: valid_read_string(filename);
requires valid_mode: valid_read_string(mode);
ensures
@@ -408,6 +415,63 @@ FILE *__gen_e_acsl_fopen(char const * restrict filename,
return __retres;
}
+/*@ requires valid_stream: \valid(stream);
+ ensures result_zero_or_EOF: \result == 0 || \result == -1;
+ assigns \result;
+ assigns \result \from (indirect: stream), (indirect: *stream);
+ */
+int __gen_e_acsl_fclose(FILE *stream)
+{
+ int __retres;
+ {
+ int __gen_e_acsl_valid;
+ __e_acsl_store_block((void *)(& stream),8UL);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_valid = __e_acsl_valid((void *)stream,sizeof(FILE),
+ (void *)stream,(void *)(& stream));
+ __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"stream",
+ (void *)stream);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"sizeof(FILE)",
+ 0,sizeof(FILE));
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
+ "\\valid(stream)",0,__gen_e_acsl_valid);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Precondition";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid(stream)";
+ __gen_e_acsl_assert_data.file = "FRAMAC_SHARE/libc/stdio.h";
+ __gen_e_acsl_assert_data.fct = "fclose";
+ __gen_e_acsl_assert_data.line = 120;
+ __gen_e_acsl_assert_data.name = "valid_stream";
+ __e_acsl_assert(__gen_e_acsl_valid,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ }
+ __retres = fclose(stream);
+ {
+ int __gen_e_acsl_or;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"\\result",0,
+ __retres);
+ if (__retres == 0) __gen_e_acsl_or = 1;
+ else {
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"\\result",0,
+ __retres);
+ __gen_e_acsl_or = __retres == -1;
+ }
+ __gen_e_acsl_assert_data_2.blocking = 1;
+ __gen_e_acsl_assert_data_2.kind = "Postcondition";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\result == 0 || \\result == -1";
+ __gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/stdio.h";
+ __gen_e_acsl_assert_data_2.fct = "fclose";
+ __gen_e_acsl_assert_data_2.line = 122;
+ __gen_e_acsl_assert_data_2.name = "result_zero_or_EOF";
+ __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_delete_block((void *)(& stream));
+ return __retres;
+ }
+}
+
void __e_acsl_globals_init(void)
{
static char __e_acsl_already_run = 0;
@@ -703,6 +767,7 @@ int main(void)
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
}
/*@ assert !\initialized(&buf2[5]); */ ;
+ __gen_e_acsl_fclose(f);
__retres = 0;
__e_acsl_delete_block((void *)(buf2));
__e_acsl_delete_block((void *)(& f));
diff --git a/src/plugins/e-acsl/tests/ptests_config b/src/plugins/e-acsl/tests/ptests_config
index 0c0f44a5c36..1d57b967441 100644
--- a/src/plugins/e-acsl/tests/ptests_config
+++ b/src/plugins/e-acsl/tests/ptests_config
@@ -1,2 +1,2 @@
-DEFAULT_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory special temporal
-dev_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory special temporal
+DEFAULT_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory libc special temporal
+dev_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only libc memory special temporal
--
GitLab