diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index f7d372e60cde991df567ff8fa17a5fb74b33c5f4..eaf0299d252f1c453d54238fcfe556737e36e511 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -35,173 +35,184 @@ char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_7;
/*@ assigns \result;
assigns \result \from \nothing; */
-extern int ( /* missing proto */ fork)();
+extern int ( /* missing proto */ fork)(void);
void __e_acsl_globals_init(void)
{
- __gen_e_acsl_literal_string_29 = "tests/builtin/strcat.c:50";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
- sizeof("tests/builtin/strcat.c:50"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
- __gen_e_acsl_literal_string_28 = "tests/builtin/strcat.c:49";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
- sizeof("tests/builtin/strcat.c:49"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
- __gen_e_acsl_literal_string_27 = "tests/builtin/strcat.c:48";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
- sizeof("tests/builtin/strcat.c:48"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
- __gen_e_acsl_literal_string_26 = "tests/builtin/strcat.c:46";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
- sizeof("tests/builtin/strcat.c:46"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
- __gen_e_acsl_literal_string_25 = "tests/builtin/strcat.c:45";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
- sizeof("tests/builtin/strcat.c:45"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
- __gen_e_acsl_literal_string_24 = "tests/builtin/strcat.c:44";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/builtin/strcat.c:44"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
- __gen_e_acsl_literal_string_23 = "tests/builtin/strcat.c:43";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/builtin/strcat.c:43"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
- __gen_e_acsl_literal_string_22 = "tests/builtin/strcat.c:42";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
- sizeof("tests/builtin/strcat.c:42"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_21 = "tests/builtin/strcat.c:41";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
- sizeof("tests/builtin/strcat.c:41"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
- __gen_e_acsl_literal_string_20 = "tests/builtin/strcat.c:40";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
- sizeof("tests/builtin/strcat.c:40"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_19 = "tests/builtin/strcat.c:37";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
- sizeof("tests/builtin/strcat.c:37"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
- __gen_e_acsl_literal_string_18 = "tests/builtin/strcat.c:36";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
- sizeof("tests/builtin/strcat.c:36"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_17 = "tests/builtin/strcat.c:35";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
- sizeof("tests/builtin/strcat.c:35"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
- __gen_e_acsl_literal_string_16 = "tests/builtin/strcat.c:34";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/builtin/strcat.c:34"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
- __gen_e_acsl_literal_string_15 = "tests/builtin/strcat.c:33";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/builtin/strcat.c:33"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/builtin/strcat.c:32";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/builtin/strcat.c:32"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/builtin/strcat.c:31";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/builtin/strcat.c:31"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/builtin/strcat.c:30";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/builtin/strcat.c:30"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_11 = "tests/builtin/strcat.c:29";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/builtin/strcat.c:29"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:28";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("tests/builtin/strcat.c:28"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:27";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/builtin/strcat.c:27"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_8 = "tests/builtin/strcat.c:26";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("tests/builtin/strcat.c:26"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __gen_e_acsl_literal_string_6 = "abcd";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("abcd"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
- __gen_e_acsl_literal_string = "TEST %d: ";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("TEST %d: "));
- __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 = "OK: Expected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("OK: Expected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
- sizeof("OK: Expected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
- sizeof("FAIL: Unexpected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
- __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
- sizeof("FAIL: Unexpected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_7 = "";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,sizeof(""));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_store_block((void *)(& __gen_e_acsl_strncat),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strncat));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strcat),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strcat));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_strtok_ptr));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& testno),(size_t)4);
- __e_acsl_full_init((void *)(& testno));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __gen_e_acsl_literal_string_29 = "tests/builtin/strcat.c:50";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
+ sizeof("tests/builtin/strcat.c:50"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
+ __gen_e_acsl_literal_string_28 = "tests/builtin/strcat.c:49";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
+ sizeof("tests/builtin/strcat.c:49"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
+ __gen_e_acsl_literal_string_27 = "tests/builtin/strcat.c:48";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
+ sizeof("tests/builtin/strcat.c:48"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
+ __gen_e_acsl_literal_string_26 = "tests/builtin/strcat.c:46";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
+ sizeof("tests/builtin/strcat.c:46"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
+ __gen_e_acsl_literal_string_25 = "tests/builtin/strcat.c:45";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
+ sizeof("tests/builtin/strcat.c:45"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
+ __gen_e_acsl_literal_string_24 = "tests/builtin/strcat.c:44";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
+ sizeof("tests/builtin/strcat.c:44"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
+ __gen_e_acsl_literal_string_23 = "tests/builtin/strcat.c:43";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
+ sizeof("tests/builtin/strcat.c:43"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
+ __gen_e_acsl_literal_string_22 = "tests/builtin/strcat.c:42";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
+ sizeof("tests/builtin/strcat.c:42"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_21 = "tests/builtin/strcat.c:41";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
+ sizeof("tests/builtin/strcat.c:41"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
+ __gen_e_acsl_literal_string_20 = "tests/builtin/strcat.c:40";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
+ sizeof("tests/builtin/strcat.c:40"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
+ __gen_e_acsl_literal_string_19 = "tests/builtin/strcat.c:37";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
+ sizeof("tests/builtin/strcat.c:37"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
+ __gen_e_acsl_literal_string_18 = "tests/builtin/strcat.c:36";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
+ sizeof("tests/builtin/strcat.c:36"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
+ __gen_e_acsl_literal_string_17 = "tests/builtin/strcat.c:35";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
+ sizeof("tests/builtin/strcat.c:35"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
+ __gen_e_acsl_literal_string_16 = "tests/builtin/strcat.c:34";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
+ sizeof("tests/builtin/strcat.c:34"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
+ __gen_e_acsl_literal_string_15 = "tests/builtin/strcat.c:33";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
+ sizeof("tests/builtin/strcat.c:33"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
+ __gen_e_acsl_literal_string_14 = "tests/builtin/strcat.c:32";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
+ sizeof("tests/builtin/strcat.c:32"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
+ __gen_e_acsl_literal_string_13 = "tests/builtin/strcat.c:31";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
+ sizeof("tests/builtin/strcat.c:31"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
+ __gen_e_acsl_literal_string_12 = "tests/builtin/strcat.c:30";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
+ sizeof("tests/builtin/strcat.c:30"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
+ __gen_e_acsl_literal_string_11 = "tests/builtin/strcat.c:29";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
+ sizeof("tests/builtin/strcat.c:29"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
+ __gen_e_acsl_literal_string_10 = "tests/builtin/strcat.c:28";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
+ sizeof("tests/builtin/strcat.c:28"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
+ __gen_e_acsl_literal_string_9 = "tests/builtin/strcat.c:27";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
+ sizeof("tests/builtin/strcat.c:27"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
+ __gen_e_acsl_literal_string_8 = "tests/builtin/strcat.c:26";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
+ sizeof("tests/builtin/strcat.c:26"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
+ __gen_e_acsl_literal_string_6 = "abcd";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
+ sizeof("abcd"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
+ __gen_e_acsl_literal_string = "TEST %d: ";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+ sizeof("TEST %d: "));
+ __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 = "OK: Expected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("OK: Expected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
+ sizeof("OK: Expected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
+ __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
+ sizeof("FAIL: Unexpected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
+ __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
+ sizeof("FAIL: Unexpected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
+ __gen_e_acsl_literal_string_7 = "";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,sizeof(""));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strncat),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strncat));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strcat),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strcat));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_waitpid),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_waitpid));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
+ __e_acsl_store_block((void *)(& __fc_p_strerror),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_strerror));
+ __e_acsl_store_block((void *)(strerror),(size_t)64);
+ __e_acsl_full_init((void *)(& strerror));
+ __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_strtok_ptr));
+ __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
+ __e_acsl_full_init((void *)(& signal_eval));
+ __e_acsl_store_block((void *)(& testno),(size_t)4);
+ __e_acsl_full_init((void *)(& testno));
+ __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
+ __e_acsl_full_init((void *)(& __fc_time));
+ __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_fopen));
+ __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+ __e_acsl_full_init((void *)(& __fc_fopen));
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ }
return;
}
@@ -247,11 +258,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& pd4),(size_t)8);
__e_acsl_full_init((void *)(& pd4));
{
- int tmp_0;
- __e_acsl_store_block((void *)(& tmp_0),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_0));
- tmp_0 = fork();
- pid_t pid = (unsigned int)tmp_0;
+ pid_t pid = fork();
__e_acsl_store_block((void *)(& pid),(size_t)4);
__e_acsl_full_init((void *)(& pid));
if (! pid) {
@@ -261,20 +268,15 @@ int main(int argc, char const **argv)
else {
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
- /*@ assert Value: initialization: \initialized(&process_status); */
+ __gen_e_acsl_waitpid(pid,& process_status,0);
+ /*@ assert Eva: initialization: \initialized(&process_status); */
signal_eval(process_status,0,__gen_e_acsl_literal_string_8);
__e_acsl_delete_block((void *)(& process_status));
}
- __e_acsl_delete_block((void *)(& tmp_0));
__e_acsl_delete_block((void *)(& pid));
}
{
- int tmp_1;
- __e_acsl_store_block((void *)(& tmp_1),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_1));
- tmp_1 = fork();
- pid_t pid_0 = (unsigned int)tmp_1;
+ pid_t pid_0 = fork();
__e_acsl_store_block((void *)(& pid_0),(size_t)4);
__e_acsl_full_init((void *)(& pid_0));
if (! pid_0) {
@@ -284,20 +286,15 @@ int main(int argc, char const **argv)
else {
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
- /*@ assert Value: initialization: \initialized(&process_status_0); */
+ __gen_e_acsl_waitpid(pid_0,& process_status_0,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_0); */
signal_eval(process_status_0,0,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status_0));
}
- __e_acsl_delete_block((void *)(& tmp_1));
__e_acsl_delete_block((void *)(& pid_0));
}
{
- int tmp_2;
- __e_acsl_store_block((void *)(& tmp_2),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_2));
- tmp_2 = fork();
- pid_t pid_1 = (unsigned int)tmp_2;
+ pid_t pid_1 = fork();
__e_acsl_store_block((void *)(& pid_1),(size_t)4);
__e_acsl_full_init((void *)(& pid_1));
if (! pid_1) {
@@ -307,68 +304,53 @@ int main(int argc, char const **argv)
else {
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
- waitpid(pid_1,& process_status_1,0);
- /*@ assert Value: initialization: \initialized(&process_status_1); */
+ __gen_e_acsl_waitpid(pid_1,& process_status_1,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,1,__gen_e_acsl_literal_string_10);
__e_acsl_delete_block((void *)(& process_status_1));
}
- __e_acsl_delete_block((void *)(& tmp_2));
__e_acsl_delete_block((void *)(& pid_1));
}
{
- int tmp_3;
- __e_acsl_store_block((void *)(& tmp_3),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_3));
- tmp_3 = fork();
- pid_t pid_2 = (unsigned int)tmp_3;
+ pid_t pid_2 = fork();
__e_acsl_store_block((void *)(& pid_2),(size_t)4);
__e_acsl_full_init((void *)(& pid_2));
if (! pid_2) {
- /*@ assert Value: dangling_pointer: ¬\dangling(&unalloc_str); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strcat(unalloc_str,(char const *)const_str);
__gen_e_acsl_exit(0);
}
else {
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
- waitpid(pid_2,& process_status_2,0);
- /*@ assert Value: initialization: \initialized(&process_status_2); */
+ __gen_e_acsl_waitpid(pid_2,& process_status_2,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,1,__gen_e_acsl_literal_string_11);
__e_acsl_delete_block((void *)(& process_status_2));
}
- __e_acsl_delete_block((void *)(& tmp_3));
__e_acsl_delete_block((void *)(& pid_2));
}
{
- int tmp_4;
- __e_acsl_store_block((void *)(& tmp_4),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_4));
- tmp_4 = fork();
- pid_t pid_3 = (unsigned int)tmp_4;
+ pid_t pid_3 = fork();
__e_acsl_store_block((void *)(& pid_3),(size_t)4);
__e_acsl_full_init((void *)(& pid_3));
if (! pid_3) {
- /*@ assert Value: dangling_pointer: ¬\dangling(&unalloc_str); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strcat(dest2,(char const *)unalloc_str);
__gen_e_acsl_exit(0);
}
else {
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
- waitpid(pid_3,& process_status_3,0);
- /*@ assert Value: initialization: \initialized(&process_status_3); */
+ __gen_e_acsl_waitpid(pid_3,& process_status_3,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_3); */
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_3));
}
- __e_acsl_delete_block((void *)(& tmp_4));
__e_acsl_delete_block((void *)(& pid_3));
}
{
- int tmp_5;
- __e_acsl_store_block((void *)(& tmp_5),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_5));
- tmp_5 = fork();
- pid_t pid_4 = (unsigned int)tmp_5;
+ pid_t pid_4 = fork();
__e_acsl_store_block((void *)(& pid_4),(size_t)4);
__e_acsl_full_init((void *)(& pid_4));
if (! pid_4) {
@@ -378,20 +360,15 @@ int main(int argc, char const **argv)
else {
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
- waitpid(pid_4,& process_status_4,0);
- /*@ assert Value: initialization: \initialized(&process_status_4); */
+ __gen_e_acsl_waitpid(pid_4,& process_status_4,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_4); */
signal_eval(process_status_4,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_4));
}
- __e_acsl_delete_block((void *)(& tmp_5));
__e_acsl_delete_block((void *)(& pid_4));
}
{
- int tmp_6;
- __e_acsl_store_block((void *)(& tmp_6),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_6));
- tmp_6 = fork();
- pid_t pid_5 = (unsigned int)tmp_6;
+ pid_t pid_5 = fork();
__e_acsl_store_block((void *)(& pid_5),(size_t)4);
__e_acsl_full_init((void *)(& pid_5));
if (! pid_5) {
@@ -401,20 +378,15 @@ int main(int argc, char const **argv)
else {
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
- waitpid(pid_5,& process_status_5,0);
- /*@ assert Value: initialization: \initialized(&process_status_5); */
+ __gen_e_acsl_waitpid(pid_5,& process_status_5,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_5); */
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_5));
}
- __e_acsl_delete_block((void *)(& tmp_6));
__e_acsl_delete_block((void *)(& pid_5));
}
{
- int tmp_7;
- __e_acsl_store_block((void *)(& tmp_7),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_7));
- tmp_7 = fork();
- pid_t pid_6 = (unsigned int)tmp_7;
+ pid_t pid_6 = fork();
__e_acsl_store_block((void *)(& pid_6),(size_t)4);
__e_acsl_full_init((void *)(& pid_6));
if (! pid_6) {
@@ -424,20 +396,15 @@ int main(int argc, char const **argv)
else {
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
- waitpid(pid_6,& process_status_6,0);
- /*@ assert Value: initialization: \initialized(&process_status_6); */
+ __gen_e_acsl_waitpid(pid_6,& process_status_6,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_6); */
signal_eval(process_status_6,1,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_6));
}
- __e_acsl_delete_block((void *)(& tmp_7));
__e_acsl_delete_block((void *)(& pid_6));
}
{
- int tmp_8;
- __e_acsl_store_block((void *)(& tmp_8),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_8));
- tmp_8 = fork();
- pid_t pid_7 = (unsigned int)tmp_8;
+ pid_t pid_7 = fork();
__e_acsl_store_block((void *)(& pid_7),(size_t)4);
__e_acsl_full_init((void *)(& pid_7));
if (! pid_7) {
@@ -447,20 +414,15 @@ int main(int argc, char const **argv)
else {
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
- waitpid(pid_7,& process_status_7,0);
- /*@ assert Value: initialization: \initialized(&process_status_7); */
+ __gen_e_acsl_waitpid(pid_7,& process_status_7,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_7); */
signal_eval(process_status_7,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_7));
}
- __e_acsl_delete_block((void *)(& tmp_8));
__e_acsl_delete_block((void *)(& pid_7));
}
{
- int tmp_9;
- __e_acsl_store_block((void *)(& tmp_9),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_9));
- tmp_9 = fork();
- pid_t pid_8 = (unsigned int)tmp_9;
+ pid_t pid_8 = fork();
__e_acsl_store_block((void *)(& pid_8),(size_t)4);
__e_acsl_full_init((void *)(& pid_8));
if (! pid_8) {
@@ -470,20 +432,15 @@ int main(int argc, char const **argv)
else {
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
- waitpid(pid_8,& process_status_8,0);
- /*@ assert Value: initialization: \initialized(&process_status_8); */
+ __gen_e_acsl_waitpid(pid_8,& process_status_8,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_8); */
signal_eval(process_status_8,1,__gen_e_acsl_literal_string_17);
__e_acsl_delete_block((void *)(& process_status_8));
}
- __e_acsl_delete_block((void *)(& tmp_9));
__e_acsl_delete_block((void *)(& pid_8));
}
{
- int tmp_10;
- __e_acsl_store_block((void *)(& tmp_10),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_10));
- tmp_10 = fork();
- pid_t pid_9 = (unsigned int)tmp_10;
+ pid_t pid_9 = fork();
__e_acsl_store_block((void *)(& pid_9),(size_t)4);
__e_acsl_full_init((void *)(& pid_9));
if (! pid_9) {
@@ -493,20 +450,15 @@ int main(int argc, char const **argv)
else {
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
- waitpid(pid_9,& process_status_9,0);
- /*@ assert Value: initialization: \initialized(&process_status_9); */
+ __gen_e_acsl_waitpid(pid_9,& process_status_9,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_9); */
signal_eval(process_status_9,1,__gen_e_acsl_literal_string_18);
__e_acsl_delete_block((void *)(& process_status_9));
}
- __e_acsl_delete_block((void *)(& tmp_10));
__e_acsl_delete_block((void *)(& pid_9));
}
{
- int tmp_11;
- __e_acsl_store_block((void *)(& tmp_11),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_11));
- tmp_11 = fork();
- pid_t pid_10 = (unsigned int)tmp_11;
+ pid_t pid_10 = fork();
__e_acsl_store_block((void *)(& pid_10),(size_t)4);
__e_acsl_full_init((void *)(& pid_10));
if (! pid_10) {
@@ -518,20 +470,15 @@ int main(int argc, char const **argv)
else {
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
- waitpid(pid_10,& process_status_10,0);
- /*@ assert Value: initialization: \initialized(&process_status_10); */
+ __gen_e_acsl_waitpid(pid_10,& process_status_10,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_10); */
signal_eval(process_status_10,0,__gen_e_acsl_literal_string_19);
__e_acsl_delete_block((void *)(& process_status_10));
}
- __e_acsl_delete_block((void *)(& tmp_11));
__e_acsl_delete_block((void *)(& pid_10));
}
{
- int tmp_12;
- __e_acsl_store_block((void *)(& tmp_12),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_12));
- tmp_12 = fork();
- pid_t pid_11 = (unsigned int)tmp_12;
+ pid_t pid_11 = fork();
__e_acsl_store_block((void *)(& pid_11),(size_t)4);
__e_acsl_full_init((void *)(& pid_11));
if (! pid_11) {
@@ -541,20 +488,15 @@ int main(int argc, char const **argv)
else {
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
- waitpid(pid_11,& process_status_11,0);
- /*@ assert Value: initialization: \initialized(&process_status_11); */
+ __gen_e_acsl_waitpid(pid_11,& process_status_11,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_11); */
signal_eval(process_status_11,0,__gen_e_acsl_literal_string_20);
__e_acsl_delete_block((void *)(& process_status_11));
}
- __e_acsl_delete_block((void *)(& tmp_12));
__e_acsl_delete_block((void *)(& pid_11));
}
{
- int tmp_13;
- __e_acsl_store_block((void *)(& tmp_13),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_13));
- tmp_13 = fork();
- pid_t pid_12 = (unsigned int)tmp_13;
+ pid_t pid_12 = fork();
__e_acsl_store_block((void *)(& pid_12),(size_t)4);
__e_acsl_full_init((void *)(& pid_12));
if (! pid_12) {
@@ -564,24 +506,19 @@ int main(int argc, char const **argv)
else {
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
- waitpid(pid_12,& process_status_12,0);
- /*@ assert Value: initialization: \initialized(&process_status_12); */
+ __gen_e_acsl_waitpid(pid_12,& process_status_12,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_12); */
signal_eval(process_status_12,1,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_12));
}
- __e_acsl_delete_block((void *)(& tmp_13));
__e_acsl_delete_block((void *)(& pid_12));
}
{
- int tmp_14;
- __e_acsl_store_block((void *)(& tmp_14),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_14));
- tmp_14 = fork();
- pid_t pid_13 = (unsigned int)tmp_14;
+ pid_t pid_13 = fork();
__e_acsl_store_block((void *)(& pid_13),(size_t)4);
__e_acsl_full_init((void *)(& pid_13));
if (! pid_13) {
- /*@ assert Value: dangling_pointer: ¬\dangling(&unalloc_str); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strncat(unalloc_str,(char const *)const_str,
(unsigned long)1);
__gen_e_acsl_exit(0);
@@ -589,44 +526,34 @@ int main(int argc, char const **argv)
else {
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
- waitpid(pid_13,& process_status_13,0);
- /*@ assert Value: initialization: \initialized(&process_status_13); */
+ __gen_e_acsl_waitpid(pid_13,& process_status_13,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_13); */
signal_eval(process_status_13,1,__gen_e_acsl_literal_string_22);
__e_acsl_delete_block((void *)(& process_status_13));
}
- __e_acsl_delete_block((void *)(& tmp_14));
__e_acsl_delete_block((void *)(& pid_13));
}
{
- int tmp_15;
- __e_acsl_store_block((void *)(& tmp_15),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_15));
- tmp_15 = fork();
- pid_t pid_14 = (unsigned int)tmp_15;
+ pid_t pid_14 = fork();
__e_acsl_store_block((void *)(& pid_14),(size_t)4);
__e_acsl_full_init((void *)(& pid_14));
if (! pid_14) {
- /*@ assert Value: dangling_pointer: ¬\dangling(&unalloc_str); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strncat(dest2,(char const *)unalloc_str,(unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
- waitpid(pid_14,& process_status_14,0);
- /*@ assert Value: initialization: \initialized(&process_status_14); */
+ __gen_e_acsl_waitpid(pid_14,& process_status_14,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_14); */
signal_eval(process_status_14,1,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_14));
}
- __e_acsl_delete_block((void *)(& tmp_15));
__e_acsl_delete_block((void *)(& pid_14));
}
{
- int tmp_16;
- __e_acsl_store_block((void *)(& tmp_16),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_16));
- tmp_16 = fork();
- pid_t pid_15 = (unsigned int)tmp_16;
+ pid_t pid_15 = fork();
__e_acsl_store_block((void *)(& pid_15),(size_t)4);
__e_acsl_full_init((void *)(& pid_15));
if (! pid_15) {
@@ -637,20 +564,15 @@ int main(int argc, char const **argv)
else {
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
- waitpid(pid_15,& process_status_15,0);
- /*@ assert Value: initialization: \initialized(&process_status_15); */
+ __gen_e_acsl_waitpid(pid_15,& process_status_15,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_15); */
signal_eval(process_status_15,1,__gen_e_acsl_literal_string_24);
__e_acsl_delete_block((void *)(& process_status_15));
}
- __e_acsl_delete_block((void *)(& tmp_16));
__e_acsl_delete_block((void *)(& pid_15));
}
{
- int tmp_17;
- __e_acsl_store_block((void *)(& tmp_17),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_17));
- tmp_17 = fork();
- pid_t pid_16 = (unsigned int)tmp_17;
+ pid_t pid_16 = fork();
__e_acsl_store_block((void *)(& pid_16),(size_t)4);
__e_acsl_full_init((void *)(& pid_16));
if (! pid_16) {
@@ -660,20 +582,15 @@ int main(int argc, char const **argv)
else {
int process_status_16;
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
- waitpid(pid_16,& process_status_16,0);
- /*@ assert Value: initialization: \initialized(&process_status_16); */
+ __gen_e_acsl_waitpid(pid_16,& process_status_16,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_16); */
signal_eval(process_status_16,1,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_16));
}
- __e_acsl_delete_block((void *)(& tmp_17));
__e_acsl_delete_block((void *)(& pid_16));
}
{
- int tmp_18;
- __e_acsl_store_block((void *)(& tmp_18),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_18));
- tmp_18 = fork();
- pid_t pid_17 = (unsigned int)tmp_18;
+ pid_t pid_17 = fork();
__e_acsl_store_block((void *)(& pid_17),(size_t)4);
__e_acsl_full_init((void *)(& pid_17));
if (! pid_17) {
@@ -684,20 +601,15 @@ int main(int argc, char const **argv)
else {
int process_status_17;
__e_acsl_store_block((void *)(& process_status_17),(size_t)4);
- waitpid(pid_17,& process_status_17,0);
- /*@ assert Value: initialization: \initialized(&process_status_17); */
+ __gen_e_acsl_waitpid(pid_17,& process_status_17,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_17); */
signal_eval(process_status_17,1,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_17));
}
- __e_acsl_delete_block((void *)(& tmp_18));
__e_acsl_delete_block((void *)(& pid_17));
}
{
- int tmp_19;
- __e_acsl_store_block((void *)(& tmp_19),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_19));
- tmp_19 = fork();
- pid_t pid_18 = (unsigned int)tmp_19;
+ pid_t pid_18 = fork();
__e_acsl_store_block((void *)(& pid_18),(size_t)4);
__e_acsl_full_init((void *)(& pid_18));
if (! pid_18) {
@@ -707,20 +619,15 @@ int main(int argc, char const **argv)
else {
int process_status_18;
__e_acsl_store_block((void *)(& process_status_18),(size_t)4);
- waitpid(pid_18,& process_status_18,0);
- /*@ assert Value: initialization: \initialized(&process_status_18); */
+ __gen_e_acsl_waitpid(pid_18,& process_status_18,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_18); */
signal_eval(process_status_18,1,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_18));
}
- __e_acsl_delete_block((void *)(& tmp_19));
__e_acsl_delete_block((void *)(& pid_18));
}
{
- int tmp_20;
- __e_acsl_store_block((void *)(& tmp_20),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_20));
- tmp_20 = fork();
- pid_t pid_19 = (unsigned int)tmp_20;
+ pid_t pid_19 = fork();
__e_acsl_store_block((void *)(& pid_19),(size_t)4);
__e_acsl_full_init((void *)(& pid_19));
if (! pid_19) {
@@ -730,20 +637,15 @@ int main(int argc, char const **argv)
else {
int process_status_19;
__e_acsl_store_block((void *)(& process_status_19),(size_t)4);
- waitpid(pid_19,& process_status_19,0);
- /*@ assert Value: initialization: \initialized(&process_status_19); */
+ __gen_e_acsl_waitpid(pid_19,& process_status_19,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_19); */
signal_eval(process_status_19,1,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_19));
}
- __e_acsl_delete_block((void *)(& tmp_20));
__e_acsl_delete_block((void *)(& pid_19));
}
{
- int tmp_21;
- __e_acsl_store_block((void *)(& tmp_21),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_21));
- tmp_21 = fork();
- pid_t pid_20 = (unsigned int)tmp_21;
+ pid_t pid_20 = fork();
__e_acsl_store_block((void *)(& pid_20),(size_t)4);
__e_acsl_full_init((void *)(& pid_20));
if (! pid_20) {
@@ -753,18 +655,19 @@ int main(int argc, char const **argv)
else {
int process_status_20;
__e_acsl_store_block((void *)(& process_status_20),(size_t)4);
- waitpid(pid_20,& process_status_20,0);
- /*@ assert Value: initialization: \initialized(&process_status_20); */
+ __gen_e_acsl_waitpid(pid_20,& process_status_20,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_20); */
signal_eval(process_status_20,1,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_20));
}
- __e_acsl_delete_block((void *)(& tmp_21));
__e_acsl_delete_block((void *)(& pid_20));
}
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
__e_acsl_delete_block((void *)(& argv));
__e_acsl_delete_block((void *)(& argc));
+ __e_acsl_delete_block((void *)(& __fc_p_strerror));
+ __e_acsl_delete_block((void *)(strerror));
__e_acsl_delete_block((void *)(& __fc_strtok_ptr));
__e_acsl_delete_block((void *)(& signal_eval));
__e_acsl_delete_block((void *)(& testno));
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 1d298cab5254eb6b868afb69ac8896ecd0b2cc4f..f107a44c9f516b82a79cd44b54d491aa01d51312 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -55,197 +55,207 @@ __inline static void fail_ncomp(int cond, char *fmt, int l, int r)
/*@ assigns \result;
assigns \result \from \nothing; */
-extern int ( /* missing proto */ fork)();
+extern int ( /* missing proto */ fork)(void);
void __e_acsl_globals_init(void)
{
- __gen_e_acsl_literal_string_32 = "tests/builtin/strcmp.c:74";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_32,
- sizeof("tests/builtin/strcmp.c:74"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_32);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_32);
- __gen_e_acsl_literal_string_31 = "tests/builtin/strcmp.c:73";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
- sizeof("tests/builtin/strcmp.c:73"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
- __gen_e_acsl_literal_string_30 = "tests/builtin/strcmp.c:72";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
- sizeof("tests/builtin/strcmp.c:72"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
- __gen_e_acsl_literal_string_29 = "tests/builtin/strcmp.c:71";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
- sizeof("tests/builtin/strcmp.c:71"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
- __gen_e_acsl_literal_string_28 = "tests/builtin/strcmp.c:68";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
- sizeof("tests/builtin/strcmp.c:68"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
- __gen_e_acsl_literal_string_27 = "tests/builtin/strcmp.c:67";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
- sizeof("tests/builtin/strcmp.c:67"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
- __gen_e_acsl_literal_string_26 = "tests/builtin/strcmp.c:66";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
- sizeof("tests/builtin/strcmp.c:66"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
- __gen_e_acsl_literal_string_25 = "tests/builtin/strcmp.c:65";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
- sizeof("tests/builtin/strcmp.c:65"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
- __gen_e_acsl_literal_string_23 = "tests/builtin/strcmp.c:62";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/builtin/strcmp.c:62"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
- __gen_e_acsl_literal_string_22 = "tests/builtin/strcmp.c:61";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
- sizeof("tests/builtin/strcmp.c:61"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_21 = "tests/builtin/strcmp.c:59";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
- sizeof("tests/builtin/strcmp.c:59"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
- __gen_e_acsl_literal_string_20 = "tests/builtin/strcmp.c:58";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
- sizeof("tests/builtin/strcmp.c:58"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_19 = "tests/builtin/strcmp.c:57";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
- sizeof("tests/builtin/strcmp.c:57"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
- __gen_e_acsl_literal_string_18 = "tests/builtin/strcmp.c:48";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
- sizeof("tests/builtin/strcmp.c:48"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_17 = "tests/builtin/strcmp.c:47";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
- sizeof("tests/builtin/strcmp.c:47"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
- __gen_e_acsl_literal_string_16 = "tests/builtin/strcmp.c:42";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/builtin/strcmp.c:42"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
- __gen_e_acsl_literal_string_15 = "tests/builtin/strcmp.c:41";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/builtin/strcmp.c:41"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/builtin/strcmp.c:39";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/builtin/strcmp.c:39"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/builtin/strcmp.c:38";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/builtin/strcmp.c:38"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/builtin/strcmp.c:37";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/builtin/strcmp.c:37"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_11 = "tests/builtin/strcmp.c:36";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/builtin/strcmp.c:36"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_10 = "tests/builtin/strcmp.c:34";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("tests/builtin/strcmp.c:34"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_9 = "tests/builtin/strcmp.c:33";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/builtin/strcmp.c:33"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_8 = "tests/builtin/strcmp.c:32";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("tests/builtin/strcmp.c:32"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __gen_e_acsl_literal_string_7 = "comparison failure: %d == %d\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
- sizeof("comparison failure: %d == %d\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
- __gen_e_acsl_literal_string_24 = "comparison failure: %d != %d\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("comparison failure: %d != %d\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
- __gen_e_acsl_literal_string_6 = "abc";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("abc"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
- __gen_e_acsl_literal_string = "TEST %d: ";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("TEST %d: "));
- __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 = "OK: Expected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("OK: Expected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
- sizeof("OK: Expected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
- sizeof("FAIL: Unexpected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
- __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
- sizeof("FAIL: Unexpected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_store_block((void *)(& __gen_e_acsl_strdup),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strdup));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strncmp),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strncmp));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strcmp),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strcmp));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
- __e_acsl_store_block((void *)(& fail_ncomp),(size_t)1);
- __e_acsl_full_init((void *)(& fail_ncomp));
- __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_strtok_ptr));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& testno),(size_t)4);
- __e_acsl_full_init((void *)(& testno));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& stderr),(size_t)8);
- __e_acsl_full_init((void *)(& stderr));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __gen_e_acsl_literal_string_32 = "tests/builtin/strcmp.c:74";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_32,
+ sizeof("tests/builtin/strcmp.c:74"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_32);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_32);
+ __gen_e_acsl_literal_string_31 = "tests/builtin/strcmp.c:73";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_31,
+ sizeof("tests/builtin/strcmp.c:73"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_31);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_31);
+ __gen_e_acsl_literal_string_30 = "tests/builtin/strcmp.c:72";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_30,
+ sizeof("tests/builtin/strcmp.c:72"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_30);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_30);
+ __gen_e_acsl_literal_string_29 = "tests/builtin/strcmp.c:71";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_29,
+ sizeof("tests/builtin/strcmp.c:71"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_29);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_29);
+ __gen_e_acsl_literal_string_28 = "tests/builtin/strcmp.c:68";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_28,
+ sizeof("tests/builtin/strcmp.c:68"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_28);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_28);
+ __gen_e_acsl_literal_string_27 = "tests/builtin/strcmp.c:67";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_27,
+ sizeof("tests/builtin/strcmp.c:67"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_27);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_27);
+ __gen_e_acsl_literal_string_26 = "tests/builtin/strcmp.c:66";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_26,
+ sizeof("tests/builtin/strcmp.c:66"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_26);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_26);
+ __gen_e_acsl_literal_string_25 = "tests/builtin/strcmp.c:65";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_25,
+ sizeof("tests/builtin/strcmp.c:65"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_25);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_25);
+ __gen_e_acsl_literal_string_23 = "tests/builtin/strcmp.c:62";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
+ sizeof("tests/builtin/strcmp.c:62"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
+ __gen_e_acsl_literal_string_22 = "tests/builtin/strcmp.c:61";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
+ sizeof("tests/builtin/strcmp.c:61"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_21 = "tests/builtin/strcmp.c:59";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
+ sizeof("tests/builtin/strcmp.c:59"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
+ __gen_e_acsl_literal_string_20 = "tests/builtin/strcmp.c:58";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
+ sizeof("tests/builtin/strcmp.c:58"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
+ __gen_e_acsl_literal_string_19 = "tests/builtin/strcmp.c:57";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
+ sizeof("tests/builtin/strcmp.c:57"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
+ __gen_e_acsl_literal_string_18 = "tests/builtin/strcmp.c:48";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
+ sizeof("tests/builtin/strcmp.c:48"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
+ __gen_e_acsl_literal_string_17 = "tests/builtin/strcmp.c:47";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
+ sizeof("tests/builtin/strcmp.c:47"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
+ __gen_e_acsl_literal_string_16 = "tests/builtin/strcmp.c:42";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
+ sizeof("tests/builtin/strcmp.c:42"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
+ __gen_e_acsl_literal_string_15 = "tests/builtin/strcmp.c:41";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
+ sizeof("tests/builtin/strcmp.c:41"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
+ __gen_e_acsl_literal_string_14 = "tests/builtin/strcmp.c:39";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
+ sizeof("tests/builtin/strcmp.c:39"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
+ __gen_e_acsl_literal_string_13 = "tests/builtin/strcmp.c:38";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
+ sizeof("tests/builtin/strcmp.c:38"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
+ __gen_e_acsl_literal_string_12 = "tests/builtin/strcmp.c:37";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
+ sizeof("tests/builtin/strcmp.c:37"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
+ __gen_e_acsl_literal_string_11 = "tests/builtin/strcmp.c:36";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
+ sizeof("tests/builtin/strcmp.c:36"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
+ __gen_e_acsl_literal_string_10 = "tests/builtin/strcmp.c:34";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
+ sizeof("tests/builtin/strcmp.c:34"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
+ __gen_e_acsl_literal_string_9 = "tests/builtin/strcmp.c:33";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
+ sizeof("tests/builtin/strcmp.c:33"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
+ __gen_e_acsl_literal_string_8 = "tests/builtin/strcmp.c:32";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
+ sizeof("tests/builtin/strcmp.c:32"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
+ __gen_e_acsl_literal_string_7 = "comparison failure: %d == %d\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
+ sizeof("comparison failure: %d == %d\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
+ __gen_e_acsl_literal_string_24 = "comparison failure: %d != %d\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
+ sizeof("comparison failure: %d != %d\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
+ __gen_e_acsl_literal_string_6 = "abc";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("abc"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
+ __gen_e_acsl_literal_string = "TEST %d: ";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+ sizeof("TEST %d: "));
+ __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 = "OK: Expected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("OK: Expected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
+ sizeof("OK: Expected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
+ __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
+ sizeof("FAIL: Unexpected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
+ __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
+ sizeof("FAIL: Unexpected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strdup),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strdup));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strncmp),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strncmp));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strcmp),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strcmp));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_waitpid),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_waitpid));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
+ __e_acsl_store_block((void *)(& fail_ncomp),(size_t)1);
+ __e_acsl_full_init((void *)(& fail_ncomp));
+ __e_acsl_store_block((void *)(& __fc_p_strerror),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_strerror));
+ __e_acsl_store_block((void *)(strerror),(size_t)64);
+ __e_acsl_full_init((void *)(& strerror));
+ __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_strtok_ptr));
+ __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
+ __e_acsl_full_init((void *)(& signal_eval));
+ __e_acsl_store_block((void *)(& testno),(size_t)4);
+ __e_acsl_full_init((void *)(& testno));
+ __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
+ __e_acsl_full_init((void *)(& __fc_time));
+ __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_fopen));
+ __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+ __e_acsl_full_init((void *)(& __fc_fopen));
+ __e_acsl_store_block((void *)(& stderr),(size_t)8);
+ __e_acsl_full_init((void *)(& stderr));
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ }
return;
}
@@ -276,11 +286,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& dr),(size_t)8);
__e_acsl_full_init((void *)(& dr));
{
- int tmp_1;
- __e_acsl_store_block((void *)(& tmp_1),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_1));
- tmp_1 = fork();
- pid_t pid = (unsigned int)tmp_1;
+ pid_t pid = fork();
__e_acsl_store_block((void *)(& pid),(size_t)4);
__e_acsl_full_init((void *)(& pid));
if (! pid) {
@@ -300,19 +306,15 @@ int main(int argc, char const **argv)
else {
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
+ __gen_e_acsl_waitpid(pid,& process_status,0);
+ /*@ assert Eva: initialization: \initialized(&process_status); */
signal_eval(process_status,0,__gen_e_acsl_literal_string_8);
__e_acsl_delete_block((void *)(& process_status));
}
- __e_acsl_delete_block((void *)(& tmp_1));
__e_acsl_delete_block((void *)(& pid));
}
{
- int tmp_4;
- __e_acsl_store_block((void *)(& tmp_4),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_4));
- tmp_4 = fork();
- pid_t pid_0 = (unsigned int)tmp_4;
+ pid_t pid_0 = fork();
__e_acsl_store_block((void *)(& pid_0),(size_t)4);
__e_acsl_full_init((void *)(& pid_0));
if (! pid_0) {
@@ -332,19 +334,15 @@ int main(int argc, char const **argv)
else {
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
+ __gen_e_acsl_waitpid(pid_0,& process_status_0,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_0); */
signal_eval(process_status_0,0,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status_0));
}
- __e_acsl_delete_block((void *)(& tmp_4));
__e_acsl_delete_block((void *)(& pid_0));
}
{
- int tmp_7;
- __e_acsl_store_block((void *)(& tmp_7),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_7));
- tmp_7 = fork();
- pid_t pid_1 = (unsigned int)tmp_7;
+ pid_t pid_1 = fork();
__e_acsl_store_block((void *)(& pid_1),(size_t)4);
__e_acsl_full_init((void *)(& pid_1));
if (! pid_1) {
@@ -364,19 +362,15 @@ int main(int argc, char const **argv)
else {
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
- waitpid(pid_1,& process_status_1,0);
+ __gen_e_acsl_waitpid(pid_1,& process_status_1,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,0,__gen_e_acsl_literal_string_10);
__e_acsl_delete_block((void *)(& process_status_1));
}
- __e_acsl_delete_block((void *)(& tmp_7));
__e_acsl_delete_block((void *)(& pid_1));
}
{
- int tmp_10;
- __e_acsl_store_block((void *)(& tmp_10),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_10));
- tmp_10 = fork();
- pid_t pid_2 = (unsigned int)tmp_10;
+ pid_t pid_2 = fork();
__e_acsl_store_block((void *)(& pid_2),(size_t)4);
__e_acsl_full_init((void *)(& pid_2));
if (! pid_2) {
@@ -398,19 +392,15 @@ int main(int argc, char const **argv)
else {
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
- waitpid(pid_2,& process_status_2,0);
+ __gen_e_acsl_waitpid(pid_2,& process_status_2,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,1,__gen_e_acsl_literal_string_11);
__e_acsl_delete_block((void *)(& process_status_2));
}
- __e_acsl_delete_block((void *)(& tmp_10));
__e_acsl_delete_block((void *)(& pid_2));
}
{
- int tmp_13;
- __e_acsl_store_block((void *)(& tmp_13),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_13));
- tmp_13 = fork();
- pid_t pid_3 = (unsigned int)tmp_13;
+ pid_t pid_3 = fork();
__e_acsl_store_block((void *)(& pid_3),(size_t)4);
__e_acsl_full_init((void *)(& pid_3));
if (! pid_3) {
@@ -432,19 +422,15 @@ int main(int argc, char const **argv)
else {
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
- waitpid(pid_3,& process_status_3,0);
+ __gen_e_acsl_waitpid(pid_3,& process_status_3,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_3); */
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_3));
}
- __e_acsl_delete_block((void *)(& tmp_13));
__e_acsl_delete_block((void *)(& pid_3));
}
{
- int tmp_16;
- __e_acsl_store_block((void *)(& tmp_16),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_16));
- tmp_16 = fork();
- pid_t pid_4 = (unsigned int)tmp_16;
+ pid_t pid_4 = fork();
__e_acsl_store_block((void *)(& pid_4),(size_t)4);
__e_acsl_full_init((void *)(& pid_4));
if (! pid_4) {
@@ -453,6 +439,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& tmp_18),(size_t)4);
__e_acsl_store_block((void *)(& tmp_17),(size_t)4);
__e_acsl_initialize((void *)(dl + 3),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(dl + 3); */
*(dl + 3) = (char)'a';
__e_acsl_full_init((void *)(& tmp_17));
tmp_17 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
@@ -466,19 +453,15 @@ int main(int argc, char const **argv)
else {
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
- waitpid(pid_4,& process_status_4,0);
+ __gen_e_acsl_waitpid(pid_4,& process_status_4,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_4); */
signal_eval(process_status_4,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_4));
}
- __e_acsl_delete_block((void *)(& tmp_16));
__e_acsl_delete_block((void *)(& pid_4));
}
{
- int tmp_19;
- __e_acsl_store_block((void *)(& tmp_19),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_19));
- tmp_19 = fork();
- pid_t pid_5 = (unsigned int)tmp_19;
+ pid_t pid_5 = fork();
__e_acsl_store_block((void *)(& pid_5),(size_t)4);
__e_acsl_full_init((void *)(& pid_5));
if (! pid_5) {
@@ -487,6 +470,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& tmp_21),(size_t)4);
__e_acsl_store_block((void *)(& tmp_20),(size_t)4);
__e_acsl_initialize((void *)(dr + 3),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(dr + 3); */
*(dr + 3) = (char)'a';
__e_acsl_full_init((void *)(& tmp_20));
tmp_20 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
@@ -500,19 +484,15 @@ int main(int argc, char const **argv)
else {
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
- waitpid(pid_5,& process_status_5,0);
+ __gen_e_acsl_waitpid(pid_5,& process_status_5,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_5); */
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_5));
}
- __e_acsl_delete_block((void *)(& tmp_19));
__e_acsl_delete_block((void *)(& pid_5));
}
{
- int tmp_22;
- __e_acsl_store_block((void *)(& tmp_22),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_22));
- tmp_22 = fork();
- pid_t pid_6 = (unsigned int)tmp_22;
+ pid_t pid_6 = fork();
__e_acsl_store_block((void *)(& pid_6),(size_t)4);
__e_acsl_full_init((void *)(& pid_6));
if (! pid_6) {
@@ -532,19 +512,15 @@ int main(int argc, char const **argv)
else {
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
- waitpid(pid_6,& process_status_6,0);
+ __gen_e_acsl_waitpid(pid_6,& process_status_6,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_6); */
signal_eval(process_status_6,1,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_6));
}
- __e_acsl_delete_block((void *)(& tmp_22));
__e_acsl_delete_block((void *)(& pid_6));
}
{
- int tmp_25;
- __e_acsl_store_block((void *)(& tmp_25),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_25));
- tmp_25 = fork();
- pid_t pid_7 = (unsigned int)tmp_25;
+ pid_t pid_7 = fork();
__e_acsl_store_block((void *)(& pid_7),(size_t)4);
__e_acsl_full_init((void *)(& pid_7));
if (! pid_7) {
@@ -564,21 +540,17 @@ int main(int argc, char const **argv)
else {
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
- waitpid(pid_7,& process_status_7,0);
+ __gen_e_acsl_waitpid(pid_7,& process_status_7,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_7); */
signal_eval(process_status_7,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_7));
}
- __e_acsl_delete_block((void *)(& tmp_25));
__e_acsl_delete_block((void *)(& pid_7));
}
free((void *)dl);
free((void *)dr);
{
- int tmp_28;
- __e_acsl_store_block((void *)(& tmp_28),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_28));
- tmp_28 = fork();
- pid_t pid_8 = (unsigned int)tmp_28;
+ pid_t pid_8 = fork();
__e_acsl_store_block((void *)(& pid_8),(size_t)4);
__e_acsl_full_init((void *)(& pid_8));
if (! pid_8) {
@@ -598,19 +570,15 @@ int main(int argc, char const **argv)
else {
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
- waitpid(pid_8,& process_status_8,0);
+ __gen_e_acsl_waitpid(pid_8,& process_status_8,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_8); */
signal_eval(process_status_8,1,__gen_e_acsl_literal_string_17);
__e_acsl_delete_block((void *)(& process_status_8));
}
- __e_acsl_delete_block((void *)(& tmp_28));
__e_acsl_delete_block((void *)(& pid_8));
}
{
- int tmp_31;
- __e_acsl_store_block((void *)(& tmp_31),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_31));
- tmp_31 = fork();
- pid_t pid_9 = (unsigned int)tmp_31;
+ pid_t pid_9 = fork();
__e_acsl_store_block((void *)(& pid_9),(size_t)4);
__e_acsl_full_init((void *)(& pid_9));
if (! pid_9) {
@@ -630,11 +598,11 @@ int main(int argc, char const **argv)
else {
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
- waitpid(pid_9,& process_status_9,0);
+ __gen_e_acsl_waitpid(pid_9,& process_status_9,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_9); */
signal_eval(process_status_9,1,__gen_e_acsl_literal_string_18);
__e_acsl_delete_block((void *)(& process_status_9));
}
- __e_acsl_delete_block((void *)(& tmp_31));
__e_acsl_delete_block((void *)(& pid_9));
}
__e_acsl_full_init((void *)(& dl));
@@ -642,11 +610,7 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& dr));
dr = __gen_e_acsl_strdup(__gen_e_acsl_literal_string_6);
{
- int tmp_34;
- __e_acsl_store_block((void *)(& tmp_34),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_34));
- tmp_34 = fork();
- pid_t pid_10 = (unsigned int)tmp_34;
+ pid_t pid_10 = fork();
__e_acsl_store_block((void *)(& pid_10),(size_t)4);
__e_acsl_full_init((void *)(& pid_10));
if (! pid_10) {
@@ -666,19 +630,15 @@ int main(int argc, char const **argv)
else {
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
- waitpid(pid_10,& process_status_10,0);
+ __gen_e_acsl_waitpid(pid_10,& process_status_10,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_10); */
signal_eval(process_status_10,0,__gen_e_acsl_literal_string_19);
__e_acsl_delete_block((void *)(& process_status_10));
}
- __e_acsl_delete_block((void *)(& tmp_34));
__e_acsl_delete_block((void *)(& pid_10));
}
{
- int tmp_37;
- __e_acsl_store_block((void *)(& tmp_37),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_37));
- tmp_37 = fork();
- pid_t pid_11 = (unsigned int)tmp_37;
+ pid_t pid_11 = fork();
__e_acsl_store_block((void *)(& pid_11),(size_t)4);
__e_acsl_full_init((void *)(& pid_11));
if (! pid_11) {
@@ -700,19 +660,15 @@ int main(int argc, char const **argv)
else {
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
- waitpid(pid_11,& process_status_11,0);
+ __gen_e_acsl_waitpid(pid_11,& process_status_11,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_11); */
signal_eval(process_status_11,0,__gen_e_acsl_literal_string_20);
__e_acsl_delete_block((void *)(& process_status_11));
}
- __e_acsl_delete_block((void *)(& tmp_37));
__e_acsl_delete_block((void *)(& pid_11));
}
{
- int tmp_40;
- __e_acsl_store_block((void *)(& tmp_40),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_40));
- tmp_40 = fork();
- pid_t pid_12 = (unsigned int)tmp_40;
+ pid_t pid_12 = fork();
__e_acsl_store_block((void *)(& pid_12),(size_t)4);
__e_acsl_full_init((void *)(& pid_12));
if (! pid_12) {
@@ -734,19 +690,15 @@ int main(int argc, char const **argv)
else {
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
- waitpid(pid_12,& process_status_12,0);
+ __gen_e_acsl_waitpid(pid_12,& process_status_12,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_12); */
signal_eval(process_status_12,0,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_12));
}
- __e_acsl_delete_block((void *)(& tmp_40));
__e_acsl_delete_block((void *)(& pid_12));
}
{
- int tmp_43;
- __e_acsl_store_block((void *)(& tmp_43),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_43));
- tmp_43 = fork();
- pid_t pid_13 = (unsigned int)tmp_43;
+ pid_t pid_13 = fork();
__e_acsl_store_block((void *)(& pid_13),(size_t)4);
__e_acsl_full_init((void *)(& pid_13));
if (! pid_13) {
@@ -768,19 +720,15 @@ int main(int argc, char const **argv)
else {
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
- waitpid(pid_13,& process_status_13,0);
+ __gen_e_acsl_waitpid(pid_13,& process_status_13,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_13); */
signal_eval(process_status_13,0,__gen_e_acsl_literal_string_22);
__e_acsl_delete_block((void *)(& process_status_13));
}
- __e_acsl_delete_block((void *)(& tmp_43));
__e_acsl_delete_block((void *)(& pid_13));
}
{
- int tmp_46;
- __e_acsl_store_block((void *)(& tmp_46),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_46));
- tmp_46 = fork();
- pid_t pid_14 = (unsigned int)tmp_46;
+ pid_t pid_14 = fork();
__e_acsl_store_block((void *)(& pid_14),(size_t)4);
__e_acsl_full_init((void *)(& pid_14));
if (! pid_14) {
@@ -802,19 +750,15 @@ int main(int argc, char const **argv)
else {
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
- waitpid(pid_14,& process_status_14,0);
+ __gen_e_acsl_waitpid(pid_14,& process_status_14,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_14); */
signal_eval(process_status_14,0,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_14));
}
- __e_acsl_delete_block((void *)(& tmp_46));
__e_acsl_delete_block((void *)(& pid_14));
}
{
- int tmp_49;
- __e_acsl_store_block((void *)(& tmp_49),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_49));
- tmp_49 = fork();
- pid_t pid_15 = (unsigned int)tmp_49;
+ pid_t pid_15 = fork();
__e_acsl_store_block((void *)(& pid_15),(size_t)4);
__e_acsl_full_init((void *)(& pid_15));
if (! pid_15) {
@@ -838,19 +782,15 @@ int main(int argc, char const **argv)
else {
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
- waitpid(pid_15,& process_status_15,0);
+ __gen_e_acsl_waitpid(pid_15,& process_status_15,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_15); */
signal_eval(process_status_15,0,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_15));
}
- __e_acsl_delete_block((void *)(& tmp_49));
__e_acsl_delete_block((void *)(& pid_15));
}
{
- int tmp_52;
- __e_acsl_store_block((void *)(& tmp_52),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_52));
- tmp_52 = fork();
- pid_t pid_16 = (unsigned int)tmp_52;
+ pid_t pid_16 = fork();
__e_acsl_store_block((void *)(& pid_16),(size_t)4);
__e_acsl_full_init((void *)(& pid_16));
if (! pid_16) {
@@ -874,19 +814,15 @@ int main(int argc, char const **argv)
else {
int process_status_16;
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
- waitpid(pid_16,& process_status_16,0);
+ __gen_e_acsl_waitpid(pid_16,& process_status_16,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_16); */
signal_eval(process_status_16,0,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_16));
}
- __e_acsl_delete_block((void *)(& tmp_52));
__e_acsl_delete_block((void *)(& pid_16));
}
{
- int tmp_55;
- __e_acsl_store_block((void *)(& tmp_55),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_55));
- tmp_55 = fork();
- pid_t pid_17 = (unsigned int)tmp_55;
+ pid_t pid_17 = fork();
__e_acsl_store_block((void *)(& pid_17),(size_t)4);
__e_acsl_full_init((void *)(& pid_17));
if (! pid_17) {
@@ -895,6 +831,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& tmp_57),(size_t)4);
__e_acsl_store_block((void *)(& tmp_56),(size_t)4);
__e_acsl_initialize((void *)(dl + 3),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(dl + 3); */
*(dl + 3) = (char)'d';
__e_acsl_full_init((void *)(& tmp_56));
tmp_56 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
@@ -910,19 +847,15 @@ int main(int argc, char const **argv)
else {
int process_status_17;
__e_acsl_store_block((void *)(& process_status_17),(size_t)4);
- waitpid(pid_17,& process_status_17,0);
+ __gen_e_acsl_waitpid(pid_17,& process_status_17,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_17); */
signal_eval(process_status_17,0,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_17));
}
- __e_acsl_delete_block((void *)(& tmp_55));
__e_acsl_delete_block((void *)(& pid_17));
}
{
- int tmp_58;
- __e_acsl_store_block((void *)(& tmp_58),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_58));
- tmp_58 = fork();
- pid_t pid_18 = (unsigned int)tmp_58;
+ pid_t pid_18 = fork();
__e_acsl_store_block((void *)(& pid_18),(size_t)4);
__e_acsl_full_init((void *)(& pid_18));
if (! pid_18) {
@@ -931,6 +864,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& tmp_60),(size_t)4);
__e_acsl_store_block((void *)(& tmp_59),(size_t)4);
__e_acsl_initialize((void *)(dr + 3),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(dr + 3); */
*(dr + 3) = (char)'d';
__e_acsl_full_init((void *)(& tmp_59));
tmp_59 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
@@ -946,19 +880,15 @@ int main(int argc, char const **argv)
else {
int process_status_18;
__e_acsl_store_block((void *)(& process_status_18),(size_t)4);
- waitpid(pid_18,& process_status_18,0);
+ __gen_e_acsl_waitpid(pid_18,& process_status_18,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_18); */
signal_eval(process_status_18,0,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_18));
}
- __e_acsl_delete_block((void *)(& tmp_58));
__e_acsl_delete_block((void *)(& pid_18));
}
{
- int tmp_61;
- __e_acsl_store_block((void *)(& tmp_61),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_61));
- tmp_61 = fork();
- pid_t pid_19 = (unsigned int)tmp_61;
+ pid_t pid_19 = fork();
__e_acsl_store_block((void *)(& pid_19),(size_t)4);
__e_acsl_full_init((void *)(& pid_19));
if (! pid_19) {
@@ -972,19 +902,15 @@ int main(int argc, char const **argv)
else {
int process_status_19;
__e_acsl_store_block((void *)(& process_status_19),(size_t)4);
- waitpid(pid_19,& process_status_19,0);
+ __gen_e_acsl_waitpid(pid_19,& process_status_19,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_19); */
signal_eval(process_status_19,1,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_19));
}
- __e_acsl_delete_block((void *)(& tmp_61));
__e_acsl_delete_block((void *)(& pid_19));
}
{
- int tmp_62;
- __e_acsl_store_block((void *)(& tmp_62),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_62));
- tmp_62 = fork();
- pid_t pid_20 = (unsigned int)tmp_62;
+ pid_t pid_20 = fork();
__e_acsl_store_block((void *)(& pid_20),(size_t)4);
__e_acsl_full_init((void *)(& pid_20));
if (! pid_20) {
@@ -998,23 +924,20 @@ int main(int argc, char const **argv)
else {
int process_status_20;
__e_acsl_store_block((void *)(& process_status_20),(size_t)4);
- waitpid(pid_20,& process_status_20,0);
+ __gen_e_acsl_waitpid(pid_20,& process_status_20,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_20); */
signal_eval(process_status_20,1,__gen_e_acsl_literal_string_30);
__e_acsl_delete_block((void *)(& process_status_20));
}
- __e_acsl_delete_block((void *)(& tmp_62));
__e_acsl_delete_block((void *)(& pid_20));
}
{
- int tmp_63;
- __e_acsl_store_block((void *)(& tmp_63),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_63));
- tmp_63 = fork();
- pid_t pid_21 = (unsigned int)tmp_63;
+ pid_t pid_21 = fork();
__e_acsl_store_block((void *)(& pid_21),(size_t)4);
__e_acsl_full_init((void *)(& pid_21));
if (! pid_21) {
__e_acsl_initialize((void *)(dl + 3),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(dl + 3); */
*(dl + 3) = (char)'d';
__e_acsl_full_init((void *)(& res));
res = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
@@ -1024,23 +947,20 @@ int main(int argc, char const **argv)
else {
int process_status_21;
__e_acsl_store_block((void *)(& process_status_21),(size_t)4);
- waitpid(pid_21,& process_status_21,0);
+ __gen_e_acsl_waitpid(pid_21,& process_status_21,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_21); */
signal_eval(process_status_21,1,__gen_e_acsl_literal_string_31);
__e_acsl_delete_block((void *)(& process_status_21));
}
- __e_acsl_delete_block((void *)(& tmp_63));
__e_acsl_delete_block((void *)(& pid_21));
}
{
- int tmp_64;
- __e_acsl_store_block((void *)(& tmp_64),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_64));
- tmp_64 = fork();
- pid_t pid_22 = (unsigned int)tmp_64;
+ pid_t pid_22 = fork();
__e_acsl_store_block((void *)(& pid_22),(size_t)4);
__e_acsl_full_init((void *)(& pid_22));
if (! pid_22) {
__e_acsl_initialize((void *)(dr + 3),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(dr + 3); */
*(dr + 3) = (char)'d';
__e_acsl_full_init((void *)(& res));
res = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
@@ -1050,11 +970,11 @@ int main(int argc, char const **argv)
else {
int process_status_22;
__e_acsl_store_block((void *)(& process_status_22),(size_t)4);
- waitpid(pid_22,& process_status_22,0);
+ __gen_e_acsl_waitpid(pid_22,& process_status_22,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_22); */
signal_eval(process_status_22,1,__gen_e_acsl_literal_string_32);
__e_acsl_delete_block((void *)(& process_status_22));
}
- __e_acsl_delete_block((void *)(& tmp_64));
__e_acsl_delete_block((void *)(& pid_22));
}
free((void *)dl);
@@ -1064,6 +984,8 @@ int main(int argc, char const **argv)
__e_acsl_delete_block((void *)(& argv));
__e_acsl_delete_block((void *)(& argc));
__e_acsl_delete_block((void *)(& fail_ncomp));
+ __e_acsl_delete_block((void *)(& __fc_p_strerror));
+ __e_acsl_delete_block((void *)(strerror));
__e_acsl_delete_block((void *)(& __fc_strtok_ptr));
__e_acsl_delete_block((void *)(& signal_eval));
__e_acsl_delete_block((void *)(& testno));
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 747de31e278bceba4f652e78425c2f6f1b26c24e..c0c88093754aaad70697038cfcf4d2deb13dbf64 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -30,150 +30,161 @@ char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_8;
/*@ assigns \result;
assigns \result \from \nothing; */
-extern int ( /* missing proto */ fork)();
+extern int ( /* missing proto */ fork)(void);
void __e_acsl_globals_init(void)
{
- __gen_e_acsl_literal_string_24 = "tests/builtin/strcpy.c:39";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
- sizeof("tests/builtin/strcpy.c:39"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
- __gen_e_acsl_literal_string_23 = "tests/builtin/strcpy.c:38";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
- sizeof("tests/builtin/strcpy.c:38"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
- __gen_e_acsl_literal_string_22 = "tests/builtin/strcpy.c:37";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
- sizeof("tests/builtin/strcpy.c:37"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
- __gen_e_acsl_literal_string_21 = "tests/builtin/strcpy.c:36";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
- sizeof("tests/builtin/strcpy.c:36"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
- __gen_e_acsl_literal_string_20 = "tests/builtin/strcpy.c:35";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
- sizeof("tests/builtin/strcpy.c:35"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
- __gen_e_acsl_literal_string_19 = "tests/builtin/strcpy.c:34";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
- sizeof("tests/builtin/strcpy.c:34"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
- __gen_e_acsl_literal_string_18 = "tests/builtin/strcpy.c:33";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
- sizeof("tests/builtin/strcpy.c:33"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
- __gen_e_acsl_literal_string_17 = "tests/builtin/strcpy.c:32";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
- sizeof("tests/builtin/strcpy.c:32"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
- __gen_e_acsl_literal_string_16 = "tests/builtin/strcpy.c:29";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
- sizeof("tests/builtin/strcpy.c:29"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
- __gen_e_acsl_literal_string_15 = "tests/builtin/strcpy.c:28";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/builtin/strcpy.c:28"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/builtin/strcpy.c:27";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/builtin/strcpy.c:27"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/builtin/strcpy.c:26";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/builtin/strcpy.c:26"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/builtin/strcpy.c:25";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/builtin/strcpy.c:25"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_11 = "tests/builtin/strcpy.c:24";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/builtin/strcpy.c:24"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_10 = "tests/builtin/strcpy.c:23";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("tests/builtin/strcpy.c:23"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_9 = "tests/builtin/strcpy.c:22";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/builtin/strcpy.c:22"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string_7 = "tests/builtin/strcpy.c:21";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
- sizeof("tests/builtin/strcpy.c:21"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
- __gen_e_acsl_literal_string_6 = "abcd";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof("abcd"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
- __gen_e_acsl_literal_string = "TEST %d: ";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("TEST %d: "));
- __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 = "OK: Expected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("OK: Expected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
- sizeof("OK: Expected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
- sizeof("FAIL: Unexpected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
- __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
- sizeof("FAIL: Unexpected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_8 = "";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,sizeof(""));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __e_acsl_store_block((void *)(& __gen_e_acsl_strdup),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strdup));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strncpy),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strncpy));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strcpy),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strcpy));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_strtok_ptr));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& testno),(size_t)4);
- __e_acsl_full_init((void *)(& testno));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __gen_e_acsl_literal_string_24 = "tests/builtin/strcpy.c:39";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_24,
+ sizeof("tests/builtin/strcpy.c:39"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_24);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_24);
+ __gen_e_acsl_literal_string_23 = "tests/builtin/strcpy.c:38";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_23,
+ sizeof("tests/builtin/strcpy.c:38"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_23);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_23);
+ __gen_e_acsl_literal_string_22 = "tests/builtin/strcpy.c:37";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_22,
+ sizeof("tests/builtin/strcpy.c:37"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_22);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_22);
+ __gen_e_acsl_literal_string_21 = "tests/builtin/strcpy.c:36";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_21,
+ sizeof("tests/builtin/strcpy.c:36"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_21);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_21);
+ __gen_e_acsl_literal_string_20 = "tests/builtin/strcpy.c:35";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_20,
+ sizeof("tests/builtin/strcpy.c:35"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_20);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_20);
+ __gen_e_acsl_literal_string_19 = "tests/builtin/strcpy.c:34";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_19,
+ sizeof("tests/builtin/strcpy.c:34"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_19);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_19);
+ __gen_e_acsl_literal_string_18 = "tests/builtin/strcpy.c:33";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_18,
+ sizeof("tests/builtin/strcpy.c:33"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_18);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_18);
+ __gen_e_acsl_literal_string_17 = "tests/builtin/strcpy.c:32";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_17,
+ sizeof("tests/builtin/strcpy.c:32"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_17);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_17);
+ __gen_e_acsl_literal_string_16 = "tests/builtin/strcpy.c:29";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_16,
+ sizeof("tests/builtin/strcpy.c:29"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_16);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_16);
+ __gen_e_acsl_literal_string_15 = "tests/builtin/strcpy.c:28";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
+ sizeof("tests/builtin/strcpy.c:28"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
+ __gen_e_acsl_literal_string_14 = "tests/builtin/strcpy.c:27";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
+ sizeof("tests/builtin/strcpy.c:27"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
+ __gen_e_acsl_literal_string_13 = "tests/builtin/strcpy.c:26";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
+ sizeof("tests/builtin/strcpy.c:26"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
+ __gen_e_acsl_literal_string_12 = "tests/builtin/strcpy.c:25";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
+ sizeof("tests/builtin/strcpy.c:25"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
+ __gen_e_acsl_literal_string_11 = "tests/builtin/strcpy.c:24";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
+ sizeof("tests/builtin/strcpy.c:24"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
+ __gen_e_acsl_literal_string_10 = "tests/builtin/strcpy.c:23";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
+ sizeof("tests/builtin/strcpy.c:23"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
+ __gen_e_acsl_literal_string_9 = "tests/builtin/strcpy.c:22";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
+ sizeof("tests/builtin/strcpy.c:22"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
+ __gen_e_acsl_literal_string_7 = "tests/builtin/strcpy.c:21";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
+ sizeof("tests/builtin/strcpy.c:21"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
+ __gen_e_acsl_literal_string_6 = "abcd";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,
+ sizeof("abcd"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
+ __gen_e_acsl_literal_string = "TEST %d: ";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+ sizeof("TEST %d: "));
+ __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 = "OK: Expected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("OK: Expected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
+ sizeof("OK: Expected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
+ __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
+ sizeof("FAIL: Unexpected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
+ __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
+ sizeof("FAIL: Unexpected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
+ __gen_e_acsl_literal_string_8 = "";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,sizeof(""));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strdup),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strdup));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strncpy),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strncpy));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strcpy),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strcpy));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_waitpid),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_waitpid));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
+ __e_acsl_store_block((void *)(& __fc_p_strerror),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_strerror));
+ __e_acsl_store_block((void *)(strerror),(size_t)64);
+ __e_acsl_full_init((void *)(& strerror));
+ __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_strtok_ptr));
+ __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
+ __e_acsl_full_init((void *)(& signal_eval));
+ __e_acsl_store_block((void *)(& testno),(size_t)4);
+ __e_acsl_full_init((void *)(& testno));
+ __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
+ __e_acsl_full_init((void *)(& __fc_time));
+ __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_fopen));
+ __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+ __e_acsl_full_init((void *)(& __fc_fopen));
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ }
return;
}
@@ -210,11 +221,7 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& unalloc_str));
free((void *)unalloc_str);
{
- int tmp_3;
- __e_acsl_store_block((void *)(& tmp_3),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_3));
- tmp_3 = fork();
- pid_t pid = (unsigned int)tmp_3;
+ pid_t pid = fork();
__e_acsl_store_block((void *)(& pid),(size_t)4);
__e_acsl_full_init((void *)(& pid));
if (! pid) {
@@ -224,19 +231,15 @@ int main(int argc, char const **argv)
else {
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
+ __gen_e_acsl_waitpid(pid,& process_status,0);
+ /*@ assert Eva: initialization: \initialized(&process_status); */
signal_eval(process_status,0,__gen_e_acsl_literal_string_7);
__e_acsl_delete_block((void *)(& process_status));
}
- __e_acsl_delete_block((void *)(& tmp_3));
__e_acsl_delete_block((void *)(& pid));
}
{
- int tmp_4;
- __e_acsl_store_block((void *)(& tmp_4),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_4));
- tmp_4 = fork();
- pid_t pid_0 = (unsigned int)tmp_4;
+ pid_t pid_0 = fork();
__e_acsl_store_block((void *)(& pid_0),(size_t)4);
__e_acsl_full_init((void *)(& pid_0));
if (! pid_0) {
@@ -246,19 +249,15 @@ int main(int argc, char const **argv)
else {
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
+ __gen_e_acsl_waitpid(pid_0,& process_status_0,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_0); */
signal_eval(process_status_0,0,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status_0));
}
- __e_acsl_delete_block((void *)(& tmp_4));
__e_acsl_delete_block((void *)(& pid_0));
}
{
- int tmp_5;
- __e_acsl_store_block((void *)(& tmp_5),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_5));
- tmp_5 = fork();
- pid_t pid_1 = (unsigned int)tmp_5;
+ pid_t pid_1 = fork();
__e_acsl_store_block((void *)(& pid_1),(size_t)4);
__e_acsl_full_init((void *)(& pid_1));
if (! pid_1) {
@@ -268,41 +267,34 @@ int main(int argc, char const **argv)
else {
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
- waitpid(pid_1,& process_status_1,0);
+ __gen_e_acsl_waitpid(pid_1,& process_status_1,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,1,__gen_e_acsl_literal_string_10);
__e_acsl_delete_block((void *)(& process_status_1));
}
- __e_acsl_delete_block((void *)(& tmp_5));
__e_acsl_delete_block((void *)(& pid_1));
}
{
- int tmp_6;
- __e_acsl_store_block((void *)(& tmp_6),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_6));
- tmp_6 = fork();
- pid_t pid_2 = (unsigned int)tmp_6;
+ pid_t pid_2 = fork();
__e_acsl_store_block((void *)(& pid_2),(size_t)4);
__e_acsl_full_init((void *)(& pid_2));
if (! pid_2) {
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strcpy(unalloc_str,(char const *)src);
__gen_e_acsl_exit(0);
}
else {
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
- waitpid(pid_2,& process_status_2,0);
+ __gen_e_acsl_waitpid(pid_2,& process_status_2,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,1,__gen_e_acsl_literal_string_11);
__e_acsl_delete_block((void *)(& process_status_2));
}
- __e_acsl_delete_block((void *)(& tmp_6));
__e_acsl_delete_block((void *)(& pid_2));
}
{
- int tmp_7;
- __e_acsl_store_block((void *)(& tmp_7),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_7));
- tmp_7 = fork();
- pid_t pid_3 = (unsigned int)tmp_7;
+ pid_t pid_3 = fork();
__e_acsl_store_block((void *)(& pid_3),(size_t)4);
__e_acsl_full_init((void *)(& pid_3));
if (! pid_3) {
@@ -312,19 +304,15 @@ int main(int argc, char const **argv)
else {
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
- waitpid(pid_3,& process_status_3,0);
+ __gen_e_acsl_waitpid(pid_3,& process_status_3,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_3); */
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_3));
}
- __e_acsl_delete_block((void *)(& tmp_7));
__e_acsl_delete_block((void *)(& pid_3));
}
{
- int tmp_8;
- __e_acsl_store_block((void *)(& tmp_8),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_8));
- tmp_8 = fork();
- pid_t pid_4 = (unsigned int)tmp_8;
+ pid_t pid_4 = fork();
__e_acsl_store_block((void *)(& pid_4),(size_t)4);
__e_acsl_full_init((void *)(& pid_4));
if (! pid_4) {
@@ -334,19 +322,15 @@ int main(int argc, char const **argv)
else {
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
- waitpid(pid_4,& process_status_4,0);
+ __gen_e_acsl_waitpid(pid_4,& process_status_4,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_4); */
signal_eval(process_status_4,0,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_4));
}
- __e_acsl_delete_block((void *)(& tmp_8));
__e_acsl_delete_block((void *)(& pid_4));
}
{
- int tmp_9;
- __e_acsl_store_block((void *)(& tmp_9),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_9));
- tmp_9 = fork();
- pid_t pid_5 = (unsigned int)tmp_9;
+ pid_t pid_5 = fork();
__e_acsl_store_block((void *)(& pid_5),(size_t)4);
__e_acsl_full_init((void *)(& pid_5));
if (! pid_5) {
@@ -356,19 +340,15 @@ int main(int argc, char const **argv)
else {
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
- waitpid(pid_5,& process_status_5,0);
+ __gen_e_acsl_waitpid(pid_5,& process_status_5,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_5); */
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_5));
}
- __e_acsl_delete_block((void *)(& tmp_9));
__e_acsl_delete_block((void *)(& pid_5));
}
{
- int tmp_10;
- __e_acsl_store_block((void *)(& tmp_10),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_10));
- tmp_10 = fork();
- pid_t pid_6 = (unsigned int)tmp_10;
+ pid_t pid_6 = fork();
__e_acsl_store_block((void *)(& pid_6),(size_t)4);
__e_acsl_full_init((void *)(& pid_6));
if (! pid_6) {
@@ -378,19 +358,15 @@ int main(int argc, char const **argv)
else {
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
- waitpid(pid_6,& process_status_6,0);
+ __gen_e_acsl_waitpid(pid_6,& process_status_6,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_6); */
signal_eval(process_status_6,0,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_6));
}
- __e_acsl_delete_block((void *)(& tmp_10));
__e_acsl_delete_block((void *)(& pid_6));
}
{
- int tmp_11;
- __e_acsl_store_block((void *)(& tmp_11),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_11));
- tmp_11 = fork();
- pid_t pid_7 = (unsigned int)tmp_11;
+ pid_t pid_7 = fork();
__e_acsl_store_block((void *)(& pid_7),(size_t)4);
__e_acsl_full_init((void *)(& pid_7));
if (! pid_7) {
@@ -400,19 +376,15 @@ int main(int argc, char const **argv)
else {
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
- waitpid(pid_7,& process_status_7,0);
+ __gen_e_acsl_waitpid(pid_7,& process_status_7,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_7); */
signal_eval(process_status_7,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_7));
}
- __e_acsl_delete_block((void *)(& tmp_11));
__e_acsl_delete_block((void *)(& pid_7));
}
{
- int tmp_12;
- __e_acsl_store_block((void *)(& tmp_12),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_12));
- tmp_12 = fork();
- pid_t pid_8 = (unsigned int)tmp_12;
+ pid_t pid_8 = fork();
__e_acsl_store_block((void *)(& pid_8),(size_t)4);
__e_acsl_full_init((void *)(& pid_8));
if (! pid_8) {
@@ -422,19 +394,15 @@ int main(int argc, char const **argv)
else {
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
- waitpid(pid_8,& process_status_8,0);
+ __gen_e_acsl_waitpid(pid_8,& process_status_8,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_8); */
signal_eval(process_status_8,0,__gen_e_acsl_literal_string_17);
__e_acsl_delete_block((void *)(& process_status_8));
}
- __e_acsl_delete_block((void *)(& tmp_12));
__e_acsl_delete_block((void *)(& pid_8));
}
{
- int tmp_13;
- __e_acsl_store_block((void *)(& tmp_13),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_13));
- tmp_13 = fork();
- pid_t pid_9 = (unsigned int)tmp_13;
+ pid_t pid_9 = fork();
__e_acsl_store_block((void *)(& pid_9),(size_t)4);
__e_acsl_full_init((void *)(& pid_9));
if (! pid_9) {
@@ -444,41 +412,34 @@ int main(int argc, char const **argv)
else {
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
- waitpid(pid_9,& process_status_9,0);
+ __gen_e_acsl_waitpid(pid_9,& process_status_9,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_9); */
signal_eval(process_status_9,1,__gen_e_acsl_literal_string_18);
__e_acsl_delete_block((void *)(& process_status_9));
}
- __e_acsl_delete_block((void *)(& tmp_13));
__e_acsl_delete_block((void *)(& pid_9));
}
{
- int tmp_14;
- __e_acsl_store_block((void *)(& tmp_14),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_14));
- tmp_14 = fork();
- pid_t pid_10 = (unsigned int)tmp_14;
+ pid_t pid_10 = fork();
__e_acsl_store_block((void *)(& pid_10),(size_t)4);
__e_acsl_full_init((void *)(& pid_10));
if (! pid_10) {
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&unalloc_str); */
__gen_e_acsl_strncpy(unalloc_str,(char const *)src,(unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
- waitpid(pid_10,& process_status_10,0);
+ __gen_e_acsl_waitpid(pid_10,& process_status_10,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_10); */
signal_eval(process_status_10,1,__gen_e_acsl_literal_string_19);
__e_acsl_delete_block((void *)(& process_status_10));
}
- __e_acsl_delete_block((void *)(& tmp_14));
__e_acsl_delete_block((void *)(& pid_10));
}
{
- int tmp_15;
- __e_acsl_store_block((void *)(& tmp_15),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_15));
- tmp_15 = fork();
- pid_t pid_11 = (unsigned int)tmp_15;
+ pid_t pid_11 = fork();
__e_acsl_store_block((void *)(& pid_11),(size_t)4);
__e_acsl_full_init((void *)(& pid_11));
if (! pid_11) {
@@ -488,19 +449,15 @@ int main(int argc, char const **argv)
else {
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
- waitpid(pid_11,& process_status_11,0);
+ __gen_e_acsl_waitpid(pid_11,& process_status_11,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_11); */
signal_eval(process_status_11,1,__gen_e_acsl_literal_string_20);
__e_acsl_delete_block((void *)(& process_status_11));
}
- __e_acsl_delete_block((void *)(& tmp_15));
__e_acsl_delete_block((void *)(& pid_11));
}
{
- int tmp_16;
- __e_acsl_store_block((void *)(& tmp_16),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_16));
- tmp_16 = fork();
- pid_t pid_12 = (unsigned int)tmp_16;
+ pid_t pid_12 = fork();
__e_acsl_store_block((void *)(& pid_12),(size_t)4);
__e_acsl_full_init((void *)(& pid_12));
if (! pid_12) {
@@ -510,19 +467,15 @@ int main(int argc, char const **argv)
else {
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
- waitpid(pid_12,& process_status_12,0);
+ __gen_e_acsl_waitpid(pid_12,& process_status_12,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_12); */
signal_eval(process_status_12,0,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_12));
}
- __e_acsl_delete_block((void *)(& tmp_16));
__e_acsl_delete_block((void *)(& pid_12));
}
{
- int tmp_17;
- __e_acsl_store_block((void *)(& tmp_17),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_17));
- tmp_17 = fork();
- pid_t pid_13 = (unsigned int)tmp_17;
+ pid_t pid_13 = fork();
__e_acsl_store_block((void *)(& pid_13),(size_t)4);
__e_acsl_full_init((void *)(& pid_13));
if (! pid_13) {
@@ -532,19 +485,15 @@ int main(int argc, char const **argv)
else {
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
- waitpid(pid_13,& process_status_13,0);
+ __gen_e_acsl_waitpid(pid_13,& process_status_13,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_13); */
signal_eval(process_status_13,1,__gen_e_acsl_literal_string_22);
__e_acsl_delete_block((void *)(& process_status_13));
}
- __e_acsl_delete_block((void *)(& tmp_17));
__e_acsl_delete_block((void *)(& pid_13));
}
{
- int tmp_18;
- __e_acsl_store_block((void *)(& tmp_18),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_18));
- tmp_18 = fork();
- pid_t pid_14 = (unsigned int)tmp_18;
+ pid_t pid_14 = fork();
__e_acsl_store_block((void *)(& pid_14),(size_t)4);
__e_acsl_full_init((void *)(& pid_14));
if (! pid_14) {
@@ -554,19 +503,15 @@ int main(int argc, char const **argv)
else {
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
- waitpid(pid_14,& process_status_14,0);
+ __gen_e_acsl_waitpid(pid_14,& process_status_14,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_14); */
signal_eval(process_status_14,0,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_14));
}
- __e_acsl_delete_block((void *)(& tmp_18));
__e_acsl_delete_block((void *)(& pid_14));
}
{
- int tmp_19;
- __e_acsl_store_block((void *)(& tmp_19),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_19));
- tmp_19 = fork();
- pid_t pid_15 = (unsigned int)tmp_19;
+ pid_t pid_15 = fork();
__e_acsl_store_block((void *)(& pid_15),(size_t)4);
__e_acsl_full_init((void *)(& pid_15));
if (! pid_15) {
@@ -576,11 +521,11 @@ int main(int argc, char const **argv)
else {
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
- waitpid(pid_15,& process_status_15,0);
+ __gen_e_acsl_waitpid(pid_15,& process_status_15,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_15); */
signal_eval(process_status_15,1,__gen_e_acsl_literal_string_24);
__e_acsl_delete_block((void *)(& process_status_15));
}
- __e_acsl_delete_block((void *)(& tmp_19));
__e_acsl_delete_block((void *)(& pid_15));
}
free((void *)src);
@@ -590,6 +535,8 @@ int main(int argc, char const **argv)
__retres = 0;
__e_acsl_delete_block((void *)(& argv));
__e_acsl_delete_block((void *)(& argc));
+ __e_acsl_delete_block((void *)(& __fc_p_strerror));
+ __e_acsl_delete_block((void *)(strerror));
__e_acsl_delete_block((void *)(& __fc_strtok_ptr));
__e_acsl_delete_block((void *)(& signal_eval));
__e_acsl_delete_block((void *)(& testno));
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 210bf3d5f1af1dab2000473c9d8538a8ba91ab96..1c9570b6a6fac636c0e77dfc12bf04dad85daedd 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -21,106 +21,116 @@ char *__gen_e_acsl_literal_string_4;
char *__gen_e_acsl_literal_string_6;
/*@ assigns \result;
assigns \result \from \nothing; */
-extern int ( /* missing proto */ fork)();
+extern int ( /* missing proto */ fork)(void);
void __e_acsl_globals_init(void)
{
- __gen_e_acsl_literal_string_8 = "the hog";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
- sizeof("the hog"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
- __gen_e_acsl_literal_string_7 = "the cat";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
- sizeof("the cat"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
- __gen_e_acsl_literal_string_15 = "tests/builtin/strlen.c:28";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
- sizeof("tests/builtin/strlen.c:28"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
- __gen_e_acsl_literal_string_14 = "tests/builtin/strlen.c:26";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
- sizeof("tests/builtin/strlen.c:26"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
- __gen_e_acsl_literal_string_13 = "tests/builtin/strlen.c:25";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
- sizeof("tests/builtin/strlen.c:25"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
- __gen_e_acsl_literal_string_12 = "tests/builtin/strlen.c:21";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
- sizeof("tests/builtin/strlen.c:21"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
- __gen_e_acsl_literal_string_11 = "tests/builtin/strlen.c:20";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
- sizeof("tests/builtin/strlen.c:20"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
- __gen_e_acsl_literal_string_10 = "tests/builtin/strlen.c:19";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
- sizeof("tests/builtin/strlen.c:19"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
- __gen_e_acsl_literal_string_9 = "tests/builtin/strlen.c:18";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
- sizeof("tests/builtin/strlen.c:18"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
- __gen_e_acsl_literal_string = "TEST %d: ";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("TEST %d: "));
- __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 = "OK: Expected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
- sizeof("OK: Expected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
- sizeof("OK: Expected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
- __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
- sizeof("FAIL: Unexpected signal at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
- __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
- sizeof("FAIL: Unexpected execution at %s\n"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
- __gen_e_acsl_literal_string_6 = "";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof(""));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
- __e_acsl_store_block((void *)(& __gen_e_acsl_strdup),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strdup));
- __e_acsl_store_block((void *)(& __gen_e_acsl_strlen),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_strlen));
- __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
- __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
- __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
- __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_strtok_ptr));
- __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
- __e_acsl_full_init((void *)(& signal_eval));
- __e_acsl_store_block((void *)(& testno),(size_t)4);
- __e_acsl_full_init((void *)(& testno));
- __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
- __e_acsl_full_init((void *)(& __fc_time));
- __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_p_fopen));
- __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
- __e_acsl_full_init((void *)(& __fc_fopen));
- __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
- __e_acsl_full_init((void *)(& __fc_rand_max));
+ static char __e_acsl_already_run = 0;
+ if (! __e_acsl_already_run) {
+ __e_acsl_already_run = 1;
+ __gen_e_acsl_literal_string_8 = "the hog";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_8,
+ sizeof("the hog"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_8);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_8);
+ __gen_e_acsl_literal_string_7 = "the cat";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_7,
+ sizeof("the cat"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_7);
+ __gen_e_acsl_literal_string_15 = "tests/builtin/strlen.c:28";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_15,
+ sizeof("tests/builtin/strlen.c:28"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_15);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_15);
+ __gen_e_acsl_literal_string_14 = "tests/builtin/strlen.c:26";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_14,
+ sizeof("tests/builtin/strlen.c:26"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_14);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_14);
+ __gen_e_acsl_literal_string_13 = "tests/builtin/strlen.c:25";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_13,
+ sizeof("tests/builtin/strlen.c:25"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_13);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_13);
+ __gen_e_acsl_literal_string_12 = "tests/builtin/strlen.c:21";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_12,
+ sizeof("tests/builtin/strlen.c:21"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_12);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_12);
+ __gen_e_acsl_literal_string_11 = "tests/builtin/strlen.c:20";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_11,
+ sizeof("tests/builtin/strlen.c:20"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_11);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_11);
+ __gen_e_acsl_literal_string_10 = "tests/builtin/strlen.c:19";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_10,
+ sizeof("tests/builtin/strlen.c:19"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_10);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_10);
+ __gen_e_acsl_literal_string_9 = "tests/builtin/strlen.c:18";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_9,
+ sizeof("tests/builtin/strlen.c:18"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_9);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_9);
+ __gen_e_acsl_literal_string = "TEST %d: ";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+ sizeof("TEST %d: "));
+ __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 = "OK: Expected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("OK: Expected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ __gen_e_acsl_literal_string_3 = "OK: Expected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_3,
+ sizeof("OK: Expected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_3);
+ __gen_e_acsl_literal_string_5 = "FAIL: Unexpected signal at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,
+ sizeof("FAIL: Unexpected signal at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_5);
+ __gen_e_acsl_literal_string_4 = "FAIL: Unexpected execution at %s\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_4,
+ sizeof("FAIL: Unexpected execution at %s\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_4);
+ __gen_e_acsl_literal_string_6 = "";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_6,sizeof(""));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strdup),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strdup));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_strlen),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_strlen));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_waitpid),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_waitpid));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_exit),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_exit));
+ __e_acsl_store_block((void *)(& __gen_e_acsl_abort),(size_t)1);
+ __e_acsl_full_init((void *)(& __gen_e_acsl_abort));
+ __e_acsl_store_block((void *)(& __fc_p_strerror),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_strerror));
+ __e_acsl_store_block((void *)(strerror),(size_t)64);
+ __e_acsl_full_init((void *)(& strerror));
+ __e_acsl_store_block((void *)(& __fc_strtok_ptr),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_strtok_ptr));
+ __e_acsl_store_block((void *)(& signal_eval),(size_t)1);
+ __e_acsl_full_init((void *)(& signal_eval));
+ __e_acsl_store_block((void *)(& testno),(size_t)4);
+ __e_acsl_full_init((void *)(& testno));
+ __e_acsl_store_block((void *)(& __fc_time),(size_t)4);
+ __e_acsl_full_init((void *)(& __fc_time));
+ __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_p_fopen));
+ __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
+ __e_acsl_full_init((void *)(& __fc_fopen));
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
+ __e_acsl_full_init((void *)(& __fc_rand_max));
+ }
return;
}
@@ -153,11 +163,7 @@ int main(int argc, char const **argv)
__e_acsl_store_block((void *)(& const_str),(size_t)8);
__e_acsl_full_init((void *)(& const_str));
{
- int tmp_0;
- __e_acsl_store_block((void *)(& tmp_0),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_0));
- tmp_0 = fork();
- pid_t pid = (unsigned int)tmp_0;
+ pid_t pid = fork();
__e_acsl_store_block((void *)(& pid),(size_t)4);
__e_acsl_full_init((void *)(& pid));
if (! pid) {
@@ -174,19 +180,15 @@ int main(int argc, char const **argv)
else {
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
- waitpid(pid,& process_status,0);
+ __gen_e_acsl_waitpid(pid,& process_status,0);
+ /*@ assert Eva: initialization: \initialized(&process_status); */
signal_eval(process_status,0,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status));
}
- __e_acsl_delete_block((void *)(& tmp_0));
__e_acsl_delete_block((void *)(& pid));
}
{
- int tmp_2;
- __e_acsl_store_block((void *)(& tmp_2),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_2));
- tmp_2 = fork();
- pid_t pid_0 = (unsigned int)tmp_2;
+ pid_t pid_0 = fork();
__e_acsl_store_block((void *)(& pid_0),(size_t)4);
__e_acsl_full_init((void *)(& pid_0));
if (! pid_0) {
@@ -203,19 +205,15 @@ int main(int argc, char const **argv)
else {
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
- waitpid(pid_0,& process_status_0,0);
+ __gen_e_acsl_waitpid(pid_0,& process_status_0,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_0); */
signal_eval(process_status_0,0,__gen_e_acsl_literal_string_10);
__e_acsl_delete_block((void *)(& process_status_0));
}
- __e_acsl_delete_block((void *)(& tmp_2));
__e_acsl_delete_block((void *)(& pid_0));
}
{
- int tmp_4;
- __e_acsl_store_block((void *)(& tmp_4),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_4));
- tmp_4 = fork();
- pid_t pid_1 = (unsigned int)tmp_4;
+ pid_t pid_1 = fork();
__e_acsl_store_block((void *)(& pid_1),(size_t)4);
__e_acsl_full_init((void *)(& pid_1));
if (! pid_1) {
@@ -232,19 +230,15 @@ int main(int argc, char const **argv)
else {
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
- waitpid(pid_1,& process_status_1,0);
+ __gen_e_acsl_waitpid(pid_1,& process_status_1,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,0,__gen_e_acsl_literal_string_11);
__e_acsl_delete_block((void *)(& process_status_1));
}
- __e_acsl_delete_block((void *)(& tmp_4));
__e_acsl_delete_block((void *)(& pid_1));
}
{
- int tmp_6;
- __e_acsl_store_block((void *)(& tmp_6),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_6));
- tmp_6 = fork();
- pid_t pid_2 = (unsigned int)tmp_6;
+ pid_t pid_2 = fork();
__e_acsl_store_block((void *)(& pid_2),(size_t)4);
__e_acsl_full_init((void *)(& pid_2));
if (! pid_2) {
@@ -261,23 +255,20 @@ int main(int argc, char const **argv)
else {
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
- waitpid(pid_2,& process_status_2,0);
+ __gen_e_acsl_waitpid(pid_2,& process_status_2,0);
+ /*@ assert Eva: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,0,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_2));
}
- __e_acsl_delete_block((void *)(& tmp_6));
__e_acsl_delete_block((void *)(& pid_2));
}
__e_acsl_initialize((void *)(heap_str + 7),sizeof(char));
+ /*@ assert Eva: mem_access: \valid(heap_str + 7); */
*(heap_str + 7) = (char)'a';
__e_acsl_initialize((void *)(& stack_str[7]),sizeof(char));
stack_str[7] = (char)'a';
{
- int tmp_8;
- __e_acsl_store_block((void *)(& tmp_8),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_8));
- tmp_8 = fork();
- pid_t pid_3 = (unsigned int)tmp_8;
+ pid_t pid_3 = fork();
__e_acsl_store_block((void *)(& pid_3),(size_t)4);
__e_acsl_full_init((void *)(& pid_3));
if (! pid_3) {
@@ -294,19 +285,14 @@ int main(int argc, char const **argv)
else {
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
- waitpid(pid_3,& process_status_3,0);
+ __gen_e_acsl_waitpid(pid_3,& process_status_3,0);
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_3));
}
- __e_acsl_delete_block((void *)(& tmp_8));
__e_acsl_delete_block((void *)(& pid_3));
}
{
- int tmp_10;
- __e_acsl_store_block((void *)(& tmp_10),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_10));
- tmp_10 = fork();
- pid_t pid_4 = (unsigned int)tmp_10;
+ pid_t pid_4 = fork();
__e_acsl_store_block((void *)(& pid_4),(size_t)4);
__e_acsl_full_init((void *)(& pid_4));
if (! pid_4) {
@@ -323,20 +309,15 @@ int main(int argc, char const **argv)
else {
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
- waitpid(pid_4,& process_status_4,0);
+ __gen_e_acsl_waitpid(pid_4,& process_status_4,0);
signal_eval(process_status_4,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_4));
}
- __e_acsl_delete_block((void *)(& tmp_10));
__e_acsl_delete_block((void *)(& pid_4));
}
free((void *)heap_str);
{
- int tmp_12;
- __e_acsl_store_block((void *)(& tmp_12),(size_t)4);
- __e_acsl_full_init((void *)(& tmp_12));
- tmp_12 = fork();
- pid_t pid_5 = (unsigned int)tmp_12;
+ pid_t pid_5 = fork();
__e_acsl_store_block((void *)(& pid_5),(size_t)4);
__e_acsl_full_init((void *)(& pid_5));
if (! pid_5) {
@@ -353,17 +334,18 @@ int main(int argc, char const **argv)
else {
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
- waitpid(pid_5,& process_status_5,0);
+ __gen_e_acsl_waitpid(pid_5,& process_status_5,0);
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_5));
}
- __e_acsl_delete_block((void *)(& tmp_12));
__e_acsl_delete_block((void *)(& pid_5));
}
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
__e_acsl_delete_block((void *)(& argv));
__e_acsl_delete_block((void *)(& argc));
+ __e_acsl_delete_block((void *)(& __fc_p_strerror));
+ __e_acsl_delete_block((void *)(strerror));
__e_acsl_delete_block((void *)(& __fc_strtok_ptr));
__e_acsl_delete_block((void *)(& signal_eval));
__e_acsl_delete_block((void *)(& testno));
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.err.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
index e1bebdd53a9c291f07d9b887d4012fd8d4737d5e..2e1d8dc73a6bbdad6a2bbe8df4350e2059a20c00 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
@@ -1,59 +1,81 @@
-tests/builtin/strcat.c:26:[kernel] warning: Calling undeclared function fork. Old style K&R code?
+[kernel:typing:implicit-function-declaration] tests/builtin/strcat.c:26: Warning:
+ Calling undeclared function fork. Old style K&R code?
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcat':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strncat':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-tests/builtin/strcat.c:26:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:364:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:365:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:370:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:377:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:377:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:370:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:368:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:352:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:353:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:354:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:354:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:357:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:359:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[e-acsl] Warning: annotating undefined function `exit':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `waitpid':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strcat':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strncat':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/strcat.c:26: Warning:
+ Neither code nor specification for function fork, generating default assigns from the prototype
+[e-acsl] FRAMAC_SHARE/libc/string.h:409: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:410: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:415: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:423: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:423: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:415: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:413: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:394: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:395: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:396: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:396: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:399: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:402: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:403: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
__e_acsl_init ∈ [--..--]
- __fc_fopen[0..15] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
testno ∈ {0}
- __fc_strtok_ptr ∈ {0}
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
__gen_e_acsl_literal_string_3 ∈ {0}
@@ -83,65 +105,111 @@ FRAMAC_SHARE/libc/string.h:359:[e-acsl] warning: E-ACSL construct `assigns claus
__gen_e_acsl_literal_string_27 ∈ {0}
__gen_e_acsl_literal_string_28 ∈ {0}
__gen_e_acsl_literal_string_29 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-tests/builtin/strcat.c:11:[value] allocating variable __malloc_main_l11
-[value] using specification for function fork
-[value] using specification for function __e_acsl_builtin_strcat
-[value] using specification for function __e_acsl_assert
-[value] using specification for function __e_acsl_delete_block
-FRAMAC_SHARE/libc/string.h:357:[value] warning: function __gen_e_acsl_strcat: postcondition got status unknown.
-[value] using specification for function exit
-[value] using specification for function waitpid
-tests/builtin/strcat.c:26:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status);
-[value] using specification for function printf
-tests/builtin/strcat.c:27:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
-tests/builtin/strcat.c:28:[value] warning: function __gen_e_acsl_strcat: precondition 'room_string' got status invalid.
-tests/builtin/strcat.c:28:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
-tests/builtin/strcat.c:29:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&unalloc_str);
-tests/builtin/strcat.c:29:[value] warning: function __gen_e_acsl_strcat: precondition 'valid_string_dst' got status invalid.
-tests/builtin/strcat.c:29:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
-tests/builtin/strcat.c:30:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&unalloc_str);
-tests/builtin/strcat.c:30:[value] warning: function __gen_e_acsl_strcat: precondition 'valid_string_src' got status invalid.
-tests/builtin/strcat.c:30:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
-tests/builtin/strcat.c:31:[value] warning: function __gen_e_acsl_strcat: precondition 'valid_string_dst' got status invalid.
-tests/builtin/strcat.c:31:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
-tests/builtin/strcat.c:32:[value] warning: function __gen_e_acsl_strcat: precondition 'valid_string_src' got status invalid.
-tests/builtin/strcat.c:32:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
-tests/builtin/strcat.c:33:[value] warning: function __gen_e_acsl_strcat: precondition 'valid_string_dst' got status invalid.
-tests/builtin/strcat.c:33:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
-tests/builtin/strcat.c:34:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
-tests/builtin/strcat.c:35:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
-tests/builtin/strcat.c:36:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_9);
-[value] using specification for function __e_acsl_initialize
-tests/builtin/strcat.c:37:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_10);
-[value] using specification for function __e_acsl_builtin_strncat
-FRAMAC_SHARE/libc/string.h:375:[value] warning: function __gen_e_acsl_strncat, behavior complete: postcondition got status unknown.
-tests/builtin/strcat.c:40:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_11);
-tests/builtin/strcat.c:41:[value] warning: function __gen_e_acsl_strncat, behavior complete: precondition 'room_string' got status invalid.
-tests/builtin/strcat.c:41:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_12);
-tests/builtin/strcat.c:42:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&unalloc_str);
-tests/builtin/strcat.c:42:[value] warning: function __gen_e_acsl_strncat: precondition 'valid_string_dst' got status invalid.
-tests/builtin/strcat.c:42:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_13);
-tests/builtin/strcat.c:43:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&unalloc_str);
-tests/builtin/strcat.c:43:[value] warning: function __gen_e_acsl_strncat: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:363:[value] warning: function __e_acsl_builtin_strncat: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:382:[value] warning: function __gen_e_acsl_strncat, behavior partial: postcondition got status unknown.
-tests/builtin/strcat.c:43:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_14);
-tests/builtin/strcat.c:44:[value] warning: function __gen_e_acsl_strncat: precondition 'valid_string_dst' got status invalid.
-tests/builtin/strcat.c:44:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_15);
-tests/builtin/strcat.c:45:[value] warning: function __gen_e_acsl_strncat: precondition 'valid_string_src' got status invalid.
-tests/builtin/strcat.c:45:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_16);
-tests/builtin/strcat.c:46:[value] warning: function __gen_e_acsl_strncat: precondition 'valid_string_dst' got status invalid.
-tests/builtin/strcat.c:46:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_17);
-tests/builtin/strcat.c:48:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_18);
-tests/builtin/strcat.c:49:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_19);
-tests/builtin/strcat.c:50:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_20);
-[value] using specification for function __e_acsl_memory_clean
-[value] done for function main
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_full_init
+[eva] using specification for function __e_acsl_mark_readonly
+[eva] tests/builtin/strcat.c:11: allocating variable __malloc_main_l11
+[eva] using specification for function fork
+[eva] using specification for function __e_acsl_builtin_strcat
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] FRAMAC_SHARE/libc/string.h:399: Warning:
+ function __gen_e_acsl_strcat: postcondition 'sum_of_lengths' got status unknown.
+[eva] using specification for function exit
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function waitpid
+[eva] using specification for function __e_acsl_initialized
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
+[eva:alarm] tests/builtin/strcat.c:26: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status);
+[eva] using specification for function printf
+[eva:alarm] tests/builtin/strcat.c:27: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_0);
+[eva:alarm] tests/builtin/strcat.c:28: Warning:
+ function __gen_e_acsl_strcat: precondition 'room_string' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:28: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_1);
+[eva:alarm] tests/builtin/strcat.c:29: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&unalloc_str);
+[eva:alarm] tests/builtin/strcat.c:29: Warning:
+ function __gen_e_acsl_strcat: precondition 'valid_string_dest' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:29: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_2);
+[eva:alarm] tests/builtin/strcat.c:30: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&unalloc_str);
+[eva:alarm] tests/builtin/strcat.c:30: Warning:
+ function __gen_e_acsl_strcat: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:30: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_3);
+[eva:alarm] tests/builtin/strcat.c:31: Warning:
+ function __gen_e_acsl_strcat: precondition 'valid_string_dest' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:31: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_4);
+[eva:alarm] tests/builtin/strcat.c:32: Warning:
+ function __gen_e_acsl_strcat: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:32: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_5);
+[eva:alarm] tests/builtin/strcat.c:33: Warning:
+ function __gen_e_acsl_strcat: precondition 'valid_string_dest' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:33: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_6);
+[eva:alarm] tests/builtin/strcat.c:34: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_7);
+[eva:alarm] tests/builtin/strcat.c:35: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_8);
+[eva:alarm] tests/builtin/strcat.c:36: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_9);
+[eva] using specification for function __e_acsl_initialize
+[eva:alarm] tests/builtin/strcat.c:37: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_10);
+[eva] using specification for function __e_acsl_builtin_strncat
+[eva:alarm] FRAMAC_SHARE/libc/string.h:420: Warning:
+ function __gen_e_acsl_strncat, behavior complete: postcondition 'sum_of_lengths' got status unknown.
+[eva:alarm] tests/builtin/strcat.c:40: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_11);
+[eva:alarm] tests/builtin/strcat.c:41: Warning:
+ function __gen_e_acsl_strncat, behavior complete: precondition 'room_string' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:41: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_12);
+[eva:alarm] tests/builtin/strcat.c:42: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&unalloc_str);
+[eva:alarm] tests/builtin/strcat.c:42: Warning:
+ function __gen_e_acsl_strncat: precondition 'valid_string_dest' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:42: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_13);
+[eva:alarm] tests/builtin/strcat.c:43: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&unalloc_str);
+[eva:alarm] tests/builtin/strcat.c:43: Warning:
+ function __gen_e_acsl_strncat: precondition 'valid_nstring_src' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:43: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_14);
+[eva:alarm] tests/builtin/strcat.c:44: Warning:
+ function __gen_e_acsl_strncat: precondition 'valid_string_dest' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:44: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_15);
+[eva:alarm] tests/builtin/strcat.c:45: Warning:
+ function __gen_e_acsl_strncat: precondition 'valid_nstring_src' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:45: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_16);
+[eva:alarm] tests/builtin/strcat.c:46: Warning:
+ function __gen_e_acsl_strncat: precondition 'valid_string_dest' got status invalid.
+[eva:alarm] tests/builtin/strcat.c:46: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_17);
+[eva:alarm] FRAMAC_SHARE/libc/string.h:428: Warning:
+ function __gen_e_acsl_strncat, behavior partial: postcondition 'sum_of_bounded_lengths' got status unknown.
+[eva:alarm] tests/builtin/strcat.c:48: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_18);
+[eva:alarm] tests/builtin/strcat.c:49: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_19);
+[eva:alarm] tests/builtin/strcat.c:50: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_20);
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.err.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index 404779b826aa132522f7e4fc775bf99d1a7e426d..f520c037f51cc7532000a21c79fe10705b4ccd9f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -1,67 +1,86 @@
-tests/builtin/strcmp.c:32:[kernel] warning: Calling undeclared function fork. Old style K&R code?
+[kernel:typing:implicit-function-declaration] tests/builtin/strcmp.c:32: Warning:
+ Calling undeclared function fork. Old style K&R code?
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcmp':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strncmp':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strdup':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:146:[kernel] warning: Neither code nor specification for function fprintf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-tests/builtin/strcmp.c:32:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:396:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:399:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:127:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:128:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:128:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:130:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:120:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:121:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:121:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:123:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:123:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[e-acsl] Warning: annotating undefined function `abort':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `exit':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `waitpid':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strcmp':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strncmp':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strdup':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:165: Warning:
+ Neither code nor specification for function fprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/strcmp.c:32: Warning:
+ Neither code nor specification for function fork, generating default assigns from the prototype
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:394: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:144: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:145: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:145: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:147: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:137: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:138: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:138: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:140: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:406: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
__e_acsl_init ∈ [--..--]
- stderr ∈ {{ NULL ; &S___fc_stderr[0] }}
- __fc_fopen[0..15] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
testno ∈ {0}
- __fc_strtok_ptr ∈ {0}
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
__gen_e_acsl_literal_string_3 ∈ {0}
@@ -94,14 +113,149 @@ FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns claus
__gen_e_acsl_literal_string_30 ∈ {0}
__gen_e_acsl_literal_string_31 ∈ {0}
__gen_e_acsl_literal_string_32 ∈ {0}
- S___fc_stderr[0..1] ∈ [--..--]
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function strdup
-FRAMAC_SHARE/libc/string.h:396:[value] warning: ignoring unsupported \allocates clause
-FRAMAC_SHARE/libc/string.h:399:[value] warning: function strdup: this postcondition evaluates to false in this context.
- If it is valid, either a precondition was not verified for this call,
- or some assigns/from clauses are incomplete (or incorrect).
-[value] done for function main
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_full_init
+[eva] using specification for function __e_acsl_mark_readonly
+[eva] using specification for function strdup
+[eva:libc:unsupported-spec] FRAMAC_SHARE/libc/string.h:443: Warning:
+ The specification of function 'strdup' is currently not supported by Eva.
+ Consider adding FRAMAC_SHARE/libc/string.c
+ to the analyzed source files.
+[eva] FRAMAC_SHARE/libc/string.h:443: Warning:
+ ignoring unsupported \allocates clause
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] FRAMAC_SHARE/libc/string.h:449: Warning:
+ function __gen_e_acsl_strdup, behavior allocation: postcondition 'allocation' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:451: Warning:
+ function __gen_e_acsl_strdup, behavior allocation: postcondition 'result_valid_string_and_same_contents' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:456: Warning:
+ function __gen_e_acsl_strdup, behavior no_allocation: postcondition 'result_null' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva] using specification for function fork
+[eva] using specification for function __e_acsl_builtin_strcmp
+[eva] FRAMAC_SHARE/libc/string.h:140:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:140: Warning:
+ function __gen_e_acsl_strcmp: postcondition 'acsl_c_equiv' got status unknown.
+[eva] using specification for function fprintf
+[eva] using specification for function abort
+[eva] using specification for function exit
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function waitpid
+[eva] using specification for function __e_acsl_initialized
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
+[eva:alarm] tests/builtin/strcmp.c:32: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status);
+[eva] using specification for function printf
+[eva:alarm] tests/builtin/strcmp.c:33: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_0);
+[eva:alarm] tests/builtin/strcmp.c:34: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:34: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_1);
+[eva] using specification for function __e_acsl_initialize
+[eva:alarm] tests/builtin/strcmp.c:36: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:36: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_2);
+[eva:alarm] tests/builtin/strcmp.c:37: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s2' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:37: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_3);
+[eva:alarm] tests/builtin/strcmp.c:38: Warning:
+ out of bounds write. assert \valid(dl + 3);
+[kernel] tests/builtin/strcmp.c:38: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/builtin/strcmp.c:38: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_4);
+[eva:alarm] tests/builtin/strcmp.c:39: Warning:
+ out of bounds write. assert \valid(dr + 3);
+[kernel] tests/builtin/strcmp.c:39: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/builtin/strcmp.c:39: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_5);
+[eva:alarm] tests/builtin/strcmp.c:41: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:41: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_6);
+[eva:alarm] tests/builtin/strcmp.c:42: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:42: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_7);
+[eva:alarm] tests/builtin/strcmp.c:44: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva:alarm] tests/builtin/strcmp.c:45: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva:alarm] tests/builtin/strcmp.c:47: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:47: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_8);
+[eva:alarm] tests/builtin/strcmp.c:48: Warning:
+ function __gen_e_acsl_strcmp: precondition 'valid_string_s2' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:48: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_9);
+[eva] using specification for function __e_acsl_builtin_strncmp
+[eva] FRAMAC_SHARE/libc/string.h:147:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function strncmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:147: Warning:
+ function __gen_e_acsl_strncmp: postcondition 'acsl_c_equiv' got status unknown.
+[eva:alarm] tests/builtin/strcmp.c:57: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_10);
+[eva:alarm] tests/builtin/strcmp.c:58: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_11);
+[eva:alarm] tests/builtin/strcmp.c:59: Warning:
+ function __gen_e_acsl_strncmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:59: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_12);
+[eva:alarm] tests/builtin/strcmp.c:61: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_13);
+[eva:alarm] tests/builtin/strcmp.c:62: Warning:
+ function __gen_e_acsl_strncmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:62: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_14);
+[eva:alarm] tests/builtin/strcmp.c:65: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_15);
+[eva:alarm] tests/builtin/strcmp.c:66: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_16);
+[eva:alarm] tests/builtin/strcmp.c:67: Warning:
+ out of bounds write. assert \valid(dl + 3);
+[kernel] tests/builtin/strcmp.c:67: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/builtin/strcmp.c:67: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_17);
+[eva:alarm] tests/builtin/strcmp.c:68: Warning:
+ out of bounds write. assert \valid(dr + 3);
+[kernel] tests/builtin/strcmp.c:68: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/builtin/strcmp.c:68: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_18);
+[eva:alarm] tests/builtin/strcmp.c:71: Warning:
+ function __gen_e_acsl_strncmp: precondition 'valid_string_s1' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:71: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_19);
+[eva:alarm] tests/builtin/strcmp.c:72: Warning:
+ function __gen_e_acsl_strncmp: precondition 'valid_string_s2' got status invalid.
+[eva:alarm] tests/builtin/strcmp.c:72: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_20);
+[eva:alarm] tests/builtin/strcmp.c:73: Warning:
+ out of bounds write. assert \valid(dl + 3);
+[kernel] tests/builtin/strcmp.c:73: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/builtin/strcmp.c:73: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_21);
+[eva:alarm] tests/builtin/strcmp.c:74: Warning:
+ out of bounds write. assert \valid(dr + 3);
+[kernel] tests/builtin/strcmp.c:74: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva:alarm] tests/builtin/strcmp.c:74: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_22);
+[eva:alarm] tests/builtin/strcmp.c:76: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva:alarm] tests/builtin/strcmp.c:77: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.err.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 2c8fe2a0aa0591be58b322e9cb5dcbf82b824117..e39196409126d5cf197fe7aab5ba02d7b0ca0b66 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -1,62 +1,82 @@
-tests/builtin/strcpy.c:21:[kernel] warning: Calling undeclared function fork. Old style K&R code?
+[kernel:typing:implicit-function-declaration] tests/builtin/strcpy.c:21: Warning:
+ Calling undeclared function fork. Old style K&R code?
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strncpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strdup':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-tests/builtin/strcpy.c:21:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:396:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:399:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:321:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:322:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:328:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:328:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:326:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:331:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:309:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:310:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:312:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:312:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:315:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:316:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[e-acsl] Warning: annotating undefined function `exit':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `waitpid':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strcpy':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strncpy':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strdup':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/strcpy.c:21: Warning:
+ Neither code nor specification for function fork, generating default assigns from the prototype
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:404: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:359: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning:
+ E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:371: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:347: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:348: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:350: Warning:
+ E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:350: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:353: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
__e_acsl_init ∈ [--..--]
- __fc_fopen[0..15] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
testno ∈ {0}
- __fc_strtok_ptr ∈ {0}
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
__gen_e_acsl_literal_string_3 ∈ {0}
@@ -81,13 +101,132 @@ FRAMAC_SHARE/libc/string.h:316:[e-acsl] warning: E-ACSL construct `assigns claus
__gen_e_acsl_literal_string_22 ∈ {0}
__gen_e_acsl_literal_string_23 ∈ {0}
__gen_e_acsl_literal_string_24 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function strdup
-FRAMAC_SHARE/libc/string.h:396:[value] warning: ignoring unsupported \allocates clause
-FRAMAC_SHARE/libc/string.h:399:[value] warning: function strdup: this postcondition evaluates to false in this context.
- If it is valid, either a precondition was not verified for this call,
- or some assigns/from clauses are incomplete (or incorrect).
-[value] done for function main
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_full_init
+[eva] using specification for function __e_acsl_mark_readonly
+[eva] using specification for function strdup
+[eva:libc:unsupported-spec] FRAMAC_SHARE/libc/string.h:443: Warning:
+ The specification of function 'strdup' is currently not supported by Eva.
+ Consider adding FRAMAC_SHARE/libc/string.c
+ to the analyzed source files.
+[eva] FRAMAC_SHARE/libc/string.h:443: Warning:
+ ignoring unsupported \allocates clause
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] FRAMAC_SHARE/libc/string.h:449: Warning:
+ function __gen_e_acsl_strdup, behavior allocation: postcondition 'allocation' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:451: Warning:
+ function __gen_e_acsl_strdup, behavior allocation: postcondition 'result_valid_string_and_same_contents' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:456: Warning:
+ function __gen_e_acsl_strdup, behavior no_allocation: postcondition 'result_null' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva] tests/builtin/strcpy.c:13: allocating variable __malloc_main_l13
+[eva] tests/builtin/strcpy.c:14: allocating variable __malloc_main_l14
+[eva] tests/builtin/strcpy.c:18: allocating variable __malloc_main_l18
+[eva] using specification for function fork
+[eva:alarm] tests/builtin/strcpy.c:21: Warning:
+ function __gen_e_acsl_strcpy: precondition 'valid_string_src' got status invalid.
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function waitpid
+[eva] using specification for function __e_acsl_initialized
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
+[eva:alarm] tests/builtin/strcpy.c:21: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status);
+[eva] using specification for function printf
+[eva] using specification for function exit
+[eva] using specification for function __e_acsl_builtin_strcpy
+[eva] FRAMAC_SHARE/libc/string.h:353:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:353: Warning:
+ function __gen_e_acsl_strcpy: postcondition 'equal_contents' got status unknown.
+[eva:alarm] tests/builtin/strcpy.c:22: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_0);
+[eva:alarm] tests/builtin/strcpy.c:23: Warning:
+ function __gen_e_acsl_strcpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:23: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_1);
+[eva:alarm] tests/builtin/strcpy.c:24: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&unalloc_str);
+[eva:alarm] tests/builtin/strcpy.c:24: Warning:
+ function __gen_e_acsl_strcpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:24: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_2);
+[eva:alarm] tests/builtin/strcpy.c:25: Warning:
+ function __gen_e_acsl_strcpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:25: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_3);
+[eva:alarm] tests/builtin/strcpy.c:26: Warning:
+ function __gen_e_acsl_strcpy: precondition 'room_string' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:26: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_4);
+[eva:alarm] tests/builtin/strcpy.c:27: Warning:
+ function __gen_e_acsl_strcpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:27: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_5);
+[eva:alarm] tests/builtin/strcpy.c:28: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_6);
+[eva:alarm] tests/builtin/strcpy.c:29: Warning:
+ function __gen_e_acsl_strcpy: precondition 'separation' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:29: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_7);
+[eva:alarm] tests/builtin/strcpy.c:32: Warning:
+ function __gen_e_acsl_strncpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:32: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_8);
+[eva:alarm] tests/builtin/strcpy.c:33: Warning:
+ function __gen_e_acsl_strncpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:33: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_9);
+[eva:alarm] tests/builtin/strcpy.c:34: Warning:
+ accessing left-value that contains escaping addresses.
+ assert ¬\dangling(&unalloc_str);
+[eva:alarm] tests/builtin/strcpy.c:34: Warning:
+ function __gen_e_acsl_strncpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:34: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_10);
+[eva:alarm] tests/builtin/strcpy.c:35: Warning:
+ function __gen_e_acsl_strncpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:35: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_11);
+[eva:alarm] tests/builtin/strcpy.c:36: Warning:
+ function __gen_e_acsl_strncpy: precondition 'room_nstring' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:36: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_12);
+[eva:alarm] tests/builtin/strcpy.c:37: Warning:
+ function __gen_e_acsl_strncpy: precondition 'valid_string_src' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:37: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_13);
+[eva] using specification for function __gmpz_init_set_ui
+[eva] using specification for function __gmpz_init_set
+[eva] using specification for function __gmpz_clear
+[eva:alarm] FRAMAC_SHARE/libc/string.h:358: Warning:
+ function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
+[eva] using specification for function __gmpz_init_set_si
+[eva] using specification for function __gmpz_init
+[eva] using specification for function __gmpz_sub
+[eva] using specification for function __gmpz_mul
+[eva] using specification for function __gmpz_cmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:360: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpz_get_ui
+[eva] using specification for function __e_acsl_builtin_strncpy
+[eva] FRAMAC_SHARE/libc/string.h:369:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:366: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:369: Warning:
+ function __gen_e_acsl_strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
+[eva:alarm] tests/builtin/strcpy.c:38: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_14);
+[eva:alarm] tests/builtin/strcpy.c:39: Warning:
+ function __gen_e_acsl_strncpy: precondition 'separation' got status invalid.
+[eva:alarm] tests/builtin/strcpy.c:39: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_15);
+[eva:alarm] tests/builtin/strcpy.c:41: Warning:
+ function free: precondition 'freeable' got status unknown.
+[eva] using specification for function __e_acsl_memory_clean
+[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.err.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.err.oracle
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 675c7462d45230c72704dbd497d4bdac24771fc0..10bba2830aa280e21895a86b3bf4455039ffba2f 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -1,52 +1,66 @@
-tests/builtin/strlen.c:18:[kernel] warning: Calling undeclared function fork. Old style K&R code?
+[kernel:typing:implicit-function-declaration] tests/builtin/strlen.c:18: Warning:
+ Calling undeclared function fork. Old style K&R code?
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `abort':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `exit':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] warning: annotating undefined function `strdup':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdio.h:150:[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
-FRAMAC_SHARE/libc/sys/wait.h:60:[kernel] warning: Neither code nor specification for function waitpid, generating default assigns from the prototype
-tests/builtin/strlen.c:18:[kernel] warning: Neither code nor specification for function fork, generating default assigns from the prototype
-FRAMAC_SHARE/libc/string.h:396:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:396:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:399:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:108:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:108:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:110:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:110:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+[e-acsl] Warning: annotating undefined function `abort':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `exit':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `waitpid':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strlen':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[e-acsl] Warning: annotating undefined function `strdup':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning:
+ Neither code nor specification for function printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtin/strlen.c:18: Warning:
+ Neither code nor specification for function fork, generating default assigns from the prototype
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:394: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning:
+ E-ACSL construct `logic function returning an integer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:406: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[value] Analyzing a complete application starting at main
-[value] Computing initial state
-[value] Initial state computed
-[value:initial-state] Values of globals at initialization
- __fc_rand_max ∈ {32767}
- __fc_heap_status ∈ [--..--]
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
__e_acsl_init ∈ [--..--]
- __fc_fopen[0..15] ∈ {0}
- __fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_heap_allocation_size ∈ [--..--]
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __fc_time ∈ [--..--]
testno ∈ {0}
- __fc_strtok_ptr ∈ {0}
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
__gen_e_acsl_literal_string_3 ∈ {0}
@@ -62,13 +76,49 @@ FRAMAC_SHARE/libc/stdlib.h:415:[e-acsl] warning: E-ACSL construct `assigns claus
__gen_e_acsl_literal_string_13 ∈ {0}
__gen_e_acsl_literal_string_14 ∈ {0}
__gen_e_acsl_literal_string_15 ∈ {0}
-[value] using specification for function __e_acsl_memory_init
-[value] using specification for function __e_acsl_store_block
-[value] using specification for function __e_acsl_full_init
-[value] using specification for function __e_acsl_mark_readonly
-[value] using specification for function strdup
-FRAMAC_SHARE/libc/string.h:396:[value] warning: ignoring unsupported \allocates clause
-FRAMAC_SHARE/libc/string.h:399:[value] warning: function strdup: this postcondition evaluates to false in this context.
- If it is valid, either a precondition was not verified for this call,
- or some assigns/from clauses are incomplete (or incorrect).
-[value] done for function main
+[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_store_block
+[eva] using specification for function __e_acsl_full_init
+[eva] using specification for function __e_acsl_mark_readonly
+[eva] using specification for function strdup
+[eva:libc:unsupported-spec] FRAMAC_SHARE/libc/string.h:443: Warning:
+ The specification of function 'strdup' is currently not supported by Eva.
+ Consider adding FRAMAC_SHARE/libc/string.c
+ to the analyzed source files.
+[eva] FRAMAC_SHARE/libc/string.h:443: Warning:
+ ignoring unsupported \allocates clause
+[eva] using specification for function __e_acsl_delete_block
+[eva:alarm] FRAMAC_SHARE/libc/string.h:449: Warning:
+ function __gen_e_acsl_strdup, behavior allocation: postcondition 'allocation' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:451: Warning:
+ function __gen_e_acsl_strdup, behavior allocation: postcondition 'result_valid_string_and_same_contents' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:456: Warning:
+ function __gen_e_acsl_strdup, behavior no_allocation: postcondition 'result_null' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva] using specification for function fork
+[eva] using specification for function __e_acsl_builtin_strlen
+[eva] using specification for function exit
+[eva] using specification for function __e_acsl_valid
+[eva] using specification for function __e_acsl_assert
+[eva] using specification for function waitpid
+[eva] using specification for function __e_acsl_initialized
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] FRAMAC_SHARE/libc/sys/wait.h:86: Warning:
+ function __gen_e_acsl_waitpid: postcondition 'initialization,stat_loc_init_on_success' got status unknown.
+[eva:alarm] tests/builtin/strlen.c:18: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status);
+[eva] using specification for function printf
+[eva:alarm] tests/builtin/strlen.c:19: Warning:
+ function __gen_e_acsl_strlen: precondition 'valid_string_s' got status invalid.
+[eva:alarm] tests/builtin/strlen.c:19: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_0);
+[eva:alarm] tests/builtin/strlen.c:20: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_1);
+[eva:alarm] tests/builtin/strlen.c:21: Warning:
+ accessing uninitialized left-value. assert \initialized(&process_status_2);
+[eva] using specification for function __e_acsl_initialize
+[eva:alarm] tests/builtin/strlen.c:23: Warning:
+ out of bounds write. assert \valid(heap_str + 7);
+[kernel] tests/builtin/strlen.c:23: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] done for function main