Skip to content
Snippets Groups Projects
Commit e27b38d2 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl:tests] Add tests for `\separated`

parent 7b0eea9f
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/memory/oracle_ci/gen_separated.c 0 → 100644
+ 585
− 0
View file @ e27b38d2
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
{
int a;
int b;
int c;
__e_acsl_store_block((void *)(& c),(size_t)4);
__e_acsl_store_block((void *)(& b),(size_t)4);
__e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& c));
c = 0;
__e_acsl_full_init((void *)(& b));
b = c;
__e_acsl_full_init((void *)(& a));
a = b;
int *d = & a;
__e_acsl_store_block((void *)(& d),(size_t)8);
__e_acsl_full_init((void *)(& d));
{
int __gen_e_acsl_valid_read;
int __gen_e_acsl_valid_read_2;
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_separated;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& a),
sizeof(int),
(void *)(& a),(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&a); */
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE","main",
"separated_guard: \\valid_read(&a)",
"tests/memory/separated.c",14);
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& b),
sizeof(int),
(void *)(& b),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&b); */
__e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","main",
"separated_guard: \\valid_read(&b)",
"tests/memory/separated.c",14);
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& c),
sizeof(int),
(void *)(& c),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&c); */
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","main",
"separated_guard: \\valid_read(&c)",
"tests/memory/separated.c",14);
__gen_e_acsl_separated = __e_acsl_separated((size_t)3,(void *)(& c),
sizeof(int),(void *)(& b),
sizeof(int),(void *)(& a),
sizeof(int));
__e_acsl_assert(__gen_e_acsl_separated,"Assertion","main",
"\\separated(&a, &b, &c)","tests/memory/separated.c",
14);
}
/*@ assert \separated(&a, &b, &c); */ ;
{
int __gen_e_acsl_valid_read_4;
int __gen_e_acsl_valid_read_5;
int __gen_e_acsl_valid_read_6;
int __gen_e_acsl_initialized;
int __gen_e_acsl_and;
int __gen_e_acsl_separated_2;
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& a),
sizeof(int),
(void *)(& a),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&a); */
__e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","main",
"separated_guard: \\valid_read(&a)",
"tests/memory/separated.c",15);
__gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& b),
sizeof(int),
(void *)(& b),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&b); */
__e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE","main",
"separated_guard: \\valid_read(&b)",
"tests/memory/separated.c",15);
__gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)(& c),
sizeof(int),
(void *)(& c),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&c); */
__e_acsl_assert(__gen_e_acsl_valid_read_6,"RTE","main",
"separated_guard: \\valid_read(&c)",
"tests/memory/separated.c",15);
__gen_e_acsl_initialized = __e_acsl_initialized((void *)(& d),
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid_read_7;
__gen_e_acsl_valid_read_7 = __e_acsl_valid_read((void *)d,
sizeof(int),
(void *)d,
(void *)(& d));
__gen_e_acsl_and = __gen_e_acsl_valid_read_7;
}
else __gen_e_acsl_and = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(d); */
__e_acsl_assert(__gen_e_acsl_and,"RTE","main",
"separated_guard: \\valid_read(d)",
"tests/memory/separated.c",15);
__gen_e_acsl_separated_2 = __e_acsl_separated((size_t)4,(void *)d,
sizeof(int),
(void *)(& c),
sizeof(int),
(void *)(& b),
sizeof(int),
(void *)(& a),
sizeof(int));
__e_acsl_assert(! __gen_e_acsl_separated_2,"Assertion","main",
"!\\separated(&a, &b, &c, d)",
"tests/memory/separated.c",15);
}
/*@ assert ¬\separated(&a, &b, &c, d); */ ;
__e_acsl_delete_block((void *)(& d));
__e_acsl_delete_block((void *)(& c));
__e_acsl_delete_block((void *)(& b));
__e_acsl_delete_block((void *)(& a));
}
{
double array[20] = {(double)0};
__e_acsl_store_block((void *)(array),(size_t)160);
__e_acsl_full_init((void *)(& array));
{
int __gen_e_acsl_valid_read_8;
int __gen_e_acsl_valid_read_9;
int __gen_e_acsl_separated_3;
__gen_e_acsl_valid_read_8 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
(size_t)80,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 9]); */
__e_acsl_assert(__gen_e_acsl_valid_read_8,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 9])",
"tests/memory/separated.c",21);
__gen_e_acsl_valid_read_9 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 10),
(size_t)80,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[10 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_9,"RTE","main",
"separated_guard: \\valid_read(&array[10 .. 19])",
"tests/memory/separated.c",21);
__gen_e_acsl_separated_3 = __e_acsl_separated((size_t)2,
(void *)((char *)(& array) +
8 * 10),80,
(void *)((char *)(& array) +
8 * 0),80);
__e_acsl_assert(__gen_e_acsl_separated_3,"Assertion","main",
"\\separated(&array[0 .. 9], &array[10 .. 19])",
"tests/memory/separated.c",21);
}
/*@ assert \separated(&array[0 .. 9], &array[10 .. 19]); */ ;
{
int __gen_e_acsl_valid_read_10;
int __gen_e_acsl_valid_read_11;
int __gen_e_acsl_separated_4;
__gen_e_acsl_valid_read_10 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
(size_t)88,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 10]); */
__e_acsl_assert(__gen_e_acsl_valid_read_10,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 10])",
"tests/memory/separated.c",22);
__gen_e_acsl_valid_read_11 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 5),
(size_t)88,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[5 .. 15]); */
__e_acsl_assert(__gen_e_acsl_valid_read_11,"RTE","main",
"separated_guard: \\valid_read(&array[5 .. 15])",
"tests/memory/separated.c",22);
__gen_e_acsl_separated_4 = __e_acsl_separated((size_t)2,
(void *)((char *)(& array) +
8 * 5),88,
(void *)((char *)(& array) +
8 * 0),88);
__e_acsl_assert(! __gen_e_acsl_separated_4,"Assertion","main",
"!\\separated(&array[0 .. 10], &array[5 .. 15])",
"tests/memory/separated.c",22);
}
/*@ assert ¬\separated(&array[0 .. 10], &array[5 .. 15]); */ ;
{
int __gen_e_acsl_valid_read_12;
int __gen_e_acsl_valid_read_13;
int __gen_e_acsl_separated_5;
__gen_e_acsl_valid_read_12 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
(size_t)160,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 19]); */
__e_acsl_assert(__gen_e_acsl_valid_read_12,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 19])",
"tests/memory/separated.c",23);
__gen_e_acsl_valid_read_13 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 5),
(size_t)88,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[5 .. 15]); */
__e_acsl_assert(__gen_e_acsl_valid_read_13,"RTE","main",
"separated_guard: \\valid_read(&array[5 .. 15])",
"tests/memory/separated.c",23);
__gen_e_acsl_separated_5 = __e_acsl_separated((size_t)2,
(void *)((char *)(& array) +
8 * 5),88,
(void *)((char *)(& array) +
8 * 0),160);
__e_acsl_assert(! __gen_e_acsl_separated_5,"Assertion","main",
"!\\separated(&array[0 .. 19], &array[5 .. 15])",
"tests/memory/separated.c",23);
}
/*@ assert ¬\separated(&array[0 .. 19], &array[5 .. 15]); */ ;
{
int __gen_e_acsl_valid_read_14;
int __gen_e_acsl_valid_read_15;
int __gen_e_acsl_separated_6;
__gen_e_acsl_valid_read_14 = __e_acsl_valid_read((void *)(array),
sizeof(double),
(void *)(array),
(void *)(array));
/*@ assert E_ACSL: separated_guard: \valid_read((double *)array); */
__e_acsl_assert(__gen_e_acsl_valid_read_14,"RTE","main",
"separated_guard: \\valid_read((double *)array)",
"tests/memory/separated.c",24);
__gen_e_acsl_valid_read_15 = __e_acsl_valid_read((void *)(& array[1]),
sizeof(double),
(void *)(& array[1]),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[1]); */
__e_acsl_assert(__gen_e_acsl_valid_read_15,"RTE","main",
"separated_guard: \\valid_read(&array[1])",
"tests/memory/separated.c",24);
__gen_e_acsl_separated_6 = __e_acsl_separated((size_t)2,
(void *)(& array[1]),
sizeof(double),
(void *)(array),
sizeof(double));
__e_acsl_assert(__gen_e_acsl_separated_6,"Assertion","main",
"\\separated((double *)array, &array[1])",
"tests/memory/separated.c",24);
}
/*@ assert \separated((double *)array, &array[1]); */ ;
{
int __gen_e_acsl_valid_read_16;
int __gen_e_acsl_valid_read_17;
int __gen_e_acsl_separated_7;
__gen_e_acsl_valid_read_16 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 0),
(size_t)16,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[0 .. 1]); */
__e_acsl_assert(__gen_e_acsl_valid_read_16,"RTE","main",
"separated_guard: \\valid_read(&array[0 .. 1])",
"tests/memory/separated.c",25);
__gen_e_acsl_valid_read_17 = __e_acsl_valid_read((void *)((char *)(& array) +
8 * 1),
(size_t)16,
(void *)(& array),
(void *)0);
/*@ assert E_ACSL: separated_guard: \valid_read(&array[1 .. 2]); */
__e_acsl_assert(__gen_e_acsl_valid_read_17,"RTE","main",
"separated_guard: \\valid_read(&array[1 .. 2])",
"tests/memory/separated.c",25);
__gen_e_acsl_separated_7 = __e_acsl_separated((size_t)2,
(void *)((char *)(& array) +
8 * 1),16,
(void *)((char *)(& array) +
8 * 0),16);
__e_acsl_assert(! __gen_e_acsl_separated_7,"Assertion","main",
"!\\separated(&array[0 .. 1], &array[1 .. 2])",
"tests/memory/separated.c",25);
}
/*@ assert ¬\separated(&array[0 .. 1], &array[1 .. 2]); */ ;
__e_acsl_delete_block((void *)(array));
}
{
int *a_0 = malloc(sizeof(int));
__e_acsl_store_block((void *)(& a_0),(size_t)8);
__e_acsl_full_init((void *)(& a_0));
int *b_0 = malloc(sizeof(int));
__e_acsl_store_block((void *)(& b_0),(size_t)8);
__e_acsl_full_init((void *)(& b_0));
int *c_0 = a_0;
__e_acsl_store_block((void *)(& c_0),(size_t)8);
__e_acsl_full_init((void *)(& c_0));
{
int __gen_e_acsl_initialized_2;
int __gen_e_acsl_and_2;
int __gen_e_acsl_initialized_3;
int __gen_e_acsl_and_3;
int __gen_e_acsl_separated_8;
__gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& a_0),
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_read_18;
__gen_e_acsl_valid_read_18 = __e_acsl_valid_read((void *)a_0,
sizeof(int),
(void *)a_0,
(void *)(& a_0));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_read_18;
}
else __gen_e_acsl_and_2 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(a_0); */
__e_acsl_assert(__gen_e_acsl_and_2,"RTE","main",
"separated_guard: \\valid_read(a_0)",
"tests/memory/separated.c",34);
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& b_0),
sizeof(int *));
if (__gen_e_acsl_initialized_3) {
int __gen_e_acsl_valid_read_19;
__gen_e_acsl_valid_read_19 = __e_acsl_valid_read((void *)b_0,
sizeof(int),
(void *)b_0,
(void *)(& b_0));
__gen_e_acsl_and_3 = __gen_e_acsl_valid_read_19;
}
else __gen_e_acsl_and_3 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(b_0); */
__e_acsl_assert(__gen_e_acsl_and_3,"RTE","main",
"separated_guard: \\valid_read(b_0)",
"tests/memory/separated.c",34);
__gen_e_acsl_separated_8 = __e_acsl_separated((size_t)2,(void *)b_0,
sizeof(int),(void *)a_0,
sizeof(int));
__e_acsl_assert(__gen_e_acsl_separated_8,"Assertion","main",
"\\separated(a_0, b_0)","tests/memory/separated.c",34);
}
/*@ assert \separated(a_0, b_0); */ ;
{
int __gen_e_acsl_initialized_4;
int __gen_e_acsl_and_4;
int __gen_e_acsl_initialized_5;
int __gen_e_acsl_and_5;
int __gen_e_acsl_initialized_6;
int __gen_e_acsl_and_6;
int __gen_e_acsl_separated_9;
__gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& a_0),
sizeof(int *));
if (__gen_e_acsl_initialized_4) {
int __gen_e_acsl_valid_read_20;
__gen_e_acsl_valid_read_20 = __e_acsl_valid_read((void *)a_0,
sizeof(int),
(void *)a_0,
(void *)(& a_0));
__gen_e_acsl_and_4 = __gen_e_acsl_valid_read_20;
}
else __gen_e_acsl_and_4 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(a_0); */
__e_acsl_assert(__gen_e_acsl_and_4,"RTE","main",
"separated_guard: \\valid_read(a_0)",
"tests/memory/separated.c",35);
__gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& b_0),
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_read_21;
__gen_e_acsl_valid_read_21 = __e_acsl_valid_read((void *)b_0,
sizeof(int),
(void *)b_0,
(void *)(& b_0));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_read_21;
}
else __gen_e_acsl_and_5 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(b_0); */
__e_acsl_assert(__gen_e_acsl_and_5,"RTE","main",
"separated_guard: \\valid_read(b_0)",
"tests/memory/separated.c",35);
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& c_0),
sizeof(int *));
if (__gen_e_acsl_initialized_6) {
int __gen_e_acsl_valid_read_22;
__gen_e_acsl_valid_read_22 = __e_acsl_valid_read((void *)c_0,
sizeof(int),
(void *)c_0,
(void *)(& c_0));
__gen_e_acsl_and_6 = __gen_e_acsl_valid_read_22;
}
else __gen_e_acsl_and_6 = 0;
/*@ assert E_ACSL: separated_guard: \valid_read(c_0); */
__e_acsl_assert(__gen_e_acsl_and_6,"RTE","main",
"separated_guard: \\valid_read(c_0)",
"tests/memory/separated.c",35);
__gen_e_acsl_separated_9 = __e_acsl_separated((size_t)3,(void *)c_0,
sizeof(int),(void *)b_0,
sizeof(int),(void *)a_0,
sizeof(int));
__e_acsl_assert(! __gen_e_acsl_separated_9,"Assertion","main",
"!\\separated(a_0, b_0, c_0)",
"tests/memory/separated.c",35);
}
/*@ assert ¬\separated(a_0, b_0, c_0); */ ;
free((void *)a_0);
free((void *)b_0);
__e_acsl_delete_block((void *)(& c_0));
__e_acsl_delete_block((void *)(& b_0));
__e_acsl_delete_block((void *)(& a_0));
}
{
double *array_0 = malloc(sizeof(double [20]));
__e_acsl_store_block((void *)(& array_0),(size_t)8);
__e_acsl_full_init((void *)(& array_0));
{
int __gen_e_acsl_valid_read_23;
int __gen_e_acsl_valid_read_24;
int __gen_e_acsl_separated_10;
__gen_e_acsl_valid_read_23 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
(size_t)80,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 9)); */
__e_acsl_assert(__gen_e_acsl_valid_read_23,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 9))",
"tests/memory/separated.c",44);
__gen_e_acsl_valid_read_24 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 10),
(size_t)80,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (10 .. 19));
*/
__e_acsl_assert(__gen_e_acsl_valid_read_24,"RTE","main",
"separated_guard: \\valid_read(array_0 + (10 .. 19))",
"tests/memory/separated.c",44);
__gen_e_acsl_separated_10 = __e_acsl_separated((size_t)2,
(void *)((char *)array_0 +
8 * 10),80,
(void *)((char *)array_0 +
8 * 0),80);
__e_acsl_assert(__gen_e_acsl_separated_10,"Assertion","main",
"\\separated(array_0 + (0 .. 9), array_0 + (10 .. 19))",
"tests/memory/separated.c",44);
}
/*@ assert \separated(array_0 + (0 .. 9), array_0 + (10 .. 19)); */ ;
{
int __gen_e_acsl_valid_read_25;
int __gen_e_acsl_valid_read_26;
int __gen_e_acsl_separated_11;
__gen_e_acsl_valid_read_25 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
(size_t)88,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 10));
*/
__e_acsl_assert(__gen_e_acsl_valid_read_25,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 10))",
"tests/memory/separated.c",45);
__gen_e_acsl_valid_read_26 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 5),
(size_t)88,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (5 .. 15));
*/
__e_acsl_assert(__gen_e_acsl_valid_read_26,"RTE","main",
"separated_guard: \\valid_read(array_0 + (5 .. 15))",
"tests/memory/separated.c",45);
__gen_e_acsl_separated_11 = __e_acsl_separated((size_t)2,
(void *)((char *)array_0 +
8 * 5),88,
(void *)((char *)array_0 +
8 * 0),88);
__e_acsl_assert(! __gen_e_acsl_separated_11,"Assertion","main",
"!\\separated(array_0 + (0 .. 10), array_0 + (5 .. 15))",
"tests/memory/separated.c",45);
}
/*@ assert ¬\separated(array_0 + (0 .. 10), array_0 + (5 .. 15)); */ ;
{
int __gen_e_acsl_valid_read_27;
int __gen_e_acsl_valid_read_28;
int __gen_e_acsl_separated_12;
__gen_e_acsl_valid_read_27 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
(size_t)160,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 19));
*/
__e_acsl_assert(__gen_e_acsl_valid_read_27,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 19))",
"tests/memory/separated.c",46);
__gen_e_acsl_valid_read_28 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 5),
(size_t)88,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (5 .. 15));
*/
__e_acsl_assert(__gen_e_acsl_valid_read_28,"RTE","main",
"separated_guard: \\valid_read(array_0 + (5 .. 15))",
"tests/memory/separated.c",46);
__gen_e_acsl_separated_12 = __e_acsl_separated((size_t)2,
(void *)((char *)array_0 +
8 * 5),88,
(void *)((char *)array_0 +
8 * 0),160);
__e_acsl_assert(! __gen_e_acsl_separated_12,"Assertion","main",
"!\\separated(array_0 + (0 .. 19), array_0 + (5 .. 15))",
"tests/memory/separated.c",46);
}
/*@ assert ¬\separated(array_0 + (0 .. 19), array_0 + (5 .. 15)); */ ;
{
int __gen_e_acsl_valid_read_29;
int __gen_e_acsl_valid_read_30;
int __gen_e_acsl_separated_13;
__gen_e_acsl_valid_read_29 = __e_acsl_valid_read((void *)(array_0 + 0),
sizeof(double),
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + 0); */
__e_acsl_assert(__gen_e_acsl_valid_read_29,"RTE","main",
"separated_guard: \\valid_read(array_0 + 0)",
"tests/memory/separated.c",47);
__gen_e_acsl_valid_read_30 = __e_acsl_valid_read((void *)(array_0 + 1),
sizeof(double),
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + 1); */
__e_acsl_assert(__gen_e_acsl_valid_read_30,"RTE","main",
"separated_guard: \\valid_read(array_0 + 1)",
"tests/memory/separated.c",47);
__gen_e_acsl_separated_13 = __e_acsl_separated((size_t)2,
(void *)(array_0 + 1),
sizeof(double),
(void *)(array_0 + 0),
sizeof(double));
__e_acsl_assert(__gen_e_acsl_separated_13,"Assertion","main",
"\\separated(array_0 + 0, array_0 + 1)",
"tests/memory/separated.c",47);
}
/*@ assert \separated(array_0 + 0, array_0 + 1); */ ;
{
int __gen_e_acsl_valid_read_31;
int __gen_e_acsl_valid_read_32;
int __gen_e_acsl_separated_14;
__gen_e_acsl_valid_read_31 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 0),
(size_t)16,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (0 .. 1)); */
__e_acsl_assert(__gen_e_acsl_valid_read_31,"RTE","main",
"separated_guard: \\valid_read(array_0 + (0 .. 1))",
"tests/memory/separated.c",48);
__gen_e_acsl_valid_read_32 = __e_acsl_valid_read((void *)((char *)array_0 +
8 * 1),
(size_t)16,
(void *)array_0,
(void *)(& array_0));
/*@ assert E_ACSL: separated_guard: \valid_read(array_0 + (1 .. 2)); */
__e_acsl_assert(__gen_e_acsl_valid_read_32,"RTE","main",
"separated_guard: \\valid_read(array_0 + (1 .. 2))",
"tests/memory/separated.c",48);
__gen_e_acsl_separated_14 = __e_acsl_separated((size_t)2,
(void *)((char *)array_0 +
8 * 1),16,
(void *)((char *)array_0 +
8 * 0),16);
__e_acsl_assert(! __gen_e_acsl_separated_14,"Assertion","main",
"!\\separated(array_0 + (0 .. 1), array_0 + (1 .. 2))",
"tests/memory/separated.c",48);
}
/*@ assert ¬\separated(array_0 + (0 .. 1), array_0 + (1 .. 2)); */ ;
free((void *)array_0);
__e_acsl_delete_block((void *)(& array_0));
}
__retres = 0;
__e_acsl_memory_clean();
return __retres;
}
src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle 0 → 100644
+ 30
− 0
View file @ e27b38d2
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/memory/separated.c:14: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:22: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:23: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:24: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:35: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:44: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:46: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:47: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/memory/separated.c:48: Warning:
function __e_acsl_assert: precondition got status unknown.
src/plugins/e-acsl/tests/memory/oracle_dev/separated.e-acsl.err.log 0 → 100644
+ 0
− 0
View file @ e27b38d2
src/plugins/e-acsl/tests/memory/separated.c 0 → 100644
+ 68
− 0
View file @ e27b38d2
/* run.config_ci, run.config_dev
COMMENT: \separated
*/
#include <stdlib.h>
int main() {
// Stack memory on different blocks
{
int a, b, c;
a = b = c = 0;
int * d = &a;
//@ assert \separated(&a, &b, &c);
//@ assert !\separated(&a, &b, &c, d);
}
// Stack memory on the same block
{
double array[20] = {0};
//@ assert \separated(array+(0..9), array+(10..19));
//@ assert !\separated(&array[0..10], &array[5..15]);
//@ assert !\separated(array+(0..19), array+(5..15));
//@ assert \separated(&array[0], &array[1]);
//@ assert !\separated(array+(0..1), array+(1..2));
//@ assert \separated(&array[15..5], &array[0..19]);
//@ assert \separated(array+(0..-3), array+(0..19));
}
// Heap memory on different blocks
{
int *a = malloc(sizeof(int));
int *b = malloc(sizeof(int));
int *c = a;
//@ assert \separated(a, b);
//@ assert !\separated(a, b, c);
free(a);
free(b);
}
// Heap memory on the same block
{
double * array = malloc(sizeof(double[20]));
//@ assert \separated(&array[0..9], &array[10..19]);
//@ assert !\separated(array+(0..10), array+(5..15));
//@ assert !\separated(&array[0..19], &array[5..15]);
//@ assert \separated(array+(0), array+(1));
//@ assert !\separated(&array[0..1], &array[1..2]);
//@ assert \separated(array+(15..5), array+(0..19));
//@ assert \separated(&array[0..-3], &array[0..19]);
free(array);
}
// Non-contiguous memory locations
{
double array[10][10][10] = {0};
//@ assert \separated(&array[0][0..2][0], &array[0][3..5][0], &array[0][6..9][0]);
//@ assert \separated(&array[0][0..2][0], &array[1][0..2][0], &array[2][0..2][0]);
//@ assert \separated(&array[0..2][0..2][0], &array[0..2][3..5][0]);
//@ assert !\separated(&array[0..3][0..2][0], &array[3..5][0..2][0]);
//@ assert \separated(&array[0..3][2..0][0], &array[3..5][0..2][0]);
}
return 0;
}
\ No newline at end of file
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