From 7945eb951109fc68d16ac63f1ba7dd54f872fc22 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 4 Oct 2023 14:37:55 +0200
Subject: [PATCH] [e-acsl] move test to dev config to avoid issue in macOS
---
src/plugins/e-acsl/tests/bts/issue-eacsl-40.c | 12 +-
.../bts/oracle/issue-eacsl-40.1.res.oracle | 2 -
.../bts/oracle/issue-eacsl-40.out.frama.c | 485 ------------------
...0.res.oracle => issue-eacsl-40.res.oracle} | 0
4 files changed, 6 insertions(+), 493 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c
rename src/plugins/e-acsl/tests/bts/oracle/{issue-eacsl-40.0.res.oracle => issue-eacsl-40.res.oracle} (100%)
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
index 2060c4c0fd1..457399dfb61 100644
--- a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
@@ -8,12 +8,12 @@
COMMENT: attributes are erased by Frama-C's kernel. The test below checks
COMMENT: whether code produced by E-ACSL's instrumentation remains parsable
COMMENT: by GCC.
- COMMENT: The 'LIBS:' line below disables the filter set by E_ACSL_test.ml
- LIBS:
- LOG: @PTEST_NAME@.out.frama.c
- OPT: @GLOBAL@ @EACSL@ -cpp-extra-args="-DNO_FCLOSE" -no-frama-c-stdlib -then-last -print -ocode @PTEST_NAME@.out.frama.c
- ENABLED_IF: %{bin-available:gcc}
- EXECNOW: BIN @PTEST_NAME@.o gcc -Wno-attributes %{dep:@PTEST_NAME@.out.frama.c} -c -o @PTEST_NAME@.o >@DEV_NULL@ 2>@DEV_NULL@
+*/
+
+/* run.config_dev
+
+ MACRO: ROOT_EACSL_GCC_OPTS_EXT -c
+
*/
#include <stdio.h>
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle
deleted file mode 100644
index efd02631129..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle
+++ /dev/null
@@ -1,2 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c
deleted file mode 100644
index e3374e0ba33..00000000000
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c
+++ /dev/null
@@ -1,485 +0,0 @@
-/* Generated by Frama-C */
-char *__gen_e_acsl_literal_string;
-char *__gen_e_acsl_literal_string_2;
-typedef long __off_t;
-typedef long __off64_t;
-typedef unsigned long uintptr_t;
-typedef unsigned long size_t;
-typedef int wchar_t;
-struct _IO_FILE;
-typedef struct _IO_FILE FILE;
-struct _IO_marker;
-struct _IO_codecvt;
-struct _IO_wide_data;
-typedef void _IO_lock_t;
-struct _IO_FILE;
-struct __e_acsl_mpz_struct {
- int _mp_alloc ;
- int _mp_size ;
- unsigned long *_mp_d ;
-};
-typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
-typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
-struct __e_acsl_mpq_struct {
- __e_acsl_mpz_struct _mp_num ;
- __e_acsl_mpz_struct _mp_den ;
-};
-typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
-typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
-typedef unsigned long __e_acsl_mp_bitcnt_t;
-enum __e_acsl_assert_data_type_t {
- E_ACSL_INT = 0,
- E_ACSL_REAL = 1,
- E_ACSL_PTR = 2,
- E_ACSL_ARRAY = 3,
- E_ACSL_FUN = 4,
- E_ACSL_STRUCT = 5,
- E_ACSL_UNION = 6,
- E_ACSL_OTHER = 1000
-};
-typedef enum __e_acsl_assert_data_type_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_type_t;
-enum __e_acsl_assert_data_ikind_t {
- E_ACSL_IBOOL = 0,
- E_ACSL_ICHAR = 1,
- E_ACSL_ISCHAR = 2,
- E_ACSL_IUCHAR = 3,
- E_ACSL_IINT = 4,
- E_ACSL_IUINT = 5,
- E_ACSL_ISHORT = 6,
- E_ACSL_IUSHORT = 7,
- E_ACSL_ILONG = 8,
- E_ACSL_IULONG = 9,
- E_ACSL_ILONGLONG = 10,
- E_ACSL_IULONGLONG = 11,
- E_ACSL_IMPZ = 12
-};
-typedef enum __e_acsl_assert_data_ikind_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_ikind_t;
-enum __e_acsl_assert_data_rkind_t {
- E_ACSL_RFLOAT = 0,
- E_ACSL_RDOUBLE = 1,
- E_ACSL_RLONGDOUBLE = 2,
- E_ACSL_RMPQ = 3
-};
-typedef enum __e_acsl_assert_data_rkind_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_rkind_t;
-union __e_acsl_assert_data_int_value_t {
- _Bool value_bool ;
- char value_char ;
- signed char value_schar ;
- unsigned char value_uchar ;
- int value_int ;
- unsigned int value_uint ;
- short value_short ;
- unsigned short value_ushort ;
- long value_long ;
- unsigned long value_ulong ;
- long long value_llong ;
- unsigned long long value_ullong ;
- struct __e_acsl_mpz_struct *value_mpz ;
-};
-typedef union __e_acsl_assert_data_int_value_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_int_value_t;
-union __e_acsl_assert_data_real_value_t {
- float value_float ;
- double value_double ;
- long double value_ldouble ;
- struct __e_acsl_mpq_struct *value_mpq ;
-};
-typedef union __e_acsl_assert_data_real_value_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_real_value_t;
-struct __e_acsl_assert_data_int_content_t {
- int is_enum ;
- __e_acsl_assert_data_ikind_t kind ;
- __e_acsl_assert_data_int_value_t value ;
-};
-typedef struct __e_acsl_assert_data_int_content_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_int_content_t;
-struct __e_acsl_assert_data_real_content_t {
- __e_acsl_assert_data_rkind_t kind ;
- __e_acsl_assert_data_real_value_t value ;
-};
-typedef struct __e_acsl_assert_data_real_content_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_real_content_t;
-union __e_acsl_assert_data_content_t {
- __e_acsl_assert_data_int_content_t int_content ;
- __e_acsl_assert_data_real_content_t real_content ;
- uintptr_t value_ptr ;
- uintptr_t value_array ;
-};
-typedef union __e_acsl_assert_data_content_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_content_t;
-struct __e_acsl_assert_data_value_t {
- char const *name ;
- __e_acsl_assert_data_type_t type ;
- __e_acsl_assert_data_content_t content ;
- struct __e_acsl_assert_data_value_t *next ;
-};
-typedef struct __e_acsl_assert_data_value_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_value_t;
-struct __e_acsl_assert_data_t {
- int blocking ;
- char const *kind ;
- char const *name ;
- char const *pred_txt ;
- char const *file ;
- char const *fct ;
- int line ;
- __e_acsl_assert_data_value_t *values ;
-};
-typedef struct __e_acsl_assert_data_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_t;
-struct __e_acsl_contract_t;
-typedef struct __e_acsl_contract_t __attribute__((__FC_BUILTIN__)) __e_acsl_contract_t;
-typedef unsigned long pthread_t;
-union pthread_attr_t {
- char __size[56] ;
- long __align ;
-};
-typedef union pthread_attr_t pthread_attr_t;
-/*@ ghost extern int __e_acsl_init; */
-
-/*@ requires !\initialized(z);
- ensures \valid(\old(z));
- assigns *z;
- assigns *z \from __e_acsl_init;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__e_acsl_mpz_struct ( __attribute__((
- __FC_BUILTIN__)) z)[1]);
-
-/*@ requires !\initialized(z);
- ensures \valid(\old(z));
- ensures \initialized(\old(z));
- assigns *z;
- assigns *z \from n;
- allocates \old(z);
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__e_acsl_mpz_struct ( __attribute__((
- __FC_BUILTIN__)) z)[1],
- unsigned long n);
-
-/*@ requires \valid(x);
- assigns *x;
- assigns *x \from *x; */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__e_acsl_mpz_struct ( __attribute__((
- __FC_BUILTIN__)) x)[1]);
-
-/*@ requires \valid_read(z1);
- requires \valid_read(z2);
- assigns \result;
- assigns \result \from *z1, *z2;
- */
-extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__e_acsl_mpz_struct const ( __attribute__((
- __FC_BUILTIN__)) z1)[1],
- __e_acsl_mpz_struct const ( __attribute__((
- __FC_BUILTIN__)) z2)[1]);
-
-/*@ requires \valid(z1);
- requires \valid_read(z2);
- requires \valid_read(z3);
- ensures \initialized(\old(z1));
- assigns *z1;
- assigns *z1 \from *z2, *z3;
- */
-extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__e_acsl_mpz_struct ( __attribute__((
- __FC_BUILTIN__)) z1)[1],
- __e_acsl_mpz_struct const ( __attribute__((
- __FC_BUILTIN__)) z2)[1],
- __e_acsl_mpz_struct const ( __attribute__((
- __FC_BUILTIN__)) z3)[1]);
-
-/*@ requires \valid_read(z);
- assigns \result;
- assigns \result \from *z; */
-extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__e_acsl_mpz_struct const ( __attribute__((
- __FC_BUILTIN__)) z)[1]);
-
-/*@ requires \valid_read(data) && \initialized(data);
- assigns \nothing;
-
- behavior blocking:
- assumes data->blocking != 0;
- requires predicate != 0;
-
- behavior non_blocking:
- assumes data->blocking == 0;
- check requires predicate != 0;
-
- complete behaviors non_blocking, blocking;
- disjoint behaviors non_blocking, blocking;
- */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int predicate,
- __e_acsl_assert_data_t *data);
-
-extern size_t __e_acsl_heap_allocation_size;
-
-extern size_t __e_acsl_heap_allocated_blocks;
-
-/*@ ghost extern int __fc_heap_status; */
-
-/*@ requires \valid(data);
- requires data->values == \null || \valid(data->values);
- assigns data->values;
- assigns data->values \from (indirect: __fc_heap_status), value;
- */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_register_int(__e_acsl_assert_data_t *data,
- char const *name,
- int is_enum,
- int value);
-
-/*@ requires \valid(data);
- requires data->values == \null || \valid(data->values);
- assigns data->values;
- assigns data->values \from (indirect: __fc_heap_status), value;
- */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_register_ulong(
- __e_acsl_assert_data_t *data,
- char const *name,
- int is_enum,
- unsigned long value);
-
-/*@ requires \valid(data);
- requires data->values == \null || \valid(data->values);
- assigns data->values;
- assigns data->values \from (indirect: __fc_heap_status), ptr;
- */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_register_ptr(__e_acsl_assert_data_t *data,
- char const *name,
- void *ptr);
-
-/*@ requires \valid(data);
- assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_clean(__e_acsl_assert_data_t *data);
-
-/*@
-axiomatic dynamic_allocation {
- predicate is_allocable{L}(integer n)
- reads __fc_heap_status;
-
- axiom never_allocable{L}:
- \forall integer i;
- i < 0 || i > 18446744073709551615UL ==> !is_allocable(i);
-
- }
- */
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_init(int *argc_ref,
- char ***argv,
- size_t ptr_size);
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
-
-/*@ ensures \result == \old(ptr);
- assigns \result;
- assigns \result \from *((char *)ptr + (0 .. size - 1)), ptr, size;
- */
- __attribute__((__FC_BUILTIN__)) void *__e_acsl_store_block(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *ptr);
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_initialize(void *ptr,
- size_t size);
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_full_init(void *ptr);
-
-/*@ assigns \nothing; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_mark_readonly(void *ptr);
-
-/*@ assigns \result;
- assigns \result \from *((char *)ptr + (0 .. size - 1)), ptr, size;
-
- behavior initialized:
- assumes \initialized((char *)ptr + (0 .. size - 1));
- ensures \result == 1;
-
- behavior uninitialized:
- assumes !\initialized((char *)ptr + (0 .. size - 1));
- ensures \result == 0;
-
- complete behaviors uninitialized, initialized;
- disjoint behaviors uninitialized, initialized;
- */
- __attribute__((__FC_BUILTIN__)) int __e_acsl_initialized(void *ptr,
- size_t size);
-
-long valid_nstring(char *s, long n, int wrtbl);
-
-long valid_nwstring(wchar_t *s, long n, int wrtbl);
-
-__inline static long valid_string__fc_inline(char *s, int wrtbl)
-{
- long tmp;
- tmp = valid_nstring(s,(long)(-1),wrtbl);
- return tmp;
-}
-
-__inline static long valid_wstring__fc_inline(wchar_t *s, int wrtbl)
-{
- long tmp;
- tmp = valid_nwstring(s,(long)(-1),wrtbl);
- return tmp;
-}
-
-extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-
-typedef unsigned long size_t;
-typedef long __off_t;
-typedef long __off64_t;
-struct _IO_FILE;
-typedef struct _IO_FILE FILE;
-struct _IO_marker;
-struct _IO_codecvt;
-struct _IO_wide_data;
-typedef void _IO_lock_t;
-struct _IO_FILE {
- int _flags ;
- char *_IO_read_ptr ;
- char *_IO_read_end ;
- char *_IO_read_base ;
- char *_IO_write_base ;
- char *_IO_write_ptr ;
- char *_IO_write_end ;
- char *_IO_buf_base ;
- char *_IO_buf_end ;
- char *_IO_save_base ;
- char *_IO_backup_base ;
- char *_IO_save_end ;
- struct _IO_marker *_markers ;
- struct _IO_FILE *_chain ;
- int _fileno ;
- int _flags2 ;
- __off_t _old_offset ;
- unsigned short _cur_column ;
- signed char _vtable_offset ;
- char _shortbuf[1] ;
- _IO_lock_t *_lock ;
- __off64_t _offset ;
- struct _IO_codecvt *_codecvt ;
- struct _IO_wide_data *_wide_data ;
- struct _IO_FILE *_freeres_list ;
- void *_freeres_buf ;
- size_t __pad5 ;
- int _mode ;
- char _unused2[((unsigned long)15 * sizeof(int) - (unsigned long)4 * sizeof(void *)) - sizeof(size_t)] ;
-};
-extern FILE *fopen(char const * restrict __filename,
- char const * restrict __modes);
-
-extern size_t fread(void * restrict __ptr, size_t __size, size_t __n,
- FILE * restrict __stream);
-
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __gen_e_acsl_literal_string = "r";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("r"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
- __gen_e_acsl_literal_string_2 = "/dev/urandom";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("/dev/urandom"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- }
- return;
-}
-
-int main(void)
-{
- int __retres;
- char buf[4];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_globals_init();
- FILE *f = fopen(__gen_e_acsl_literal_string_2,__gen_e_acsl_literal_string);
- if (f) {
- char buf_0[4];
- size_t tmp_0;
- __e_acsl_store_block((void *)(buf_0),4UL);
- tmp_0 = fread((void *)(buf_0),(size_t)1,(size_t)4,f);
- {
- size_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_tmp_0;
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl_mul;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_le;
- unsigned long __gen_e_acsl_size;
- __gen_e_acsl_ = (size_t)1;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data =
- {.values = (void *)0};
- __gmpz_init_set_ui(__gen_e_acsl_tmp_0,tmp_0);
- __gmpz_init_set_ui(__gen_e_acsl__2,__gen_e_acsl_);
- __gmpz_init(__gen_e_acsl_mul);
- __gmpz_mul(__gen_e_acsl_mul,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_tmp_0),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init_set_ui(__gen_e_acsl__3,18446744073709551615UL);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"tmp_0",0,
- tmp_0);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,
- "__gen_e_acsl_",0,__gen_e_acsl_);
- __gen_e_acsl_assert_data.blocking = 1;
- __gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "tmp_0 * __gen_e_acsl_ <= 18446744073709551615";
- __gen_e_acsl_assert_data.file = "issue-eacsl-40.c";
- __gen_e_acsl_assert_data.fct = "main";
- __gen_e_acsl_assert_data.line = 26;
- __gen_e_acsl_assert_data.name = "size_lesser_or_eq_than_SIZE_MAX";
- __e_acsl_assert(__gen_e_acsl_le <= 0,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
- __e_acsl_initialize((void *)(buf_0),__gen_e_acsl_size);
- __gmpz_clear(__gen_e_acsl_tmp_0);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl_mul);
- __gmpz_clear(__gen_e_acsl__3);
- }
- int res = (int)tmp_0;
- if (res == 4) {
- {
- int __gen_e_acsl_initialized;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
- {.values = (void *)0};
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& buf_0[3]),
- sizeof(char));
- __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
- "&buf_0[3]",(void *)(& buf_0[3]));
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
- "sizeof(char)",0,sizeof(char));
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "\\initialized(&buf_0[3])",0,
- __gen_e_acsl_initialized);
- __gen_e_acsl_assert_data_2.blocking = 1;
- __gen_e_acsl_assert_data_2.kind = "Assertion";
- __gen_e_acsl_assert_data_2.pred_txt = "\\initialized(&buf_0[3])";
- __gen_e_acsl_assert_data_2.file = "issue-eacsl-40.c";
- __gen_e_acsl_assert_data_2.fct = "main";
- __gen_e_acsl_assert_data_2.line = 31;
- __e_acsl_assert(__gen_e_acsl_initialized,
- & __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- }
- /*@ assert \initialized(&buf_0[3]); */ ;
- __e_acsl_initialize((void *)(buf_0),sizeof(char));
- buf_0[0] = buf_0[3];
- }
- else {
- __retres = 2;
- __e_acsl_delete_block((void *)(buf_0));
- goto return_label;
- }
- __e_acsl_delete_block((void *)(buf_0));
- }
- else {
- __retres = 1;
- goto return_label;
- }
- __retres = 0;
- return_label: {
- __e_acsl_memory_clean();
- return __retres;
- }
-}
-
-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
--
GitLab