diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
new file mode 100644
index 0000000000000000000000000000000000000000..6a5a747d509ac2596667b6f684ccf9e640a62b0f
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c
@@ -0,0 +1,585 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..beb1260483ced4c4fd7fec20e74713d99c944702
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle
@@ -0,0 +1,30 @@
+[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.
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/separated.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/separated.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/memory/separated.c b/src/plugins/e-acsl/tests/memory/separated.c
new file mode 100644
index 0000000000000000000000000000000000000000..f63bc50c481ce6e32f517c41545ba6792b913088
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/separated.c
@@ -0,0 +1,68 @@
+/* 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