diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle index 0491679011cca98bc2b52203673139ae77988bd6..ef84cf94d261391ff55db72a03f35a11bc6d6c40 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle @@ -3,7 +3,3 @@ (warn-once: no further messages from category 'parser:decimal-float' will be emitted) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/bts/bts1307.i:11: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/bts/bts1307.i:11: Warning: - function __gen_e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status invalid. diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle index 8a979d24b47fbca95ad85e05fbdfd4446a7fd8eb..efd026311297e55d8fefb674326118e6ece88624 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle @@ -1,4 +1,2 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/bts/bts1324.i:6: Warning: - function __e_acsl_assert: precondition got status unknown. diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle index 929213a9cd28be0c159806a3a650b1cf7b651dfe..3731cb4dd09cd7786331ee6473a3a0fdf691a7c2 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle @@ -2,11 +2,3 @@ [e-acsl] translation done in project "e-acsl". [eva:builtins:missing-spec] tests/bts/bts1390.c:13: Warning: The builtin for function memchr will not be used, as its frama-c libc specification is not available. -[eva:alarm] tests/bts/bts1390.c:11: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/bts/bts1390.c:8: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/bts/bts1390.c:12: Warning: - function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] tests/bts/bts1390.c:17: Warning: - out of bounds read. assert \valid_read(s); diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle index f96be2395e669ee4f969c86a91991270c922660a..5e19b9d7d6eecf52c360612ac19e7e7406a776f2 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle @@ -2,7 +2,7 @@ [e-acsl] Warning: annotating undefined function `atoi': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:78: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:77: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle index c0d14a505d07b9519cd7815386d12346a4c15e42..994e5e176d8b6f2c1d0a276505cc9b85773538e7 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle @@ -4,19 +4,30 @@ if there are memory-related annotations. [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:372: Warning: + E-ACSL construct `logic functions performing read accesses' + is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/string.h:375: Warning: + E-ACSL construct `logic functions performing read accesses' + is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:363: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning: + Some assumes clauses couldn't be translated. + Ignoring complete and disjoint behaviors annotations. +[e-acsl] FRAMAC_SHARE/libc/string.h:362: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/string.h:373: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:372: Warning: - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:375: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:376: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c index 33236edf86c22697136f4cbc4a78fa60a60cecac..803635b65a0f4926d91013284a3f86351cf24aa9 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c @@ -96,6 +96,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out) float *__gen_e_acsl_at_3; float *__gen_e_acsl_at_2; float *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; { int __gen_e_acsl_valid; int __gen_e_acsl_valid_2; @@ -103,6 +104,8 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out) __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8); __e_acsl_store_block((void *)(& Mwmin),(size_t)8); __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)1); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1); __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float), (void *)Mtmin_in, (void *)(& Mtmin_in)); @@ -126,87 +129,93 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out) __gen_e_acsl_at = Mtmin_out; bar(Mtmin_in,Mwmin,Mtmin_out); { - int __gen_e_acsl_valid_read; - int __gen_e_acsl_valid_read_2; - int __gen_e_acsl_and; - int __gen_e_acsl_if; - __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2, - sizeof(float), - (void *)__gen_e_acsl_at_2, - (void *)(& __gen_e_acsl_at_2)); - __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","bar", - "mem_access: \\valid_read(__gen_e_acsl_at_2)", - "tests/bts/bts1307.i",26); - __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at, + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_valid_read; + int __gen_e_acsl_valid_read_2; + int __gen_e_acsl_and; + int __gen_e_acsl_if; + __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2, sizeof(float), - (void *)__gen_e_acsl_at, - (void *)(& __gen_e_acsl_at)); - __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","bar", - "mem_access: \\valid_read(__gen_e_acsl_at)", - "tests/bts/bts1307.i",26); - if (*__gen_e_acsl_at == *__gen_e_acsl_at_2) { - __e_acsl_mpq_t __gen_e_acsl_; - __e_acsl_mpq_t __gen_e_acsl__2; - __e_acsl_mpq_t __gen_e_acsl_mul; - __e_acsl_mpq_t __gen_e_acsl__3; - int __gen_e_acsl_lt; - __gmpq_init(__gen_e_acsl_); - __gmpq_set_str(__gen_e_acsl_,"085/100",10); - __gmpq_init(__gen_e_acsl__2); - __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_4); - __gmpq_init(__gen_e_acsl_mul); - __gmpq_mul(__gen_e_acsl_mul, - (__e_acsl_mpq_struct const *)(__gen_e_acsl_), - (__e_acsl_mpq_struct const *)(__gen_e_acsl__2)); - __gmpq_init(__gen_e_acsl__3); - __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3); - __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3), - (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul)); - __gen_e_acsl_and = __gen_e_acsl_lt < 0; - __gmpq_clear(__gen_e_acsl_); - __gmpq_clear(__gen_e_acsl__2); - __gmpq_clear(__gen_e_acsl_mul); - __gmpq_clear(__gen_e_acsl__3); - } - else __gen_e_acsl_and = 0; - if (__gen_e_acsl_and) { - int __gen_e_acsl_valid_read_3; - __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5, + (void *)__gen_e_acsl_at_2, + (void *)(& __gen_e_acsl_at_2)); + __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","bar", + "mem_access: \\valid_read(__gen_e_acsl_at_2)", + "tests/bts/bts1307.i",26); + __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at, sizeof(float), - (void *)__gen_e_acsl_at_5, - (void *)(& __gen_e_acsl_at_5)); - __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","bar", - "mem_access: \\valid_read(__gen_e_acsl_at_5)", + (void *)__gen_e_acsl_at, + (void *)(& __gen_e_acsl_at)); + __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","bar", + "mem_access: \\valid_read(__gen_e_acsl_at)", + "tests/bts/bts1307.i",26); + if (*__gen_e_acsl_at == *__gen_e_acsl_at_2) { + __e_acsl_mpq_t __gen_e_acsl_; + __e_acsl_mpq_t __gen_e_acsl__2; + __e_acsl_mpq_t __gen_e_acsl_mul; + __e_acsl_mpq_t __gen_e_acsl__3; + int __gen_e_acsl_lt; + __gmpq_init(__gen_e_acsl_); + __gmpq_set_str(__gen_e_acsl_,"085/100",10); + __gmpq_init(__gen_e_acsl__2); + __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_4); + __gmpq_init(__gen_e_acsl_mul); + __gmpq_mul(__gen_e_acsl_mul, + (__e_acsl_mpq_struct const *)(__gen_e_acsl_), + (__e_acsl_mpq_struct const *)(__gen_e_acsl__2)); + __gmpq_init(__gen_e_acsl__3); + __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3); + __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3), + (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul)); + __gen_e_acsl_and = __gen_e_acsl_lt < 0; + __gmpq_clear(__gen_e_acsl_); + __gmpq_clear(__gen_e_acsl__2); + __gmpq_clear(__gen_e_acsl_mul); + __gmpq_clear(__gen_e_acsl__3); + } + else __gen_e_acsl_and = 0; + if (__gen_e_acsl_and) { + int __gen_e_acsl_valid_read_3; + __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5, + sizeof(float), + (void *)__gen_e_acsl_at_5, + (void *)(& __gen_e_acsl_at_5)); + __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","bar", + "mem_access: \\valid_read(__gen_e_acsl_at_5)", + "tests/bts/bts1307.i",26); + __gen_e_acsl_if = (double)*__gen_e_acsl_at_5 != 0.; + } + else { + __e_acsl_mpq_t __gen_e_acsl__4; + __e_acsl_mpq_t __gen_e_acsl__5; + __e_acsl_mpq_t __gen_e_acsl_mul_2; + __e_acsl_mpq_t __gen_e_acsl__6; + int __gen_e_acsl_ne; + __gmpq_init(__gen_e_acsl__4); + __gmpq_set_str(__gen_e_acsl__4,"085/100",10); + __gmpq_init(__gen_e_acsl__5); + __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_6); + __gmpq_init(__gen_e_acsl_mul_2); + __gmpq_mul(__gen_e_acsl_mul_2, + (__e_acsl_mpq_struct const *)(__gen_e_acsl__4), + (__e_acsl_mpq_struct const *)(__gen_e_acsl__5)); + __gmpq_init(__gen_e_acsl__6); + __gmpq_set_d(__gen_e_acsl__6,0.); + __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2), + (__e_acsl_mpq_struct const *)(__gen_e_acsl__6)); + __gen_e_acsl_if = __gen_e_acsl_ne != 0; + __gmpq_clear(__gen_e_acsl__4); + __gmpq_clear(__gen_e_acsl__5); + __gmpq_clear(__gen_e_acsl_mul_2); + __gmpq_clear(__gen_e_acsl__6); + } + __e_acsl_assert(__gen_e_acsl_if,"Postcondition","bar", + "UnderEstimate_Motoring:\n *\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85 * *\\old(Mwmin) != 0.", "tests/bts/bts1307.i",26); - __gen_e_acsl_if = (double)*__gen_e_acsl_at_5 != 0.; - } - else { - __e_acsl_mpq_t __gen_e_acsl__4; - __e_acsl_mpq_t __gen_e_acsl__5; - __e_acsl_mpq_t __gen_e_acsl_mul_2; - __e_acsl_mpq_t __gen_e_acsl__6; - int __gen_e_acsl_ne; - __gmpq_init(__gen_e_acsl__4); - __gmpq_set_str(__gen_e_acsl__4,"085/100",10); - __gmpq_init(__gen_e_acsl__5); - __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_6); - __gmpq_init(__gen_e_acsl_mul_2); - __gmpq_mul(__gen_e_acsl_mul_2, - (__e_acsl_mpq_struct const *)(__gen_e_acsl__4), - (__e_acsl_mpq_struct const *)(__gen_e_acsl__5)); - __gmpq_init(__gen_e_acsl__6); - __gmpq_set_d(__gen_e_acsl__6,0.); - __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2), - (__e_acsl_mpq_struct const *)(__gen_e_acsl__6)); - __gen_e_acsl_if = __gen_e_acsl_ne != 0; - __gmpq_clear(__gen_e_acsl__4); - __gmpq_clear(__gen_e_acsl__5); - __gmpq_clear(__gen_e_acsl_mul_2); - __gmpq_clear(__gen_e_acsl__6); } - __e_acsl_assert(__gen_e_acsl_if,"Postcondition","bar", - "*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85 * *\\old(Mwmin) != 0.", - "tests/bts/bts1307.i",26); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& Mtmin_out)); __e_acsl_delete_block((void *)(& Mwmin)); __e_acsl_delete_block((void *)(& Mtmin_in)); @@ -229,6 +238,7 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out) float *__gen_e_acsl_at_3; float *__gen_e_acsl_at_2; float *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; { int __gen_e_acsl_valid; int __gen_e_acsl_valid_2; @@ -236,6 +246,8 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out) __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8); __e_acsl_store_block((void *)(& Mwmax),(size_t)8); __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)1); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1); __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float), (void *)Mtmax_in, (void *)(& Mtmax_in)); @@ -256,72 +268,79 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out) __gen_e_acsl_at = Mtmax_out; foo(Mtmax_in,Mwmax,Mtmax_out); { - __e_acsl_mpq_t __gen_e_acsl_; - __e_acsl_mpq_t __gen_e_acsl__2; - __e_acsl_mpq_t __gen_e_acsl__3; - __e_acsl_mpq_t __gen_e_acsl_div; - __e_acsl_mpq_t __gen_e_acsl__4; - __e_acsl_mpq_t __gen_e_acsl_mul; - __e_acsl_mpq_t __gen_e_acsl__5; - __e_acsl_mpq_t __gen_e_acsl_mul_2; - __e_acsl_mpq_t __gen_e_acsl_sub; - __e_acsl_mpq_t __gen_e_acsl__6; - __e_acsl_mpq_t __gen_e_acsl_add; - __e_acsl_mpq_t __gen_e_acsl__7; - int __gen_e_acsl_ne; - __gmpq_init(__gen_e_acsl_); - __gmpq_set_str(__gen_e_acsl_,"5",10); - __gmpq_init(__gen_e_acsl__2); - __gmpq_set_si(__gen_e_acsl__2,5L,1UL); - __gmpq_init(__gen_e_acsl__3); - __gmpq_set_si(__gen_e_acsl__3,80L,1UL); - __gmpq_init(__gen_e_acsl_div); - __gmpq_div(__gen_e_acsl_div, - (__e_acsl_mpq_struct const *)(__gen_e_acsl__2), - (__e_acsl_mpq_struct const *)(__gen_e_acsl__3)); - __gmpq_init(__gen_e_acsl__4); - __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_3); - __gmpq_init(__gen_e_acsl_mul); - __gmpq_mul(__gen_e_acsl_mul, - (__e_acsl_mpq_struct const *)(__gen_e_acsl_div), - (__e_acsl_mpq_struct const *)(__gen_e_acsl__4)); - __gmpq_init(__gen_e_acsl__5); - __gmpq_set_str(__gen_e_acsl__5,"04/10",10); - __gmpq_init(__gen_e_acsl_mul_2); - __gmpq_mul(__gen_e_acsl_mul_2, - (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul), - (__e_acsl_mpq_struct const *)(__gen_e_acsl__5)); - __gmpq_init(__gen_e_acsl_sub); - __gmpq_sub(__gen_e_acsl_sub,(__e_acsl_mpq_struct const *)(__gen_e_acsl_), - (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2)); - __gmpq_init(__gen_e_acsl__6); - __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_2); - __gmpq_init(__gen_e_acsl_add); - __gmpq_add(__gen_e_acsl_add, - (__e_acsl_mpq_struct const *)(__gen_e_acsl__6), - (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub)); - __gmpq_init(__gen_e_acsl__7); - __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at); - __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7), - (__e_acsl_mpq_struct const *)(__gen_e_acsl_add)); - __e_acsl_assert(__gen_e_acsl_ne != 0,"Postcondition","foo", - "*\\old(Mtmax_out) != *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)", - "tests/bts/bts1307.i",11); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) { + __e_acsl_mpq_t __gen_e_acsl_; + __e_acsl_mpq_t __gen_e_acsl__2; + __e_acsl_mpq_t __gen_e_acsl__3; + __e_acsl_mpq_t __gen_e_acsl_div; + __e_acsl_mpq_t __gen_e_acsl__4; + __e_acsl_mpq_t __gen_e_acsl_mul; + __e_acsl_mpq_t __gen_e_acsl__5; + __e_acsl_mpq_t __gen_e_acsl_mul_2; + __e_acsl_mpq_t __gen_e_acsl_sub; + __e_acsl_mpq_t __gen_e_acsl__6; + __e_acsl_mpq_t __gen_e_acsl_add; + __e_acsl_mpq_t __gen_e_acsl__7; + int __gen_e_acsl_ne; + __gmpq_init(__gen_e_acsl_); + __gmpq_set_str(__gen_e_acsl_,"5",10); + __gmpq_init(__gen_e_acsl__2); + __gmpq_set_si(__gen_e_acsl__2,5L,1UL); + __gmpq_init(__gen_e_acsl__3); + __gmpq_set_si(__gen_e_acsl__3,80L,1UL); + __gmpq_init(__gen_e_acsl_div); + __gmpq_div(__gen_e_acsl_div, + (__e_acsl_mpq_struct const *)(__gen_e_acsl__2), + (__e_acsl_mpq_struct const *)(__gen_e_acsl__3)); + __gmpq_init(__gen_e_acsl__4); + __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_3); + __gmpq_init(__gen_e_acsl_mul); + __gmpq_mul(__gen_e_acsl_mul, + (__e_acsl_mpq_struct const *)(__gen_e_acsl_div), + (__e_acsl_mpq_struct const *)(__gen_e_acsl__4)); + __gmpq_init(__gen_e_acsl__5); + __gmpq_set_str(__gen_e_acsl__5,"04/10",10); + __gmpq_init(__gen_e_acsl_mul_2); + __gmpq_mul(__gen_e_acsl_mul_2, + (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul), + (__e_acsl_mpq_struct const *)(__gen_e_acsl__5)); + __gmpq_init(__gen_e_acsl_sub); + __gmpq_sub(__gen_e_acsl_sub, + (__e_acsl_mpq_struct const *)(__gen_e_acsl_), + (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2)); + __gmpq_init(__gen_e_acsl__6); + __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_2); + __gmpq_init(__gen_e_acsl_add); + __gmpq_add(__gen_e_acsl_add, + (__e_acsl_mpq_struct const *)(__gen_e_acsl__6), + (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub)); + __gmpq_init(__gen_e_acsl__7); + __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at); + __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7), + (__e_acsl_mpq_struct const *)(__gen_e_acsl_add)); + __e_acsl_assert(__gen_e_acsl_ne != 0,"Postcondition","foo", + "OverEstimate_Motoring:\n *\\old(Mtmax_out) != *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)", + "tests/bts/bts1307.i",11); + __gmpq_clear(__gen_e_acsl_); + __gmpq_clear(__gen_e_acsl__2); + __gmpq_clear(__gen_e_acsl__3); + __gmpq_clear(__gen_e_acsl_div); + __gmpq_clear(__gen_e_acsl__4); + __gmpq_clear(__gen_e_acsl_mul); + __gmpq_clear(__gen_e_acsl__5); + __gmpq_clear(__gen_e_acsl_mul_2); + __gmpq_clear(__gen_e_acsl_sub); + __gmpq_clear(__gen_e_acsl__6); + __gmpq_clear(__gen_e_acsl_add); + __gmpq_clear(__gen_e_acsl__7); + } + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& Mtmax_out)); __e_acsl_delete_block((void *)(& Mwmax)); __e_acsl_delete_block((void *)(& Mtmax_in)); - __gmpq_clear(__gen_e_acsl_); - __gmpq_clear(__gen_e_acsl__2); - __gmpq_clear(__gen_e_acsl__3); - __gmpq_clear(__gen_e_acsl_div); - __gmpq_clear(__gen_e_acsl__4); - __gmpq_clear(__gen_e_acsl_mul); - __gmpq_clear(__gen_e_acsl__5); - __gmpq_clear(__gen_e_acsl_mul_2); - __gmpq_clear(__gen_e_acsl_sub); - __gmpq_clear(__gen_e_acsl__6); - __gmpq_clear(__gen_e_acsl_add); - __gmpq_clear(__gen_e_acsl__7); return; } } diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c index a0a428c6ea0988debf0aad02354d54c2e9f1bab4..5e4a49720f5feeb37d719e78341692224a12d81f 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c @@ -52,12 +52,13 @@ int main(void) */ int __gen_e_acsl_sorted(int *t, int n) { - int __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; int __retres; - __e_acsl_store_block((void *)(& t),(size_t)8); { int __gen_e_acsl_forall; int __gen_e_acsl_i; + __e_acsl_store_block((void *)(& t),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)1); __gen_e_acsl_forall = 1; __gen_e_acsl_i = 0 + 1; while (1) { @@ -88,16 +89,19 @@ int __gen_e_acsl_sorted(int *t, int n) __gen_e_acsl_i ++; } e_acsl_end_loop1: ; - __gen_e_acsl_at = __gen_e_acsl_forall; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + __gen_e_acsl_forall); } __retres = sorted(t,n); { - int __gen_e_acsl_implies; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = __retres == 1; - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","sorted", - "\\old(\\forall int i; 0 < i < n ==> *(t + (i - 1)) <= *(t + i)) ==>\n\\result == 1", - "tests/bts/bts1324.i",7); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == 1, + "Postcondition","sorted", + "yes: \\result == 1", + "tests/bts/bts1324.i",7); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& t)); return __retres; } diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c index 058f7b605d8f8d53d6ce9381ff5d84428bc63a14..c771114ecdc191d1419d51435dab70942430b47f 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c @@ -30,7 +30,6 @@ void *memchr(void const *buf, int c, size_t n) __e_acsl_full_init((void *)(& s)); i = 0; while ((size_t)i < n) { - /*@ assert Eva: mem_access: \valid_read(s); */ if ((int)*s == c) { __e_acsl_full_init((void *)(& __retres)); __retres = (void *)s; @@ -64,46 +63,18 @@ void *memchr(void const *buf, int c, size_t n) */ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n) { - int __gen_e_acsl_at_4; - int __gen_e_acsl_at_3; - void const *__gen_e_acsl_at_2; - int __gen_e_acsl_at; + int __gen_e_acsl_at_2; + void const *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; void *__retres; __e_acsl_store_block((void *)(& __retres),(size_t)8); - __e_acsl_store_block((void *)(& buf),(size_t)8); - { - int __gen_e_acsl_forall_2; - unsigned int __gen_e_acsl_k; - __gen_e_acsl_forall_2 = 1; - __gen_e_acsl_k = 0U; - while (1) { - if (__gen_e_acsl_k < (unsigned int)((int)((unsigned int)n))) ; - else break; - { - int __gen_e_acsl_valid_read_3; - __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k), - sizeof(char), - (void *)buf, - (void *)(& buf)); - __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","memchr", - "mem_access: \\valid_read((char *)buf + __gen_e_acsl_k)", - "tests/bts/bts1390.c",11); - if ((int)*((char *)buf + __gen_e_acsl_k) != c) ; - else { - __gen_e_acsl_forall_2 = 0; - goto e_acsl_end_loop3; - } - } - __gen_e_acsl_k ++; - } - e_acsl_end_loop3: ; - __gen_e_acsl_at_4 = __gen_e_acsl_forall_2; - } - __gen_e_acsl_at_3 = c; - __gen_e_acsl_at_2 = buf; { int __gen_e_acsl_exists; unsigned int __gen_e_acsl_i; + int __gen_e_acsl_forall; + unsigned int __gen_e_acsl_k; + __e_acsl_store_block((void *)(& buf),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); __gen_e_acsl_exists = 0; __gen_e_acsl_i = 0U; while (1) { @@ -127,17 +98,45 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n) __gen_e_acsl_i ++; } e_acsl_end_loop1: ; - __gen_e_acsl_at = __gen_e_acsl_exists; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + __gen_e_acsl_exists); + __gen_e_acsl_forall = 1; + __gen_e_acsl_k = 0U; + while (1) { + if (__gen_e_acsl_k < (unsigned int)((int)((unsigned int)n))) ; + else break; + { + int __gen_e_acsl_valid_read_2; + __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k), + sizeof(char), + (void *)buf, + (void *)(& buf)); + __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","memchr", + "mem_access: \\valid_read((char *)buf + __gen_e_acsl_k)", + "tests/bts/bts1390.c",11); + if ((int)*((char *)buf + __gen_e_acsl_k) != c) ; + else { + __gen_e_acsl_forall = 0; + goto e_acsl_end_loop2; + } + } + __gen_e_acsl_k ++; + } + e_acsl_end_loop2: ; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + __gen_e_acsl_forall); } + __gen_e_acsl_at_2 = c; + __gen_e_acsl_at = buf; __retres = memchr(buf,c,n); { - int __gen_e_acsl_implies; - int __gen_e_acsl_implies_2; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else { - int __gen_e_acsl_forall; + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_forall_2; unsigned int __gen_e_acsl_j; - __gen_e_acsl_forall = 1; + __gen_e_acsl_forall_2 = 1; __gen_e_acsl_j = 0; while (1) { { @@ -148,34 +147,35 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n) else break; } { - int __gen_e_acsl_valid_read_2; - __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j), + int __gen_e_acsl_valid_read_3; + __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)__gen_e_acsl_at + __gen_e_acsl_j), sizeof(char), - (void *)__gen_e_acsl_at_2, - (void *)(& __gen_e_acsl_at_2)); - __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","memchr", - "mem_access: \\valid_read((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j)", + (void *)__gen_e_acsl_at, + (void *)(& __gen_e_acsl_at)); + __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","memchr", + "mem_access: \\valid_read((char *)__gen_e_acsl_at + __gen_e_acsl_j)", "tests/bts/bts1390.c",9); - if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at_3) + if ((int)*((char *)__gen_e_acsl_at + __gen_e_acsl_j) != __gen_e_acsl_at_2) ; else { - __gen_e_acsl_forall = 0; - goto e_acsl_end_loop2; + __gen_e_acsl_forall_2 = 0; + goto e_acsl_end_loop3; } } __gen_e_acsl_j ++; } - e_acsl_end_loop2: ; - __gen_e_acsl_implies = __gen_e_acsl_forall; + e_acsl_end_loop3: ; + __e_acsl_assert(__gen_e_acsl_forall_2,"Postcondition","memchr", + "exists:\n \\forall int j;\n 0 <= j < (int)\\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf) + j) != \\old(c)", + "tests/bts/bts1390.c",9); } - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","memchr", - "\\old(\\exists integer i; 0 <= i < (int)n && (int)*((char *)buf + i) == c) ==>\n(\\forall int j;\n 0 <= j < (int)\\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf) + j) != \\old(c))", - "tests/bts/bts1390.c",9); - if (! __gen_e_acsl_at_4) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = __retres == (void *)0; - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","memchr", - "\\old(\\forall integer k; 0 <= k < (int)n ==> (int)*((char *)buf + k) != c) ==>\n\\result == (void *)0", - "tests/bts/bts1390.c",12); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == (void *)0, + "Postcondition","memchr", + "not_exists: \\result == (void *)0", + "tests/bts/bts1390.c",12); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& buf)); __e_acsl_delete_block((void *)(& __retres)); return __retres; diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c index bbf7b668bdeb592b79c4c964bcaffffc11ab6bcd..58c0df1de84e4233601befe38ea728af74dfe708 100644 --- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c +++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c @@ -53,6 +53,7 @@ char *__gen_e_acsl_strncpy(char * __restrict dest, __e_acsl_mpz_t __gen_e_acsl_at_3; char *__gen_e_acsl_at_2; char *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; char *__retres; { __e_acsl_mpz_t __gen_e_acsl_n; @@ -64,6 +65,7 @@ char *__gen_e_acsl_strncpy(char * __restrict dest, unsigned long __gen_e_acsl__3; int __gen_e_acsl_valid; __e_acsl_store_block((void *)(& dest),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); __gmpz_init_set_ui(__gen_e_acsl_n,n); __gmpz_init_set_si(__gen_e_acsl_,1L); __gmpz_init(__gen_e_acsl_sub); @@ -135,6 +137,7 @@ char *__gen_e_acsl_strncpy(char * __restrict dest, __e_acsl_assert(__gen_e_acsl_initialized,"Postcondition","strncpy", "\\initialized(\\old(dest) + (0 .. \\old(n) - 1))", "FRAMAC_SHARE/libc/string.h",370); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& dest)); __gmpz_clear(__gen_e_acsl__4); __gmpz_clear(__gen_e_acsl_sub_3); diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c index c1d683e5f6d17e3e7acd9762ac651218ce782be7..6a00983f31056b0fcd24ff0e3cfd5c23ef11b549 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c @@ -126,6 +126,43 @@ void n(void) return; } +/*@ requires X > -1000; + ensures X ≡ \old(Y); + + behavior neg: + assumes Y < 0; + requires Y < 1; + ensures X ≡ \old(Y); + + behavior pos: + assumes Y ≥ 0; + requires Y > -1; + ensures X ≡ \old(Y); + + behavior odd: + assumes Y % 2 ≡ 1; + requires Y % 2 - 1 ≡ 0; + ensures X ≡ \old(Y); + + behavior even: + assumes Y % 2 ≡ 0; + requires Y % 2 + 1 ≡ 1; + ensures X ≡ \old(Y); + + complete behaviors even, odd, pos, neg; + complete behaviors odd, even; + complete behaviors neg, pos; + disjoint behaviors odd, even; + disjoint behaviors neg, pos; + */ +void __gen_e_acsl_o(void); + +void o(void) +{ + X = Y; + return; +} + int main(void) { int __retres; @@ -138,10 +175,157 @@ int main(void) __gen_e_acsl_l(); __gen_e_acsl_m(); __gen_e_acsl_n(); + __gen_e_acsl_o(); __retres = 0; return __retres; } +/*@ requires X > -1000; + ensures X ≡ \old(Y); + + behavior neg: + assumes Y < 0; + requires Y < 1; + ensures X ≡ \old(Y); + + behavior pos: + assumes Y ≥ 0; + requires Y > -1; + ensures X ≡ \old(Y); + + behavior odd: + assumes Y % 2 ≡ 1; + requires Y % 2 - 1 ≡ 0; + ensures X ≡ \old(Y); + + behavior even: + assumes Y % 2 ≡ 0; + requires Y % 2 + 1 ≡ 1; + ensures X ≡ \old(Y); + + complete behaviors even, odd, pos, neg; + complete behaviors odd, even; + complete behaviors neg, pos; + disjoint behaviors odd, even; + disjoint behaviors neg, pos; + */ +void __gen_e_acsl_o(void) +{ + int __gen_e_acsl_at_5; + int __gen_e_acsl_at_4; + int __gen_e_acsl_at_3; + int __gen_e_acsl_at_2; + int __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; + { + int __gen_e_acsl_assumes_value; + int __gen_e_acsl_active_bhvrs; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)4); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + Y < 0); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + Y >= 0); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)2, + Y % 2 == 1); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)3, + Y % 2 == 0); + __e_acsl_assert(X > -1000,"Precondition","o","X > -1000", + "tests/constructs/function_contract.i",77); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(Y < 1,"Precondition","o", + "neg: Y < 1", + "tests/constructs/function_contract.i", + 82); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(Y > -1,"Precondition", + "o","pos: Y > -1", + "tests/constructs/function_contract.i", + 87); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)2); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(Y % 2 - 1 == 0, + "Precondition","o", + "odd: Y % 2 - 1 == 0", + "tests/constructs/function_contract.i", + 92); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)3); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(Y % 2 + 1 == 1, + "Precondition","o", + "even: Y % 2 + 1 == 1", + "tests/constructs/function_contract.i", + 97); + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)2,1,0); + if (__gen_e_acsl_active_bhvrs != 1) { + __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,"Precondition","o", + "complete behaviors pos, neg", + "tests/constructs/function_contract.i",107); + __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,"Precondition","o", + "disjoint behaviors pos, neg", + "tests/constructs/function_contract.i",107); + } + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)2,2,3); + if (__gen_e_acsl_active_bhvrs != 1) { + __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,"Precondition","o", + "complete behaviors odd, even", + "tests/constructs/function_contract.i",107); + __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,"Precondition","o", + "disjoint behaviors odd, even", + "tests/constructs/function_contract.i",107); + } + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract); + __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,"Precondition","o", + "all behaviors complete", + "tests/constructs/function_contract.i",107); + } + __gen_e_acsl_at_5 = Y; + __gen_e_acsl_at_4 = Y; + __gen_e_acsl_at_3 = Y; + __gen_e_acsl_at_2 = Y; + __gen_e_acsl_at = Y; + o(); + { + int __gen_e_acsl_assumes_value_2; + __e_acsl_assert(X == __gen_e_acsl_at,"Postcondition","o","X == \\old(Y)", + "tests/constructs/function_contract.i",78); + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert(X == __gen_e_acsl_at_2, + "Postcondition","o", + "neg: X == \\old(Y)", + "tests/constructs/function_contract.i", + 83); + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert(X == __gen_e_acsl_at_3, + "Postcondition","o", + "pos: X == \\old(Y)", + "tests/constructs/function_contract.i", + 88); + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)2); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert(X == __gen_e_acsl_at_4, + "Postcondition","o", + "odd: X == \\old(Y)", + "tests/constructs/function_contract.i", + 93); + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)3); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert(X == __gen_e_acsl_at_5, + "Postcondition","o", + "even: X == \\old(Y)", + "tests/constructs/function_contract.i", + 98); + __e_acsl_contract_clean(__gen_e_acsl_contract); + return; + } +} + /*@ requires X > 0; requires X < 10; @@ -155,28 +339,32 @@ int main(void) */ void __gen_e_acsl_n(void) { - int __gen_e_acsl_at_2; - int __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + X == 7); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + X == 5); __e_acsl_assert(X > 0,"Precondition","n","X > 0", "tests/constructs/function_contract.i",65); __e_acsl_assert(X < 10,"Precondition","n","X < 10", "tests/constructs/function_contract.i",66); - __gen_e_acsl_at_2 = X == 5; - __gen_e_acsl_at = X == 7; n(); { - int __gen_e_acsl_implies; - int __gen_e_acsl_implies_2; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = X == 8; - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","n", - "\\old(X == 7) ==> X == 8", - "tests/constructs/function_contract.i",69); - if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = X == 98; - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","n", - "\\old(X == 5) ==> X == 98", - "tests/constructs/function_contract.i",72); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(X == 8,"Postcondition", + "n","b1: X == 8", + "tests/constructs/function_contract.i", + 69); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(X == 98,"Postcondition", + "n","b2: X == 98", + "tests/constructs/function_contract.i", + 72); + __e_acsl_contract_clean(__gen_e_acsl_contract); return; } } @@ -193,42 +381,37 @@ void __gen_e_acsl_n(void) */ void __gen_e_acsl_m(void) { - long __gen_e_acsl_at_4; - int __gen_e_acsl_at_3; - int __gen_e_acsl_at_2; - int __gen_e_acsl_at; - __gen_e_acsl_at_4 = (long)X; - { - int __gen_e_acsl_and_2; - if (X == 5) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0; - __gen_e_acsl_at_3 = __gen_e_acsl_and_2; - } + long __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; { int __gen_e_acsl_and; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + X == 7); if (X == 5) __gen_e_acsl_and = Y == 2; else __gen_e_acsl_and = 0; - __gen_e_acsl_at_2 = __gen_e_acsl_and; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + __gen_e_acsl_and); } - __gen_e_acsl_at = X == 7; + __gen_e_acsl_at = (long)X; m(); { - int __gen_e_acsl_implies; - int __gen_e_acsl_implies_2; - int __gen_e_acsl_implies_3; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = X == 95; - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","m", - "\\old(X == 7) ==> X == 95", - "tests/constructs/function_contract.i",56); - if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = X == 7; - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","m", - "\\old(X == 5 && Y == 2) ==> X == 7", - "tests/constructs/function_contract.i",60); - if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_3 = 1; - else __gen_e_acsl_implies_3 = (long)X == __gen_e_acsl_at_4 + Y; - __e_acsl_assert(__gen_e_acsl_implies_3,"Postcondition","m", - "\\old(X == 5 && Y == 2) ==> X == \\old(X) + Y", - "tests/constructs/function_contract.i",61); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(X == 95,"Postcondition", + "m","b1: X == 95", + "tests/constructs/function_contract.i", + 56); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert((long)X == __gen_e_acsl_at + Y,"Postcondition","m", + "b2: X == \\old(X) + Y", + "tests/constructs/function_contract.i",61); + __e_acsl_assert(X == 7,"Postcondition","m","b2: X == 7", + "tests/constructs/function_contract.i",60); + } + __e_acsl_contract_clean(__gen_e_acsl_contract); return; } } @@ -255,31 +438,33 @@ int __gen_e_acsl_l(void) */ void __gen_e_acsl_k(void) { + __e_acsl_contract_t *__gen_e_acsl_contract; { - int __gen_e_acsl_implies; int __gen_e_acsl_and; - int __gen_e_acsl_implies_2; - int __gen_e_acsl_and_2; - int __gen_e_acsl_implies_3; - if (! (X == 1)) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = X == 0; - __e_acsl_assert(__gen_e_acsl_implies,"Precondition","k", - "X == 1 ==> X == 0", - "tests/constructs/function_contract.i",38); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + X == 1); if (X == 3) __gen_e_acsl_and = Y == 2; else __gen_e_acsl_and = 0; - if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = X == 3; - __e_acsl_assert(__gen_e_acsl_implies_2,"Precondition","k", - "X == 3 && Y == 2 ==> X == 3", - "tests/constructs/function_contract.i",42); - if (X == 3) __gen_e_acsl_and_2 = Y == 2; else __gen_e_acsl_and_2 = 0; - if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_3 = 1; - else __gen_e_acsl_implies_3 = X + (long)Y == 5L; - __e_acsl_assert(__gen_e_acsl_implies_3,"Precondition","k", - "X == 3 && Y == 2 ==> X + Y == 5", - "tests/constructs/function_contract.i",43); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + __gen_e_acsl_and); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(X == 0,"Precondition", + "k","b1: X == 0", + "tests/constructs/function_contract.i", + 38); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert(X + (long)Y == 5L,"Precondition","k","b2: X + Y == 5", + "tests/constructs/function_contract.i",43); + __e_acsl_assert(X == 3,"Precondition","k","b2: X == 3", + "tests/constructs/function_contract.i",42); + } } k(); + __e_acsl_contract_clean(__gen_e_acsl_contract); return; } @@ -294,18 +479,46 @@ void __gen_e_acsl_k(void) */ void __gen_e_acsl_j(void) { - __e_acsl_assert(X == 5,"Precondition","j","X == 5", - "tests/constructs/function_contract.i",27); - __e_acsl_assert((long)X == 3L + Y,"Precondition","j","X == 3 + Y", - "tests/constructs/function_contract.i",30); - __e_acsl_assert(Y == 2,"Precondition","j","Y == 2", - "tests/constructs/function_contract.i",31); + __e_acsl_contract_t *__gen_e_acsl_contract; + { + int __gen_e_acsl_assumes_value; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0,1); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1,1); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(X == 5,"Precondition", + "j","b1: X == 5", + "tests/constructs/function_contract.i", + 27); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert(Y == 2,"Precondition","j","b2: Y == 2", + "tests/constructs/function_contract.i",31); + __e_acsl_assert((long)X == 3L + Y,"Precondition","j","b2: X == 3 + Y", + "tests/constructs/function_contract.i",30); + } + } j(); - __e_acsl_assert(X == 3,"Postcondition","j","X == 3", - "tests/constructs/function_contract.i",28); - __e_acsl_assert((long)X == Y + 1L,"Postcondition","j","X == Y + 1", - "tests/constructs/function_contract.i",32); - return; + { + int __gen_e_acsl_assumes_value_2; + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert(X == 3,"Postcondition", + "j","b1: X == 3", + "tests/constructs/function_contract.i", + 28); + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert((long)X == Y + 1L, + "Postcondition","j", + "b2: X == Y + 1", + "tests/constructs/function_contract.i", + 32); + __e_acsl_contract_clean(__gen_e_acsl_contract); + return; + } } /*@ requires X ≡ 3; diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c index e088e9e145e72e17c2e2febe71f962453dfbf2e0..af5ff59ccca7697363bb104e4ea13add52b0d793 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c @@ -3,7 +3,11 @@ #include "stdio.h" int main(void) { + __e_acsl_contract_t *__gen_e_acsl_contract_3; + __e_acsl_contract_t *__gen_e_acsl_contract_2; + __e_acsl_contract_t *__gen_e_acsl_contract; int __retres; + int z; int x = 0; int y = 2; /*@ ensures x ≡ 1; */ @@ -35,49 +39,79 @@ int main(void) /*@ requires x ≡ 3; requires y ≡ 2; */ x += y; - __e_acsl_assert(x == 5,"Precondition","main","x == 5", - "tests/constructs/stmt_contract.i",25); - __e_acsl_assert((long)x == 3L + y,"Precondition","main","x == 3 + y", - "tests/constructs/stmt_contract.i",28); - __e_acsl_assert(y == 2,"Precondition","main","y == 2", - "tests/constructs/stmt_contract.i",29); - /*@ behavior b1: - requires x ≡ 5; - ensures x ≡ 3; - - behavior b2: - requires x ≡ 3 + y; - requires y ≡ 2; - ensures x ≡ y + 1; - */ - x = 3; - __e_acsl_assert(x == 3,"Postcondition","main","x == 3", - "tests/constructs/stmt_contract.i",26); - __e_acsl_assert((long)x == y + 1L,"Postcondition","main","x == y + 1", - "tests/constructs/stmt_contract.i",30); { - int __gen_e_acsl_implies; + int __gen_e_acsl_assumes_value_2; + { + int __gen_e_acsl_assumes_value; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + 1); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + 1); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(x == 5,"Precondition", + "main","b1: x == 5", + "tests/constructs/stmt_contract.i", + 25); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { + __e_acsl_assert(y == 2,"Precondition","main","b2: y == 2", + "tests/constructs/stmt_contract.i",29); + __e_acsl_assert((long)x == 3L + y,"Precondition","main", + "b2: x == 3 + y","tests/constructs/stmt_contract.i", + 28); + } + } + /*@ behavior b1: + requires x ≡ 5; + ensures x ≡ 3; + + behavior b2: + requires x ≡ 3 + y; + requires y ≡ 2; + ensures x ≡ y + 1; + */ + x = 3; + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert(x == 3,"Postcondition", + "main","b1: x == 3", + "tests/constructs/stmt_contract.i", + 26); + __gen_e_acsl_assumes_value_2 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value_2) __e_acsl_assert((long)x == y + 1L, + "Postcondition","main", + "b2: x == y + 1", + "tests/constructs/stmt_contract.i", + 30); + __e_acsl_contract_clean(__gen_e_acsl_contract); + } + { int __gen_e_acsl_and_2; - int __gen_e_acsl_implies_2; - int __gen_e_acsl_and_3; - int __gen_e_acsl_implies_3; - if (! (x == 1)) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = x == 0; - __e_acsl_assert(__gen_e_acsl_implies,"Precondition","main", - "x == 1 ==> x == 0","tests/constructs/stmt_contract.i", - 35); + int __gen_e_acsl_assumes_value_3; + __gen_e_acsl_contract_2 = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract_2,(size_t)0, + x == 1); if (x == 3) __gen_e_acsl_and_2 = y == 2; else __gen_e_acsl_and_2 = 0; - if (! __gen_e_acsl_and_2) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = x == 3; - __e_acsl_assert(__gen_e_acsl_implies_2,"Precondition","main", - "x == 3 && y == 2 ==> x == 3", - "tests/constructs/stmt_contract.i",39); - if (x == 3) __gen_e_acsl_and_3 = y == 2; else __gen_e_acsl_and_3 = 0; - if (! __gen_e_acsl_and_3) __gen_e_acsl_implies_3 = 1; - else __gen_e_acsl_implies_3 = x + (long)y == 5L; - __e_acsl_assert(__gen_e_acsl_implies_3,"Precondition","main", - "x == 3 && y == 2 ==> x + y == 5", - "tests/constructs/stmt_contract.i",40); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract_2,(size_t)1, + __gen_e_acsl_and_2); + __gen_e_acsl_assumes_value_3 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract_2,(size_t)0); + if (__gen_e_acsl_assumes_value_3) __e_acsl_assert(x == 0,"Precondition", + "main","b1: x == 0", + "tests/constructs/stmt_contract.i", + 35); + __gen_e_acsl_assumes_value_3 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract_2,(size_t)1); + if (__gen_e_acsl_assumes_value_3) { + __e_acsl_assert(x + (long)y == 5L,"Precondition","main", + "b2: x + y == 5","tests/constructs/stmt_contract.i",40); + __e_acsl_assert(x == 3,"Precondition","main","b2: x == 3", + "tests/constructs/stmt_contract.i",39); + } } /*@ behavior b1: assumes x ≡ 1; @@ -90,6 +124,7 @@ int main(void) requires x + y ≡ 5; */ x += y; + __e_acsl_contract_clean(__gen_e_acsl_contract_2); __e_acsl_assert(x == 5,"Precondition","main","x == 5", "tests/constructs/stmt_contract.i",43); /*@ requires x ≡ 5; */ @@ -99,8 +134,63 @@ int main(void) /*@ requires y ≡ 2; */ x += y; } + { + int __gen_e_acsl_assumes_value_4; + { + int __gen_e_acsl_active_bhvrs; + __gen_e_acsl_contract_3 = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract_3, + (size_t)0,x >= 0); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract_3, + (size_t)1,x < 0); + __e_acsl_assert(x > -1000,"Precondition","main","x > -1000", + "tests/constructs/stmt_contract.i",49); + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract_3); + if (__gen_e_acsl_active_bhvrs != 1) { + __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,"Precondition","main", + "all behaviors complete", + "tests/constructs/stmt_contract.i",64); + __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,"Precondition","main", + "all behaviors disjoint", + "tests/constructs/stmt_contract.i",64); + } + } + /*@ requires x > -1000; + ensures z ≥ 0; + assigns x; + + behavior pos: + assumes x ≥ 0; + ensures z ≡ x; + + behavior neg: + assumes x < 0; + ensures z ≡ -x; + + complete behaviors neg, pos; + disjoint behaviors neg, pos; + */ + if (x < 0) z = - x; else z = x; + __e_acsl_assert(z >= 0,"Postcondition","main","z >= 0", + "tests/constructs/stmt_contract.i",51); + __gen_e_acsl_assumes_value_4 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract_3,(size_t)0); + if (__gen_e_acsl_assumes_value_4) __e_acsl_assert(z == x,"Postcondition", + "main","pos: z == x", + "tests/constructs/stmt_contract.i", + 55); + __gen_e_acsl_assumes_value_4 = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract_3,(size_t)1); + if (__gen_e_acsl_assumes_value_4) __e_acsl_assert((long)z == - ((long)x), + "Postcondition","main", + "neg: z == -x", + "tests/constructs/stmt_contract.i", + 59); + __e_acsl_contract_clean(__gen_e_acsl_contract_3); + } __e_acsl_assert(x == 7,"Precondition","main","x == 7", - "tests/constructs/stmt_contract.i",47); + "tests/constructs/stmt_contract.i",70); /*@ requires x ≡ 7; ensures x ≡ 7; */ { @@ -108,7 +198,7 @@ int main(void) goto return_label; } __e_acsl_assert(x == 7,"Postcondition","main","x == 7", - "tests/constructs/stmt_contract.i",48); + "tests/constructs/stmt_contract.i",71); return_label: return __retres; } diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle index efd026311297e55d8fefb674326118e6ece88624..b1c4f6eb72229f64ba5bf67742a6f9968e207c4c 100644 --- a/src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle @@ -1,2 +1,5 @@ [e-acsl] beginning translation. +[e-acsl] tests/constructs/stmt_contract.i:64: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c index 7e89333ec36d22ebdedfa96617458c5ea8bc0cd1..421fdfe0f58470d21711a0f432e2e77add1b2f4e 100644 --- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c +++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c @@ -133,44 +133,37 @@ int main(void) */ int __gen_e_acsl_search(int elt) { - int __gen_e_acsl_at_2; - int __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; int __retres; { + int __gen_e_acsl_exists; + int __gen_e_acsl_j; int __gen_e_acsl_forall; + int __gen_e_acsl_j_2; + int __gen_e_acsl_forall_2; int __gen_e_acsl_i; - __gen_e_acsl_forall = 1; - __gen_e_acsl_i = 0; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __gen_e_acsl_exists = 0; + __gen_e_acsl_j = 0; while (1) { - if (__gen_e_acsl_i < 9) ; else break; - __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,"RTE","search", - "index_bound: (int)(__gen_e_acsl_i + 1) < 10", - "tests/examples/linear_search.i",7); - __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),"RTE","search", - "index_bound: 0 <= (int)(__gen_e_acsl_i + 1)", - "tests/examples/linear_search.i",7); - __e_acsl_assert(__gen_e_acsl_i < 10,"RTE","search", - "index_bound: __gen_e_acsl_i < 10", - "tests/examples/linear_search.i",7); - __e_acsl_assert(0 <= __gen_e_acsl_i,"RTE","search", - "index_bound: 0 <= __gen_e_acsl_i", - "tests/examples/linear_search.i",7); - if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ; + if (__gen_e_acsl_j < 10) ; else break; + __e_acsl_assert(__gen_e_acsl_j < 10,"RTE","search", + "index_bound: __gen_e_acsl_j < 10", + "tests/examples/linear_search.i",9); + __e_acsl_assert(0 <= __gen_e_acsl_j,"RTE","search", + "index_bound: 0 <= __gen_e_acsl_j", + "tests/examples/linear_search.i",9); + if (! (A[__gen_e_acsl_j] == elt)) ; else { - __gen_e_acsl_forall = 0; + __gen_e_acsl_exists = 1; goto e_acsl_end_loop3; } - __gen_e_acsl_i ++; + __gen_e_acsl_j ++; } e_acsl_end_loop3: ; - __e_acsl_assert(__gen_e_acsl_forall,"Precondition","search", - "\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]", - "tests/examples/linear_search.i",7); - } - { - int __gen_e_acsl_forall_2; - int __gen_e_acsl_j_2; - __gen_e_acsl_forall_2 = 1; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + __gen_e_acsl_exists); + __gen_e_acsl_forall = 1; __gen_e_acsl_j_2 = 0; while (1) { if (__gen_e_acsl_j_2 < 10) ; else break; @@ -182,51 +175,60 @@ int __gen_e_acsl_search(int elt) "tests/examples/linear_search.i",12); if (A[__gen_e_acsl_j_2] != elt) ; else { - __gen_e_acsl_forall_2 = 0; - goto e_acsl_end_loop5; + __gen_e_acsl_forall = 0; + goto e_acsl_end_loop4; } __gen_e_acsl_j_2 ++; } - e_acsl_end_loop5: ; - __gen_e_acsl_at_2 = __gen_e_acsl_forall_2; - } - { - int __gen_e_acsl_exists; - int __gen_e_acsl_j; - __gen_e_acsl_exists = 0; - __gen_e_acsl_j = 0; + e_acsl_end_loop4: ; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + __gen_e_acsl_forall); + __gen_e_acsl_forall_2 = 1; + __gen_e_acsl_i = 0; while (1) { - if (__gen_e_acsl_j < 10) ; else break; - __e_acsl_assert(__gen_e_acsl_j < 10,"RTE","search", - "index_bound: __gen_e_acsl_j < 10", - "tests/examples/linear_search.i",9); - __e_acsl_assert(0 <= __gen_e_acsl_j,"RTE","search", - "index_bound: 0 <= __gen_e_acsl_j", - "tests/examples/linear_search.i",9); - if (! (A[__gen_e_acsl_j] == elt)) ; + if (__gen_e_acsl_i < 9) ; else break; + __e_acsl_assert((int)(__gen_e_acsl_i + 1L) < 10,"RTE","search", + "index_bound: (int)(__gen_e_acsl_i + 1) < 10", + "tests/examples/linear_search.i",7); + __e_acsl_assert(0 <= (int)(__gen_e_acsl_i + 1L),"RTE","search", + "index_bound: 0 <= (int)(__gen_e_acsl_i + 1)", + "tests/examples/linear_search.i",7); + __e_acsl_assert(__gen_e_acsl_i < 10,"RTE","search", + "index_bound: __gen_e_acsl_i < 10", + "tests/examples/linear_search.i",7); + __e_acsl_assert(0 <= __gen_e_acsl_i,"RTE","search", + "index_bound: 0 <= __gen_e_acsl_i", + "tests/examples/linear_search.i",7); + if (A[__gen_e_acsl_i] <= A[__gen_e_acsl_i + 1]) ; else { - __gen_e_acsl_exists = 1; - goto e_acsl_end_loop4; + __gen_e_acsl_forall_2 = 0; + goto e_acsl_end_loop5; } - __gen_e_acsl_j ++; + __gen_e_acsl_i ++; } - e_acsl_end_loop4: ; - __gen_e_acsl_at = __gen_e_acsl_exists; + e_acsl_end_loop5: ; + __e_acsl_assert(__gen_e_acsl_forall_2,"Precondition","search", + "\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i + 1]", + "tests/examples/linear_search.i",7); } __retres = search(elt); { - int __gen_e_acsl_implies; - int __gen_e_acsl_implies_2; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = __retres == 1; - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","search", - "\\old(\\exists integer j; 0 <= j < 10 && A[j] == elt) ==> \\result == 1", - "tests/examples/linear_search.i",10); - if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = __retres == 0; - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","search", - "\\old(\\forall integer j; 0 <= j < 10 ==> A[j] != elt) ==> \\result == 0", - "tests/examples/linear_search.i",13); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == 1, + "Postcondition","search", + "exists: \\result == 1", + "tests/examples/linear_search.i", + 10); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == 0, + "Postcondition","search", + "not_exists: \\result == 0", + "tests/examples/linear_search.i", + 13); + __e_acsl_contract_clean(__gen_e_acsl_contract); return __retres; } } diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle index 99a62eef221249385b08dee71e0d519b78fc0716..7440543ece019a5c93a6944f9668cd7afbe7aa64 100644 --- a/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle +++ b/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle @@ -2,23 +2,3 @@ [e-acsl] translation done in project "e-acsl". [eva:alarm] tests/examples/linear_search.i:30: Warning: function __gen_e_acsl_search: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:7: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:18: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:18: Warning: - loop invariant got status unknown. -[eva:alarm] tests/examples/linear_search.i:10: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:13: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:10: Warning: - function __gen_e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] tests/examples/linear_search.i:13: Warning: - function __gen_e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] tests/examples/linear_search.i:31: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:33: Warning: - function __gen_e_acsl_search: precondition got status unknown. -[eva:alarm] tests/examples/linear_search.i:34: Warning: - function __e_acsl_assert: precondition got status unknown. diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle index ff43a1afe080ae9d69fc234a872bed6bf18923b8..161e12fd16ae235aa8141ba0bb62f4d4a33703e0 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle @@ -14,29 +14,29 @@ [e-acsl] Warning: annotating undefined function `fork': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] tests/format/fprintf.c:10: Warning: +[e-acsl] FRAMAC_SHARE/libc/unistd.h:854: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning: +[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: 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/stdio.h:120: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdio.h:118: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdio.h:122: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdio.h:94: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning: E-ACSL construct `predicate with no definition nor reads clause' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:472: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. @@ -47,70 +47,3 @@ function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown. [kernel:annot:missing-spec] tests/format/fprintf.c:15: Warning: Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype -[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/format/fprintf.c:15: Warning: - accessing uninitialized left-value. assert \initialized(&process_status); -[eva:invalid-assigns] tests/format/fprintf.c:16: - Completely invalid destination for assigns clause *stream. Ignoring. -[eva:alarm] tests/format/fprintf.c:16: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_0); -[eva:alarm] tests/format/fprintf.c:19: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_1); -[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] tests/format/fprintf.c:21: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_2); -[eva:invalid-assigns] tests/format/fprintf.c:22: - Completely invalid destination for assigns clause *stream. Ignoring. -[eva:alarm] tests/format/fprintf.c:22: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_3); -[kernel:annot:missing-spec] tests/format/fprintf.c:27: Warning: - Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype -[eva:alarm] tests/format/fprintf.c:27: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_4); -[eva:alarm] tests/format/fprintf.c:28: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_5); -[kernel:annot:missing-spec] tests/format/fprintf.c:34: Warning: - Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype -[eva:alarm] tests/format/fprintf.c:34: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_6); -[eva:alarm] tests/format/fprintf.c:35: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_7); -[eva:alarm] tests/format/fprintf.c:36: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_8); -[eva:invalid-assigns] tests/format/fprintf.c:37: - Completely invalid destination for assigns clause *(buffer + (0 ..)). - Ignoring. -[eva:alarm] tests/format/fprintf.c:37: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_9); -[eva:invalid-assigns] tests/format/fprintf.c:38: - Completely invalid destination for assigns clause *(buffer + (0 ..)). - Ignoring. -[eva:alarm] tests/format/fprintf.c:38: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_10); -[kernel:annot:missing-spec] tests/format/fprintf.c:41: Warning: - Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype -[eva:alarm] tests/format/fprintf.c:41: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_11); -[eva:alarm] tests/format/fprintf.c:42: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_12); -[eva:invalid-assigns] tests/format/fprintf.c:43: - Completely invalid destination for assigns clause *(buffer + (0 ..)). - Ignoring. -[eva:alarm] tests/format/fprintf.c:43: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_13); -[eva:alarm] tests/format/fprintf.c:44: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_14); -[eva:invalid-assigns] tests/format/fprintf.c:45: - Completely invalid destination for assigns clause *(buffer + (0 ..)). - Ignoring. -[eva:alarm] tests/format/fprintf.c:45: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_15); -[eva:invalid-assigns] tests/format/fprintf.c:46: - Completely invalid destination for assigns clause *(buffer + (0 ..)). - Ignoring. -[eva:alarm] tests/format/fprintf.c:46: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_16); diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c index 4a64f9d92fb70c755451b60949dcaafcf82036f6..4df6d3c070c6019f667faceb9916a9efb8740000 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c +++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c @@ -137,21 +137,27 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options) { int *__gen_e_acsl_at_2; int *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; pid_t __retres; { - int __gen_e_acsl_implies; + int __gen_e_acsl_assumes_value; __e_acsl_store_block((void *)(& stat_loc),(size_t)8); - if (! (stat_loc != (int *)0)) __gen_e_acsl_implies = 1; - else { + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + stat_loc == (int *)0); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + stat_loc != (int *)0); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { int __gen_e_acsl_valid; __gen_e_acsl_valid = __e_acsl_valid((void *)stat_loc,sizeof(int), (void *)stat_loc, (void *)(& stat_loc)); - __gen_e_acsl_implies = __gen_e_acsl_valid; + __e_acsl_assert(__gen_e_acsl_valid,"Precondition","waitpid", + "stat_loc_non_null: \\valid(stat_loc)", + "FRAMAC_SHARE/libc/sys/wait.h",92); } - __e_acsl_assert(__gen_e_acsl_implies,"Precondition","waitpid", - "stat_loc != \\null ==> \\valid(stat_loc)", - "FRAMAC_SHARE/libc/sys/wait.h",92); } __gen_e_acsl_at_2 = stat_loc; __gen_e_acsl_at = stat_loc; @@ -159,7 +165,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options) { int __gen_e_acsl_or; int __gen_e_acsl_and; - int __gen_e_acsl_implies_2; + int __gen_e_acsl_implies; if (__retres == -1) __gen_e_acsl_or = 1; else __gen_e_acsl_or = __retres >= 0; __e_acsl_assert(__gen_e_acsl_or,"Postcondition","waitpid", @@ -167,16 +173,17 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options) "FRAMAC_SHARE/libc/sys/wait.h",84); if (__retres >= 0) __gen_e_acsl_and = __gen_e_acsl_at != (int *)0; else __gen_e_acsl_and = 0; - if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1; + if (! __gen_e_acsl_and) __gen_e_acsl_implies = 1; else { int __gen_e_acsl_initialized; __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2, sizeof(int)); - __gen_e_acsl_implies_2 = __gen_e_acsl_initialized; + __gen_e_acsl_implies = __gen_e_acsl_initialized; } - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","waitpid", + __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","waitpid", "\\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))", "FRAMAC_SHARE/libc/sys/wait.h",86); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& stat_loc)); return __retres; } @@ -419,7 +426,6 @@ int main(int argc, char const **argv) int process_status; __e_acsl_store_block((void *)(& process_status),(size_t)4); __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)); } @@ -434,7 +440,6 @@ int main(int argc, char const **argv) int process_status_0; __e_acsl_store_block((void *)(& process_status_0),(size_t)4); __gen_e_acsl_waitpid(pid_0,& process_status_0,0); - /*@ assert Eva: initialization: \initialized(&process_status_0); */ signal_eval(process_status_0,1,__gen_e_acsl_literal_string_9); __e_acsl_delete_block((void *)(& process_status_0)); } @@ -454,7 +459,6 @@ int main(int argc, char const **argv) int process_status_1; __e_acsl_store_block((void *)(& process_status_1),(size_t)4); __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_12); __e_acsl_delete_block((void *)(& process_status_1)); } @@ -471,7 +475,6 @@ int main(int argc, char const **argv) int process_status_2; __e_acsl_store_block((void *)(& process_status_2),(size_t)4); __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_13); __e_acsl_delete_block((void *)(& process_status_2)); } @@ -488,7 +491,6 @@ int main(int argc, char const **argv) int process_status_3; __e_acsl_store_block((void *)(& process_status_3),(size_t)4); __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_14); __e_acsl_delete_block((void *)(& process_status_3)); } @@ -504,7 +506,6 @@ int main(int argc, char const **argv) int process_status_4; __e_acsl_store_block((void *)(& process_status_4),(size_t)4); __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_15); __e_acsl_delete_block((void *)(& process_status_4)); } @@ -519,7 +520,6 @@ int main(int argc, char const **argv) int process_status_5; __e_acsl_store_block((void *)(& process_status_5),(size_t)4); __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_16); __e_acsl_delete_block((void *)(& process_status_5)); } @@ -535,7 +535,6 @@ int main(int argc, char const **argv) int process_status_6; __e_acsl_store_block((void *)(& process_status_6),(size_t)4); __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_19); __e_acsl_delete_block((void *)(& process_status_6)); } @@ -551,7 +550,6 @@ int main(int argc, char const **argv) int process_status_7; __e_acsl_store_block((void *)(& process_status_7),(size_t)4); __gen_e_acsl_waitpid(pid_7,& process_status_7,0); - /*@ assert Eva: initialization: \initialized(&process_status_7); */ signal_eval(process_status_7,0,__gen_e_acsl_literal_string_21); __e_acsl_delete_block((void *)(& process_status_7)); } @@ -567,7 +565,6 @@ int main(int argc, char const **argv) int process_status_8; __e_acsl_store_block((void *)(& process_status_8),(size_t)4); __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_23); __e_acsl_delete_block((void *)(& process_status_8)); } @@ -583,7 +580,6 @@ int main(int argc, char const **argv) int process_status_9; __e_acsl_store_block((void *)(& process_status_9),(size_t)4); __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_24); __e_acsl_delete_block((void *)(& process_status_9)); } @@ -599,7 +595,6 @@ int main(int argc, char const **argv) int process_status_10; __e_acsl_store_block((void *)(& process_status_10),(size_t)4); __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_25); __e_acsl_delete_block((void *)(& process_status_10)); } @@ -616,7 +611,6 @@ int main(int argc, char const **argv) int process_status_11; __e_acsl_store_block((void *)(& process_status_11),(size_t)4); __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_26); __e_acsl_delete_block((void *)(& process_status_11)); } @@ -633,7 +627,6 @@ int main(int argc, char const **argv) int process_status_12; __e_acsl_store_block((void *)(& process_status_12),(size_t)4); __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_27); __e_acsl_delete_block((void *)(& process_status_12)); } @@ -650,7 +643,6 @@ int main(int argc, char const **argv) int process_status_13; __e_acsl_store_block((void *)(& process_status_13),(size_t)4); __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_28); __e_acsl_delete_block((void *)(& process_status_13)); } @@ -667,7 +659,6 @@ int main(int argc, char const **argv) int process_status_14; __e_acsl_store_block((void *)(& process_status_14),(size_t)4); __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_29); __e_acsl_delete_block((void *)(& process_status_14)); } @@ -684,7 +675,6 @@ int main(int argc, char const **argv) int process_status_15; __e_acsl_store_block((void *)(& process_status_15),(size_t)4); __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_30); __e_acsl_delete_block((void *)(& process_status_15)); } @@ -701,7 +691,6 @@ int main(int argc, char const **argv) int process_status_16; __e_acsl_store_block((void *)(& process_status_16),(size_t)4); __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_31); __e_acsl_delete_block((void *)(& process_status_16)); } diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c index 74db87f2f2cf38f6ea5fde6db54d0c38cdf73c16..86a8665ee99080f618094bcf2f7a7024b80ca31f 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c +++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c @@ -552,9 +552,6 @@ void test_specifier_application(char const *allowed, char const *fmt, int process_status; __e_acsl_store_block((void *)(& process_status),(size_t)4); __gen_e_acsl_waitpid(pid,& process_status,0); - /*@ assert - Eva: initialization: \initialized(&process_status); - */ signal_eval(process_status,0,(char const *)at); __e_acsl_delete_block((void *)(& process_status)); } @@ -572,9 +569,6 @@ void test_specifier_application(char const *allowed, char const *fmt, int process_status_0; __e_acsl_store_block((void *)(& process_status_0),(size_t)4); __gen_e_acsl_waitpid(pid_0,& process_status_0,0); - /*@ assert - Eva: initialization: \initialized(&process_status_0); - */ signal_eval(process_status_0,1,(char const *)at); __e_acsl_delete_block((void *)(& process_status_0)); } @@ -614,21 +608,27 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options) { int *__gen_e_acsl_at_2; int *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; pid_t __retres; { - int __gen_e_acsl_implies; + int __gen_e_acsl_assumes_value; __e_acsl_store_block((void *)(& stat_loc),(size_t)8); - if (! (stat_loc != (int *)0)) __gen_e_acsl_implies = 1; - else { + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + stat_loc == (int *)0); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + stat_loc != (int *)0); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { int __gen_e_acsl_valid; __gen_e_acsl_valid = __e_acsl_valid((void *)stat_loc,sizeof(int), (void *)stat_loc, (void *)(& stat_loc)); - __gen_e_acsl_implies = __gen_e_acsl_valid; + __e_acsl_assert(__gen_e_acsl_valid,"Precondition","waitpid", + "stat_loc_non_null: \\valid(stat_loc)", + "FRAMAC_SHARE/libc/sys/wait.h",92); } - __e_acsl_assert(__gen_e_acsl_implies,"Precondition","waitpid", - "stat_loc != \\null ==> \\valid(stat_loc)", - "FRAMAC_SHARE/libc/sys/wait.h",92); } __gen_e_acsl_at_2 = stat_loc; __gen_e_acsl_at = stat_loc; @@ -636,7 +636,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options) { int __gen_e_acsl_or; int __gen_e_acsl_and; - int __gen_e_acsl_implies_2; + int __gen_e_acsl_implies; if (__retres == -1) __gen_e_acsl_or = 1; else __gen_e_acsl_or = __retres >= 0; __e_acsl_assert(__gen_e_acsl_or,"Postcondition","waitpid", @@ -644,16 +644,17 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options) "FRAMAC_SHARE/libc/sys/wait.h",84); if (__retres >= 0) __gen_e_acsl_and = __gen_e_acsl_at != (int *)0; else __gen_e_acsl_and = 0; - if (! __gen_e_acsl_and) __gen_e_acsl_implies_2 = 1; + if (! __gen_e_acsl_and) __gen_e_acsl_implies = 1; else { int __gen_e_acsl_initialized; __gen_e_acsl_initialized = __e_acsl_initialized((void *)__gen_e_acsl_at_2, sizeof(int)); - __gen_e_acsl_implies_2 = __gen_e_acsl_initialized; + __gen_e_acsl_implies = __gen_e_acsl_initialized; } - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","waitpid", + __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","waitpid", "\\result >= 0 && \\old(stat_loc) != \\null ==> \\initialized(\\old(stat_loc))", "FRAMAC_SHARE/libc/sys/wait.h",86); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& stat_loc)); return __retres; } @@ -735,25 +736,77 @@ char *__gen_e_acsl_strcpy(char * __restrict dest, char const * __restrict src) */ char *__gen_e_acsl_strchr(char const *s, int c) { - char const *__gen_e_acsl_at; + char const *__gen_e_acsl_at_3; + char const *__gen_e_acsl_at_2; + int __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; char *__retres; __e_acsl_store_block((void *)(& __retres),(size_t)8); __e_acsl_store_block((void *)(& s),(size_t)8); - __gen_e_acsl_at = s; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)3); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)2,1); + __gen_e_acsl_at_3 = s; + __gen_e_acsl_at_2 = s; + __gen_e_acsl_at = c; __retres = strchr(s,c); { - int __gen_e_acsl_or; - if (__retres == (char *)0) __gen_e_acsl_or = 1; - else { + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_initialized; + int __gen_e_acsl_and; void *__gen_e_acsl_base_addr; void *__gen_e_acsl_base_addr_2; + __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& __retres), + sizeof(char *)); + if (__gen_e_acsl_initialized) { + int __gen_e_acsl_valid_read; + __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__retres, + sizeof(char), + (void *)__retres, + (void *)(& __retres)); + __gen_e_acsl_and = __gen_e_acsl_valid_read; + } + else __gen_e_acsl_and = 0; + __e_acsl_assert(__gen_e_acsl_and,"RTE","strchr", + "mem_access: \\valid_read(__retres)", + "FRAMAC_SHARE/libc/string.h",161); __gen_e_acsl_base_addr = __e_acsl_base_addr((void *)__retres); - __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at); - __gen_e_acsl_or = __gen_e_acsl_base_addr == __gen_e_acsl_base_addr_2; + __gen_e_acsl_base_addr_2 = __e_acsl_base_addr((void *)__gen_e_acsl_at_2); + __e_acsl_assert(__gen_e_acsl_base_addr == __gen_e_acsl_base_addr_2, + "Postcondition","strchr", + "found: \\base_addr(\\result) == \\base_addr(\\old(s))", + "FRAMAC_SHARE/libc/string.h",162); + __e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at), + "Postcondition","strchr", + "found: *\\result == (char)\\old(c)", + "FRAMAC_SHARE/libc/string.h",161); + } + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == (char *)0, + "Postcondition","strchr", + "not_found: \\result == \\null", + "FRAMAC_SHARE/libc/string.h", + 168); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)2); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_or; + if (__retres == (char *)0) __gen_e_acsl_or = 1; + else { + void *__gen_e_acsl_base_addr_3; + void *__gen_e_acsl_base_addr_4; + __gen_e_acsl_base_addr_3 = __e_acsl_base_addr((void *)__retres); + __gen_e_acsl_base_addr_4 = __e_acsl_base_addr((void *)__gen_e_acsl_at_3); + __gen_e_acsl_or = __gen_e_acsl_base_addr_3 == __gen_e_acsl_base_addr_4; + } + __e_acsl_assert(__gen_e_acsl_or,"Postcondition","strchr", + "default: \\result == \\null || \\base_addr(\\result) == \\base_addr(\\old(s))", + "FRAMAC_SHARE/libc/string.h",171); } - __e_acsl_assert(__gen_e_acsl_or,"Postcondition","strchr", - "\\result == \\null || \\base_addr(\\result) == \\base_addr(\\old(s))", - "FRAMAC_SHARE/libc/string.h",171); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& s)); __e_acsl_delete_block((void *)(& __retres)); return __retres; @@ -2545,7 +2598,6 @@ int main(int argc, char const **argv) int process_status; __e_acsl_store_block((void *)(& process_status),(size_t)4); __gen_e_acsl_waitpid(pid,& process_status,0); - /*@ assert Eva: initialization: \initialized(&process_status); */ signal_eval(process_status,0,__gen_e_acsl_literal_string_12); __e_acsl_delete_block((void *)(& process_status)); } @@ -2561,7 +2613,6 @@ int main(int argc, char const **argv) int process_status_0; __e_acsl_store_block((void *)(& process_status_0),(size_t)4); __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_14); __e_acsl_delete_block((void *)(& process_status_0)); } @@ -2577,7 +2628,6 @@ int main(int argc, char const **argv) int process_status_1; __e_acsl_store_block((void *)(& process_status_1),(size_t)4); __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_16); __e_acsl_delete_block((void *)(& process_status_1)); } @@ -2593,7 +2643,6 @@ int main(int argc, char const **argv) int process_status_2; __e_acsl_store_block((void *)(& process_status_2),(size_t)4); __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_18); __e_acsl_delete_block((void *)(& process_status_2)); } @@ -2617,7 +2666,6 @@ int main(int argc, char const **argv) int process_status_3; __e_acsl_store_block((void *)(& process_status_3),(size_t)4); __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_19); __e_acsl_delete_block((void *)(& process_status_3)); } @@ -2632,7 +2680,6 @@ int main(int argc, char const **argv) int process_status_4; __e_acsl_store_block((void *)(& process_status_4),(size_t)4); __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_21); __e_acsl_delete_block((void *)(& process_status_4)); } @@ -2647,7 +2694,6 @@ int main(int argc, char const **argv) int process_status_5; __e_acsl_store_block((void *)(& process_status_5),(size_t)4); __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_23); __e_acsl_delete_block((void *)(& process_status_5)); } @@ -2662,7 +2708,6 @@ int main(int argc, char const **argv) int process_status_6; __e_acsl_store_block((void *)(& process_status_6),(size_t)4); __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_25); __e_acsl_delete_block((void *)(& process_status_6)); } @@ -2677,7 +2722,6 @@ int main(int argc, char const **argv) int process_status_7; __e_acsl_store_block((void *)(& process_status_7),(size_t)4); __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_27); __e_acsl_delete_block((void *)(& process_status_7)); } @@ -2692,7 +2736,6 @@ int main(int argc, char const **argv) int process_status_8; __e_acsl_store_block((void *)(& process_status_8),(size_t)4); __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_29); __e_acsl_delete_block((void *)(& process_status_8)); } @@ -2716,7 +2759,6 @@ int main(int argc, char const **argv) int process_status_9; __e_acsl_store_block((void *)(& process_status_9),(size_t)4); __gen_e_acsl_waitpid(pid_9,& process_status_9,0); - /*@ assert Eva: initialization: \initialized(&process_status_9); */ signal_eval(process_status_9,0,__gen_e_acsl_literal_string_40); __e_acsl_delete_block((void *)(& process_status_9)); } @@ -2731,7 +2773,6 @@ int main(int argc, char const **argv) int process_status_10; __e_acsl_store_block((void *)(& process_status_10),(size_t)4); __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_42); __e_acsl_delete_block((void *)(& process_status_10)); } @@ -2746,7 +2787,6 @@ int main(int argc, char const **argv) int process_status_11; __e_acsl_store_block((void *)(& process_status_11),(size_t)4); __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_44); __e_acsl_delete_block((void *)(& process_status_11)); } @@ -2764,7 +2804,6 @@ int main(int argc, char const **argv) int process_status_12; __e_acsl_store_block((void *)(& process_status_12),(size_t)4); __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_49); __e_acsl_delete_block((void *)(& process_status_12)); } @@ -2779,7 +2818,6 @@ int main(int argc, char const **argv) int process_status_13; __e_acsl_store_block((void *)(& process_status_13),(size_t)4); __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_49); __e_acsl_delete_block((void *)(& process_status_13)); } @@ -2794,7 +2832,6 @@ int main(int argc, char const **argv) int process_status_14; __e_acsl_store_block((void *)(& process_status_14),(size_t)4); __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_52); __e_acsl_delete_block((void *)(& process_status_14)); } @@ -2809,7 +2846,6 @@ int main(int argc, char const **argv) int process_status_15; __e_acsl_store_block((void *)(& process_status_15),(size_t)4); __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_52); __e_acsl_delete_block((void *)(& process_status_15)); } @@ -2824,7 +2860,6 @@ int main(int argc, char const **argv) int process_status_16; __e_acsl_store_block((void *)(& process_status_16),(size_t)4); __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_55); __e_acsl_delete_block((void *)(& process_status_16)); } @@ -2839,7 +2874,6 @@ int main(int argc, char const **argv) int process_status_17; __e_acsl_store_block((void *)(& process_status_17),(size_t)4); __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_55); __e_acsl_delete_block((void *)(& process_status_17)); } @@ -2854,7 +2888,6 @@ int main(int argc, char const **argv) int process_status_18; __e_acsl_store_block((void *)(& process_status_18),(size_t)4); __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_55); __e_acsl_delete_block((void *)(& process_status_18)); } @@ -2872,7 +2905,6 @@ int main(int argc, char const **argv) int process_status_19; __e_acsl_store_block((void *)(& process_status_19),(size_t)4); __gen_e_acsl_waitpid(pid_19,& process_status_19,0); - /*@ assert Eva: initialization: \initialized(&process_status_19); */ signal_eval(process_status_19,0,__gen_e_acsl_literal_string_60); __e_acsl_delete_block((void *)(& process_status_19)); } @@ -2887,7 +2919,6 @@ int main(int argc, char const **argv) int process_status_20; __e_acsl_store_block((void *)(& process_status_20),(size_t)4); __gen_e_acsl_waitpid(pid_20,& process_status_20,0); - /*@ assert Eva: initialization: \initialized(&process_status_20); */ signal_eval(process_status_20,0,__gen_e_acsl_literal_string_60); __e_acsl_delete_block((void *)(& process_status_20)); } @@ -2902,7 +2933,6 @@ int main(int argc, char const **argv) int process_status_21; __e_acsl_store_block((void *)(& process_status_21),(size_t)4); __gen_e_acsl_waitpid(pid_21,& process_status_21,0); - /*@ assert Eva: initialization: \initialized(&process_status_21); */ signal_eval(process_status_21,0,__gen_e_acsl_literal_string_63); __e_acsl_delete_block((void *)(& process_status_21)); } @@ -2917,7 +2947,6 @@ int main(int argc, char const **argv) int process_status_22; __e_acsl_store_block((void *)(& process_status_22),(size_t)4); __gen_e_acsl_waitpid(pid_22,& process_status_22,0); - /*@ assert Eva: initialization: \initialized(&process_status_22); */ signal_eval(process_status_22,0,__gen_e_acsl_literal_string_63); __e_acsl_delete_block((void *)(& process_status_22)); } @@ -2932,7 +2961,6 @@ int main(int argc, char const **argv) int process_status_23; __e_acsl_store_block((void *)(& process_status_23),(size_t)4); __gen_e_acsl_waitpid(pid_23,& process_status_23,0); - /*@ assert Eva: initialization: \initialized(&process_status_23); */ signal_eval(process_status_23,0,__gen_e_acsl_literal_string_66); __e_acsl_delete_block((void *)(& process_status_23)); } @@ -2947,7 +2975,6 @@ int main(int argc, char const **argv) int process_status_24; __e_acsl_store_block((void *)(& process_status_24),(size_t)4); __gen_e_acsl_waitpid(pid_24,& process_status_24,0); - /*@ assert Eva: initialization: \initialized(&process_status_24); */ signal_eval(process_status_24,0,__gen_e_acsl_literal_string_66); __e_acsl_delete_block((void *)(& process_status_24)); } @@ -2962,7 +2989,6 @@ int main(int argc, char const **argv) int process_status_25; __e_acsl_store_block((void *)(& process_status_25),(size_t)4); __gen_e_acsl_waitpid(pid_25,& process_status_25,0); - /*@ assert Eva: initialization: \initialized(&process_status_25); */ signal_eval(process_status_25,0,__gen_e_acsl_literal_string_66); __e_acsl_delete_block((void *)(& process_status_25)); } @@ -2980,7 +3006,6 @@ int main(int argc, char const **argv) int process_status_26; __e_acsl_store_block((void *)(& process_status_26),(size_t)4); __gen_e_acsl_waitpid(pid_26,& process_status_26,0); - /*@ assert Eva: initialization: \initialized(&process_status_26); */ signal_eval(process_status_26,0,__gen_e_acsl_literal_string_72); __e_acsl_delete_block((void *)(& process_status_26)); } @@ -2995,7 +3020,6 @@ int main(int argc, char const **argv) int process_status_27; __e_acsl_store_block((void *)(& process_status_27),(size_t)4); __gen_e_acsl_waitpid(pid_27,& process_status_27,0); - /*@ assert Eva: initialization: \initialized(&process_status_27); */ signal_eval(process_status_27,0,__gen_e_acsl_literal_string_72); __e_acsl_delete_block((void *)(& process_status_27)); } @@ -3010,7 +3034,6 @@ int main(int argc, char const **argv) int process_status_28; __e_acsl_store_block((void *)(& process_status_28),(size_t)4); __gen_e_acsl_waitpid(pid_28,& process_status_28,0); - /*@ assert Eva: initialization: \initialized(&process_status_28); */ signal_eval(process_status_28,0,__gen_e_acsl_literal_string_75); __e_acsl_delete_block((void *)(& process_status_28)); } @@ -3025,7 +3048,6 @@ int main(int argc, char const **argv) int process_status_29; __e_acsl_store_block((void *)(& process_status_29),(size_t)4); __gen_e_acsl_waitpid(pid_29,& process_status_29,0); - /*@ assert Eva: initialization: \initialized(&process_status_29); */ signal_eval(process_status_29,0,__gen_e_acsl_literal_string_75); __e_acsl_delete_block((void *)(& process_status_29)); } @@ -3040,7 +3062,6 @@ int main(int argc, char const **argv) int process_status_30; __e_acsl_store_block((void *)(& process_status_30),(size_t)4); __gen_e_acsl_waitpid(pid_30,& process_status_30,0); - /*@ assert Eva: initialization: \initialized(&process_status_30); */ signal_eval(process_status_30,0,__gen_e_acsl_literal_string_78); __e_acsl_delete_block((void *)(& process_status_30)); } @@ -3055,7 +3076,6 @@ int main(int argc, char const **argv) int process_status_31; __e_acsl_store_block((void *)(& process_status_31),(size_t)4); __gen_e_acsl_waitpid(pid_31,& process_status_31,0); - /*@ assert Eva: initialization: \initialized(&process_status_31); */ signal_eval(process_status_31,0,__gen_e_acsl_literal_string_78); __e_acsl_delete_block((void *)(& process_status_31)); } @@ -3070,7 +3090,6 @@ int main(int argc, char const **argv) int process_status_32; __e_acsl_store_block((void *)(& process_status_32),(size_t)4); __gen_e_acsl_waitpid(pid_32,& process_status_32,0); - /*@ assert Eva: initialization: \initialized(&process_status_32); */ signal_eval(process_status_32,0,__gen_e_acsl_literal_string_80); __e_acsl_delete_block((void *)(& process_status_32)); } @@ -3085,7 +3104,6 @@ int main(int argc, char const **argv) int process_status_33; __e_acsl_store_block((void *)(& process_status_33),(size_t)4); __gen_e_acsl_waitpid(pid_33,& process_status_33,0); - /*@ assert Eva: initialization: \initialized(&process_status_33); */ signal_eval(process_status_33,0,__gen_e_acsl_literal_string_80); __e_acsl_delete_block((void *)(& process_status_33)); } @@ -3100,7 +3118,6 @@ int main(int argc, char const **argv) int process_status_34; __e_acsl_store_block((void *)(& process_status_34),(size_t)4); __gen_e_acsl_waitpid(pid_34,& process_status_34,0); - /*@ assert Eva: initialization: \initialized(&process_status_34); */ signal_eval(process_status_34,0,__gen_e_acsl_literal_string_83); __e_acsl_delete_block((void *)(& process_status_34)); } @@ -3115,7 +3132,6 @@ int main(int argc, char const **argv) int process_status_35; __e_acsl_store_block((void *)(& process_status_35),(size_t)4); __gen_e_acsl_waitpid(pid_35,& process_status_35,0); - /*@ assert Eva: initialization: \initialized(&process_status_35); */ signal_eval(process_status_35,0,__gen_e_acsl_literal_string_83); __e_acsl_delete_block((void *)(& process_status_35)); } @@ -3130,7 +3146,6 @@ int main(int argc, char const **argv) int process_status_36; __e_acsl_store_block((void *)(& process_status_36),(size_t)4); __gen_e_acsl_waitpid(pid_36,& process_status_36,0); - /*@ assert Eva: initialization: \initialized(&process_status_36); */ signal_eval(process_status_36,0,__gen_e_acsl_literal_string_86); __e_acsl_delete_block((void *)(& process_status_36)); } @@ -3145,7 +3160,6 @@ int main(int argc, char const **argv) int process_status_37; __e_acsl_store_block((void *)(& process_status_37),(size_t)4); __gen_e_acsl_waitpid(pid_37,& process_status_37,0); - /*@ assert Eva: initialization: \initialized(&process_status_37); */ signal_eval(process_status_37,0,__gen_e_acsl_literal_string_86); __e_acsl_delete_block((void *)(& process_status_37)); } @@ -3160,7 +3174,6 @@ int main(int argc, char const **argv) int process_status_38; __e_acsl_store_block((void *)(& process_status_38),(size_t)4); __gen_e_acsl_waitpid(pid_38,& process_status_38,0); - /*@ assert Eva: initialization: \initialized(&process_status_38); */ signal_eval(process_status_38,0,__gen_e_acsl_literal_string_89); __e_acsl_delete_block((void *)(& process_status_38)); } @@ -3175,7 +3188,6 @@ int main(int argc, char const **argv) int process_status_39; __e_acsl_store_block((void *)(& process_status_39),(size_t)4); __gen_e_acsl_waitpid(pid_39,& process_status_39,0); - /*@ assert Eva: initialization: \initialized(&process_status_39); */ signal_eval(process_status_39,0,__gen_e_acsl_literal_string_89); __e_acsl_delete_block((void *)(& process_status_39)); } @@ -3190,7 +3202,6 @@ int main(int argc, char const **argv) int process_status_40; __e_acsl_store_block((void *)(& process_status_40),(size_t)4); __gen_e_acsl_waitpid(pid_40,& process_status_40,0); - /*@ assert Eva: initialization: \initialized(&process_status_40); */ signal_eval(process_status_40,0,__gen_e_acsl_literal_string_92); __e_acsl_delete_block((void *)(& process_status_40)); } @@ -3205,7 +3216,6 @@ int main(int argc, char const **argv) int process_status_41; __e_acsl_store_block((void *)(& process_status_41),(size_t)4); __gen_e_acsl_waitpid(pid_41,& process_status_41,0); - /*@ assert Eva: initialization: \initialized(&process_status_41); */ signal_eval(process_status_41,0,__gen_e_acsl_literal_string_94); __e_acsl_delete_block((void *)(& process_status_41)); } @@ -3220,7 +3230,6 @@ int main(int argc, char const **argv) int process_status_42; __e_acsl_store_block((void *)(& process_status_42),(size_t)4); __gen_e_acsl_waitpid(pid_42,& process_status_42,0); - /*@ assert Eva: initialization: \initialized(&process_status_42); */ signal_eval(process_status_42,0,__gen_e_acsl_literal_string_96); __e_acsl_delete_block((void *)(& process_status_42)); } @@ -3235,7 +3244,6 @@ int main(int argc, char const **argv) int process_status_43; __e_acsl_store_block((void *)(& process_status_43),(size_t)4); __gen_e_acsl_waitpid(pid_43,& process_status_43,0); - /*@ assert Eva: initialization: \initialized(&process_status_43); */ signal_eval(process_status_43,0,__gen_e_acsl_literal_string_96); __e_acsl_delete_block((void *)(& process_status_43)); } @@ -3250,7 +3258,6 @@ int main(int argc, char const **argv) int process_status_44; __e_acsl_store_block((void *)(& process_status_44),(size_t)4); __gen_e_acsl_waitpid(pid_44,& process_status_44,0); - /*@ assert Eva: initialization: \initialized(&process_status_44); */ signal_eval(process_status_44,0,__gen_e_acsl_literal_string_99); __e_acsl_delete_block((void *)(& process_status_44)); } @@ -3265,7 +3272,6 @@ int main(int argc, char const **argv) int process_status_45; __e_acsl_store_block((void *)(& process_status_45),(size_t)4); __gen_e_acsl_waitpid(pid_45,& process_status_45,0); - /*@ assert Eva: initialization: \initialized(&process_status_45); */ signal_eval(process_status_45,0,__gen_e_acsl_literal_string_99); __e_acsl_delete_block((void *)(& process_status_45)); } @@ -3280,7 +3286,6 @@ int main(int argc, char const **argv) int process_status_46; __e_acsl_store_block((void *)(& process_status_46),(size_t)4); __gen_e_acsl_waitpid(pid_46,& process_status_46,0); - /*@ assert Eva: initialization: \initialized(&process_status_46); */ signal_eval(process_status_46,0,__gen_e_acsl_literal_string_102); __e_acsl_delete_block((void *)(& process_status_46)); } @@ -3295,7 +3300,6 @@ int main(int argc, char const **argv) int process_status_47; __e_acsl_store_block((void *)(& process_status_47),(size_t)4); __gen_e_acsl_waitpid(pid_47,& process_status_47,0); - /*@ assert Eva: initialization: \initialized(&process_status_47); */ signal_eval(process_status_47,0,__gen_e_acsl_literal_string_102); __e_acsl_delete_block((void *)(& process_status_47)); } @@ -3310,7 +3314,6 @@ int main(int argc, char const **argv) int process_status_48; __e_acsl_store_block((void *)(& process_status_48),(size_t)4); __gen_e_acsl_waitpid(pid_48,& process_status_48,0); - /*@ assert Eva: initialization: \initialized(&process_status_48); */ signal_eval(process_status_48,0,__gen_e_acsl_literal_string_102); __e_acsl_delete_block((void *)(& process_status_48)); } @@ -3328,7 +3331,6 @@ int main(int argc, char const **argv) int process_status_49; __e_acsl_store_block((void *)(& process_status_49),(size_t)4); __gen_e_acsl_waitpid(pid_49,& process_status_49,0); - /*@ assert Eva: initialization: \initialized(&process_status_49); */ signal_eval(process_status_49,0,__gen_e_acsl_literal_string_108); __e_acsl_delete_block((void *)(& process_status_49)); } @@ -3343,7 +3345,6 @@ int main(int argc, char const **argv) int process_status_50; __e_acsl_store_block((void *)(& process_status_50),(size_t)4); __gen_e_acsl_waitpid(pid_50,& process_status_50,0); - /*@ assert Eva: initialization: \initialized(&process_status_50); */ signal_eval(process_status_50,0,__gen_e_acsl_literal_string_108); __e_acsl_delete_block((void *)(& process_status_50)); } @@ -3358,7 +3359,6 @@ int main(int argc, char const **argv) int process_status_51; __e_acsl_store_block((void *)(& process_status_51),(size_t)4); __gen_e_acsl_waitpid(pid_51,& process_status_51,0); - /*@ assert Eva: initialization: \initialized(&process_status_51); */ signal_eval(process_status_51,0,__gen_e_acsl_literal_string_111); __e_acsl_delete_block((void *)(& process_status_51)); } @@ -3373,7 +3373,6 @@ int main(int argc, char const **argv) int process_status_52; __e_acsl_store_block((void *)(& process_status_52),(size_t)4); __gen_e_acsl_waitpid(pid_52,& process_status_52,0); - /*@ assert Eva: initialization: \initialized(&process_status_52); */ signal_eval(process_status_52,0,__gen_e_acsl_literal_string_111); __e_acsl_delete_block((void *)(& process_status_52)); } @@ -3388,7 +3387,6 @@ int main(int argc, char const **argv) int process_status_53; __e_acsl_store_block((void *)(& process_status_53),(size_t)4); __gen_e_acsl_waitpid(pid_53,& process_status_53,0); - /*@ assert Eva: initialization: \initialized(&process_status_53); */ signal_eval(process_status_53,0,__gen_e_acsl_literal_string_114); __e_acsl_delete_block((void *)(& process_status_53)); } @@ -3403,7 +3401,6 @@ int main(int argc, char const **argv) int process_status_54; __e_acsl_store_block((void *)(& process_status_54),(size_t)4); __gen_e_acsl_waitpid(pid_54,& process_status_54,0); - /*@ assert Eva: initialization: \initialized(&process_status_54); */ signal_eval(process_status_54,0,__gen_e_acsl_literal_string_114); __e_acsl_delete_block((void *)(& process_status_54)); } @@ -3418,7 +3415,6 @@ int main(int argc, char const **argv) int process_status_55; __e_acsl_store_block((void *)(& process_status_55),(size_t)4); __gen_e_acsl_waitpid(pid_55,& process_status_55,0); - /*@ assert Eva: initialization: \initialized(&process_status_55); */ signal_eval(process_status_55,0,__gen_e_acsl_literal_string_114); __e_acsl_delete_block((void *)(& process_status_55)); } @@ -3436,7 +3432,6 @@ int main(int argc, char const **argv) int process_status_56; __e_acsl_store_block((void *)(& process_status_56),(size_t)4); __gen_e_acsl_waitpid(pid_56,& process_status_56,0); - /*@ assert Eva: initialization: \initialized(&process_status_56); */ signal_eval(process_status_56,0,__gen_e_acsl_literal_string_119); __e_acsl_delete_block((void *)(& process_status_56)); } @@ -3451,7 +3446,6 @@ int main(int argc, char const **argv) int process_status_57; __e_acsl_store_block((void *)(& process_status_57),(size_t)4); __gen_e_acsl_waitpid(pid_57,& process_status_57,0); - /*@ assert Eva: initialization: \initialized(&process_status_57); */ signal_eval(process_status_57,0,__gen_e_acsl_literal_string_119); __e_acsl_delete_block((void *)(& process_status_57)); } @@ -3466,7 +3460,6 @@ int main(int argc, char const **argv) int process_status_58; __e_acsl_store_block((void *)(& process_status_58),(size_t)4); __gen_e_acsl_waitpid(pid_58,& process_status_58,0); - /*@ assert Eva: initialization: \initialized(&process_status_58); */ signal_eval(process_status_58,0,__gen_e_acsl_literal_string_122); __e_acsl_delete_block((void *)(& process_status_58)); } @@ -3481,7 +3474,6 @@ int main(int argc, char const **argv) int process_status_59; __e_acsl_store_block((void *)(& process_status_59),(size_t)4); __gen_e_acsl_waitpid(pid_59,& process_status_59,0); - /*@ assert Eva: initialization: \initialized(&process_status_59); */ signal_eval(process_status_59,0,__gen_e_acsl_literal_string_122); __e_acsl_delete_block((void *)(& process_status_59)); } @@ -3496,7 +3488,6 @@ int main(int argc, char const **argv) int process_status_60; __e_acsl_store_block((void *)(& process_status_60),(size_t)4); __gen_e_acsl_waitpid(pid_60,& process_status_60,0); - /*@ assert Eva: initialization: \initialized(&process_status_60); */ signal_eval(process_status_60,0,__gen_e_acsl_literal_string_125); __e_acsl_delete_block((void *)(& process_status_60)); } @@ -3511,7 +3502,6 @@ int main(int argc, char const **argv) int process_status_61; __e_acsl_store_block((void *)(& process_status_61),(size_t)4); __gen_e_acsl_waitpid(pid_61,& process_status_61,0); - /*@ assert Eva: initialization: \initialized(&process_status_61); */ signal_eval(process_status_61,0,__gen_e_acsl_literal_string_125); __e_acsl_delete_block((void *)(& process_status_61)); } @@ -3526,7 +3516,6 @@ int main(int argc, char const **argv) int process_status_62; __e_acsl_store_block((void *)(& process_status_62),(size_t)4); __gen_e_acsl_waitpid(pid_62,& process_status_62,0); - /*@ assert Eva: initialization: \initialized(&process_status_62); */ signal_eval(process_status_62,0,__gen_e_acsl_literal_string_125); __e_acsl_delete_block((void *)(& process_status_62)); } @@ -3544,7 +3533,6 @@ int main(int argc, char const **argv) int process_status_63; __e_acsl_store_block((void *)(& process_status_63),(size_t)4); __gen_e_acsl_waitpid(pid_63,& process_status_63,0); - /*@ assert Eva: initialization: \initialized(&process_status_63); */ signal_eval(process_status_63,0,__gen_e_acsl_literal_string_130); __e_acsl_delete_block((void *)(& process_status_63)); } @@ -3559,7 +3547,6 @@ int main(int argc, char const **argv) int process_status_64; __e_acsl_store_block((void *)(& process_status_64),(size_t)4); __gen_e_acsl_waitpid(pid_64,& process_status_64,0); - /*@ assert Eva: initialization: \initialized(&process_status_64); */ signal_eval(process_status_64,0,__gen_e_acsl_literal_string_130); __e_acsl_delete_block((void *)(& process_status_64)); } @@ -3574,7 +3561,6 @@ int main(int argc, char const **argv) int process_status_65; __e_acsl_store_block((void *)(& process_status_65),(size_t)4); __gen_e_acsl_waitpid(pid_65,& process_status_65,0); - /*@ assert Eva: initialization: \initialized(&process_status_65); */ signal_eval(process_status_65,0,__gen_e_acsl_literal_string_133); __e_acsl_delete_block((void *)(& process_status_65)); } @@ -3589,7 +3575,6 @@ int main(int argc, char const **argv) int process_status_66; __e_acsl_store_block((void *)(& process_status_66),(size_t)4); __gen_e_acsl_waitpid(pid_66,& process_status_66,0); - /*@ assert Eva: initialization: \initialized(&process_status_66); */ signal_eval(process_status_66,0,__gen_e_acsl_literal_string_133); __e_acsl_delete_block((void *)(& process_status_66)); } @@ -3604,7 +3589,6 @@ int main(int argc, char const **argv) int process_status_67; __e_acsl_store_block((void *)(& process_status_67),(size_t)4); __gen_e_acsl_waitpid(pid_67,& process_status_67,0); - /*@ assert Eva: initialization: \initialized(&process_status_67); */ signal_eval(process_status_67,0,__gen_e_acsl_literal_string_135); __e_acsl_delete_block((void *)(& process_status_67)); } @@ -3619,7 +3603,6 @@ int main(int argc, char const **argv) int process_status_68; __e_acsl_store_block((void *)(& process_status_68),(size_t)4); __gen_e_acsl_waitpid(pid_68,& process_status_68,0); - /*@ assert Eva: initialization: \initialized(&process_status_68); */ signal_eval(process_status_68,0,__gen_e_acsl_literal_string_135); __e_acsl_delete_block((void *)(& process_status_68)); } @@ -3634,7 +3617,6 @@ int main(int argc, char const **argv) int process_status_69; __e_acsl_store_block((void *)(& process_status_69),(size_t)4); __gen_e_acsl_waitpid(pid_69,& process_status_69,0); - /*@ assert Eva: initialization: \initialized(&process_status_69); */ signal_eval(process_status_69,0,__gen_e_acsl_literal_string_138); __e_acsl_delete_block((void *)(& process_status_69)); } @@ -3652,7 +3634,6 @@ int main(int argc, char const **argv) int process_status_70; __e_acsl_store_block((void *)(& process_status_70),(size_t)4); __gen_e_acsl_waitpid(pid_70,& process_status_70,0); - /*@ assert Eva: initialization: \initialized(&process_status_70); */ signal_eval(process_status_70,0,__gen_e_acsl_literal_string_143); __e_acsl_delete_block((void *)(& process_status_70)); } @@ -3667,7 +3648,6 @@ int main(int argc, char const **argv) int process_status_71; __e_acsl_store_block((void *)(& process_status_71),(size_t)4); __gen_e_acsl_waitpid(pid_71,& process_status_71,0); - /*@ assert Eva: initialization: \initialized(&process_status_71); */ signal_eval(process_status_71,0,__gen_e_acsl_literal_string_143); __e_acsl_delete_block((void *)(& process_status_71)); } @@ -3682,7 +3662,6 @@ int main(int argc, char const **argv) int process_status_72; __e_acsl_store_block((void *)(& process_status_72),(size_t)4); __gen_e_acsl_waitpid(pid_72,& process_status_72,0); - /*@ assert Eva: initialization: \initialized(&process_status_72); */ signal_eval(process_status_72,0,__gen_e_acsl_literal_string_146); __e_acsl_delete_block((void *)(& process_status_72)); } @@ -3697,7 +3676,6 @@ int main(int argc, char const **argv) int process_status_73; __e_acsl_store_block((void *)(& process_status_73),(size_t)4); __gen_e_acsl_waitpid(pid_73,& process_status_73,0); - /*@ assert Eva: initialization: \initialized(&process_status_73); */ signal_eval(process_status_73,0,__gen_e_acsl_literal_string_146); __e_acsl_delete_block((void *)(& process_status_73)); } @@ -3712,7 +3690,6 @@ int main(int argc, char const **argv) int process_status_74; __e_acsl_store_block((void *)(& process_status_74),(size_t)4); __gen_e_acsl_waitpid(pid_74,& process_status_74,0); - /*@ assert Eva: initialization: \initialized(&process_status_74); */ signal_eval(process_status_74,0,__gen_e_acsl_literal_string_149); __e_acsl_delete_block((void *)(& process_status_74)); } @@ -3727,7 +3704,6 @@ int main(int argc, char const **argv) int process_status_75; __e_acsl_store_block((void *)(& process_status_75),(size_t)4); __gen_e_acsl_waitpid(pid_75,& process_status_75,0); - /*@ assert Eva: initialization: \initialized(&process_status_75); */ signal_eval(process_status_75,0,__gen_e_acsl_literal_string_149); __e_acsl_delete_block((void *)(& process_status_75)); } @@ -3742,7 +3718,6 @@ int main(int argc, char const **argv) int process_status_76; __e_acsl_store_block((void *)(& process_status_76),(size_t)4); __gen_e_acsl_waitpid(pid_76,& process_status_76,0); - /*@ assert Eva: initialization: \initialized(&process_status_76); */ signal_eval(process_status_76,0,__gen_e_acsl_literal_string_152); __e_acsl_delete_block((void *)(& process_status_76)); } @@ -3757,7 +3732,6 @@ int main(int argc, char const **argv) int process_status_77; __e_acsl_store_block((void *)(& process_status_77),(size_t)4); __gen_e_acsl_waitpid(pid_77,& process_status_77,0); - /*@ assert Eva: initialization: \initialized(&process_status_77); */ signal_eval(process_status_77,0,__gen_e_acsl_literal_string_152); __e_acsl_delete_block((void *)(& process_status_77)); } @@ -3772,7 +3746,6 @@ int main(int argc, char const **argv) int process_status_78; __e_acsl_store_block((void *)(& process_status_78),(size_t)4); __gen_e_acsl_waitpid(pid_78,& process_status_78,0); - /*@ assert Eva: initialization: \initialized(&process_status_78); */ signal_eval(process_status_78,1,__gen_e_acsl_literal_string_155); __e_acsl_delete_block((void *)(& process_status_78)); } @@ -3787,7 +3760,6 @@ int main(int argc, char const **argv) int process_status_79; __e_acsl_store_block((void *)(& process_status_79),(size_t)4); __gen_e_acsl_waitpid(pid_79,& process_status_79,0); - /*@ assert Eva: initialization: \initialized(&process_status_79); */ signal_eval(process_status_79,1,__gen_e_acsl_literal_string_157); __e_acsl_delete_block((void *)(& process_status_79)); } @@ -3802,7 +3774,6 @@ int main(int argc, char const **argv) int process_status_80; __e_acsl_store_block((void *)(& process_status_80),(size_t)4); __gen_e_acsl_waitpid(pid_80,& process_status_80,0); - /*@ assert Eva: initialization: \initialized(&process_status_80); */ signal_eval(process_status_80,1,__gen_e_acsl_literal_string_159); __e_acsl_delete_block((void *)(& process_status_80)); } @@ -3817,7 +3788,6 @@ int main(int argc, char const **argv) int process_status_81; __e_acsl_store_block((void *)(& process_status_81),(size_t)4); __gen_e_acsl_waitpid(pid_81,& process_status_81,0); - /*@ assert Eva: initialization: \initialized(&process_status_81); */ signal_eval(process_status_81,0,__gen_e_acsl_literal_string_161); __e_acsl_delete_block((void *)(& process_status_81)); } @@ -3832,7 +3802,6 @@ int main(int argc, char const **argv) int process_status_82; __e_acsl_store_block((void *)(& process_status_82),(size_t)4); __gen_e_acsl_waitpid(pid_82,& process_status_82,0); - /*@ assert Eva: initialization: \initialized(&process_status_82); */ signal_eval(process_status_82,0,__gen_e_acsl_literal_string_161); __e_acsl_delete_block((void *)(& process_status_82)); } @@ -3847,7 +3816,6 @@ int main(int argc, char const **argv) int process_status_83; __e_acsl_store_block((void *)(& process_status_83),(size_t)4); __gen_e_acsl_waitpid(pid_83,& process_status_83,0); - /*@ assert Eva: initialization: \initialized(&process_status_83); */ signal_eval(process_status_83,0,__gen_e_acsl_literal_string_163); __e_acsl_delete_block((void *)(& process_status_83)); } @@ -3862,7 +3830,6 @@ int main(int argc, char const **argv) int process_status_84; __e_acsl_store_block((void *)(& process_status_84),(size_t)4); __gen_e_acsl_waitpid(pid_84,& process_status_84,0); - /*@ assert Eva: initialization: \initialized(&process_status_84); */ signal_eval(process_status_84,0,__gen_e_acsl_literal_string_163); __e_acsl_delete_block((void *)(& process_status_84)); } @@ -3877,7 +3844,6 @@ int main(int argc, char const **argv) int process_status_85; __e_acsl_store_block((void *)(& process_status_85),(size_t)4); __gen_e_acsl_waitpid(pid_85,& process_status_85,0); - /*@ assert Eva: initialization: \initialized(&process_status_85); */ signal_eval(process_status_85,0,__gen_e_acsl_literal_string_164); __e_acsl_delete_block((void *)(& process_status_85)); } @@ -3892,7 +3858,6 @@ int main(int argc, char const **argv) int process_status_86; __e_acsl_store_block((void *)(& process_status_86),(size_t)4); __gen_e_acsl_waitpid(pid_86,& process_status_86,0); - /*@ assert Eva: initialization: \initialized(&process_status_86); */ signal_eval(process_status_86,0,__gen_e_acsl_literal_string_164); __e_acsl_delete_block((void *)(& process_status_86)); } @@ -3907,7 +3872,6 @@ int main(int argc, char const **argv) int process_status_87; __e_acsl_store_block((void *)(& process_status_87),(size_t)4); __gen_e_acsl_waitpid(pid_87,& process_status_87,0); - /*@ assert Eva: initialization: \initialized(&process_status_87); */ signal_eval(process_status_87,1,__gen_e_acsl_literal_string_165); __e_acsl_delete_block((void *)(& process_status_87)); } @@ -3922,7 +3886,6 @@ int main(int argc, char const **argv) int process_status_88; __e_acsl_store_block((void *)(& process_status_88),(size_t)4); __gen_e_acsl_waitpid(pid_88,& process_status_88,0); - /*@ assert Eva: initialization: \initialized(&process_status_88); */ signal_eval(process_status_88,1,__gen_e_acsl_literal_string_165); __e_acsl_delete_block((void *)(& process_status_88)); } @@ -3937,7 +3900,6 @@ int main(int argc, char const **argv) int process_status_89; __e_acsl_store_block((void *)(& process_status_89),(size_t)4); __gen_e_acsl_waitpid(pid_89,& process_status_89,0); - /*@ assert Eva: initialization: \initialized(&process_status_89); */ signal_eval(process_status_89,1,__gen_e_acsl_literal_string_166); __e_acsl_delete_block((void *)(& process_status_89)); } @@ -3952,7 +3914,6 @@ int main(int argc, char const **argv) int process_status_90; __e_acsl_store_block((void *)(& process_status_90),(size_t)4); __gen_e_acsl_waitpid(pid_90,& process_status_90,0); - /*@ assert Eva: initialization: \initialized(&process_status_90); */ signal_eval(process_status_90,1,__gen_e_acsl_literal_string_166); __e_acsl_delete_block((void *)(& process_status_90)); } @@ -3967,7 +3928,6 @@ int main(int argc, char const **argv) int process_status_91; __e_acsl_store_block((void *)(& process_status_91),(size_t)4); __gen_e_acsl_waitpid(pid_91,& process_status_91,0); - /*@ assert Eva: initialization: \initialized(&process_status_91); */ signal_eval(process_status_91,1,__gen_e_acsl_literal_string_167); __e_acsl_delete_block((void *)(& process_status_91)); } @@ -3982,7 +3942,6 @@ int main(int argc, char const **argv) int process_status_92; __e_acsl_store_block((void *)(& process_status_92),(size_t)4); __gen_e_acsl_waitpid(pid_92,& process_status_92,0); - /*@ assert Eva: initialization: \initialized(&process_status_92); */ signal_eval(process_status_92,1,__gen_e_acsl_literal_string_167); __e_acsl_delete_block((void *)(& process_status_92)); } @@ -3998,7 +3957,6 @@ int main(int argc, char const **argv) int process_status_93; __e_acsl_store_block((void *)(& process_status_93),(size_t)4); __gen_e_acsl_waitpid(pid_93,& process_status_93,0); - /*@ assert Eva: initialization: \initialized(&process_status_93); */ signal_eval(process_status_93,1,__gen_e_acsl_literal_string_168); __e_acsl_delete_block((void *)(& process_status_93)); } @@ -4014,7 +3972,6 @@ int main(int argc, char const **argv) int process_status_94; __e_acsl_store_block((void *)(& process_status_94),(size_t)4); __gen_e_acsl_waitpid(pid_94,& process_status_94,0); - /*@ assert Eva: initialization: \initialized(&process_status_94); */ signal_eval(process_status_94,1,__gen_e_acsl_literal_string_168); __e_acsl_delete_block((void *)(& process_status_94)); } @@ -4029,7 +3986,6 @@ int main(int argc, char const **argv) int process_status_95; __e_acsl_store_block((void *)(& process_status_95),(size_t)4); __gen_e_acsl_waitpid(pid_95,& process_status_95,0); - /*@ assert Eva: initialization: \initialized(&process_status_95); */ signal_eval(process_status_95,0,__gen_e_acsl_literal_string_170); __e_acsl_delete_block((void *)(& process_status_95)); } @@ -4044,7 +4000,6 @@ int main(int argc, char const **argv) int process_status_96; __e_acsl_store_block((void *)(& process_status_96),(size_t)4); __gen_e_acsl_waitpid(pid_96,& process_status_96,0); - /*@ assert Eva: initialization: \initialized(&process_status_96); */ signal_eval(process_status_96,0,__gen_e_acsl_literal_string_170); __e_acsl_delete_block((void *)(& process_status_96)); } @@ -4059,7 +4014,6 @@ int main(int argc, char const **argv) int process_status_97; __e_acsl_store_block((void *)(& process_status_97),(size_t)4); __gen_e_acsl_waitpid(pid_97,& process_status_97,0); - /*@ assert Eva: initialization: \initialized(&process_status_97); */ signal_eval(process_status_97,0,__gen_e_acsl_literal_string_172); __e_acsl_delete_block((void *)(& process_status_97)); } @@ -4074,7 +4028,6 @@ int main(int argc, char const **argv) int process_status_98; __e_acsl_store_block((void *)(& process_status_98),(size_t)4); __gen_e_acsl_waitpid(pid_98,& process_status_98,0); - /*@ assert Eva: initialization: \initialized(&process_status_98); */ signal_eval(process_status_98,0,__gen_e_acsl_literal_string_172); __e_acsl_delete_block((void *)(& process_status_98)); } @@ -4089,7 +4042,6 @@ int main(int argc, char const **argv) int process_status_99; __e_acsl_store_block((void *)(& process_status_99),(size_t)4); __gen_e_acsl_waitpid(pid_99,& process_status_99,0); - /*@ assert Eva: initialization: \initialized(&process_status_99); */ signal_eval(process_status_99,0,__gen_e_acsl_literal_string_174); __e_acsl_delete_block((void *)(& process_status_99)); } @@ -4104,7 +4056,6 @@ int main(int argc, char const **argv) int process_status_100; __e_acsl_store_block((void *)(& process_status_100),(size_t)4); __gen_e_acsl_waitpid(pid_100,& process_status_100,0); - /*@ assert Eva: initialization: \initialized(&process_status_100); */ signal_eval(process_status_100,0,__gen_e_acsl_literal_string_174); __e_acsl_delete_block((void *)(& process_status_100)); } @@ -4119,7 +4070,6 @@ int main(int argc, char const **argv) int process_status_101; __e_acsl_store_block((void *)(& process_status_101),(size_t)4); __gen_e_acsl_waitpid(pid_101,& process_status_101,0); - /*@ assert Eva: initialization: \initialized(&process_status_101); */ signal_eval(process_status_101,0,__gen_e_acsl_literal_string_177); __e_acsl_delete_block((void *)(& process_status_101)); } @@ -4134,7 +4084,6 @@ int main(int argc, char const **argv) int process_status_102; __e_acsl_store_block((void *)(& process_status_102),(size_t)4); __gen_e_acsl_waitpid(pid_102,& process_status_102,0); - /*@ assert Eva: initialization: \initialized(&process_status_102); */ signal_eval(process_status_102,0,__gen_e_acsl_literal_string_177); __e_acsl_delete_block((void *)(& process_status_102)); } @@ -4149,7 +4098,6 @@ int main(int argc, char const **argv) int process_status_103; __e_acsl_store_block((void *)(& process_status_103),(size_t)4); __gen_e_acsl_waitpid(pid_103,& process_status_103,0); - /*@ assert Eva: initialization: \initialized(&process_status_103); */ signal_eval(process_status_103,0,__gen_e_acsl_literal_string_180); __e_acsl_delete_block((void *)(& process_status_103)); } @@ -4164,7 +4112,6 @@ int main(int argc, char const **argv) int process_status_104; __e_acsl_store_block((void *)(& process_status_104),(size_t)4); __gen_e_acsl_waitpid(pid_104,& process_status_104,0); - /*@ assert Eva: initialization: \initialized(&process_status_104); */ signal_eval(process_status_104,0,__gen_e_acsl_literal_string_180); __e_acsl_delete_block((void *)(& process_status_104)); } @@ -4179,7 +4126,6 @@ int main(int argc, char const **argv) int process_status_105; __e_acsl_store_block((void *)(& process_status_105),(size_t)4); __gen_e_acsl_waitpid(pid_105,& process_status_105,0); - /*@ assert Eva: initialization: \initialized(&process_status_105); */ signal_eval(process_status_105,0,__gen_e_acsl_literal_string_183); __e_acsl_delete_block((void *)(& process_status_105)); } @@ -4194,7 +4140,6 @@ int main(int argc, char const **argv) int process_status_106; __e_acsl_store_block((void *)(& process_status_106),(size_t)4); __gen_e_acsl_waitpid(pid_106,& process_status_106,0); - /*@ assert Eva: initialization: \initialized(&process_status_106); */ signal_eval(process_status_106,0,__gen_e_acsl_literal_string_183); __e_acsl_delete_block((void *)(& process_status_106)); } @@ -4209,7 +4154,6 @@ int main(int argc, char const **argv) int process_status_107; __e_acsl_store_block((void *)(& process_status_107),(size_t)4); __gen_e_acsl_waitpid(pid_107,& process_status_107,0); - /*@ assert Eva: initialization: \initialized(&process_status_107); */ signal_eval(process_status_107,0,__gen_e_acsl_literal_string_186); __e_acsl_delete_block((void *)(& process_status_107)); } @@ -4224,7 +4168,6 @@ int main(int argc, char const **argv) int process_status_108; __e_acsl_store_block((void *)(& process_status_108),(size_t)4); __gen_e_acsl_waitpid(pid_108,& process_status_108,0); - /*@ assert Eva: initialization: \initialized(&process_status_108); */ signal_eval(process_status_108,0,__gen_e_acsl_literal_string_186); __e_acsl_delete_block((void *)(& process_status_108)); } @@ -4239,7 +4182,6 @@ int main(int argc, char const **argv) int process_status_109; __e_acsl_store_block((void *)(& process_status_109),(size_t)4); __gen_e_acsl_waitpid(pid_109,& process_status_109,0); - /*@ assert Eva: initialization: \initialized(&process_status_109); */ signal_eval(process_status_109,0,__gen_e_acsl_literal_string_186); __e_acsl_delete_block((void *)(& process_status_109)); } @@ -4254,7 +4196,6 @@ int main(int argc, char const **argv) int process_status_110; __e_acsl_store_block((void *)(& process_status_110),(size_t)4); __gen_e_acsl_waitpid(pid_110,& process_status_110,0); - /*@ assert Eva: initialization: \initialized(&process_status_110); */ signal_eval(process_status_110,0,__gen_e_acsl_literal_string_186); __e_acsl_delete_block((void *)(& process_status_110)); } @@ -4269,7 +4210,6 @@ int main(int argc, char const **argv) int process_status_111; __e_acsl_store_block((void *)(& process_status_111),(size_t)4); __gen_e_acsl_waitpid(pid_111,& process_status_111,0); - /*@ assert Eva: initialization: \initialized(&process_status_111); */ signal_eval(process_status_111,1,__gen_e_acsl_literal_string_190); __e_acsl_delete_block((void *)(& process_status_111)); } @@ -4284,7 +4224,6 @@ int main(int argc, char const **argv) int process_status_112; __e_acsl_store_block((void *)(& process_status_112),(size_t)4); __gen_e_acsl_waitpid(pid_112,& process_status_112,0); - /*@ assert Eva: initialization: \initialized(&process_status_112); */ signal_eval(process_status_112,1,__gen_e_acsl_literal_string_190); __e_acsl_delete_block((void *)(& process_status_112)); } @@ -4299,7 +4238,6 @@ int main(int argc, char const **argv) int process_status_113; __e_acsl_store_block((void *)(& process_status_113),(size_t)4); __gen_e_acsl_waitpid(pid_113,& process_status_113,0); - /*@ assert Eva: initialization: \initialized(&process_status_113); */ signal_eval(process_status_113,1,__gen_e_acsl_literal_string_190); __e_acsl_delete_block((void *)(& process_status_113)); } @@ -4314,7 +4252,6 @@ int main(int argc, char const **argv) int process_status_114; __e_acsl_store_block((void *)(& process_status_114),(size_t)4); __gen_e_acsl_waitpid(pid_114,& process_status_114,0); - /*@ assert Eva: initialization: \initialized(&process_status_114); */ signal_eval(process_status_114,1,__gen_e_acsl_literal_string_190); __e_acsl_delete_block((void *)(& process_status_114)); } @@ -4329,7 +4266,6 @@ int main(int argc, char const **argv) int process_status_115; __e_acsl_store_block((void *)(& process_status_115),(size_t)4); __gen_e_acsl_waitpid(pid_115,& process_status_115,0); - /*@ assert Eva: initialization: \initialized(&process_status_115); */ signal_eval(process_status_115,1,__gen_e_acsl_literal_string_191); __e_acsl_delete_block((void *)(& process_status_115)); } @@ -4344,7 +4280,6 @@ int main(int argc, char const **argv) int process_status_116; __e_acsl_store_block((void *)(& process_status_116),(size_t)4); __gen_e_acsl_waitpid(pid_116,& process_status_116,0); - /*@ assert Eva: initialization: \initialized(&process_status_116); */ signal_eval(process_status_116,1,__gen_e_acsl_literal_string_191); __e_acsl_delete_block((void *)(& process_status_116)); } @@ -4359,7 +4294,6 @@ int main(int argc, char const **argv) int process_status_117; __e_acsl_store_block((void *)(& process_status_117),(size_t)4); __gen_e_acsl_waitpid(pid_117,& process_status_117,0); - /*@ assert Eva: initialization: \initialized(&process_status_117); */ signal_eval(process_status_117,1,__gen_e_acsl_literal_string_191); __e_acsl_delete_block((void *)(& process_status_117)); } @@ -4374,7 +4308,6 @@ int main(int argc, char const **argv) int process_status_118; __e_acsl_store_block((void *)(& process_status_118),(size_t)4); __gen_e_acsl_waitpid(pid_118,& process_status_118,0); - /*@ assert Eva: initialization: \initialized(&process_status_118); */ signal_eval(process_status_118,1,__gen_e_acsl_literal_string_191); __e_acsl_delete_block((void *)(& process_status_118)); } @@ -4390,7 +4323,6 @@ int main(int argc, char const **argv) int process_status_119; __e_acsl_store_block((void *)(& process_status_119),(size_t)4); __gen_e_acsl_waitpid(pid_119,& process_status_119,0); - /*@ assert Eva: initialization: \initialized(&process_status_119); */ signal_eval(process_status_119,1,__gen_e_acsl_literal_string_192); __e_acsl_delete_block((void *)(& process_status_119)); } @@ -4406,7 +4338,6 @@ int main(int argc, char const **argv) int process_status_120; __e_acsl_store_block((void *)(& process_status_120),(size_t)4); __gen_e_acsl_waitpid(pid_120,& process_status_120,0); - /*@ assert Eva: initialization: \initialized(&process_status_120); */ signal_eval(process_status_120,1,__gen_e_acsl_literal_string_192); __e_acsl_delete_block((void *)(& process_status_120)); } @@ -4422,7 +4353,6 @@ int main(int argc, char const **argv) int process_status_121; __e_acsl_store_block((void *)(& process_status_121),(size_t)4); __gen_e_acsl_waitpid(pid_121,& process_status_121,0); - /*@ assert Eva: initialization: \initialized(&process_status_121); */ signal_eval(process_status_121,1,__gen_e_acsl_literal_string_192); __e_acsl_delete_block((void *)(& process_status_121)); } @@ -4438,7 +4368,6 @@ int main(int argc, char const **argv) int process_status_122; __e_acsl_store_block((void *)(& process_status_122),(size_t)4); __gen_e_acsl_waitpid(pid_122,& process_status_122,0); - /*@ assert Eva: initialization: \initialized(&process_status_122); */ signal_eval(process_status_122,1,__gen_e_acsl_literal_string_192); __e_acsl_delete_block((void *)(& process_status_122)); } @@ -4453,7 +4382,6 @@ int main(int argc, char const **argv) int process_status_123; __e_acsl_store_block((void *)(& process_status_123),(size_t)4); __gen_e_acsl_waitpid(pid_123,& process_status_123,0); - /*@ assert Eva: initialization: \initialized(&process_status_123); */ signal_eval(process_status_123,1,__gen_e_acsl_literal_string_193); __e_acsl_delete_block((void *)(& process_status_123)); } @@ -4468,7 +4396,6 @@ int main(int argc, char const **argv) int process_status_124; __e_acsl_store_block((void *)(& process_status_124),(size_t)4); __gen_e_acsl_waitpid(pid_124,& process_status_124,0); - /*@ assert Eva: initialization: \initialized(&process_status_124); */ signal_eval(process_status_124,1,__gen_e_acsl_literal_string_193); __e_acsl_delete_block((void *)(& process_status_124)); } @@ -4483,7 +4410,6 @@ int main(int argc, char const **argv) int process_status_125; __e_acsl_store_block((void *)(& process_status_125),(size_t)4); __gen_e_acsl_waitpid(pid_125,& process_status_125,0); - /*@ assert Eva: initialization: \initialized(&process_status_125); */ signal_eval(process_status_125,1,__gen_e_acsl_literal_string_193); __e_acsl_delete_block((void *)(& process_status_125)); } @@ -4498,7 +4424,6 @@ int main(int argc, char const **argv) int process_status_126; __e_acsl_store_block((void *)(& process_status_126),(size_t)4); __gen_e_acsl_waitpid(pid_126,& process_status_126,0); - /*@ assert Eva: initialization: \initialized(&process_status_126); */ signal_eval(process_status_126,1,__gen_e_acsl_literal_string_193); __e_acsl_delete_block((void *)(& process_status_126)); } @@ -4513,7 +4438,6 @@ int main(int argc, char const **argv) int process_status_127; __e_acsl_store_block((void *)(& process_status_127),(size_t)4); __gen_e_acsl_waitpid(pid_127,& process_status_127,0); - /*@ assert Eva: initialization: \initialized(&process_status_127); */ signal_eval(process_status_127,1,__gen_e_acsl_literal_string_194); __e_acsl_delete_block((void *)(& process_status_127)); } @@ -4528,7 +4452,6 @@ int main(int argc, char const **argv) int process_status_128; __e_acsl_store_block((void *)(& process_status_128),(size_t)4); __gen_e_acsl_waitpid(pid_128,& process_status_128,0); - /*@ assert Eva: initialization: \initialized(&process_status_128); */ signal_eval(process_status_128,1,__gen_e_acsl_literal_string_194); __e_acsl_delete_block((void *)(& process_status_128)); } @@ -4543,7 +4466,6 @@ int main(int argc, char const **argv) int process_status_129; __e_acsl_store_block((void *)(& process_status_129),(size_t)4); __gen_e_acsl_waitpid(pid_129,& process_status_129,0); - /*@ assert Eva: initialization: \initialized(&process_status_129); */ signal_eval(process_status_129,1,__gen_e_acsl_literal_string_194); __e_acsl_delete_block((void *)(& process_status_129)); } @@ -4558,7 +4480,6 @@ int main(int argc, char const **argv) int process_status_130; __e_acsl_store_block((void *)(& process_status_130),(size_t)4); __gen_e_acsl_waitpid(pid_130,& process_status_130,0); - /*@ assert Eva: initialization: \initialized(&process_status_130); */ signal_eval(process_status_130,1,__gen_e_acsl_literal_string_194); __e_acsl_delete_block((void *)(& process_status_130)); } @@ -4573,7 +4494,6 @@ int main(int argc, char const **argv) int process_status_131; __e_acsl_store_block((void *)(& process_status_131),(size_t)4); __gen_e_acsl_waitpid(pid_131,& process_status_131,0); - /*@ assert Eva: initialization: \initialized(&process_status_131); */ signal_eval(process_status_131,0,__gen_e_acsl_literal_string_196); __e_acsl_delete_block((void *)(& process_status_131)); } @@ -4588,7 +4508,6 @@ int main(int argc, char const **argv) int process_status_132; __e_acsl_store_block((void *)(& process_status_132),(size_t)4); __gen_e_acsl_waitpid(pid_132,& process_status_132,0); - /*@ assert Eva: initialization: \initialized(&process_status_132); */ signal_eval(process_status_132,0,__gen_e_acsl_literal_string_196); __e_acsl_delete_block((void *)(& process_status_132)); } @@ -4603,7 +4522,6 @@ int main(int argc, char const **argv) int process_status_133; __e_acsl_store_block((void *)(& process_status_133),(size_t)4); __gen_e_acsl_waitpid(pid_133,& process_status_133,0); - /*@ assert Eva: initialization: \initialized(&process_status_133); */ signal_eval(process_status_133,0,__gen_e_acsl_literal_string_196); __e_acsl_delete_block((void *)(& process_status_133)); } @@ -4618,7 +4536,6 @@ int main(int argc, char const **argv) int process_status_134; __e_acsl_store_block((void *)(& process_status_134),(size_t)4); __gen_e_acsl_waitpid(pid_134,& process_status_134,0); - /*@ assert Eva: initialization: \initialized(&process_status_134); */ signal_eval(process_status_134,0,__gen_e_acsl_literal_string_196); __e_acsl_delete_block((void *)(& process_status_134)); } @@ -4633,7 +4550,6 @@ int main(int argc, char const **argv) int process_status_135; __e_acsl_store_block((void *)(& process_status_135),(size_t)4); __gen_e_acsl_waitpid(pid_135,& process_status_135,0); - /*@ assert Eva: initialization: \initialized(&process_status_135); */ signal_eval(process_status_135,0,__gen_e_acsl_literal_string_201); __e_acsl_delete_block((void *)(& process_status_135)); } @@ -4648,7 +4564,6 @@ int main(int argc, char const **argv) int process_status_136; __e_acsl_store_block((void *)(& process_status_136),(size_t)4); __gen_e_acsl_waitpid(pid_136,& process_status_136,0); - /*@ assert Eva: initialization: \initialized(&process_status_136); */ signal_eval(process_status_136,0,__gen_e_acsl_literal_string_201); __e_acsl_delete_block((void *)(& process_status_136)); } @@ -4663,7 +4578,6 @@ int main(int argc, char const **argv) int process_status_137; __e_acsl_store_block((void *)(& process_status_137),(size_t)4); __gen_e_acsl_waitpid(pid_137,& process_status_137,0); - /*@ assert Eva: initialization: \initialized(&process_status_137); */ signal_eval(process_status_137,0,__gen_e_acsl_literal_string_201); __e_acsl_delete_block((void *)(& process_status_137)); } @@ -4678,7 +4592,6 @@ int main(int argc, char const **argv) int process_status_138; __e_acsl_store_block((void *)(& process_status_138),(size_t)4); __gen_e_acsl_waitpid(pid_138,& process_status_138,0); - /*@ assert Eva: initialization: \initialized(&process_status_138); */ signal_eval(process_status_138,0,__gen_e_acsl_literal_string_201); __e_acsl_delete_block((void *)(& process_status_138)); } @@ -4693,7 +4606,6 @@ int main(int argc, char const **argv) int process_status_139; __e_acsl_store_block((void *)(& process_status_139),(size_t)4); __gen_e_acsl_waitpid(pid_139,& process_status_139,0); - /*@ assert Eva: initialization: \initialized(&process_status_139); */ signal_eval(process_status_139,0,__gen_e_acsl_literal_string_206); __e_acsl_delete_block((void *)(& process_status_139)); } @@ -4708,7 +4620,6 @@ int main(int argc, char const **argv) int process_status_140; __e_acsl_store_block((void *)(& process_status_140),(size_t)4); __gen_e_acsl_waitpid(pid_140,& process_status_140,0); - /*@ assert Eva: initialization: \initialized(&process_status_140); */ signal_eval(process_status_140,0,__gen_e_acsl_literal_string_206); __e_acsl_delete_block((void *)(& process_status_140)); } @@ -4723,7 +4634,6 @@ int main(int argc, char const **argv) int process_status_141; __e_acsl_store_block((void *)(& process_status_141),(size_t)4); __gen_e_acsl_waitpid(pid_141,& process_status_141,0); - /*@ assert Eva: initialization: \initialized(&process_status_141); */ signal_eval(process_status_141,0,__gen_e_acsl_literal_string_206); __e_acsl_delete_block((void *)(& process_status_141)); } @@ -4738,7 +4648,6 @@ int main(int argc, char const **argv) int process_status_142; __e_acsl_store_block((void *)(& process_status_142),(size_t)4); __gen_e_acsl_waitpid(pid_142,& process_status_142,0); - /*@ assert Eva: initialization: \initialized(&process_status_142); */ signal_eval(process_status_142,0,__gen_e_acsl_literal_string_206); __e_acsl_delete_block((void *)(& process_status_142)); } @@ -4753,7 +4662,6 @@ int main(int argc, char const **argv) int process_status_143; __e_acsl_store_block((void *)(& process_status_143),(size_t)4); __gen_e_acsl_waitpid(pid_143,& process_status_143,0); - /*@ assert Eva: initialization: \initialized(&process_status_143); */ signal_eval(process_status_143,0,__gen_e_acsl_literal_string_211); __e_acsl_delete_block((void *)(& process_status_143)); } @@ -4768,7 +4676,6 @@ int main(int argc, char const **argv) int process_status_144; __e_acsl_store_block((void *)(& process_status_144),(size_t)4); __gen_e_acsl_waitpid(pid_144,& process_status_144,0); - /*@ assert Eva: initialization: \initialized(&process_status_144); */ signal_eval(process_status_144,0,__gen_e_acsl_literal_string_211); __e_acsl_delete_block((void *)(& process_status_144)); } @@ -4783,7 +4690,6 @@ int main(int argc, char const **argv) int process_status_145; __e_acsl_store_block((void *)(& process_status_145),(size_t)4); __gen_e_acsl_waitpid(pid_145,& process_status_145,0); - /*@ assert Eva: initialization: \initialized(&process_status_145); */ signal_eval(process_status_145,0,__gen_e_acsl_literal_string_211); __e_acsl_delete_block((void *)(& process_status_145)); } @@ -4798,7 +4704,6 @@ int main(int argc, char const **argv) int process_status_146; __e_acsl_store_block((void *)(& process_status_146),(size_t)4); __gen_e_acsl_waitpid(pid_146,& process_status_146,0); - /*@ assert Eva: initialization: \initialized(&process_status_146); */ signal_eval(process_status_146,0,__gen_e_acsl_literal_string_211); __e_acsl_delete_block((void *)(& process_status_146)); } @@ -4813,7 +4718,6 @@ int main(int argc, char const **argv) int process_status_147; __e_acsl_store_block((void *)(& process_status_147),(size_t)4); __gen_e_acsl_waitpid(pid_147,& process_status_147,0); - /*@ assert Eva: initialization: \initialized(&process_status_147); */ signal_eval(process_status_147,0,__gen_e_acsl_literal_string_216); __e_acsl_delete_block((void *)(& process_status_147)); } @@ -4828,7 +4732,6 @@ int main(int argc, char const **argv) int process_status_148; __e_acsl_store_block((void *)(& process_status_148),(size_t)4); __gen_e_acsl_waitpid(pid_148,& process_status_148,0); - /*@ assert Eva: initialization: \initialized(&process_status_148); */ signal_eval(process_status_148,0,__gen_e_acsl_literal_string_216); __e_acsl_delete_block((void *)(& process_status_148)); } @@ -4843,7 +4746,6 @@ int main(int argc, char const **argv) int process_status_149; __e_acsl_store_block((void *)(& process_status_149),(size_t)4); __gen_e_acsl_waitpid(pid_149,& process_status_149,0); - /*@ assert Eva: initialization: \initialized(&process_status_149); */ signal_eval(process_status_149,0,__gen_e_acsl_literal_string_216); __e_acsl_delete_block((void *)(& process_status_149)); } @@ -4858,7 +4760,6 @@ int main(int argc, char const **argv) int process_status_150; __e_acsl_store_block((void *)(& process_status_150),(size_t)4); __gen_e_acsl_waitpid(pid_150,& process_status_150,0); - /*@ assert Eva: initialization: \initialized(&process_status_150); */ signal_eval(process_status_150,0,__gen_e_acsl_literal_string_216); __e_acsl_delete_block((void *)(& process_status_150)); } @@ -4873,7 +4774,6 @@ int main(int argc, char const **argv) int process_status_151; __e_acsl_store_block((void *)(& process_status_151),(size_t)4); __gen_e_acsl_waitpid(pid_151,& process_status_151,0); - /*@ assert Eva: initialization: \initialized(&process_status_151); */ signal_eval(process_status_151,0,__gen_e_acsl_literal_string_221); __e_acsl_delete_block((void *)(& process_status_151)); } @@ -4888,7 +4788,6 @@ int main(int argc, char const **argv) int process_status_152; __e_acsl_store_block((void *)(& process_status_152),(size_t)4); __gen_e_acsl_waitpid(pid_152,& process_status_152,0); - /*@ assert Eva: initialization: \initialized(&process_status_152); */ signal_eval(process_status_152,0,__gen_e_acsl_literal_string_221); __e_acsl_delete_block((void *)(& process_status_152)); } @@ -4903,7 +4802,6 @@ int main(int argc, char const **argv) int process_status_153; __e_acsl_store_block((void *)(& process_status_153),(size_t)4); __gen_e_acsl_waitpid(pid_153,& process_status_153,0); - /*@ assert Eva: initialization: \initialized(&process_status_153); */ signal_eval(process_status_153,0,__gen_e_acsl_literal_string_221); __e_acsl_delete_block((void *)(& process_status_153)); } @@ -4918,7 +4816,6 @@ int main(int argc, char const **argv) int process_status_154; __e_acsl_store_block((void *)(& process_status_154),(size_t)4); __gen_e_acsl_waitpid(pid_154,& process_status_154,0); - /*@ assert Eva: initialization: \initialized(&process_status_154); */ signal_eval(process_status_154,0,__gen_e_acsl_literal_string_221); __e_acsl_delete_block((void *)(& process_status_154)); } @@ -4933,7 +4830,6 @@ int main(int argc, char const **argv) int process_status_155; __e_acsl_store_block((void *)(& process_status_155),(size_t)4); __gen_e_acsl_waitpid(pid_155,& process_status_155,0); - /*@ assert Eva: initialization: \initialized(&process_status_155); */ signal_eval(process_status_155,0,__gen_e_acsl_literal_string_226); __e_acsl_delete_block((void *)(& process_status_155)); } @@ -4948,7 +4844,6 @@ int main(int argc, char const **argv) int process_status_156; __e_acsl_store_block((void *)(& process_status_156),(size_t)4); __gen_e_acsl_waitpid(pid_156,& process_status_156,0); - /*@ assert Eva: initialization: \initialized(&process_status_156); */ signal_eval(process_status_156,0,__gen_e_acsl_literal_string_226); __e_acsl_delete_block((void *)(& process_status_156)); } @@ -4963,7 +4858,6 @@ int main(int argc, char const **argv) int process_status_157; __e_acsl_store_block((void *)(& process_status_157),(size_t)4); __gen_e_acsl_waitpid(pid_157,& process_status_157,0); - /*@ assert Eva: initialization: \initialized(&process_status_157); */ signal_eval(process_status_157,0,__gen_e_acsl_literal_string_226); __e_acsl_delete_block((void *)(& process_status_157)); } @@ -4978,7 +4872,6 @@ int main(int argc, char const **argv) int process_status_158; __e_acsl_store_block((void *)(& process_status_158),(size_t)4); __gen_e_acsl_waitpid(pid_158,& process_status_158,0); - /*@ assert Eva: initialization: \initialized(&process_status_158); */ signal_eval(process_status_158,0,__gen_e_acsl_literal_string_226); __e_acsl_delete_block((void *)(& process_status_158)); } @@ -4993,7 +4886,6 @@ int main(int argc, char const **argv) int process_status_159; __e_acsl_store_block((void *)(& process_status_159),(size_t)4); __gen_e_acsl_waitpid(pid_159,& process_status_159,0); - /*@ assert Eva: initialization: \initialized(&process_status_159); */ signal_eval(process_status_159,0,__gen_e_acsl_literal_string_231); __e_acsl_delete_block((void *)(& process_status_159)); } @@ -5008,7 +4900,6 @@ int main(int argc, char const **argv) int process_status_160; __e_acsl_store_block((void *)(& process_status_160),(size_t)4); __gen_e_acsl_waitpid(pid_160,& process_status_160,0); - /*@ assert Eva: initialization: \initialized(&process_status_160); */ signal_eval(process_status_160,0,__gen_e_acsl_literal_string_231); __e_acsl_delete_block((void *)(& process_status_160)); } @@ -5023,7 +4914,6 @@ int main(int argc, char const **argv) int process_status_161; __e_acsl_store_block((void *)(& process_status_161),(size_t)4); __gen_e_acsl_waitpid(pid_161,& process_status_161,0); - /*@ assert Eva: initialization: \initialized(&process_status_161); */ signal_eval(process_status_161,1,__gen_e_acsl_literal_string_233); __e_acsl_delete_block((void *)(& process_status_161)); } @@ -5038,7 +4928,6 @@ int main(int argc, char const **argv) int process_status_162; __e_acsl_store_block((void *)(& process_status_162),(size_t)4); __gen_e_acsl_waitpid(pid_162,& process_status_162,0); - /*@ assert Eva: initialization: \initialized(&process_status_162); */ signal_eval(process_status_162,1,__gen_e_acsl_literal_string_233); __e_acsl_delete_block((void *)(& process_status_162)); } @@ -5053,7 +4942,6 @@ int main(int argc, char const **argv) int process_status_163; __e_acsl_store_block((void *)(& process_status_163),(size_t)4); __gen_e_acsl_waitpid(pid_163,& process_status_163,0); - /*@ assert Eva: initialization: \initialized(&process_status_163); */ signal_eval(process_status_163,1,__gen_e_acsl_literal_string_234); __e_acsl_delete_block((void *)(& process_status_163)); } @@ -5068,7 +4956,6 @@ int main(int argc, char const **argv) int process_status_164; __e_acsl_store_block((void *)(& process_status_164),(size_t)4); __gen_e_acsl_waitpid(pid_164,& process_status_164,0); - /*@ assert Eva: initialization: \initialized(&process_status_164); */ signal_eval(process_status_164,1,__gen_e_acsl_literal_string_234); __e_acsl_delete_block((void *)(& process_status_164)); } @@ -5083,7 +4970,6 @@ int main(int argc, char const **argv) int process_status_165; __e_acsl_store_block((void *)(& process_status_165),(size_t)4); __gen_e_acsl_waitpid(pid_165,& process_status_165,0); - /*@ assert Eva: initialization: \initialized(&process_status_165); */ signal_eval(process_status_165,1,__gen_e_acsl_literal_string_235); __e_acsl_delete_block((void *)(& process_status_165)); } @@ -5098,7 +4984,6 @@ int main(int argc, char const **argv) int process_status_166; __e_acsl_store_block((void *)(& process_status_166),(size_t)4); __gen_e_acsl_waitpid(pid_166,& process_status_166,0); - /*@ assert Eva: initialization: \initialized(&process_status_166); */ signal_eval(process_status_166,1,__gen_e_acsl_literal_string_235); __e_acsl_delete_block((void *)(& process_status_166)); } @@ -5113,7 +4998,6 @@ int main(int argc, char const **argv) int process_status_167; __e_acsl_store_block((void *)(& process_status_167),(size_t)4); __gen_e_acsl_waitpid(pid_167,& process_status_167,0); - /*@ assert Eva: initialization: \initialized(&process_status_167); */ signal_eval(process_status_167,0,__gen_e_acsl_literal_string_237); __e_acsl_delete_block((void *)(& process_status_167)); } @@ -5128,7 +5012,6 @@ int main(int argc, char const **argv) int process_status_168; __e_acsl_store_block((void *)(& process_status_168),(size_t)4); __gen_e_acsl_waitpid(pid_168,& process_status_168,0); - /*@ assert Eva: initialization: \initialized(&process_status_168); */ signal_eval(process_status_168,0,__gen_e_acsl_literal_string_237); __e_acsl_delete_block((void *)(& process_status_168)); } @@ -5143,7 +5026,6 @@ int main(int argc, char const **argv) int process_status_169; __e_acsl_store_block((void *)(& process_status_169),(size_t)4); __gen_e_acsl_waitpid(pid_169,& process_status_169,0); - /*@ assert Eva: initialization: \initialized(&process_status_169); */ signal_eval(process_status_169,1,__gen_e_acsl_literal_string_239); __e_acsl_delete_block((void *)(& process_status_169)); } @@ -5158,7 +5040,6 @@ int main(int argc, char const **argv) int process_status_170; __e_acsl_store_block((void *)(& process_status_170),(size_t)4); __gen_e_acsl_waitpid(pid_170,& process_status_170,0); - /*@ assert Eva: initialization: \initialized(&process_status_170); */ signal_eval(process_status_170,1,__gen_e_acsl_literal_string_239); __e_acsl_delete_block((void *)(& process_status_170)); } @@ -5173,7 +5054,6 @@ int main(int argc, char const **argv) int process_status_171; __e_acsl_store_block((void *)(& process_status_171),(size_t)4); __gen_e_acsl_waitpid(pid_171,& process_status_171,0); - /*@ assert Eva: initialization: \initialized(&process_status_171); */ signal_eval(process_status_171,1,__gen_e_acsl_literal_string_240); __e_acsl_delete_block((void *)(& process_status_171)); } @@ -5188,7 +5068,6 @@ int main(int argc, char const **argv) int process_status_172; __e_acsl_store_block((void *)(& process_status_172),(size_t)4); __gen_e_acsl_waitpid(pid_172,& process_status_172,0); - /*@ assert Eva: initialization: \initialized(&process_status_172); */ signal_eval(process_status_172,1,__gen_e_acsl_literal_string_240); __e_acsl_delete_block((void *)(& process_status_172)); } @@ -5203,7 +5082,6 @@ int main(int argc, char const **argv) int process_status_173; __e_acsl_store_block((void *)(& process_status_173),(size_t)4); __gen_e_acsl_waitpid(pid_173,& process_status_173,0); - /*@ assert Eva: initialization: \initialized(&process_status_173); */ signal_eval(process_status_173,1,__gen_e_acsl_literal_string_241); __e_acsl_delete_block((void *)(& process_status_173)); } @@ -5218,7 +5096,6 @@ int main(int argc, char const **argv) int process_status_174; __e_acsl_store_block((void *)(& process_status_174),(size_t)4); __gen_e_acsl_waitpid(pid_174,& process_status_174,0); - /*@ assert Eva: initialization: \initialized(&process_status_174); */ signal_eval(process_status_174,1,__gen_e_acsl_literal_string_241); __e_acsl_delete_block((void *)(& process_status_174)); } @@ -5233,7 +5110,6 @@ int main(int argc, char const **argv) int process_status_175; __e_acsl_store_block((void *)(& process_status_175),(size_t)4); __gen_e_acsl_waitpid(pid_175,& process_status_175,0); - /*@ assert Eva: initialization: \initialized(&process_status_175); */ signal_eval(process_status_175,0,__gen_e_acsl_literal_string_243); __e_acsl_delete_block((void *)(& process_status_175)); } @@ -5248,7 +5124,6 @@ int main(int argc, char const **argv) int process_status_176; __e_acsl_store_block((void *)(& process_status_176),(size_t)4); __gen_e_acsl_waitpid(pid_176,& process_status_176,0); - /*@ assert Eva: initialization: \initialized(&process_status_176); */ signal_eval(process_status_176,0,__gen_e_acsl_literal_string_243); __e_acsl_delete_block((void *)(& process_status_176)); } @@ -5263,7 +5138,6 @@ int main(int argc, char const **argv) int process_status_177; __e_acsl_store_block((void *)(& process_status_177),(size_t)4); __gen_e_acsl_waitpid(pid_177,& process_status_177,0); - /*@ assert Eva: initialization: \initialized(&process_status_177); */ signal_eval(process_status_177,1,__gen_e_acsl_literal_string_245); __e_acsl_delete_block((void *)(& process_status_177)); } @@ -5278,7 +5152,6 @@ int main(int argc, char const **argv) int process_status_178; __e_acsl_store_block((void *)(& process_status_178),(size_t)4); __gen_e_acsl_waitpid(pid_178,& process_status_178,0); - /*@ assert Eva: initialization: \initialized(&process_status_178); */ signal_eval(process_status_178,1,__gen_e_acsl_literal_string_245); __e_acsl_delete_block((void *)(& process_status_178)); } @@ -5293,7 +5166,6 @@ int main(int argc, char const **argv) int process_status_179; __e_acsl_store_block((void *)(& process_status_179),(size_t)4); __gen_e_acsl_waitpid(pid_179,& process_status_179,0); - /*@ assert Eva: initialization: \initialized(&process_status_179); */ signal_eval(process_status_179,1,__gen_e_acsl_literal_string_246); __e_acsl_delete_block((void *)(& process_status_179)); } @@ -5308,7 +5180,6 @@ int main(int argc, char const **argv) int process_status_180; __e_acsl_store_block((void *)(& process_status_180),(size_t)4); __gen_e_acsl_waitpid(pid_180,& process_status_180,0); - /*@ assert Eva: initialization: \initialized(&process_status_180); */ signal_eval(process_status_180,1,__gen_e_acsl_literal_string_246); __e_acsl_delete_block((void *)(& process_status_180)); } @@ -5323,7 +5194,6 @@ int main(int argc, char const **argv) int process_status_181; __e_acsl_store_block((void *)(& process_status_181),(size_t)4); __gen_e_acsl_waitpid(pid_181,& process_status_181,0); - /*@ assert Eva: initialization: \initialized(&process_status_181); */ signal_eval(process_status_181,1,__gen_e_acsl_literal_string_247); __e_acsl_delete_block((void *)(& process_status_181)); } @@ -5338,7 +5208,6 @@ int main(int argc, char const **argv) int process_status_182; __e_acsl_store_block((void *)(& process_status_182),(size_t)4); __gen_e_acsl_waitpid(pid_182,& process_status_182,0); - /*@ assert Eva: initialization: \initialized(&process_status_182); */ signal_eval(process_status_182,1,__gen_e_acsl_literal_string_247); __e_acsl_delete_block((void *)(& process_status_182)); } @@ -5353,7 +5222,6 @@ int main(int argc, char const **argv) int process_status_183; __e_acsl_store_block((void *)(& process_status_183),(size_t)4); __gen_e_acsl_waitpid(pid_183,& process_status_183,0); - /*@ assert Eva: initialization: \initialized(&process_status_183); */ signal_eval(process_status_183,0,__gen_e_acsl_literal_string_249); __e_acsl_delete_block((void *)(& process_status_183)); } @@ -5368,7 +5236,6 @@ int main(int argc, char const **argv) int process_status_184; __e_acsl_store_block((void *)(& process_status_184),(size_t)4); __gen_e_acsl_waitpid(pid_184,& process_status_184,0); - /*@ assert Eva: initialization: \initialized(&process_status_184); */ signal_eval(process_status_184,0,__gen_e_acsl_literal_string_249); __e_acsl_delete_block((void *)(& process_status_184)); } @@ -5383,7 +5250,6 @@ int main(int argc, char const **argv) int process_status_185; __e_acsl_store_block((void *)(& process_status_185),(size_t)4); __gen_e_acsl_waitpid(pid_185,& process_status_185,0); - /*@ assert Eva: initialization: \initialized(&process_status_185); */ signal_eval(process_status_185,1,__gen_e_acsl_literal_string_251); __e_acsl_delete_block((void *)(& process_status_185)); } @@ -5398,7 +5264,6 @@ int main(int argc, char const **argv) int process_status_186; __e_acsl_store_block((void *)(& process_status_186),(size_t)4); __gen_e_acsl_waitpid(pid_186,& process_status_186,0); - /*@ assert Eva: initialization: \initialized(&process_status_186); */ signal_eval(process_status_186,1,__gen_e_acsl_literal_string_251); __e_acsl_delete_block((void *)(& process_status_186)); } @@ -5413,7 +5278,6 @@ int main(int argc, char const **argv) int process_status_187; __e_acsl_store_block((void *)(& process_status_187),(size_t)4); __gen_e_acsl_waitpid(pid_187,& process_status_187,0); - /*@ assert Eva: initialization: \initialized(&process_status_187); */ signal_eval(process_status_187,1,__gen_e_acsl_literal_string_252); __e_acsl_delete_block((void *)(& process_status_187)); } @@ -5428,7 +5292,6 @@ int main(int argc, char const **argv) int process_status_188; __e_acsl_store_block((void *)(& process_status_188),(size_t)4); __gen_e_acsl_waitpid(pid_188,& process_status_188,0); - /*@ assert Eva: initialization: \initialized(&process_status_188); */ signal_eval(process_status_188,1,__gen_e_acsl_literal_string_252); __e_acsl_delete_block((void *)(& process_status_188)); } @@ -5443,7 +5306,6 @@ int main(int argc, char const **argv) int process_status_189; __e_acsl_store_block((void *)(& process_status_189),(size_t)4); __gen_e_acsl_waitpid(pid_189,& process_status_189,0); - /*@ assert Eva: initialization: \initialized(&process_status_189); */ signal_eval(process_status_189,1,__gen_e_acsl_literal_string_253); __e_acsl_delete_block((void *)(& process_status_189)); } @@ -5458,7 +5320,6 @@ int main(int argc, char const **argv) int process_status_190; __e_acsl_store_block((void *)(& process_status_190),(size_t)4); __gen_e_acsl_waitpid(pid_190,& process_status_190,0); - /*@ assert Eva: initialization: \initialized(&process_status_190); */ signal_eval(process_status_190,1,__gen_e_acsl_literal_string_253); __e_acsl_delete_block((void *)(& process_status_190)); } @@ -5473,7 +5334,6 @@ int main(int argc, char const **argv) int process_status_191; __e_acsl_store_block((void *)(& process_status_191),(size_t)4); __gen_e_acsl_waitpid(pid_191,& process_status_191,0); - /*@ assert Eva: initialization: \initialized(&process_status_191); */ signal_eval(process_status_191,1,__gen_e_acsl_literal_string_255); __e_acsl_delete_block((void *)(& process_status_191)); } @@ -5488,7 +5348,6 @@ int main(int argc, char const **argv) int process_status_192; __e_acsl_store_block((void *)(& process_status_192),(size_t)4); __gen_e_acsl_waitpid(pid_192,& process_status_192,0); - /*@ assert Eva: initialization: \initialized(&process_status_192); */ signal_eval(process_status_192,1,__gen_e_acsl_literal_string_255); __e_acsl_delete_block((void *)(& process_status_192)); } @@ -5503,7 +5362,6 @@ int main(int argc, char const **argv) int process_status_193; __e_acsl_store_block((void *)(& process_status_193),(size_t)4); __gen_e_acsl_waitpid(pid_193,& process_status_193,0); - /*@ assert Eva: initialization: \initialized(&process_status_193); */ signal_eval(process_status_193,0,__gen_e_acsl_literal_string_257); __e_acsl_delete_block((void *)(& process_status_193)); } @@ -5518,7 +5376,6 @@ int main(int argc, char const **argv) int process_status_194; __e_acsl_store_block((void *)(& process_status_194),(size_t)4); __gen_e_acsl_waitpid(pid_194,& process_status_194,0); - /*@ assert Eva: initialization: \initialized(&process_status_194); */ signal_eval(process_status_194,0,__gen_e_acsl_literal_string_257); __e_acsl_delete_block((void *)(& process_status_194)); } @@ -5533,7 +5390,6 @@ int main(int argc, char const **argv) int process_status_195; __e_acsl_store_block((void *)(& process_status_195),(size_t)4); __gen_e_acsl_waitpid(pid_195,& process_status_195,0); - /*@ assert Eva: initialization: \initialized(&process_status_195); */ signal_eval(process_status_195,1,__gen_e_acsl_literal_string_258); __e_acsl_delete_block((void *)(& process_status_195)); } @@ -5548,7 +5404,6 @@ int main(int argc, char const **argv) int process_status_196; __e_acsl_store_block((void *)(& process_status_196),(size_t)4); __gen_e_acsl_waitpid(pid_196,& process_status_196,0); - /*@ assert Eva: initialization: \initialized(&process_status_196); */ signal_eval(process_status_196,1,__gen_e_acsl_literal_string_258); __e_acsl_delete_block((void *)(& process_status_196)); } @@ -5563,7 +5418,6 @@ int main(int argc, char const **argv) int process_status_197; __e_acsl_store_block((void *)(& process_status_197),(size_t)4); __gen_e_acsl_waitpid(pid_197,& process_status_197,0); - /*@ assert Eva: initialization: \initialized(&process_status_197); */ signal_eval(process_status_197,1,__gen_e_acsl_literal_string_259); __e_acsl_delete_block((void *)(& process_status_197)); } @@ -5578,7 +5432,6 @@ int main(int argc, char const **argv) int process_status_198; __e_acsl_store_block((void *)(& process_status_198),(size_t)4); __gen_e_acsl_waitpid(pid_198,& process_status_198,0); - /*@ assert Eva: initialization: \initialized(&process_status_198); */ signal_eval(process_status_198,1,__gen_e_acsl_literal_string_259); __e_acsl_delete_block((void *)(& process_status_198)); } @@ -5593,7 +5446,6 @@ int main(int argc, char const **argv) int process_status_199; __e_acsl_store_block((void *)(& process_status_199),(size_t)4); __gen_e_acsl_waitpid(pid_199,& process_status_199,0); - /*@ assert Eva: initialization: \initialized(&process_status_199); */ signal_eval(process_status_199,1,__gen_e_acsl_literal_string_261); __e_acsl_delete_block((void *)(& process_status_199)); } @@ -5608,7 +5460,6 @@ int main(int argc, char const **argv) int process_status_200; __e_acsl_store_block((void *)(& process_status_200),(size_t)4); __gen_e_acsl_waitpid(pid_200,& process_status_200,0); - /*@ assert Eva: initialization: \initialized(&process_status_200); */ signal_eval(process_status_200,1,__gen_e_acsl_literal_string_261); __e_acsl_delete_block((void *)(& process_status_200)); } @@ -5623,7 +5474,6 @@ int main(int argc, char const **argv) int process_status_201; __e_acsl_store_block((void *)(& process_status_201),(size_t)4); __gen_e_acsl_waitpid(pid_201,& process_status_201,0); - /*@ assert Eva: initialization: \initialized(&process_status_201); */ signal_eval(process_status_201,0,__gen_e_acsl_literal_string_263); __e_acsl_delete_block((void *)(& process_status_201)); } @@ -5638,7 +5488,6 @@ int main(int argc, char const **argv) int process_status_202; __e_acsl_store_block((void *)(& process_status_202),(size_t)4); __gen_e_acsl_waitpid(pid_202,& process_status_202,0); - /*@ assert Eva: initialization: \initialized(&process_status_202); */ signal_eval(process_status_202,0,__gen_e_acsl_literal_string_263); __e_acsl_delete_block((void *)(& process_status_202)); } @@ -5653,7 +5502,6 @@ int main(int argc, char const **argv) int process_status_203; __e_acsl_store_block((void *)(& process_status_203),(size_t)4); __gen_e_acsl_waitpid(pid_203,& process_status_203,0); - /*@ assert Eva: initialization: \initialized(&process_status_203); */ signal_eval(process_status_203,1,__gen_e_acsl_literal_string_264); __e_acsl_delete_block((void *)(& process_status_203)); } @@ -5668,7 +5516,6 @@ int main(int argc, char const **argv) int process_status_204; __e_acsl_store_block((void *)(& process_status_204),(size_t)4); __gen_e_acsl_waitpid(pid_204,& process_status_204,0); - /*@ assert Eva: initialization: \initialized(&process_status_204); */ signal_eval(process_status_204,1,__gen_e_acsl_literal_string_264); __e_acsl_delete_block((void *)(& process_status_204)); } @@ -5683,7 +5530,6 @@ int main(int argc, char const **argv) int process_status_205; __e_acsl_store_block((void *)(& process_status_205),(size_t)4); __gen_e_acsl_waitpid(pid_205,& process_status_205,0); - /*@ assert Eva: initialization: \initialized(&process_status_205); */ signal_eval(process_status_205,1,__gen_e_acsl_literal_string_265); __e_acsl_delete_block((void *)(& process_status_205)); } @@ -5698,7 +5544,6 @@ int main(int argc, char const **argv) int process_status_206; __e_acsl_store_block((void *)(& process_status_206),(size_t)4); __gen_e_acsl_waitpid(pid_206,& process_status_206,0); - /*@ assert Eva: initialization: \initialized(&process_status_206); */ signal_eval(process_status_206,1,__gen_e_acsl_literal_string_265); __e_acsl_delete_block((void *)(& process_status_206)); } @@ -5713,7 +5558,6 @@ int main(int argc, char const **argv) int process_status_207; __e_acsl_store_block((void *)(& process_status_207),(size_t)4); __gen_e_acsl_waitpid(pid_207,& process_status_207,0); - /*@ assert Eva: initialization: \initialized(&process_status_207); */ signal_eval(process_status_207,1,__gen_e_acsl_literal_string_267); __e_acsl_delete_block((void *)(& process_status_207)); } @@ -5728,7 +5572,6 @@ int main(int argc, char const **argv) int process_status_208; __e_acsl_store_block((void *)(& process_status_208),(size_t)4); __gen_e_acsl_waitpid(pid_208,& process_status_208,0); - /*@ assert Eva: initialization: \initialized(&process_status_208); */ signal_eval(process_status_208,1,__gen_e_acsl_literal_string_267); __e_acsl_delete_block((void *)(& process_status_208)); } @@ -5743,7 +5586,6 @@ int main(int argc, char const **argv) int process_status_209; __e_acsl_store_block((void *)(& process_status_209),(size_t)4); __gen_e_acsl_waitpid(pid_209,& process_status_209,0); - /*@ assert Eva: initialization: \initialized(&process_status_209); */ signal_eval(process_status_209,0,__gen_e_acsl_literal_string_269); __e_acsl_delete_block((void *)(& process_status_209)); } @@ -5758,7 +5600,6 @@ int main(int argc, char const **argv) int process_status_210; __e_acsl_store_block((void *)(& process_status_210),(size_t)4); __gen_e_acsl_waitpid(pid_210,& process_status_210,0); - /*@ assert Eva: initialization: \initialized(&process_status_210); */ signal_eval(process_status_210,0,__gen_e_acsl_literal_string_269); __e_acsl_delete_block((void *)(& process_status_210)); } @@ -5773,7 +5614,6 @@ int main(int argc, char const **argv) int process_status_211; __e_acsl_store_block((void *)(& process_status_211),(size_t)4); __gen_e_acsl_waitpid(pid_211,& process_status_211,0); - /*@ assert Eva: initialization: \initialized(&process_status_211); */ signal_eval(process_status_211,1,__gen_e_acsl_literal_string_270); __e_acsl_delete_block((void *)(& process_status_211)); } @@ -5788,7 +5628,6 @@ int main(int argc, char const **argv) int process_status_212; __e_acsl_store_block((void *)(& process_status_212),(size_t)4); __gen_e_acsl_waitpid(pid_212,& process_status_212,0); - /*@ assert Eva: initialization: \initialized(&process_status_212); */ signal_eval(process_status_212,1,__gen_e_acsl_literal_string_270); __e_acsl_delete_block((void *)(& process_status_212)); } @@ -5803,7 +5642,6 @@ int main(int argc, char const **argv) int process_status_213; __e_acsl_store_block((void *)(& process_status_213),(size_t)4); __gen_e_acsl_waitpid(pid_213,& process_status_213,0); - /*@ assert Eva: initialization: \initialized(&process_status_213); */ signal_eval(process_status_213,1,__gen_e_acsl_literal_string_271); __e_acsl_delete_block((void *)(& process_status_213)); } @@ -5818,7 +5656,6 @@ int main(int argc, char const **argv) int process_status_214; __e_acsl_store_block((void *)(& process_status_214),(size_t)4); __gen_e_acsl_waitpid(pid_214,& process_status_214,0); - /*@ assert Eva: initialization: \initialized(&process_status_214); */ signal_eval(process_status_214,1,__gen_e_acsl_literal_string_271); __e_acsl_delete_block((void *)(& process_status_214)); } @@ -5833,7 +5670,6 @@ int main(int argc, char const **argv) int process_status_215; __e_acsl_store_block((void *)(& process_status_215),(size_t)4); __gen_e_acsl_waitpid(pid_215,& process_status_215,0); - /*@ assert Eva: initialization: \initialized(&process_status_215); */ signal_eval(process_status_215,1,__gen_e_acsl_literal_string_273); __e_acsl_delete_block((void *)(& process_status_215)); } @@ -5848,7 +5684,6 @@ int main(int argc, char const **argv) int process_status_216; __e_acsl_store_block((void *)(& process_status_216),(size_t)4); __gen_e_acsl_waitpid(pid_216,& process_status_216,0); - /*@ assert Eva: initialization: \initialized(&process_status_216); */ signal_eval(process_status_216,1,__gen_e_acsl_literal_string_273); __e_acsl_delete_block((void *)(& process_status_216)); } @@ -5863,7 +5698,6 @@ int main(int argc, char const **argv) int process_status_217; __e_acsl_store_block((void *)(& process_status_217),(size_t)4); __gen_e_acsl_waitpid(pid_217,& process_status_217,0); - /*@ assert Eva: initialization: \initialized(&process_status_217); */ signal_eval(process_status_217,0,__gen_e_acsl_literal_string_275); __e_acsl_delete_block((void *)(& process_status_217)); } @@ -5878,7 +5712,6 @@ int main(int argc, char const **argv) int process_status_218; __e_acsl_store_block((void *)(& process_status_218),(size_t)4); __gen_e_acsl_waitpid(pid_218,& process_status_218,0); - /*@ assert Eva: initialization: \initialized(&process_status_218); */ signal_eval(process_status_218,0,__gen_e_acsl_literal_string_275); __e_acsl_delete_block((void *)(& process_status_218)); } @@ -5893,7 +5726,6 @@ int main(int argc, char const **argv) int process_status_219; __e_acsl_store_block((void *)(& process_status_219),(size_t)4); __gen_e_acsl_waitpid(pid_219,& process_status_219,0); - /*@ assert Eva: initialization: \initialized(&process_status_219); */ signal_eval(process_status_219,1,__gen_e_acsl_literal_string_276); __e_acsl_delete_block((void *)(& process_status_219)); } @@ -5908,7 +5740,6 @@ int main(int argc, char const **argv) int process_status_220; __e_acsl_store_block((void *)(& process_status_220),(size_t)4); __gen_e_acsl_waitpid(pid_220,& process_status_220,0); - /*@ assert Eva: initialization: \initialized(&process_status_220); */ signal_eval(process_status_220,1,__gen_e_acsl_literal_string_276); __e_acsl_delete_block((void *)(& process_status_220)); } @@ -5923,7 +5754,6 @@ int main(int argc, char const **argv) int process_status_221; __e_acsl_store_block((void *)(& process_status_221),(size_t)4); __gen_e_acsl_waitpid(pid_221,& process_status_221,0); - /*@ assert Eva: initialization: \initialized(&process_status_221); */ signal_eval(process_status_221,1,__gen_e_acsl_literal_string_277); __e_acsl_delete_block((void *)(& process_status_221)); } @@ -5938,7 +5768,6 @@ int main(int argc, char const **argv) int process_status_222; __e_acsl_store_block((void *)(& process_status_222),(size_t)4); __gen_e_acsl_waitpid(pid_222,& process_status_222,0); - /*@ assert Eva: initialization: \initialized(&process_status_222); */ signal_eval(process_status_222,1,__gen_e_acsl_literal_string_277); __e_acsl_delete_block((void *)(& process_status_222)); } @@ -5953,7 +5782,6 @@ int main(int argc, char const **argv) int process_status_223; __e_acsl_store_block((void *)(& process_status_223),(size_t)4); __gen_e_acsl_waitpid(pid_223,& process_status_223,0); - /*@ assert Eva: initialization: \initialized(&process_status_223); */ signal_eval(process_status_223,0,__gen_e_acsl_literal_string_279); __e_acsl_delete_block((void *)(& process_status_223)); } @@ -5968,7 +5796,6 @@ int main(int argc, char const **argv) int process_status_224; __e_acsl_store_block((void *)(& process_status_224),(size_t)4); __gen_e_acsl_waitpid(pid_224,& process_status_224,0); - /*@ assert Eva: initialization: \initialized(&process_status_224); */ signal_eval(process_status_224,0,__gen_e_acsl_literal_string_280); __e_acsl_delete_block((void *)(& process_status_224)); } @@ -5983,7 +5810,6 @@ int main(int argc, char const **argv) int process_status_225; __e_acsl_store_block((void *)(& process_status_225),(size_t)4); __gen_e_acsl_waitpid(pid_225,& process_status_225,0); - /*@ assert Eva: initialization: \initialized(&process_status_225); */ signal_eval(process_status_225,0,__gen_e_acsl_literal_string_281); __e_acsl_delete_block((void *)(& process_status_225)); } @@ -5998,7 +5824,6 @@ int main(int argc, char const **argv) int process_status_226; __e_acsl_store_block((void *)(& process_status_226),(size_t)4); __gen_e_acsl_waitpid(pid_226,& process_status_226,0); - /*@ assert Eva: initialization: \initialized(&process_status_226); */ signal_eval(process_status_226,1,__gen_e_acsl_literal_string_282); __e_acsl_delete_block((void *)(& process_status_226)); } @@ -6013,7 +5838,6 @@ int main(int argc, char const **argv) int process_status_227; __e_acsl_store_block((void *)(& process_status_227),(size_t)4); __gen_e_acsl_waitpid(pid_227,& process_status_227,0); - /*@ assert Eva: initialization: \initialized(&process_status_227); */ signal_eval(process_status_227,1,__gen_e_acsl_literal_string_283); __e_acsl_delete_block((void *)(& process_status_227)); } @@ -6029,7 +5853,6 @@ int main(int argc, char const **argv) int process_status_228; __e_acsl_store_block((void *)(& process_status_228),(size_t)4); __gen_e_acsl_waitpid(pid_228,& process_status_228,0); - /*@ assert Eva: initialization: \initialized(&process_status_228); */ signal_eval(process_status_228,1,__gen_e_acsl_literal_string_284); __e_acsl_delete_block((void *)(& process_status_228)); } @@ -6044,7 +5867,6 @@ int main(int argc, char const **argv) int process_status_229; __e_acsl_store_block((void *)(& process_status_229),(size_t)4); __gen_e_acsl_waitpid(pid_229,& process_status_229,0); - /*@ assert Eva: initialization: \initialized(&process_status_229); */ signal_eval(process_status_229,1,__gen_e_acsl_literal_string_285); __e_acsl_delete_block((void *)(& process_status_229)); } @@ -6059,7 +5881,6 @@ int main(int argc, char const **argv) int process_status_230; __e_acsl_store_block((void *)(& process_status_230),(size_t)4); __gen_e_acsl_waitpid(pid_230,& process_status_230,0); - /*@ assert Eva: initialization: \initialized(&process_status_230); */ signal_eval(process_status_230,0,__gen_e_acsl_literal_string_287); __e_acsl_delete_block((void *)(& process_status_230)); } @@ -6074,7 +5895,6 @@ int main(int argc, char const **argv) int process_status_231; __e_acsl_store_block((void *)(& process_status_231),(size_t)4); __gen_e_acsl_waitpid(pid_231,& process_status_231,0); - /*@ assert Eva: initialization: \initialized(&process_status_231); */ signal_eval(process_status_231,1,__gen_e_acsl_literal_string_288); __e_acsl_delete_block((void *)(& process_status_231)); } @@ -6089,7 +5909,6 @@ int main(int argc, char const **argv) int process_status_232; __e_acsl_store_block((void *)(& process_status_232),(size_t)4); __gen_e_acsl_waitpid(pid_232,& process_status_232,0); - /*@ assert Eva: initialization: \initialized(&process_status_232); */ signal_eval(process_status_232,0,__gen_e_acsl_literal_string_290); __e_acsl_delete_block((void *)(& process_status_232)); } @@ -6104,7 +5923,6 @@ int main(int argc, char const **argv) int process_status_233; __e_acsl_store_block((void *)(& process_status_233),(size_t)4); __gen_e_acsl_waitpid(pid_233,& process_status_233,0); - /*@ assert Eva: initialization: \initialized(&process_status_233); */ signal_eval(process_status_233,0,__gen_e_acsl_literal_string_291); __e_acsl_delete_block((void *)(& process_status_233)); } @@ -6119,7 +5937,6 @@ int main(int argc, char const **argv) int process_status_234; __e_acsl_store_block((void *)(& process_status_234),(size_t)4); __gen_e_acsl_waitpid(pid_234,& process_status_234,0); - /*@ assert Eva: initialization: \initialized(&process_status_234); */ signal_eval(process_status_234,1,__gen_e_acsl_literal_string_292); __e_acsl_delete_block((void *)(& process_status_234)); } @@ -6134,7 +5951,6 @@ int main(int argc, char const **argv) int process_status_235; __e_acsl_store_block((void *)(& process_status_235),(size_t)4); __gen_e_acsl_waitpid(pid_235,& process_status_235,0); - /*@ assert Eva: initialization: \initialized(&process_status_235); */ signal_eval(process_status_235,1,__gen_e_acsl_literal_string_293); __e_acsl_delete_block((void *)(& process_status_235)); } @@ -6150,7 +5966,6 @@ int main(int argc, char const **argv) int process_status_236; __e_acsl_store_block((void *)(& process_status_236),(size_t)4); __gen_e_acsl_waitpid(pid_236,& process_status_236,0); - /*@ assert Eva: initialization: \initialized(&process_status_236); */ signal_eval(process_status_236,1,__gen_e_acsl_literal_string_294); __e_acsl_delete_block((void *)(& process_status_236)); } @@ -6158,7 +5973,6 @@ int main(int argc, char const **argv) { pid_t pid_237 = __gen_e_acsl_fork(); if (! pid_237) { - /*@ assert Eva: initialization: \initialized(&s2); */ __e_acsl_builtin_printf("s",__gen_e_acsl_literal_string_289,s2); __gen_e_acsl_exit(0); } @@ -6166,7 +5980,6 @@ int main(int argc, char const **argv) int process_status_237; __e_acsl_store_block((void *)(& process_status_237),(size_t)4); __gen_e_acsl_waitpid(pid_237,& process_status_237,0); - /*@ assert Eva: initialization: \initialized(&process_status_237); */ signal_eval(process_status_237,1,__gen_e_acsl_literal_string_295); __e_acsl_delete_block((void *)(& process_status_237)); } @@ -6182,7 +5995,6 @@ int main(int argc, char const **argv) int process_status_238; __e_acsl_store_block((void *)(& process_status_238),(size_t)4); __gen_e_acsl_waitpid(pid_238,& process_status_238,0); - /*@ assert Eva: initialization: \initialized(&process_status_238); */ signal_eval(process_status_238,0,__gen_e_acsl_literal_string_296); __e_acsl_delete_block((void *)(& process_status_238)); } @@ -6198,7 +6010,6 @@ int main(int argc, char const **argv) int process_status_239; __e_acsl_store_block((void *)(& process_status_239),(size_t)4); __gen_e_acsl_waitpid(pid_239,& process_status_239,0); - /*@ assert Eva: initialization: \initialized(&process_status_239); */ signal_eval(process_status_239,1,__gen_e_acsl_literal_string_297); __e_acsl_delete_block((void *)(& process_status_239)); } @@ -6213,7 +6024,6 @@ int main(int argc, char const **argv) int process_status_240; __e_acsl_store_block((void *)(& process_status_240),(size_t)4); __gen_e_acsl_waitpid(pid_240,& process_status_240,0); - /*@ assert Eva: initialization: \initialized(&process_status_240); */ signal_eval(process_status_240,0,__gen_e_acsl_literal_string_299); __e_acsl_delete_block((void *)(& process_status_240)); } @@ -6228,7 +6038,6 @@ int main(int argc, char const **argv) int process_status_241; __e_acsl_store_block((void *)(& process_status_241),(size_t)4); __gen_e_acsl_waitpid(pid_241,& process_status_241,0); - /*@ assert Eva: initialization: \initialized(&process_status_241); */ signal_eval(process_status_241,0,__gen_e_acsl_literal_string_301); __e_acsl_delete_block((void *)(& process_status_241)); } @@ -6243,7 +6052,6 @@ int main(int argc, char const **argv) int process_status_242; __e_acsl_store_block((void *)(& process_status_242),(size_t)4); __gen_e_acsl_waitpid(pid_242,& process_status_242,0); - /*@ assert Eva: initialization: \initialized(&process_status_242); */ signal_eval(process_status_242,0,__gen_e_acsl_literal_string_303); __e_acsl_delete_block((void *)(& process_status_242)); } @@ -6258,7 +6066,6 @@ int main(int argc, char const **argv) int process_status_243; __e_acsl_store_block((void *)(& process_status_243),(size_t)4); __gen_e_acsl_waitpid(pid_243,& process_status_243,0); - /*@ assert Eva: initialization: \initialized(&process_status_243); */ signal_eval(process_status_243,0,__gen_e_acsl_literal_string_305); __e_acsl_delete_block((void *)(& process_status_243)); } @@ -6273,7 +6080,6 @@ int main(int argc, char const **argv) int process_status_244; __e_acsl_store_block((void *)(& process_status_244),(size_t)4); __gen_e_acsl_waitpid(pid_244,& process_status_244,0); - /*@ assert Eva: initialization: \initialized(&process_status_244); */ signal_eval(process_status_244,1,__gen_e_acsl_literal_string_307); __e_acsl_delete_block((void *)(& process_status_244)); } @@ -6288,7 +6094,6 @@ int main(int argc, char const **argv) int process_status_245; __e_acsl_store_block((void *)(& process_status_245),(size_t)4); __gen_e_acsl_waitpid(pid_245,& process_status_245,0); - /*@ assert Eva: initialization: \initialized(&process_status_245); */ signal_eval(process_status_245,0,__gen_e_acsl_literal_string_309); __e_acsl_delete_block((void *)(& process_status_245)); } @@ -6303,7 +6108,6 @@ int main(int argc, char const **argv) int process_status_246; __e_acsl_store_block((void *)(& process_status_246),(size_t)4); __gen_e_acsl_waitpid(pid_246,& process_status_246,0); - /*@ assert Eva: initialization: \initialized(&process_status_246); */ signal_eval(process_status_246,1,__gen_e_acsl_literal_string_310); __e_acsl_delete_block((void *)(& process_status_246)); } @@ -6318,7 +6122,6 @@ int main(int argc, char const **argv) int process_status_247; __e_acsl_store_block((void *)(& process_status_247),(size_t)4); __gen_e_acsl_waitpid(pid_247,& process_status_247,0); - /*@ assert Eva: initialization: \initialized(&process_status_247); */ signal_eval(process_status_247,1,__gen_e_acsl_literal_string_311); __e_acsl_delete_block((void *)(& process_status_247)); } @@ -6333,7 +6136,6 @@ int main(int argc, char const **argv) int process_status_248; __e_acsl_store_block((void *)(& process_status_248),(size_t)4); __gen_e_acsl_waitpid(pid_248,& process_status_248,0); - /*@ assert Eva: initialization: \initialized(&process_status_248); */ signal_eval(process_status_248,0,__gen_e_acsl_literal_string_313); __e_acsl_delete_block((void *)(& process_status_248)); } @@ -6348,7 +6150,6 @@ int main(int argc, char const **argv) int process_status_249; __e_acsl_store_block((void *)(& process_status_249),(size_t)4); __gen_e_acsl_waitpid(pid_249,& process_status_249,0); - /*@ assert Eva: initialization: \initialized(&process_status_249); */ signal_eval(process_status_249,1,__gen_e_acsl_literal_string_314); __e_acsl_delete_block((void *)(& process_status_249)); } @@ -6363,7 +6164,6 @@ int main(int argc, char const **argv) int process_status_250; __e_acsl_store_block((void *)(& process_status_250),(size_t)4); __gen_e_acsl_waitpid(pid_250,& process_status_250,0); - /*@ assert Eva: initialization: \initialized(&process_status_250); */ signal_eval(process_status_250,1,__gen_e_acsl_literal_string_315); __e_acsl_delete_block((void *)(& process_status_250)); } @@ -6379,7 +6179,6 @@ int main(int argc, char const **argv) int process_status_251; __e_acsl_store_block((void *)(& process_status_251),(size_t)4); __gen_e_acsl_waitpid(pid_251,& process_status_251,0); - /*@ assert Eva: initialization: \initialized(&process_status_251); */ signal_eval(process_status_251,1,__gen_e_acsl_literal_string_316); __e_acsl_delete_block((void *)(& process_status_251)); } @@ -6394,7 +6193,6 @@ int main(int argc, char const **argv) int process_status_252; __e_acsl_store_block((void *)(& process_status_252),(size_t)4); __gen_e_acsl_waitpid(pid_252,& process_status_252,0); - /*@ assert Eva: initialization: \initialized(&process_status_252); */ signal_eval(process_status_252,1,__gen_e_acsl_literal_string_318); __e_acsl_delete_block((void *)(& process_status_252)); } @@ -6409,7 +6207,6 @@ int main(int argc, char const **argv) int process_status_253; __e_acsl_store_block((void *)(& process_status_253),(size_t)4); __gen_e_acsl_waitpid(pid_253,& process_status_253,0); - /*@ assert Eva: initialization: \initialized(&process_status_253); */ signal_eval(process_status_253,1,__gen_e_acsl_literal_string_320); __e_acsl_delete_block((void *)(& process_status_253)); } @@ -6424,7 +6221,6 @@ int main(int argc, char const **argv) int process_status_254; __e_acsl_store_block((void *)(& process_status_254),(size_t)4); __gen_e_acsl_waitpid(pid_254,& process_status_254,0); - /*@ assert Eva: initialization: \initialized(&process_status_254); */ signal_eval(process_status_254,1,__gen_e_acsl_literal_string_322); __e_acsl_delete_block((void *)(& process_status_254)); } @@ -6439,7 +6235,6 @@ int main(int argc, char const **argv) int process_status_255; __e_acsl_store_block((void *)(& process_status_255),(size_t)4); __gen_e_acsl_waitpid(pid_255,& process_status_255,0); - /*@ assert Eva: initialization: \initialized(&process_status_255); */ signal_eval(process_status_255,1,__gen_e_acsl_literal_string_324); __e_acsl_delete_block((void *)(& process_status_255)); } @@ -6454,7 +6249,6 @@ int main(int argc, char const **argv) int process_status_256; __e_acsl_store_block((void *)(& process_status_256),(size_t)4); __gen_e_acsl_waitpid(pid_256,& process_status_256,0); - /*@ assert Eva: initialization: \initialized(&process_status_256); */ signal_eval(process_status_256,1,__gen_e_acsl_literal_string_326); __e_acsl_delete_block((void *)(& process_status_256)); } @@ -6469,7 +6263,6 @@ int main(int argc, char const **argv) int process_status_257; __e_acsl_store_block((void *)(& process_status_257),(size_t)4); __gen_e_acsl_waitpid(pid_257,& process_status_257,0); - /*@ assert Eva: initialization: \initialized(&process_status_257); */ signal_eval(process_status_257,1,__gen_e_acsl_literal_string_328); __e_acsl_delete_block((void *)(& process_status_257)); } @@ -6484,7 +6277,6 @@ int main(int argc, char const **argv) int process_status_258; __e_acsl_store_block((void *)(& process_status_258),(size_t)4); __gen_e_acsl_waitpid(pid_258,& process_status_258,0); - /*@ assert Eva: initialization: \initialized(&process_status_258); */ signal_eval(process_status_258,1,__gen_e_acsl_literal_string_330); __e_acsl_delete_block((void *)(& process_status_258)); } @@ -6499,7 +6291,6 @@ int main(int argc, char const **argv) int process_status_259; __e_acsl_store_block((void *)(& process_status_259),(size_t)4); __gen_e_acsl_waitpid(pid_259,& process_status_259,0); - /*@ assert Eva: initialization: \initialized(&process_status_259); */ signal_eval(process_status_259,1,__gen_e_acsl_literal_string_332); __e_acsl_delete_block((void *)(& process_status_259)); } @@ -6514,7 +6305,6 @@ int main(int argc, char const **argv) int process_status_260; __e_acsl_store_block((void *)(& process_status_260),(size_t)4); __gen_e_acsl_waitpid(pid_260,& process_status_260,0); - /*@ assert Eva: initialization: \initialized(&process_status_260); */ signal_eval(process_status_260,1,__gen_e_acsl_literal_string_333); __e_acsl_delete_block((void *)(& process_status_260)); } @@ -6529,7 +6319,6 @@ int main(int argc, char const **argv) int process_status_261; __e_acsl_store_block((void *)(& process_status_261),(size_t)4); __gen_e_acsl_waitpid(pid_261,& process_status_261,0); - /*@ assert Eva: initialization: \initialized(&process_status_261); */ signal_eval(process_status_261,1,__gen_e_acsl_literal_string_335); __e_acsl_delete_block((void *)(& process_status_261)); } @@ -6544,7 +6333,6 @@ int main(int argc, char const **argv) int process_status_262; __e_acsl_store_block((void *)(& process_status_262),(size_t)4); __gen_e_acsl_waitpid(pid_262,& process_status_262,0); - /*@ assert Eva: initialization: \initialized(&process_status_262); */ signal_eval(process_status_262,1,__gen_e_acsl_literal_string_337); __e_acsl_delete_block((void *)(& process_status_262)); } diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle index 61b4cbef62c5fb1201aee5ba31e520cc5c13c490..7e9dbd5e9e4cc0ccf159e9c4c9bdbb7ba25a2110 100644 --- a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle @@ -25,12 +25,15 @@ if there are memory-related annotations. [e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:92: Warning: +[e-acsl] FRAMAC_SHARE/libc/sys/wait.h:79: 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/unistd.h:854: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. @@ -40,24 +43,39 @@ Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:351: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:357: Warning: E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: + E-ACSL construct `user-defined logic type' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/string.h:167: Warning: + E-ACSL construct `user-defined logic type' is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:171: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning: + Some assumes clauses couldn't be translated. + Ignoring complete and disjoint behaviors annotations. +[e-acsl] FRAMAC_SHARE/libc/string.h:157: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: - E-ACSL construct `user-defined logic type' is not yet supported. +[e-acsl] FRAMAC_SHARE/libc/string.h:163: Warning: + E-ACSL construct `logic functions performing read accesses' + is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:167: Warning: - E-ACSL construct `user-defined logic type' is not yet supported. +[e-acsl] FRAMAC_SHARE/libc/string.h:164: Warning: + E-ACSL construct `logic functions with labels' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/string.h:165: Warning: + invalid E-ACSL construct + `non integer variable p in quantification + found: ∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c)'. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:125: Warning: E-ACSL construct `logic functions with labels' is not yet supported. @@ -69,17 +87,17 @@ E-ACSL construct `logic functions performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:127: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:470: 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] FRAMAC_SHARE/libc/stdlib.h:472: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:473: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:457: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:473: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:459: Warning: E-ACSL construct `abnormal termination case in behavior' is not yet supported. Ignoring annotation. @@ -90,565 +108,3 @@ function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown. [kernel:annot:missing-spec] tests/format/printf.c:180: Warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype -[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/format/printf.c:180: Warning: - accessing uninitialized left-value. assert \initialized(&process_status); -[kernel:annot:missing-spec] tests/format/signalled.h:17: Warning: - Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype -[eva:alarm] tests/format/printf.c:183: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_0); -[eva:alarm] tests/format/printf.c:186: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_1); -[eva:alarm] tests/format/printf.c:189: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_2); -[eva:alarm] tests/format/printf.c:194: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_3); -[eva:alarm] tests/format/printf.c:197: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_4); -[eva:alarm] tests/format/printf.c:199: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_5); -[eva:alarm] tests/format/printf.c:201: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_6); -[eva:alarm] tests/format/printf.c:204: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_7); -[eva:alarm] tests/format/printf.c:206: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_8); -[eva:alarm] tests/format/printf.c:51: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/string.h:357: Warning: - function __gen_e_acsl_strcpy: postcondition 'equal_contents' got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/string.h:165: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_first_occur' got status unknown. -[eva:alarm] tests/format/printf.c:59: Warning: - accessing uninitialized left-value. assert \initialized(&process_status); -[eva:alarm] FRAMAC_SHARE/libc/string.h:161: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_char' got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/string.h:161: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_char' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] FRAMAC_SHARE/libc/string.h:162: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_same_base' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] FRAMAC_SHARE/libc/string.h:163: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_in_length' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] FRAMAC_SHARE/libc/string.h:164: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_valid_string' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] FRAMAC_SHARE/libc/string.h:165: Warning: - function __gen_e_acsl_strchr, behavior found: postcondition 'result_first_occur' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] FRAMAC_SHARE/libc/string.h:168: Warning: - function __gen_e_acsl_strchr, behavior not_found: postcondition 'result_null' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] tests/format/printf.c:62: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_0); -[eva:alarm] tests/format/signalled.h:17: Warning: - signed overflow. assert testno + 1 ≤ 2147483647; -[eva:alarm] tests/format/printf.c:224: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_9); -[eva:alarm] tests/format/printf.c:225: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_10); -[eva:alarm] tests/format/printf.c:226: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_11); -[eva:alarm] tests/format/printf.c:233: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_12); -[eva:alarm] tests/format/printf.c:233: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_13); -[eva:alarm] tests/format/printf.c:234: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_14); -[eva:alarm] tests/format/printf.c:234: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_15); -[eva:alarm] tests/format/printf.c:235: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_16); -[eva:alarm] tests/format/printf.c:235: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_17); -[eva:alarm] tests/format/printf.c:235: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_18); -[eva:alarm] tests/format/printf.c:239: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_19); -[eva:alarm] tests/format/printf.c:239: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_20); -[eva:alarm] tests/format/printf.c:240: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_21); -[eva:alarm] tests/format/printf.c:240: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_22); -[eva:alarm] tests/format/printf.c:241: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_23); -[eva:alarm] tests/format/printf.c:241: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_24); -[eva:alarm] tests/format/printf.c:241: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_25); -[eva:alarm] tests/format/printf.c:245: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_26); -[eva:alarm] tests/format/printf.c:245: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_27); -[eva:alarm] tests/format/printf.c:246: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_28); -[eva:alarm] tests/format/printf.c:246: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_29); -[eva:alarm] tests/format/printf.c:247: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_30); -[eva:alarm] tests/format/printf.c:247: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_31); -[eva:alarm] tests/format/printf.c:249: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_32); -[eva:alarm] tests/format/printf.c:249: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_33); -[eva:alarm] tests/format/printf.c:250: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_34); -[eva:alarm] tests/format/printf.c:250: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_35); -[eva:alarm] tests/format/printf.c:251: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_36); -[eva:alarm] tests/format/printf.c:251: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_37); -[eva:alarm] tests/format/printf.c:252: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_38); -[eva:alarm] tests/format/printf.c:252: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_39); -[eva:alarm] tests/format/printf.c:254: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_40); -[eva:alarm] tests/format/printf.c:257: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_41); -[eva:alarm] tests/format/printf.c:261: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_42); -[eva:alarm] tests/format/printf.c:261: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_43); -[eva:alarm] tests/format/printf.c:262: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_44); -[eva:alarm] tests/format/printf.c:262: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_45); -[eva:alarm] tests/format/printf.c:263: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_46); -[eva:alarm] tests/format/printf.c:263: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_47); -[eva:alarm] tests/format/printf.c:263: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_48); -[eva:alarm] tests/format/printf.c:267: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_49); -[eva:alarm] tests/format/printf.c:267: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_50); -[eva:alarm] tests/format/printf.c:268: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_51); -[eva:alarm] tests/format/printf.c:268: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_52); -[eva:alarm] tests/format/printf.c:269: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_53); -[eva:alarm] tests/format/printf.c:269: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_54); -[eva:alarm] tests/format/printf.c:269: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_55); -[eva:alarm] tests/format/printf.c:277: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_56); -[eva:alarm] tests/format/printf.c:277: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_57); -[eva:alarm] tests/format/printf.c:281: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_58); -[eva:alarm] tests/format/printf.c:281: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_59); -[eva:alarm] tests/format/printf.c:282: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_60); -[eva:alarm] tests/format/printf.c:282: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_61); -[eva:alarm] tests/format/printf.c:282: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_62); -[eva:alarm] tests/format/printf.c:289: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_63); -[eva:alarm] tests/format/printf.c:289: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_64); -[eva:alarm] tests/format/printf.c:290: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_65); -[eva:alarm] tests/format/printf.c:290: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_66); -[eva:alarm] tests/format/printf.c:295: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_67); -[eva:alarm] tests/format/printf.c:295: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_68); -[eva:alarm] tests/format/printf.c:296: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_69); -[eva:alarm] tests/format/printf.c:300: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_70); -[eva:alarm] tests/format/printf.c:300: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_71); -[eva:alarm] tests/format/printf.c:301: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_72); -[eva:alarm] tests/format/printf.c:301: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_73); -[eva:alarm] tests/format/printf.c:302: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_74); -[eva:alarm] tests/format/printf.c:302: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_75); -[eva:alarm] tests/format/printf.c:303: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_76); -[eva:alarm] tests/format/printf.c:303: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_77); -[eva:alarm] tests/format/printf.c:307: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_78); -[eva:alarm] tests/format/printf.c:308: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_79); -[eva:alarm] tests/format/printf.c:309: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_80); -[eva:alarm] tests/format/printf.c:312: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_81); -[eva:alarm] tests/format/printf.c:312: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_82); -[eva:alarm] tests/format/printf.c:313: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_83); -[eva:alarm] tests/format/printf.c:313: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_84); -[eva:alarm] tests/format/printf.c:314: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_85); -[eva:alarm] tests/format/printf.c:314: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_86); -[eva:alarm] tests/format/printf.c:315: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_87); -[eva:alarm] tests/format/printf.c:315: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_88); -[eva:alarm] tests/format/printf.c:316: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_89); -[eva:alarm] tests/format/printf.c:316: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_90); -[eva:alarm] tests/format/printf.c:317: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_91); -[eva:alarm] tests/format/printf.c:317: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_92); -[eva:alarm] tests/format/printf.c:318: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_93); -[eva:alarm] tests/format/printf.c:318: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_94); -[eva:alarm] tests/format/printf.c:321: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_95); -[eva:alarm] tests/format/printf.c:321: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_96); -[eva:alarm] tests/format/printf.c:322: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_97); -[eva:alarm] tests/format/printf.c:322: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_98); -[eva:alarm] tests/format/printf.c:323: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_99); -[eva:alarm] tests/format/printf.c:323: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_100); -[eva:alarm] tests/format/printf.c:324: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_101); -[eva:alarm] tests/format/printf.c:324: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_102); -[eva:alarm] tests/format/printf.c:326: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_103); -[eva:alarm] tests/format/printf.c:326: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_104); -[eva:alarm] tests/format/printf.c:330: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_105); -[eva:alarm] tests/format/printf.c:330: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_106); -[eva:alarm] tests/format/printf.c:333: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_107); -[eva:alarm] tests/format/printf.c:333: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_108); -[eva:alarm] tests/format/printf.c:333: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_109); -[eva:alarm] tests/format/printf.c:333: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_110); -[eva:alarm] tests/format/printf.c:334: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_111); -[eva:alarm] tests/format/printf.c:334: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_112); -[eva:alarm] tests/format/printf.c:334: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_113); -[eva:alarm] tests/format/printf.c:334: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_114); -[eva:alarm] tests/format/printf.c:335: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_115); -[eva:alarm] tests/format/printf.c:335: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_116); -[eva:alarm] tests/format/printf.c:335: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_117); -[eva:alarm] tests/format/printf.c:335: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_118); -[eva:alarm] tests/format/printf.c:336: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_119); -[eva:alarm] tests/format/printf.c:336: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_120); -[eva:alarm] tests/format/printf.c:336: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_121); -[eva:alarm] tests/format/printf.c:336: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_122); -[eva:alarm] tests/format/printf.c:337: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_123); -[eva:alarm] tests/format/printf.c:337: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_124); -[eva:alarm] tests/format/printf.c:337: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_125); -[eva:alarm] tests/format/printf.c:337: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_126); -[eva:alarm] tests/format/printf.c:338: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_127); -[eva:alarm] tests/format/printf.c:338: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_128); -[eva:alarm] tests/format/printf.c:338: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_129); -[eva:alarm] tests/format/printf.c:338: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_130); -[eva:alarm] tests/format/printf.c:341: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_131); -[eva:alarm] tests/format/printf.c:341: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_132); -[eva:alarm] tests/format/printf.c:341: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_133); -[eva:alarm] tests/format/printf.c:341: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_134); -[eva:alarm] tests/format/printf.c:342: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_135); -[eva:alarm] tests/format/printf.c:342: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_136); -[eva:alarm] tests/format/printf.c:342: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_137); -[eva:alarm] tests/format/printf.c:342: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_138); -[eva:alarm] tests/format/printf.c:344: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_139); -[eva:alarm] tests/format/printf.c:344: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_140); -[eva:alarm] tests/format/printf.c:344: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_141); -[eva:alarm] tests/format/printf.c:344: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_142); -[eva:alarm] tests/format/printf.c:346: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_143); -[eva:alarm] tests/format/printf.c:346: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_144); -[eva:alarm] tests/format/printf.c:346: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_145); -[eva:alarm] tests/format/printf.c:346: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_146); -[eva:alarm] tests/format/printf.c:347: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_147); -[eva:alarm] tests/format/printf.c:347: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_148); -[eva:alarm] tests/format/printf.c:347: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_149); -[eva:alarm] tests/format/printf.c:347: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_150); -[eva:alarm] tests/format/printf.c:348: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_151); -[eva:alarm] tests/format/printf.c:348: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_152); -[eva:alarm] tests/format/printf.c:348: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_153); -[eva:alarm] tests/format/printf.c:348: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_154); -[eva:alarm] tests/format/printf.c:350: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_155); -[eva:alarm] tests/format/printf.c:350: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_156); -[eva:alarm] tests/format/printf.c:350: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_157); -[eva:alarm] tests/format/printf.c:350: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_158); -[eva:alarm] tests/format/printf.c:354: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_159); -[eva:alarm] tests/format/printf.c:354: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_160); -[eva:alarm] tests/format/printf.c:355: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_161); -[eva:alarm] tests/format/printf.c:355: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_162); -[eva:alarm] tests/format/printf.c:356: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_163); -[eva:alarm] tests/format/printf.c:356: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_164); -[eva:alarm] tests/format/printf.c:357: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_165); -[eva:alarm] tests/format/printf.c:357: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_166); -[eva:alarm] tests/format/printf.c:358: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_167); -[eva:alarm] tests/format/printf.c:358: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_168); -[eva:alarm] tests/format/printf.c:359: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_169); -[eva:alarm] tests/format/printf.c:359: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_170); -[eva:alarm] tests/format/printf.c:360: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_171); -[eva:alarm] tests/format/printf.c:360: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_172); -[eva:alarm] tests/format/printf.c:361: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_173); -[eva:alarm] tests/format/printf.c:361: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_174); -[eva:alarm] tests/format/printf.c:362: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_175); -[eva:alarm] tests/format/printf.c:362: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_176); -[eva:alarm] tests/format/printf.c:363: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_177); -[eva:alarm] tests/format/printf.c:363: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_178); -[eva:alarm] tests/format/printf.c:364: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_179); -[eva:alarm] tests/format/printf.c:364: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_180); -[eva:alarm] tests/format/printf.c:365: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_181); -[eva:alarm] tests/format/printf.c:365: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_182); -[eva:alarm] tests/format/printf.c:366: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_183); -[eva:alarm] tests/format/printf.c:366: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_184); -[eva:alarm] tests/format/printf.c:367: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_185); -[eva:alarm] tests/format/printf.c:367: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_186); -[eva:alarm] tests/format/printf.c:368: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_187); -[eva:alarm] tests/format/printf.c:368: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_188); -[eva:alarm] tests/format/printf.c:369: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_189); -[eva:alarm] tests/format/printf.c:369: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_190); -[eva:alarm] tests/format/printf.c:372: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_191); -[eva:alarm] tests/format/printf.c:372: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_192); -[eva:alarm] tests/format/printf.c:373: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_193); -[eva:alarm] tests/format/printf.c:373: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_194); -[eva:alarm] tests/format/printf.c:374: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_195); -[eva:alarm] tests/format/printf.c:374: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_196); -[eva:alarm] tests/format/printf.c:375: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_197); -[eva:alarm] tests/format/printf.c:375: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_198); -[eva:alarm] tests/format/printf.c:376: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_199); -[eva:alarm] tests/format/printf.c:376: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_200); -[eva:alarm] tests/format/printf.c:377: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_201); -[eva:alarm] tests/format/printf.c:377: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_202); -[eva:alarm] tests/format/printf.c:378: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_203); -[eva:alarm] tests/format/printf.c:378: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_204); -[eva:alarm] tests/format/printf.c:379: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_205); -[eva:alarm] tests/format/printf.c:379: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_206); -[eva:alarm] tests/format/printf.c:380: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_207); -[eva:alarm] tests/format/printf.c:380: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_208); -[eva:alarm] tests/format/printf.c:381: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_209); -[eva:alarm] tests/format/printf.c:381: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_210); -[eva:alarm] tests/format/printf.c:382: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_211); -[eva:alarm] tests/format/printf.c:382: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_212); -[eva:alarm] tests/format/printf.c:383: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_213); -[eva:alarm] tests/format/printf.c:383: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_214); -[eva:alarm] tests/format/printf.c:384: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_215); -[eva:alarm] tests/format/printf.c:384: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_216); -[eva:alarm] tests/format/printf.c:385: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_217); -[eva:alarm] tests/format/printf.c:385: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_218); -[eva:alarm] tests/format/printf.c:386: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_219); -[eva:alarm] tests/format/printf.c:386: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_220); -[eva:alarm] tests/format/printf.c:387: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_221); -[eva:alarm] tests/format/printf.c:387: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_222); -[eva:alarm] tests/format/printf.c:390: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_223); -[eva:alarm] tests/format/printf.c:391: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_224); -[eva:alarm] tests/format/printf.c:392: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_225); -[eva:alarm] tests/format/printf.c:393: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_226); -[eva:alarm] tests/format/printf.c:394: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_227); -[eva:alarm] tests/format/printf.c:395: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_228); -[eva:alarm] tests/format/printf.c:396: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_229); -[eva:alarm] tests/format/printf.c:399: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_230); -[eva:alarm] tests/format/printf.c:400: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_231); -[eva:alarm] tests/format/printf.c:407: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_232); -[eva:alarm] tests/format/printf.c:408: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_233); -[eva:alarm] tests/format/printf.c:409: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_234); -[eva:alarm] tests/format/printf.c:410: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_235); -[eva:alarm] tests/format/printf.c:415: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_236); -[eva:alarm] tests/format/printf.c:416: Warning: - accessing uninitialized left-value. assert \initialized(&s2); -[eva:alarm] tests/format/printf.c:416: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_237); -[eva:alarm] tests/format/printf.c:419: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_238); -[eva:alarm] tests/format/printf.c:421: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_239); -[eva:alarm] tests/format/printf.c:424: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_240); -[eva:alarm] tests/format/printf.c:425: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_241); -[eva:alarm] tests/format/printf.c:426: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_242); -[eva:alarm] tests/format/printf.c:427: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_243); -[eva:alarm] tests/format/printf.c:428: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_244); -[eva:alarm] tests/format/printf.c:453: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_245); -[eva:alarm] tests/format/printf.c:454: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_246); -[eva:alarm] tests/format/printf.c:455: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_247); -[eva:alarm] tests/format/printf.c:458: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_248); -[eva:alarm] tests/format/printf.c:459: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_249); -[eva:alarm] tests/format/printf.c:460: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_250); -[eva:alarm] tests/format/printf.c:461: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_251); -[eva:alarm] tests/format/printf.c:464: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_252); -[eva:alarm] tests/format/printf.c:465: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_253); -[eva:alarm] tests/format/printf.c:466: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_254); -[eva:alarm] tests/format/printf.c:467: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_255); -[eva:alarm] tests/format/printf.c:468: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_256); -[eva:alarm] tests/format/printf.c:469: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_257); -[eva:alarm] tests/format/printf.c:470: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_258); -[eva:alarm] tests/format/printf.c:471: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_259); -[eva:alarm] tests/format/printf.c:472: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_260); -[eva:alarm] tests/format/printf.c:473: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_261); -[eva:alarm] tests/format/printf.c:476: Warning: - accessing uninitialized left-value. assert \initialized(&process_status_262); diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle index 270dcdb0d84448a3889a178d504aa1b53f9de220..bdd131d8e73293fe5368b6c090950b25c70897d4 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle @@ -2,22 +2,9 @@ [e-acsl] Warning: annotating undefined function `isupper': the generated program may miss memory instrumentation if there are memory-related annotations. -[e-acsl] tests/memory/ctype_macros.c:39: Warning: - E-ACSL construct `disjoint behaviors' is not yet supported. - Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/ctype.h:174: Warning: +[e-acsl] FRAMAC_SHARE/libc/ctype.h:173: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". [eva:alarm] tests/memory/ctype_macros.c:37: Warning: function __gen_e_acsl_isupper: precondition 'c_uchar_or_eof' got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/ctype.h:174: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/ctype.h:178: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/ctype.h:181: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva:alarm] FRAMAC_SHARE/libc/ctype.h:178: Warning: - function __gen_e_acsl_isupper, behavior definitely_match: postcondition 'nonzero_result' got status unknown. (Behavior may be inactive, no reduction performed.) -[eva:alarm] FRAMAC_SHARE/libc/ctype.h:181: Warning: - function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition 'zero_result' got status unknown. (Behavior may be inactive, no reduction performed.) diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c index 2a3a6d2b1575bed6649e16d34d73779167cac8dc..cbf17bff568232f8b793732e40a59e0997ce068c 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c @@ -73,60 +73,66 @@ int main(int argc, char const **argv) */ int __gen_e_acsl_isupper(int c) { - int __gen_e_acsl_at_2; - int __gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; int __retres; { int __gen_e_acsl_and; int __gen_e_acsl_or; - if (0 <= c) __gen_e_acsl_and = c <= 255; else __gen_e_acsl_and = 0; - if (__gen_e_acsl_and) __gen_e_acsl_or = 1; - else __gen_e_acsl_or = c == -1; - __e_acsl_assert(__gen_e_acsl_or,"Precondition","isupper", - "(0 <= c <= 255) || c == -1","FRAMAC_SHARE/libc/ctype.h", - 174); - } - { + int __gen_e_acsl_or_2; + int __gen_e_acsl_and_4; int __gen_e_acsl_or_3; - int __gen_e_acsl_or_4; - if (c == -1) __gen_e_acsl_or_3 = 1; + int __gen_e_acsl_active_bhvrs; + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + if (65 <= c) __gen_e_acsl_and = c <= 90; else __gen_e_acsl_and = 0; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + __gen_e_acsl_and); + if (c == -1) __gen_e_acsl_or = 1; else { - int __gen_e_acsl_and_3; - if (0 <= c) __gen_e_acsl_and_3 = c < 65; else __gen_e_acsl_and_3 = 0; - __gen_e_acsl_or_3 = __gen_e_acsl_and_3; + int __gen_e_acsl_and_2; + if (0 <= c) __gen_e_acsl_and_2 = c < 65; else __gen_e_acsl_and_2 = 0; + __gen_e_acsl_or = __gen_e_acsl_and_2; } - if (__gen_e_acsl_or_3) __gen_e_acsl_or_4 = 1; + if (__gen_e_acsl_or) __gen_e_acsl_or_2 = 1; else { - int __gen_e_acsl_and_4; - if (90 < c) __gen_e_acsl_and_4 = c <= 127; else __gen_e_acsl_and_4 = 0; - __gen_e_acsl_or_4 = __gen_e_acsl_and_4; + int __gen_e_acsl_and_3; + if (90 < c) __gen_e_acsl_and_3 = c <= 127; else __gen_e_acsl_and_3 = 0; + __gen_e_acsl_or_2 = __gen_e_acsl_and_3; } - __gen_e_acsl_at_2 = __gen_e_acsl_or_4; - } - { - int __gen_e_acsl_and_2; - if (65 <= c) __gen_e_acsl_and_2 = c <= 90; else __gen_e_acsl_and_2 = 0; - __gen_e_acsl_at = __gen_e_acsl_and_2; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + __gen_e_acsl_or_2); + if (0 <= c) __gen_e_acsl_and_4 = c <= 255; else __gen_e_acsl_and_4 = 0; + if (__gen_e_acsl_and_4) __gen_e_acsl_or_3 = 1; + else __gen_e_acsl_or_3 = c == -1; + __e_acsl_assert(__gen_e_acsl_or_3,"Precondition","isupper", + "(0 <= c <= 255) || c == -1","FRAMAC_SHARE/libc/ctype.h", + 174); + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract); + __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,"Precondition","isupper", + "all behaviors disjoint","FRAMAC_SHARE/libc/ctype.h",173); } __retres = isupper(c); { - int __gen_e_acsl_implies; - int __gen_e_acsl_implies_2; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else { - int __gen_e_acsl_or_2; - if (__retres < 0) __gen_e_acsl_or_2 = 1; - else __gen_e_acsl_or_2 = __retres > 0; - __gen_e_acsl_implies = __gen_e_acsl_or_2; + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_or_4; + if (__retres < 0) __gen_e_acsl_or_4 = 1; + else __gen_e_acsl_or_4 = __retres > 0; + __e_acsl_assert(__gen_e_acsl_or_4,"Postcondition","isupper", + "definitely_match: \\result < 0 || \\result > 0", + "FRAMAC_SHARE/libc/ctype.h",178); } - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","isupper", - "\\old(\'A\' <= c <= \'Z\') ==> \\result < 0 || \\result > 0", - "FRAMAC_SHARE/libc/ctype.h",178); - if (! __gen_e_acsl_at_2) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = __retres == 0; - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","isupper", - "\\old(c == -1 || (0 <= c < \'A\') || (\'Z\' < c <= 127)) ==> \\result == 0", - "FRAMAC_SHARE/libc/ctype.h",181); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == 0, + "Postcondition", + "isupper", + "definitely_not_match: \\result == 0", + "FRAMAC_SHARE/libc/ctype.h", + 181); + __e_acsl_contract_clean(__gen_e_acsl_contract); return __retres; } } diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c index 53c57ee917932634a7b3679989189b5acb02a2ca..594eb809025228428f8d77a55c247c7157cab650 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c @@ -54,7 +54,6 @@ int main(int argc, char const **argv) int res2 = __gen_e_acsl_posix_memalign((void **)memptr,(unsigned long)256, (unsigned long)15); - /*@ assert Eva: initialization: \initialized(memptr); */ char *p = *memptr; __e_acsl_store_block((void *)(& p),(size_t)8); __e_acsl_full_init((void *)(& p)); @@ -216,11 +215,13 @@ int main(int argc, char const **argv) */ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size) { + __e_acsl_contract_t *__gen_e_acsl_contract; int __retres; { int __gen_e_acsl_valid; int __gen_e_acsl_and; __e_acsl_store_block((void *)(& memptr),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); __gen_e_acsl_valid = __e_acsl_valid((void *)memptr,sizeof(void *), (void *)memptr,(void *)(& memptr)); __e_acsl_assert(__gen_e_acsl_valid,"Precondition","posix_memalign", @@ -254,8 +255,30 @@ int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size) "FRAMAC_SHARE/libc/stdlib.h",668); } __retres = posix_memalign(memptr,alignment,size); - __e_acsl_delete_block((void *)(& memptr)); - return __retres; + { + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == 0, + "Postcondition", + "posix_memalign", + "allocation: \\result == 0", + "FRAMAC_SHARE/libc/stdlib.h", + 680); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_or; + if (__retres < 0) __gen_e_acsl_or = 1; + else __gen_e_acsl_or = __retres > 0; + __e_acsl_assert(__gen_e_acsl_or,"Postcondition","posix_memalign", + "no_allocation: \\result < 0 || \\result > 0", + "FRAMAC_SHARE/libc/stdlib.h",685); + } + __e_acsl_contract_clean(__gen_e_acsl_contract); + __e_acsl_delete_block((void *)(& memptr)); + return __retres; + } } diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c index 384a5a75de5fb66faa03dd8cbb4933b1c4c1cbd5..a41cd36b70d5ce51151560e0f1658d9b1a2b1af0 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c @@ -63,17 +63,18 @@ int main(void) */ struct list *__gen_e_acsl_f(struct list *l) { - struct list *__gen_e_acsl_at_4; - int __gen_e_acsl_at_3; struct list *__gen_e_acsl_at_2; - int __gen_e_acsl_at; + struct list *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; struct list *__retres; __e_acsl_store_block((void *)(& __retres),(size_t)8); - __e_acsl_store_block((void *)(& l),(size_t)8); - __gen_e_acsl_at_4 = l; { int __gen_e_acsl_valid; int __gen_e_acsl_or; + __e_acsl_store_block((void *)(& l),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + l == (struct list *)0); __gen_e_acsl_valid = __e_acsl_valid((void *)l,sizeof(struct list), (void *)l,(void *)(& l)); if (! __gen_e_acsl_valid) __gen_e_acsl_or = 1; @@ -101,24 +102,29 @@ struct list *__gen_e_acsl_f(struct list *l) else __gen_e_acsl_and = 0; __gen_e_acsl_or = ! __gen_e_acsl_and; } - __gen_e_acsl_at_3 = __gen_e_acsl_or; + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + __gen_e_acsl_or); } __gen_e_acsl_at_2 = l; - __gen_e_acsl_at = l == (struct list *)0; + __gen_e_acsl_at = l; __retres = f(l); { - int __gen_e_acsl_implies; - int __gen_e_acsl_implies_2; - if (! __gen_e_acsl_at) __gen_e_acsl_implies = 1; - else __gen_e_acsl_implies = __retres == __gen_e_acsl_at_2; - __e_acsl_assert(__gen_e_acsl_implies,"Postcondition","f", - "\\old(l == \\null) ==> \\result == \\old(l)", - "tests/memory/valid_in_contract.c",15); - if (! __gen_e_acsl_at_3) __gen_e_acsl_implies_2 = 1; - else __gen_e_acsl_implies_2 = __retres == __gen_e_acsl_at_4; - __e_acsl_assert(__gen_e_acsl_implies_2,"Postcondition","f", - "\\old(!\\valid{Here}(l) || !\\valid{Here}(l->next)) ==> \\result == \\old(l)", - "tests/memory/valid_in_contract.c",18); + int __gen_e_acsl_assumes_value; + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == __gen_e_acsl_at, + "Postcondition","f", + "B1: \\result == \\old(l)", + "tests/memory/valid_in_contract.c", + 15); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) __e_acsl_assert(__retres == __gen_e_acsl_at_2, + "Postcondition","f", + "B2: \\result == \\old(l)", + "tests/memory/valid_in_contract.c", + 18); + __e_acsl_contract_clean(__gen_e_acsl_contract); __e_acsl_delete_block((void *)(& l)); __e_acsl_delete_block((void *)(& __retres)); return __retres; diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle index bcfe10a812c72940b682369df2ac5f11caaaecba..a08399a71e09e3fde121d5d0a7439511ae6e23f0 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle @@ -4,30 +4,21 @@ if there are memory-related annotations. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. -[e-acsl] tests/memory/memalign.c:38: Warning: - E-ACSL construct `complete behaviors' is not yet supported. - Ignoring annotation. -[e-acsl] tests/memory/memalign.c:38: Warning: - E-ACSL construct `disjoint behaviors' is not yet supported. - Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:669: Warning: - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning: E-ACSL construct `predicate performing read accesses' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning: - E-ACSL construct `assigns clause in behavior' is not yet supported. - Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning: E-ACSL construct `predicate performing read accesses' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: + Some assumes clauses couldn't be translated. + Ignoring complete and disjoint behaviors annotations. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:679: Warning: + E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:680: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. + Ignoring annotation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:668: Warning: - function __e_acsl_assert: precondition got status unknown. -[eva] FRAMAC_SHARE/libc/stdlib.h:665: Warning: - ignoring unsupported \allocates clause -[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:679: Warning: - function __gen_e_acsl_posix_memalign, behavior allocation: postcondition 'allocation' got status unknown. -[eva:alarm] tests/memory/memalign.c:14: Warning: - accessing uninitialized left-value. assert \initialized(memptr); diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle index 504ec1ce5e1e7ec93e53ba27fd59cb2f6fd01097..2a20efd543f570f710b1f32d7177806c057ed931 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle +++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle @@ -1,18 +1,15 @@ [eva:alarm] tests/special/e-acsl-valid.c:37: Warning: function f: precondition \valid(y) got status unknown. [e-acsl] beginning translation. -[e-acsl] tests/special/e-acsl-valid.c:25: Warning: +[e-acsl] tests/special/e-acsl-valid.c:28: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] tests/special/e-acsl-valid.c:26: Warning: E-ACSL construct `variant' is not yet supported. Ignoring annotation. -[e-acsl] tests/special/e-acsl-valid.c:26: Warning: - E-ACSL construct `complete behaviors' is not yet supported. - Ignoring annotation. -[e-acsl] tests/special/e-acsl-valid.c:26: Warning: - E-ACSL construct `disjoint behaviors' is not yet supported. +[e-acsl] tests/special/e-acsl-valid.c:24: Warning: + E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] tests/special/e-acsl-valid.c:10: Warning: +[e-acsl] tests/special/e-acsl-valid.c:12: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c index 1df7f9c88591481a05ac5957fbda8240e2a866ff..890e84bc928baf7442348bff76b96f4437330ebc 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c +++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c @@ -100,19 +100,97 @@ int main(void) */ void __gen_e_acsl_f(int *x, int *y) { + int *__gen_e_acsl_at_4; + int *__gen_e_acsl_at_3; + long __gen_e_acsl_at_2; + int *__gen_e_acsl_at; + __e_acsl_contract_t *__gen_e_acsl_contract; { int __gen_e_acsl_valid; + int __gen_e_acsl_active_bhvrs; __e_acsl_store_block((void *)(& y),(size_t)8); __e_acsl_store_block((void *)(& x),(size_t)8); + __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, + *x == 1); + __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, + *x == 0); __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y, (void *)(& y)); __e_acsl_assert(__gen_e_acsl_valid,"Precondition","f","\\valid(y)", "tests/special/e-acsl-valid.c",10); + __e_acsl_assert(*x >= 0,"Precondition","f","*x >= 0", + "tests/special/e-acsl-valid.c",11); + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract); + __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,"Precondition","f", + "all behaviors complete","tests/special/e-acsl-valid.c", + 24); + __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors + ((__e_acsl_contract_t const *)__gen_e_acsl_contract); + __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,"Precondition","f", + "all behaviors disjoint","tests/special/e-acsl-valid.c", + 24); + } + __gen_e_acsl_at_4 = x; + __gen_e_acsl_at_3 = x; + { + int __gen_e_acsl_valid_read; + __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int), + (void *)x,(void *)(& x)); + __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f", + "mem_access: \\valid_read(x)", + "tests/special/e-acsl-valid.c",12); + __gen_e_acsl_at_2 = (long)*x; } + __gen_e_acsl_at = x; f(x,y); - __e_acsl_delete_block((void *)(& y)); - __e_acsl_delete_block((void *)(& x)); - return; + { + int __gen_e_acsl_valid_read_2; + int __gen_e_acsl_assumes_value; + __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at, + sizeof(int), + (void *)__gen_e_acsl_at, + (void *)(& __gen_e_acsl_at)); + __e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","f", + "mem_access: \\valid_read(__gen_e_acsl_at)", + "tests/special/e-acsl-valid.c",12); + __e_acsl_assert((long)*__gen_e_acsl_at == __gen_e_acsl_at_2 + 1L, + "Postcondition","f","*\\old(x) == \\old(*x) + 1", + "tests/special/e-acsl-valid.c",12); + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)0); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_valid_read_3; + __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3, + sizeof(int), + (void *)__gen_e_acsl_at_3, + (void *)(& __gen_e_acsl_at_3)); + __e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","f", + "mem_access: \\valid_read(__gen_e_acsl_at_3)", + "tests/special/e-acsl-valid.c",17); + __e_acsl_assert(*__gen_e_acsl_at_3 < 0,"Postcondition","f", + "b1: *\\old(x) < 0","tests/special/e-acsl-valid.c",17); + } + __gen_e_acsl_assumes_value = __e_acsl_contract_get_behavior_assumes + ((__e_acsl_contract_t const *)__gen_e_acsl_contract,(size_t)1); + if (__gen_e_acsl_assumes_value) { + int __gen_e_acsl_valid_read_4; + __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4, + sizeof(int), + (void *)__gen_e_acsl_at_4, + (void *)(& __gen_e_acsl_at_4)); + __e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","f", + "mem_access: \\valid_read(__gen_e_acsl_at_4)", + "tests/special/e-acsl-valid.c",20); + __e_acsl_assert(*__gen_e_acsl_at_4 == 1,"Postcondition","f", + "b2: *\\old(x) == 1","tests/special/e-acsl-valid.c",20); + } + __e_acsl_contract_clean(__gen_e_acsl_contract); + __e_acsl_delete_block((void *)(& y)); + __e_acsl_delete_block((void *)(& x)); + return; + } } diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle index b55cb5a92eafcf2f00321298635858249ab4b402..466e50c6150635682a7fa2664722e39de64c0707 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle @@ -5,7 +5,7 @@ [e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning: +[e-acsl] FRAMAC_SHARE/libc/stdlib.h:485: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle index c88bb93bb619661810e3435aa84bf288519fdd55..101a07c7fb68b6985cbe8896de359855582c12bd 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle @@ -24,7 +24,7 @@ Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: +[e-acsl] FRAMAC_SHARE/libc/string.h:92: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:98: Warning: