Skip to content
Snippets Groups Projects
Commit 7945eb95 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[e-acsl] move test to dev config to avoid issue in macOS

parent c4e62ad5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
+ 6
− 6
View file @ 7945eb95
...@@ -8,12 +8,12 @@ ...@@ -8,12 +8,12 @@
COMMENT: attributes are erased by Frama-C's kernel. The test below checks 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: whether code produced by E-ACSL's instrumentation remains parsable
COMMENT: by GCC. COMMENT: by GCC.
COMMENT: The 'LIBS:' line below disables the filter set by E_ACSL_test.ml */
LIBS:
LOG: @PTEST_NAME@.out.frama.c /* run.config_dev
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} MACRO: ROOT_EACSL_GCC_OPTS_EXT -c
EXECNOW: BIN @PTEST_NAME@.o gcc -Wno-attributes %{dep:@PTEST_NAME@.out.frama.c} -c -o @PTEST_NAME@.o >@DEV_NULL@ 2>@DEV_NULL@
*/ */
#include <stdio.h> #include <stdio.h>
......
src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle deleted 100644 → 0
+ 0
− 2
View file @ c4e62ad5
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c deleted 100644 → 0
+ 0
− 485
View file @ c4e62ad5
/* 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;
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment