Commit ca38c040 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov Committed by Julien Signoles
Browse files

New tests

parent 4fb19e96
Like full-model, but also test instrumentation with -e-acsl-replace-libc-functions
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "sys/time.h"
#include "sys/wait.h"
char *__gen_e_acsl_literal_string_8;
char *__gen_e_acsl_literal_string_7;
char *__gen_e_acsl_literal_string_15;
char *__gen_e_acsl_literal_string_14;
char *__gen_e_acsl_literal_string_13;
char *__gen_e_acsl_literal_string_12;
char *__gen_e_acsl_literal_string_11;
char *__gen_e_acsl_literal_string_10;
char *__gen_e_acsl_literal_string_9;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string_5;
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)();
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 *)(& 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)4096);
__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;
}
int main(int argc, char const **argv)
{
int __retres;
int len;
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
__e_acsl_store_block((void *)(& len),(size_t)4);
__e_acsl_store_block((void *)(& __retres),(size_t)4);
char *empty_str = (char *)__gen_e_acsl_literal_string_6;
__e_acsl_store_block((void *)(& empty_str),(size_t)8);
__e_acsl_full_init((void *)(& empty_str));
char *heap_str = __gen_e_acsl_strdup(__gen_e_acsl_literal_string_7);
__e_acsl_store_block((void *)(& heap_str),(size_t)8);
__e_acsl_full_init((void *)(& heap_str));
char stack_str[8] =
{(char)'t',
(char)'h',
(char)'e',
(char)' ',
(char)'d',
(char)'o',
(char)'g',
(char)'\000'};
__e_acsl_store_block((void *)(stack_str),(size_t)8);
__e_acsl_full_init((void *)(& stack_str));
char *const_str = (char *)__gen_e_acsl_literal_string_8;
__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;
__e_acsl_store_block((void *)(& pid),(size_t)4);
__e_acsl_full_init((void *)(& pid));
if (! pid) {
size_t tmp_1;
__e_acsl_store_block((void *)(& tmp_1),(size_t)8);
__e_acsl_full_init((void *)(& tmp_1));
tmp_1 = __gen_e_acsl_strlen((char const *)empty_str);
__e_acsl_full_init((void *)(& len));
len = tmp_1 != (size_t)0;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_1));
}
else {
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
waitpid(pid,& process_status,0);
/*@ assert Value: initialisation: \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;
__e_acsl_store_block((void *)(& pid_0),(size_t)4);
__e_acsl_full_init((void *)(& pid_0));
if (! pid_0) {
size_t tmp_3;
__e_acsl_store_block((void *)(& tmp_3),(size_t)8);
__e_acsl_full_init((void *)(& tmp_3));
tmp_3 = __gen_e_acsl_strlen((char const *)heap_str);
__e_acsl_full_init((void *)(& len));
len = tmp_3 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_3));
}
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: initialisation: \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;
__e_acsl_store_block((void *)(& pid_1),(size_t)4);
__e_acsl_full_init((void *)(& pid_1));
if (! pid_1) {
size_t tmp_5;
__e_acsl_store_block((void *)(& tmp_5),(size_t)8);
__e_acsl_full_init((void *)(& tmp_5));
tmp_5 = __gen_e_acsl_strlen((char const *)(stack_str));
__e_acsl_full_init((void *)(& len));
len = tmp_5 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_5));
}
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: initialisation: \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;
__e_acsl_store_block((void *)(& pid_2),(size_t)4);
__e_acsl_full_init((void *)(& pid_2));
if (! pid_2) {
size_t tmp_7;
__e_acsl_store_block((void *)(& tmp_7),(size_t)8);
__e_acsl_full_init((void *)(& tmp_7));
tmp_7 = __gen_e_acsl_strlen((char const *)const_str);
__e_acsl_full_init((void *)(& len));
len = tmp_7 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_7));
}
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: initialisation: \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));
*(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;
__e_acsl_store_block((void *)(& pid_3),(size_t)4);
__e_acsl_full_init((void *)(& pid_3));
if (! pid_3) {
size_t tmp_9;
__e_acsl_store_block((void *)(& tmp_9),(size_t)8);
__e_acsl_full_init((void *)(& tmp_9));
tmp_9 = __gen_e_acsl_strlen((char const *)heap_str);
__e_acsl_full_init((void *)(& len));
len = tmp_9 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_9));
}
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: initialisation: \initialized(&process_status_3); */
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;
__e_acsl_store_block((void *)(& pid_4),(size_t)4);
__e_acsl_full_init((void *)(& pid_4));
if (! pid_4) {
size_t tmp_11;
__e_acsl_store_block((void *)(& tmp_11),(size_t)8);
__e_acsl_full_init((void *)(& tmp_11));
tmp_11 = __gen_e_acsl_strlen((char const *)(stack_str));
__e_acsl_full_init((void *)(& len));
len = tmp_11 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_11));
}
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: initialisation: \initialized(&process_status_4); */
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;
__e_acsl_store_block((void *)(& pid_5),(size_t)4);
__e_acsl_full_init((void *)(& pid_5));
if (! pid_5) {
size_t tmp_13;
__e_acsl_store_block((void *)(& tmp_13),(size_t)8);
__e_acsl_full_init((void *)(& tmp_13));
tmp_13 = __gen_e_acsl_strlen((char const *)heap_str);
__e_acsl_full_init((void *)(& len));
len = tmp_13 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
__e_acsl_delete_block((void *)(& tmp_13));
}
else {
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
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 *)(& signal_eval));
__e_acsl_delete_block((void *)(& testno));
__e_acsl_delete_block((void *)(& __fc_time));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
__e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(& const_str));
__e_acsl_delete_block((void *)(stack_str));
__e_acsl_delete_block((void *)(& heap_str));
__e_acsl_delete_block((void *)(& empty_str));
__e_acsl_delete_block((void *)(& len));
__e_acsl_delete_block((void *)(& __retres));
__e_acsl_memory_clean();
return __retres;
}
tests/builtin/strcat.c:26:[kernel] 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:57:[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:276:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:277:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:282:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:289:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:289:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:280:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:282:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:264:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:265:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:266:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:266:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:269:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:269:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:271:[e-acsl] 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 ∈ [--..--]
__e_acsl_init ∈ [--..--]
__fc_fopen[0..511] ∈ {0}
__fc_p_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_internal_heap ∈ [--..--]
__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}
__gen_e_acsl_literal_string ∈ {0}
__gen_e_acsl_literal_string_2 ∈ {0}
__gen_e_acsl_literal_string_3 ∈ {0}
__gen_e_acsl_literal_string_4 ∈ {0}
__gen_e_acsl_literal_string_5 ∈ {0}
__gen_e_acsl_literal_string_6 ∈ {0}
__gen_e_acsl_literal_string_7 ∈ {0}
__gen_e_acsl_literal_string_8 ∈ {0}
__gen_e_acsl_literal_string_9 ∈ {0}
__gen_e_acsl_literal_string_10 ∈ {0}
__gen_e_acsl_literal_string_11 ∈ {0}
__gen_e_acsl_literal_string_12 ∈ {0}
__gen_e_acsl_literal_string_13 ∈ {0}
__gen_e_acsl_literal_string_14 ∈ {0}
__gen_e_acsl_literal_string_15 ∈ {0}
__gen_e_acsl_literal_string_16 ∈ {0}
__gen_e_acsl_literal_string_17 ∈ {0}
__gen_e_acsl_literal_string_18 ∈ {0}
__gen_e_acsl_literal_string_19 ∈ {0}
__gen_e_acsl_literal_string_20 ∈ {0}
__gen_e_acsl_literal_string_21 ∈ {0}
__gen_e_acsl_literal_string_22 ∈ {0}
__gen_e_acsl_literal_string_23 ∈ {0}
__gen_e_acsl_literal_string_24 ∈ {0}
__gen_e_acsl_literal_string_25 ∈ {0}
__gen_e_acsl_literal_string_26 ∈ {0}
__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:269:[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);
FRAMAC_SHARE/libc/string.h:266:[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);
FRAMAC_SHARE/libc/string.h:265:[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);
FRAMAC_SHARE/libc/string.h:264:[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: accessing uninitialized left-value. assert \initialized(&process_status_4);
tests/builtin/strcat.c:32:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
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:287:[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);
FRAMAC_SHARE/libc/string.h:283:[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);
FRAMAC_SHARE/libc/string.h:277:[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);
FRAMAC_SHARE/libc/string.h:276:[value] warning: function __gen_e_acsl_strncat: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:276:[value] warning: function __e_acsl_builtin_strncat: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:294:[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: accessing uninitialized left-value. assert \initialized(&process_status_15);
FRAMAC_SHARE/libc/string.h:276:[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: 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
tests/builtin/strcmp.c:32:[kernel] 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:57:[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:308:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:308:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' 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:111:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:112:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:112:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:114:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:104:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.