diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 631226b2fe3ac6eb9798284c6a2cd5fb49146e06..b68a16c8ae191100bf7696cdd39403fb8ce7fd16 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
############################
+-* E-ACSL [2021-06-04] Do not translate contracts of E-ACSL built-ins.
+
#############################
Plugin E-ACSL 23.0 (Vanadium)
#############################
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 92d0e9bfef74a16e235e04f84301a1f25b2ce6cc..95e8177eaab3ea44db06987a7c26de20c2d803c7 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -34,6 +34,9 @@ let is_fc_or_compiler_builtin vi =
&&
let prefix = String.sub vi.vname 0 prefix_length in
Datatype.String.equal prefix "__builtin_")
+ ||
+ (Options.Replace_libc_functions.get ()
+ && Functions.RTL.has_rtl_replacement vi.vname)
let is_fc_stdlib_generated vi =
Cil.hasAttribute "fc_stdlib_generated" vi.vattr
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
index ae145b13224ff965dc48e8a56ce5258fbbce5896..c2bfeb3f43d81709cc3a5d4eada221e6ac1cac83 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
@@ -75,159 +75,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
*/
pid_t __gen_e_acsl_fork(void);
-/*@ requires valid_string_src: valid_read_string(src);
- requires valid_string_dest: valid_string(dest);
- requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
- ensures
- sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
- ensures
- initialization: dest:
- \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
- ensures
- dest_null_terminated:
- *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest +
- (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
- \result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src);
-
-/*@ requires valid_nstring_src: valid_read_nstring(src, n);
- requires valid_string_dest: valid_string(dest);
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
- \from *(src + (0 .. n));
- assigns \result \from dest;
-
- behavior complete:
- assumes
- valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
- requires
- room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
- ensures
- sum_of_lengths:
- strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
- assigns *(dest +
- (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
- \result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
-
- behavior partial:
- assumes
- valid_string_src_too_large:
- ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
- requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
- ensures
- sum_of_bounded_lengths:
- strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
- \result;
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
- size_t n);
-
-/*@ requires valid_nstring_src: valid_read_nstring(src, n);
- requires valid_string_dest: valid_string(dest);
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result;
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
- \from *(src + (0 .. n));
- assigns \result \from dest;
-
- behavior complete:
- assumes
- valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n;
- requires
- room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src)));
- ensures
- sum_of_lengths:
- strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
- assigns *(dest +
- (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
- \result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
-
- behavior partial:
- assumes
- valid_string_src_too_large:
- ¬(valid_read_string(src) ∧ strlen(src) ≤ n);
- requires room_string: \valid((dest + strlen(dest)) + (0 .. n));
- ensures
- sum_of_bounded_lengths:
- strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n);
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)),
- \result;
- assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *__gen_e_acsl_strncat(char * restrict dest, char const * restrict src,
- size_t n)
-{
- char *__gen_e_acsl_at;
- __e_acsl_contract_t *__gen_e_acsl_contract;
- char *__retres;
- __e_acsl_store_block((void *)(& dest),(size_t)8);
- __gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
- __gen_e_acsl_at = dest;
- __retres = __e_acsl_builtin_strncat(dest,src,n);
- __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strncat",
- "result_ptr: \\result == \\old(dest)",
- "FRAMAC_SHARE/libc/string.h",430);
- __e_acsl_contract_clean(__gen_e_acsl_contract);
- __e_acsl_delete_block((void *)(& dest));
- return __retres;
-}
-
-/*@ requires valid_string_src: valid_read_string(src);
- requires valid_string_dest: valid_string(dest);
- requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)));
- ensures
- sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src));
- ensures
- initialization: dest:
- \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src))));
- ensures
- dest_null_terminated:
- *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest +
- (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))),
- \result;
- assigns
- *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
-{
- char *__gen_e_acsl_at;
- char *__retres;
- __e_acsl_store_block((void *)(& dest),(size_t)8);
- __gen_e_acsl_at = dest;
- __retres = __e_acsl_builtin_strcat(dest,src);
- __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strcat",
- "result_ptr: \\result == \\old(dest)",
- "FRAMAC_SHARE/libc/string.h",421);
- __e_acsl_delete_block((void *)(& dest));
- return __retres;
-}
-
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
@@ -498,11 +345,7 @@ int main(int argc, char const **argv)
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
char *const_str = (char *)__gen_e_acsl_literal_string_6;
- __e_acsl_store_block((void *)(& const_str),(size_t)8);
- __e_acsl_full_init((void *)(& const_str));
char *unalloc_str = malloc((unsigned long)5);
- __e_acsl_store_block((void *)(& unalloc_str),(size_t)8);
- __e_acsl_full_init((void *)(& unalloc_str));
char *_barrier = malloc((unsigned long)1);
char *empty_str = (char *)__gen_e_acsl_literal_string_7;
free((void *)unalloc_str);
@@ -538,7 +381,7 @@ int main(int argc, char const **argv)
{
pid_t pid = __gen_e_acsl_fork();
if (! pid) {
- __gen_e_acsl_strcat(dest1,(char const *)const_str);
+ __e_acsl_builtin_strcat(dest1,(char const *)const_str);
__gen_e_acsl_exit(0);
}
else {
@@ -552,7 +395,7 @@ int main(int argc, char const **argv)
{
pid_t pid_0 = __gen_e_acsl_fork();
if (! pid_0) {
- __gen_e_acsl_strcat(dest3,(char const *)empty_str);
+ __e_acsl_builtin_strcat(dest3,(char const *)empty_str);
__gen_e_acsl_exit(0);
}
else {
@@ -566,7 +409,7 @@ int main(int argc, char const **argv)
{
pid_t pid_1 = __gen_e_acsl_fork();
if (! pid_1) {
- __gen_e_acsl_strcat(dest2,(char const *)const_str);
+ __e_acsl_builtin_strcat(dest2,(char const *)const_str);
__gen_e_acsl_exit(0);
}
else {
@@ -580,7 +423,7 @@ int main(int argc, char const **argv)
{
pid_t pid_2 = __gen_e_acsl_fork();
if (! pid_2) {
- __gen_e_acsl_strcat(unalloc_str,(char const *)const_str);
+ __e_acsl_builtin_strcat(unalloc_str,(char const *)const_str);
__gen_e_acsl_exit(0);
}
else {
@@ -594,7 +437,7 @@ int main(int argc, char const **argv)
{
pid_t pid_3 = __gen_e_acsl_fork();
if (! pid_3) {
- __gen_e_acsl_strcat(dest2,(char const *)unalloc_str);
+ __e_acsl_builtin_strcat(dest2,(char const *)unalloc_str);
__gen_e_acsl_exit(0);
}
else {
@@ -608,7 +451,7 @@ int main(int argc, char const **argv)
{
pid_t pid_4 = __gen_e_acsl_fork();
if (! pid_4) {
- __gen_e_acsl_strcat((char *)0,__gen_e_acsl_literal_string_7);
+ __e_acsl_builtin_strcat((char *)0,__gen_e_acsl_literal_string_7);
__gen_e_acsl_exit(0);
}
else {
@@ -622,7 +465,7 @@ int main(int argc, char const **argv)
{
pid_t pid_5 = __gen_e_acsl_fork();
if (! pid_5) {
- __gen_e_acsl_strcat(dest1,(char const *)0);
+ __e_acsl_builtin_strcat(dest1,(char const *)0);
__gen_e_acsl_exit(0);
}
else {
@@ -636,7 +479,7 @@ int main(int argc, char const **argv)
{
pid_t pid_6 = __gen_e_acsl_fork();
if (! pid_6) {
- __gen_e_acsl_strcat(const_str,(char const *)const_str);
+ __e_acsl_builtin_strcat(const_str,(char const *)const_str);
__gen_e_acsl_exit(0);
}
else {
@@ -650,7 +493,7 @@ int main(int argc, char const **argv)
{
pid_t pid_7 = __gen_e_acsl_fork();
if (! pid_7) {
- __gen_e_acsl_strcat(pd1,(char const *)pd1);
+ __e_acsl_builtin_strcat(pd1,(char const *)pd1);
__gen_e_acsl_exit(0);
}
else {
@@ -664,7 +507,7 @@ int main(int argc, char const **argv)
{
pid_t pid_8 = __gen_e_acsl_fork();
if (! pid_8) {
- __gen_e_acsl_strcat(pd1 + 3,(char const *)pd1);
+ __e_acsl_builtin_strcat(pd1 + 3,(char const *)pd1);
__gen_e_acsl_exit(0);
}
else {
@@ -678,7 +521,7 @@ int main(int argc, char const **argv)
{
pid_t pid_9 = __gen_e_acsl_fork();
if (! pid_9) {
- __gen_e_acsl_strcat(pd4 + 4,(char const *)pd4);
+ __e_acsl_builtin_strcat(pd4 + 4,(char const *)pd4);
__gen_e_acsl_exit(0);
}
else {
@@ -694,7 +537,7 @@ int main(int argc, char const **argv)
if (! pid_10) {
__e_acsl_initialize((void *)(pd4 + 5),sizeof(char));
*(pd4 + 5) = (char)'\000';
- __gen_e_acsl_strcat(pd4 + 5,(char const *)pd4);
+ __e_acsl_builtin_strcat(pd4 + 5,(char const *)pd4);
__gen_e_acsl_exit(0);
}
else {
@@ -746,8 +589,8 @@ int main(int argc, char const **argv)
{
pid_t pid_11 = __gen_e_acsl_fork();
if (! pid_11) {
- __gen_e_acsl_strncat(dest1_0,(char const *)const_str,
- (unsigned long)4);
+ __e_acsl_builtin_strncat(dest1_0,(char const *)const_str,
+ (unsigned long)4);
__gen_e_acsl_exit(0);
}
else {
@@ -761,8 +604,8 @@ int main(int argc, char const **argv)
{
pid_t pid_12 = __gen_e_acsl_fork();
if (! pid_12) {
- __gen_e_acsl_strncat(dest2_0,(char const *)const_str,
- (unsigned long)4);
+ __e_acsl_builtin_strncat(dest2_0,(char const *)const_str,
+ (unsigned long)4);
__gen_e_acsl_exit(0);
}
else {
@@ -776,8 +619,8 @@ int main(int argc, char const **argv)
{
pid_t pid_13 = __gen_e_acsl_fork();
if (! pid_13) {
- __gen_e_acsl_strncat(unalloc_str,(char const *)const_str,
- (unsigned long)1);
+ __e_acsl_builtin_strncat(unalloc_str,(char const *)const_str,
+ (unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
@@ -791,8 +634,8 @@ int main(int argc, char const **argv)
{
pid_t pid_14 = __gen_e_acsl_fork();
if (! pid_14) {
- __gen_e_acsl_strncat(dest2_0,(char const *)unalloc_str,
- (unsigned long)1);
+ __e_acsl_builtin_strncat(dest2_0,(char const *)unalloc_str,
+ (unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
@@ -806,8 +649,8 @@ int main(int argc, char const **argv)
{
pid_t pid_15 = __gen_e_acsl_fork();
if (! pid_15) {
- __gen_e_acsl_strncat((char *)0,(char const *)const_str,
- (unsigned long)1);
+ __e_acsl_builtin_strncat((char *)0,(char const *)const_str,
+ (unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
@@ -821,7 +664,7 @@ int main(int argc, char const **argv)
{
pid_t pid_16 = __gen_e_acsl_fork();
if (! pid_16) {
- __gen_e_acsl_strncat(dest2_0,(char const *)0,(unsigned long)1);
+ __e_acsl_builtin_strncat(dest2_0,(char const *)0,(unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
@@ -835,8 +678,8 @@ int main(int argc, char const **argv)
{
pid_t pid_17 = __gen_e_acsl_fork();
if (! pid_17) {
- __gen_e_acsl_strncat(const_str,(char const *)const_str,
- (unsigned long)1);
+ __e_acsl_builtin_strncat(const_str,(char const *)const_str,
+ (unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
@@ -850,7 +693,7 @@ int main(int argc, char const **argv)
{
pid_t pid_18 = __gen_e_acsl_fork();
if (! pid_18) {
- __gen_e_acsl_strncat(pd1_0,(char const *)pd1_0,(unsigned long)1);
+ __e_acsl_builtin_strncat(pd1_0,(char const *)pd1_0,(unsigned long)1);
__gen_e_acsl_exit(0);
}
else {
@@ -864,7 +707,8 @@ int main(int argc, char const **argv)
{
pid_t pid_19 = __gen_e_acsl_fork();
if (! pid_19) {
- __gen_e_acsl_strncat(pd1_0 + 3,(char const *)pd1_0,(unsigned long)5);
+ __e_acsl_builtin_strncat(pd1_0 + 3,(char const *)pd1_0,
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -878,7 +722,8 @@ int main(int argc, char const **argv)
{
pid_t pid_20 = __gen_e_acsl_fork();
if (! pid_20) {
- __gen_e_acsl_strncat(pd4_0 + 4,(char const *)pd4_0,(unsigned long)5);
+ __e_acsl_builtin_strncat(pd4_0 + 4,(char const *)pd4_0,
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -899,8 +744,6 @@ int main(int argc, char const **argv)
}
}
__retres = 0;
- __e_acsl_delete_block((void *)(& unalloc_str));
- __e_acsl_delete_block((void *)(& const_str));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
index 5032458f73323645d0ec6794819761816c63528d..5c56e4f5c0923e9f0ea9df75a97d12fb18ddbd47 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
@@ -85,25 +85,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
*/
pid_t __gen_e_acsl_fork(void);
-/*@ requires valid_string_s1: valid_read_string(s1);
- requires valid_string_s2: valid_read_string(s2);
- ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2));
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
- */
-int __gen_e_acsl_strcmp(char const *s1, char const *s2);
-
-/*@ requires valid_string_s1: valid_read_nstring(s1, n);
- requires valid_string_s2: valid_read_nstring(s2, n);
- ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n));
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
- */
-int __gen_e_acsl_strncmp(char const *s1, char const *s2, size_t n);
-
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
@@ -201,35 +182,6 @@ char *__gen_e_acsl_strdup(char const *s)
}
}
-/*@ requires valid_string_s1: valid_read_nstring(s1, n);
- requires valid_string_s2: valid_read_nstring(s2, n);
- ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n));
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 .. n - 1))),
- (indirect: *(s2 + (0 .. n - 1))), (indirect: n);
- */
-int __gen_e_acsl_strncmp(char const *s1, char const *s2, size_t n)
-{
- int __retres;
- __retres = __e_acsl_builtin_strncmp(s1,s2,n);
- return __retres;
-}
-
-/*@ requires valid_string_s1: valid_read_string(s1);
- requires valid_string_s2: valid_read_string(s2);
- ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2));
- assigns \result;
- assigns \result
- \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..)));
- */
-int __gen_e_acsl_strcmp(char const *s1, char const *s2)
-{
- int __retres;
- __retres = __e_acsl_builtin_strcmp(s1,s2);
- return __retres;
-}
-
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
@@ -539,8 +491,8 @@ int main(int argc, char const **argv)
if (! pid) {
int tmp_2;
int tmp_3;
- tmp_2 = __gen_e_acsl_strcmp(cl,cr);
- tmp_3 = __gen_e_acsl_strcmp(cl,cr);
+ tmp_2 = __e_acsl_builtin_strcmp(cl,cr);
+ tmp_3 = __e_acsl_builtin_strcmp(cl,cr);
fail_ncomp(tmp_3 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_2,0);
__gen_e_acsl_exit(0);
}
@@ -557,8 +509,8 @@ int main(int argc, char const **argv)
if (! pid_0) {
int tmp_5;
int tmp_6;
- tmp_5 = __gen_e_acsl_strcmp((char const *)(al),(char const *)(ar));
- tmp_6 = __gen_e_acsl_strcmp((char const *)(al),(char const *)(ar));
+ tmp_5 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)(ar));
+ tmp_6 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)(ar));
fail_ncomp(tmp_6 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_5,0);
__gen_e_acsl_exit(0);
}
@@ -575,8 +527,8 @@ int main(int argc, char const **argv)
if (! pid_1) {
int tmp_8;
int tmp_9;
- tmp_8 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
- tmp_9 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
+ tmp_8 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)dr);
+ tmp_9 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)dr);
fail_ncomp(tmp_9 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_8,0);
__gen_e_acsl_exit(0);
}
@@ -594,8 +546,8 @@ int main(int argc, char const **argv)
if (! pid_2) {
int tmp_11;
int tmp_12;
- tmp_11 = __gen_e_acsl_strcmp((char const *)(al),(char const *)(ar));
- tmp_12 = __gen_e_acsl_strcmp((char const *)(al),(char const *)(ar));
+ tmp_11 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)(ar));
+ tmp_12 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)(ar));
fail_ncomp(tmp_12 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_11,0);
__gen_e_acsl_exit(0);
}
@@ -614,8 +566,8 @@ int main(int argc, char const **argv)
if (! pid_3) {
int tmp_14;
int tmp_15;
- tmp_14 = __gen_e_acsl_strcmp((char const *)(al),(char const *)(ar));
- tmp_15 = __gen_e_acsl_strcmp((char const *)(al),(char const *)(ar));
+ tmp_14 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)(ar));
+ tmp_15 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)(ar));
fail_ncomp(tmp_15 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_14,0);
__gen_e_acsl_exit(0);
}
@@ -633,8 +585,8 @@ int main(int argc, char const **argv)
if (! pid_4) {
int tmp_17;
int tmp_18;
- tmp_17 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
- tmp_18 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
+ tmp_17 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)dr);
+ tmp_18 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)dr);
fail_ncomp(tmp_18 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_17,0);
__gen_e_acsl_exit(0);
}
@@ -653,8 +605,8 @@ int main(int argc, char const **argv)
if (! pid_5) {
int tmp_20;
int tmp_21;
- tmp_20 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
- tmp_21 = __gen_e_acsl_strcmp((char const *)dl,(char const *)dr);
+ tmp_20 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)dr);
+ tmp_21 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)dr);
fail_ncomp(tmp_21 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_20,0);
__gen_e_acsl_exit(0);
}
@@ -671,8 +623,8 @@ int main(int argc, char const **argv)
if (! pid_6) {
int tmp_23;
int tmp_24;
- tmp_23 = __gen_e_acsl_strcmp((char const *)dl,(char const *)0);
- tmp_24 = __gen_e_acsl_strcmp((char const *)dl,(char const *)0);
+ tmp_23 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)0);
+ tmp_24 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)0);
fail_ncomp(tmp_24 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_23,0);
__gen_e_acsl_exit(0);
}
@@ -689,8 +641,8 @@ int main(int argc, char const **argv)
if (! pid_7) {
int tmp_26;
int tmp_27;
- tmp_26 = __gen_e_acsl_strcmp((char const *)0,(char const *)dr);
- tmp_27 = __gen_e_acsl_strcmp((char const *)0,(char const *)dr);
+ tmp_26 = __e_acsl_builtin_strcmp((char const *)0,(char const *)dr);
+ tmp_27 = __e_acsl_builtin_strcmp((char const *)0,(char const *)dr);
fail_ncomp(tmp_27 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_26,0);
__gen_e_acsl_exit(0);
}
@@ -709,8 +661,8 @@ int main(int argc, char const **argv)
if (! pid_8) {
int tmp_29;
int tmp_30;
- tmp_29 = __gen_e_acsl_strcmp((char const *)dl,(char const *)(ar));
- tmp_30 = __gen_e_acsl_strcmp((char const *)dl,(char const *)(ar));
+ tmp_29 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)(ar));
+ tmp_30 = __e_acsl_builtin_strcmp((char const *)dl,(char const *)(ar));
fail_ncomp(tmp_30 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_29,0);
__gen_e_acsl_exit(0);
}
@@ -727,8 +679,8 @@ int main(int argc, char const **argv)
if (! pid_9) {
int tmp_32;
int tmp_33;
- tmp_32 = __gen_e_acsl_strcmp((char const *)(al),(char const *)dr);
- tmp_33 = __gen_e_acsl_strcmp((char const *)(al),(char const *)dr);
+ tmp_32 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)dr);
+ tmp_33 = __e_acsl_builtin_strcmp((char const *)(al),(char const *)dr);
fail_ncomp(tmp_33 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_32,0);
__gen_e_acsl_exit(0);
}
@@ -749,8 +701,8 @@ int main(int argc, char const **argv)
if (! pid_10) {
int tmp_35;
int tmp_36;
- tmp_35 = __gen_e_acsl_strncmp(cl,cr,(unsigned long)3);
- tmp_36 = __gen_e_acsl_strncmp(cl,cr,(unsigned long)3);
+ tmp_35 = __e_acsl_builtin_strncmp(cl,cr,(unsigned long)3);
+ tmp_36 = __e_acsl_builtin_strncmp(cl,cr,(unsigned long)3);
fail_ncomp(tmp_36 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_35,0);
__gen_e_acsl_exit(0);
}
@@ -767,10 +719,10 @@ int main(int argc, char const **argv)
if (! pid_11) {
int tmp_38;
int tmp_39;
- tmp_38 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)3);
- tmp_39 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)3);
+ tmp_38 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)3);
+ tmp_39 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)3);
fail_ncomp(tmp_39 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_38,0);
__gen_e_acsl_exit(0);
}
@@ -787,10 +739,10 @@ int main(int argc, char const **argv)
if (! pid_12) {
int tmp_41;
int tmp_42;
- tmp_41 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)3);
- tmp_42 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)3);
+ tmp_41 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)3);
+ tmp_42 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)3);
fail_ncomp(tmp_42 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_41,0);
__gen_e_acsl_exit(0);
}
@@ -807,10 +759,10 @@ int main(int argc, char const **argv)
if (! pid_13) {
int tmp_44;
int tmp_45;
- tmp_44 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)6);
- tmp_45 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)6);
+ tmp_44 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)6);
+ tmp_45 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)6);
fail_ncomp(tmp_45 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_44,0);
__gen_e_acsl_exit(0);
}
@@ -827,10 +779,10 @@ int main(int argc, char const **argv)
if (! pid_14) {
int tmp_47;
int tmp_48;
- tmp_47 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)6);
- tmp_48 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)6);
+ tmp_47 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)6);
+ tmp_48 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)6);
fail_ncomp(tmp_48 != 0,(char *)__gen_e_acsl_literal_string_7,tmp_47,0);
__gen_e_acsl_exit(0);
}
@@ -848,10 +800,10 @@ int main(int argc, char const **argv)
if (! pid_15) {
int tmp_50;
int tmp_51;
- tmp_50 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)4);
- tmp_51 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)4);
+ tmp_50 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)4);
+ tmp_51 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)4);
fail_ncomp(tmp_51 == 0,(char *)__gen_e_acsl_literal_string_24,tmp_50,0);
__gen_e_acsl_exit(0);
}
@@ -870,10 +822,10 @@ int main(int argc, char const **argv)
if (! pid_16) {
int tmp_53;
int tmp_54;
- tmp_53 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)4);
- tmp_54 = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)4);
+ tmp_53 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)4);
+ tmp_54 = __e_acsl_builtin_strncmp((char const *)(nal),
+ (char const *)(nar),(unsigned long)4);
fail_ncomp(tmp_54 == 0,(char *)__gen_e_acsl_literal_string_24,tmp_53,0);
__gen_e_acsl_exit(0);
}
@@ -891,10 +843,10 @@ int main(int argc, char const **argv)
if (! pid_17) {
int tmp_56;
int tmp_57;
- tmp_56 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)4);
- tmp_57 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)4);
+ tmp_56 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)4);
+ tmp_57 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)4);
fail_ncomp(tmp_57 == 0,(char *)__gen_e_acsl_literal_string_24,tmp_56,0);
__gen_e_acsl_exit(0);
}
@@ -913,10 +865,10 @@ int main(int argc, char const **argv)
if (! pid_18) {
int tmp_59;
int tmp_60;
- tmp_59 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)4);
- tmp_60 = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)4);
+ tmp_59 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)4);
+ tmp_60 = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)4);
fail_ncomp(tmp_60 == 0,(char *)__gen_e_acsl_literal_string_24,tmp_59,0);
__gen_e_acsl_exit(0);
}
@@ -931,8 +883,8 @@ int main(int argc, char const **argv)
{
pid_t pid_19 = __gen_e_acsl_fork();
if (! pid_19) {
- res = __gen_e_acsl_strncmp((char const *)(nal),(char const *)(nar),
- (unsigned long)5);
+ res = __e_acsl_builtin_strncmp((char const *)(nal),(char const *)(nar),
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -948,8 +900,8 @@ int main(int argc, char const **argv)
{
pid_t pid_20 = __gen_e_acsl_fork();
if (! pid_20) {
- res = __gen_e_acsl_strncmp((char const *)(al),(char const *)(ar),
- (unsigned long)5);
+ res = __e_acsl_builtin_strncmp((char const *)(al),(char const *)(ar),
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -963,8 +915,8 @@ int main(int argc, char const **argv)
{
pid_t pid_21 = __gen_e_acsl_fork();
if (! pid_21) {
- res = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)5);
+ res = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -980,8 +932,8 @@ int main(int argc, char const **argv)
{
pid_t pid_22 = __gen_e_acsl_fork();
if (! pid_22) {
- res = __gen_e_acsl_strncmp((char const *)dl,(char const *)dr,
- (unsigned long)5);
+ res = __e_acsl_builtin_strncmp((char const *)dl,(char const *)dr,
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
index 93d63197ed80be0e7170a58068a95c2d46d23744..3642669d9d345e9377703f99c1c579c008fc728e 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
@@ -70,42 +70,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
*/
pid_t __gen_e_acsl_fork(void);
-/*@ requires valid_string_src: valid_read_string(src);
- requires room_string: \valid(dest + (0 .. strlen(src)));
- requires
- separation:
- \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
- ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (0 .. strlen{Old}(src))), \result;
- assigns *(dest + (0 .. strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src);
-
-/*@ requires valid_nstring_src: valid_read_nstring(src, n);
- requires room_nstring: \valid(dest + (0 .. n - 1));
- requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
- ensures result_ptr: \result ≡ \old(dest);
- ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
- assigns \result \from dest;
-
- behavior complete:
- assumes src_fits: strlen(src) < n;
- ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
-
- behavior partial:
- assumes src_too_long: n ≤ strlen(src);
- ensures
- equal_prefix:
- memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
- */
-char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
- size_t n);
-
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
@@ -164,7 +128,6 @@ char *__gen_e_acsl_strdup(char const *s)
{
__e_acsl_contract_t *__gen_e_acsl_contract;
char *__retres;
- __e_acsl_store_block((void *)(& __retres),(size_t)8);
__gen_e_acsl_contract = __e_acsl_contract_init((size_t)2);
__retres = strdup(s);
{
@@ -177,226 +140,10 @@ char *__gen_e_acsl_strdup(char const *s)
"FRAMAC_SHARE/libc/string.h",
485);
__e_acsl_contract_clean(__gen_e_acsl_contract);
- __e_acsl_delete_block((void *)(& __retres));
return __retres;
}
}
-/*@ requires valid_nstring_src: valid_read_nstring(src, n);
- requires room_nstring: \valid(dest + (0 .. n - 1));
- requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1));
- ensures result_ptr: \result ≡ \old(dest);
- ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1));
- assigns *(dest + (0 .. n - 1)), \result;
- assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1));
- assigns \result \from dest;
-
- behavior complete:
- assumes src_fits: strlen(src) < n;
- ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0;
-
- behavior partial:
- assumes src_too_long: n ≤ strlen(src);
- ensures
- equal_prefix:
- memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0;
- */
-char *__gen_e_acsl_strncpy(char * restrict dest, char const * restrict src,
- size_t n)
-{
- __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;
- {
- unsigned long __gen_e_acsl_size;
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl__2;
- __e_acsl_mpz_t __gen_e_acsl_sub_2;
- __e_acsl_mpz_t __gen_e_acsl_add;
- unsigned long __gen_e_acsl__3;
- unsigned long __gen_e_acsl_if;
- int __gen_e_acsl_valid;
- unsigned long __gen_e_acsl_size_2;
- unsigned long __gen_e_acsl__4;
- unsigned long __gen_e_acsl_if_2;
- int __gen_e_acsl_valid_read;
- unsigned long __gen_e_acsl_size_3;
- unsigned long __gen_e_acsl__5;
- unsigned long __gen_e_acsl_if_3;
- int __gen_e_acsl_valid_read_2;
- unsigned long __gen_e_acsl_size_4;
- unsigned long __gen_e_acsl__6;
- unsigned long __gen_e_acsl_if_4;
- unsigned long __gen_e_acsl_size_5;
- unsigned long __gen_e_acsl__7;
- unsigned long __gen_e_acsl_if_5;
- int __gen_e_acsl_separated;
- __e_acsl_store_block((void *)(& src),(size_t)8);
- __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);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init(__gen_e_acsl_sub_2);
- __gmpz_sub(__gen_e_acsl_sub_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl__3 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size = 1UL * __gen_e_acsl__3;
- if (__gen_e_acsl_size <= 0UL) __gen_e_acsl_if = 0UL;
- else __gen_e_acsl_if = __gen_e_acsl_size;
- __gen_e_acsl_valid = __e_acsl_valid((void *)(dest + 1 * 0),
- __gen_e_acsl_if,(void *)dest,
- (void *)(& dest));
- __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","strncpy",
- "room_nstring: \\valid(dest + (0 .. n - 1))",
- "FRAMAC_SHARE/libc/string.h",367);
- __gen_e_acsl__4 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_2 = 1UL * __gen_e_acsl__4;
- if (__gen_e_acsl_size_2 <= 0UL) __gen_e_acsl_if_2 = 0UL;
- else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(dest + 1 * 0),
- __gen_e_acsl_if_2,
- (void *)dest,
- (void *)(& dest));
- /*@ assert E_ACSL: separated_guard: \valid_read(dest + (0 .. n - 1)); */
- __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","strncpy",
- "separated_guard: \\valid_read(dest + (0 .. n - 1))",
- "FRAMAC_SHARE/libc/string.h",369);
- __gen_e_acsl__5 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_3 = 1UL * __gen_e_acsl__5;
- if (__gen_e_acsl_size_3 <= 0UL) __gen_e_acsl_if_3 = 0UL;
- else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
- __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(src + 1 * 0),
- __gen_e_acsl_if_3,
- (void *)src,
- (void *)(& src));
- /*@ assert E_ACSL: separated_guard: \valid_read(src + (0 .. n - 1)); */
- __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","strncpy",
- "separated_guard: \\valid_read(src + (0 .. n - 1))",
- "FRAMAC_SHARE/libc/string.h",369);
- __gen_e_acsl__6 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_4 = 1UL * __gen_e_acsl__6;
- if (__gen_e_acsl_size_4 <= 0UL) __gen_e_acsl_if_4 = 0UL;
- else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
- __gen_e_acsl__7 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gen_e_acsl_size_5 = 1UL * __gen_e_acsl__7;
- if (__gen_e_acsl_size_5 <= 0UL) __gen_e_acsl_if_5 = 0UL;
- else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
- __gen_e_acsl_separated = __e_acsl_separated((size_t)2,dest + 1 * 0,
- __gen_e_acsl_if_4,
- src + 1 * 0,
- __gen_e_acsl_if_5);
- __e_acsl_assert(__gen_e_acsl_separated,1,"Precondition","strncpy",
- "separation: \\separated(dest + (0 .. n - 1), src + (0 .. n - 1))",
- "FRAMAC_SHARE/libc/string.h",369);
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl__2);
- __gmpz_clear(__gen_e_acsl_sub_2);
- __gmpz_clear(__gen_e_acsl_add);
- }
- {
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __gmpz_init_set_ui(__gen_e_acsl_n_2,n);
- __gmpz_init_set(__gen_e_acsl_at_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
- __gmpz_clear(__gen_e_acsl_n_2);
- }
- __gen_e_acsl_at_2 = dest;
- __gen_e_acsl_at = dest;
- __retres = __e_acsl_builtin_strncpy(dest,src,n);
- {
- unsigned long __gen_e_acsl_size_6;
- __e_acsl_mpz_t __gen_e_acsl__8;
- __e_acsl_mpz_t __gen_e_acsl_sub_3;
- __e_acsl_mpz_t __gen_e_acsl__9;
- __e_acsl_mpz_t __gen_e_acsl_sub_4;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- unsigned long __gen_e_acsl__10;
- unsigned long __gen_e_acsl_if_6;
- int __gen_e_acsl_initialized;
- __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strncpy",
- "result_ptr: \\result == \\old(dest)",
- "FRAMAC_SHARE/libc/string.h",372);
- __gmpz_init_set_si(__gen_e_acsl__8,1L);
- __gmpz_init(__gen_e_acsl_sub_3);
- __gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gmpz_init_set_si(__gen_e_acsl__9,0L);
- __gmpz_init(__gen_e_acsl_sub_4);
- __gmpz_sub(__gen_e_acsl_sub_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
- __gen_e_acsl__10 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gen_e_acsl_size_6 = 1UL * __gen_e_acsl__10;
- if (__gen_e_acsl_size_6 <= 0UL) __gen_e_acsl_if_6 = 0UL;
- else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
- __gen_e_acsl_initialized = __e_acsl_initialized((void *)(__gen_e_acsl_at_2 +
- 1 * 0),
- __gen_e_acsl_if_6);
- __e_acsl_assert(__gen_e_acsl_initialized,1,"Postcondition","strncpy",
- "initialization: \\initialized(\\old(dest) + (0 .. \\old(n) - 1))",
- "FRAMAC_SHARE/libc/string.h",373);
- __e_acsl_contract_clean(__gen_e_acsl_contract);
- __e_acsl_delete_block((void *)(& src));
- __e_acsl_delete_block((void *)(& dest));
- __gmpz_clear(__gen_e_acsl__8);
- __gmpz_clear(__gen_e_acsl_sub_3);
- __gmpz_clear(__gen_e_acsl__9);
- __gmpz_clear(__gen_e_acsl_sub_4);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_at_3);
- return __retres;
- }
-}
-
-/*@ requires valid_string_src: valid_read_string(src);
- requires room_string: \valid(dest + (0 .. strlen(src)));
- requires
- separation:
- \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src)));
- ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0;
- ensures result_ptr: \result ≡ \old(dest);
- assigns *(dest + (0 .. strlen{Old}(src))), \result;
- assigns *(dest + (0 .. strlen{Old}(src)))
- \from *(src + (0 .. strlen{Old}(src)));
- assigns \result \from dest;
- */
-char *__gen_e_acsl_strcpy(char * restrict dest, char const * restrict src)
-{
- char *__gen_e_acsl_at;
- char *__retres;
- __e_acsl_store_block((void *)(& src),(size_t)8);
- __e_acsl_store_block((void *)(& dest),(size_t)8);
- __gen_e_acsl_at = dest;
- __retres = __e_acsl_builtin_strcpy(dest,src);
- __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","strcpy",
- "result_ptr: \\result == \\old(dest)",
- "FRAMAC_SHARE/libc/string.h",361);
- __e_acsl_delete_block((void *)(& src));
- __e_acsl_delete_block((void *)(& dest));
- return __retres;
-}
-
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
@@ -642,34 +389,20 @@ int main(int argc, char const **argv)
__e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
char empty_str[1] = {(char)'\000'};
- __e_acsl_store_block((void *)(empty_str),(size_t)1);
- __e_acsl_full_init((void *)(& empty_str));
char *const_str = (char *)__gen_e_acsl_literal_string_6;
- __e_acsl_store_block((void *)(& const_str),(size_t)8);
- __e_acsl_full_init((void *)(& const_str));
char *src = __gen_e_acsl_strdup(__gen_e_acsl_literal_string_6);
- __e_acsl_store_block((void *)(& src),(size_t)8);
- __e_acsl_full_init((void *)(& src));
char *dest1 = malloc((unsigned long)5);
- __e_acsl_store_block((void *)(& dest1),(size_t)8);
- __e_acsl_full_init((void *)(& dest1));
char *dest2 = malloc((unsigned long)4);
- __e_acsl_store_block((void *)(& dest2),(size_t)8);
- __e_acsl_full_init((void *)(& dest2));
char dest3[256] =
{(char)'a', (char)'b', (char)'c', (char)'d', (char)'\000'};
- __e_acsl_store_block((void *)(dest3),(size_t)256);
- __e_acsl_full_init((void *)(& dest3));
size_t len = (unsigned long)0;
char *unalloc_str = malloc((unsigned long)5);
- __e_acsl_store_block((void *)(& unalloc_str),(size_t)8);
- __e_acsl_full_init((void *)(& unalloc_str));
char *_barrier = malloc((unsigned long)1);
free((void *)unalloc_str);
{
pid_t pid = __gen_e_acsl_fork();
if (! pid) {
- __gen_e_acsl_strcpy(dest1,(char const *)src);
+ __e_acsl_builtin_strcpy(dest1,(char const *)src);
__gen_e_acsl_exit(0);
}
else {
@@ -683,7 +416,7 @@ int main(int argc, char const **argv)
{
pid_t pid_0 = __gen_e_acsl_fork();
if (! pid_0) {
- __gen_e_acsl_strcpy(empty_str,__gen_e_acsl_literal_string_8);
+ __e_acsl_builtin_strcpy(empty_str,__gen_e_acsl_literal_string_8);
__gen_e_acsl_exit(0);
}
else {
@@ -697,7 +430,7 @@ int main(int argc, char const **argv)
{
pid_t pid_1 = __gen_e_acsl_fork();
if (! pid_1) {
- __gen_e_acsl_strcpy(dest2,(char const *)src);
+ __e_acsl_builtin_strcpy(dest2,(char const *)src);
__gen_e_acsl_exit(0);
}
else {
@@ -711,7 +444,7 @@ int main(int argc, char const **argv)
{
pid_t pid_2 = __gen_e_acsl_fork();
if (! pid_2) {
- __gen_e_acsl_strcpy(unalloc_str,(char const *)src);
+ __e_acsl_builtin_strcpy(unalloc_str,(char const *)src);
__gen_e_acsl_exit(0);
}
else {
@@ -725,7 +458,7 @@ int main(int argc, char const **argv)
{
pid_t pid_3 = __gen_e_acsl_fork();
if (! pid_3) {
- __gen_e_acsl_strcpy(const_str,(char const *)src);
+ __e_acsl_builtin_strcpy(const_str,(char const *)src);
__gen_e_acsl_exit(0);
}
else {
@@ -739,7 +472,7 @@ int main(int argc, char const **argv)
{
pid_t pid_4 = __gen_e_acsl_fork();
if (! pid_4) {
- __gen_e_acsl_strcpy(src,(char const *)const_str);
+ __e_acsl_builtin_strcpy(src,(char const *)const_str);
__gen_e_acsl_exit(0);
}
else {
@@ -753,7 +486,7 @@ int main(int argc, char const **argv)
{
pid_t pid_5 = __gen_e_acsl_fork();
if (! pid_5) {
- __gen_e_acsl_strcpy(src,(char const *)src);
+ __e_acsl_builtin_strcpy(src,(char const *)src);
__gen_e_acsl_exit(0);
}
else {
@@ -767,7 +500,7 @@ int main(int argc, char const **argv)
{
pid_t pid_6 = __gen_e_acsl_fork();
if (! pid_6) {
- __gen_e_acsl_strcpy(& dest3[5],(char const *)(dest3));
+ __e_acsl_builtin_strcpy(& dest3[5],(char const *)(dest3));
__gen_e_acsl_exit(0);
}
else {
@@ -781,7 +514,7 @@ int main(int argc, char const **argv)
{
pid_t pid_7 = __gen_e_acsl_fork();
if (! pid_7) {
- __gen_e_acsl_strcpy(& dest3[4],(char const *)(dest3));
+ __e_acsl_builtin_strcpy(& dest3[4],(char const *)(dest3));
__gen_e_acsl_exit(0);
}
else {
@@ -795,7 +528,7 @@ int main(int argc, char const **argv)
{
pid_t pid_8 = __gen_e_acsl_fork();
if (! pid_8) {
- __gen_e_acsl_strncpy(dest1,(char const *)src,(unsigned long)5);
+ __e_acsl_builtin_strncpy(dest1,(char const *)src,(unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -809,7 +542,7 @@ int main(int argc, char const **argv)
{
pid_t pid_9 = __gen_e_acsl_fork();
if (! pid_9) {
- __gen_e_acsl_strncpy(dest1,(char const *)src,(unsigned long)6);
+ __e_acsl_builtin_strncpy(dest1,(char const *)src,(unsigned long)6);
__gen_e_acsl_exit(0);
}
else {
@@ -823,7 +556,8 @@ int main(int argc, char const **argv)
{
pid_t pid_10 = __gen_e_acsl_fork();
if (! pid_10) {
- __gen_e_acsl_strncpy(unalloc_str,(char const *)src,(unsigned long)5);
+ __e_acsl_builtin_strncpy(unalloc_str,(char const *)src,
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -837,7 +571,7 @@ int main(int argc, char const **argv)
{
pid_t pid_11 = __gen_e_acsl_fork();
if (! pid_11) {
- __gen_e_acsl_strncpy(const_str,(char const *)src,(unsigned long)5);
+ __e_acsl_builtin_strncpy(const_str,(char const *)src,(unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -851,7 +585,7 @@ int main(int argc, char const **argv)
{
pid_t pid_12 = __gen_e_acsl_fork();
if (! pid_12) {
- __gen_e_acsl_strncpy(src,(char const *)const_str,(unsigned long)5);
+ __e_acsl_builtin_strncpy(src,(char const *)const_str,(unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -865,7 +599,7 @@ int main(int argc, char const **argv)
{
pid_t pid_13 = __gen_e_acsl_fork();
if (! pid_13) {
- __gen_e_acsl_strncpy(src,(char const *)src,(unsigned long)5);
+ __e_acsl_builtin_strncpy(src,(char const *)src,(unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -879,7 +613,8 @@ int main(int argc, char const **argv)
{
pid_t pid_14 = __gen_e_acsl_fork();
if (! pid_14) {
- __gen_e_acsl_strncpy(& dest3[5],(char const *)(dest3),(unsigned long)5);
+ __e_acsl_builtin_strncpy(& dest3[5],(char const *)(dest3),
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -893,7 +628,8 @@ int main(int argc, char const **argv)
{
pid_t pid_15 = __gen_e_acsl_fork();
if (! pid_15) {
- __gen_e_acsl_strncpy(& dest3[4],(char const *)(dest3),(unsigned long)5);
+ __e_acsl_builtin_strncpy(& dest3[4],(char const *)(dest3),
+ (unsigned long)5);
__gen_e_acsl_exit(0);
}
else {
@@ -908,13 +644,6 @@ int main(int argc, char const **argv)
free((void *)dest1);
free((void *)dest2);
__retres = 0;
- __e_acsl_delete_block((void *)(& unalloc_str));
- __e_acsl_delete_block((void *)(dest3));
- __e_acsl_delete_block((void *)(& dest2));
- __e_acsl_delete_block((void *)(& dest1));
- __e_acsl_delete_block((void *)(& src));
- __e_acsl_delete_block((void *)(& const_str));
- __e_acsl_delete_block((void *)(empty_str));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
index c41b52a79621e44ffd8faabe1a653779c03485f0..61f84cad5685515b4827dd8036335a21b4161a11 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
@@ -68,13 +68,6 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options);
*/
pid_t __gen_e_acsl_fork(void);
-/*@ requires valid_string_s: valid_read_string(s);
- ensures acsl_c_equiv: \result ≡ strlen(\old(s));
- assigns \result;
- assigns \result \from (indirect: *(s + (0 ..)));
- */
-size_t __gen_e_acsl_strlen(char const *s);
-
/*@ requires valid_string_s: valid_read_string(s);
assigns \result;
assigns \result
@@ -149,18 +142,6 @@ char *__gen_e_acsl_strdup(char const *s)
}
}
-/*@ requires valid_string_s: valid_read_string(s);
- ensures acsl_c_equiv: \result ≡ strlen(\old(s));
- assigns \result;
- assigns \result \from (indirect: *(s + (0 ..)));
- */
-size_t __gen_e_acsl_strlen(char const *s)
-{
- size_t __retres;
- __retres = __e_acsl_builtin_strlen(s);
- return __retres;
-}
-
/*@ ensures
result_ok_child_or_error:
\result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1;
@@ -390,7 +371,7 @@ int main(int argc, char const **argv)
pid_t pid = __gen_e_acsl_fork();
if (! pid) {
size_t tmp_1;
- tmp_1 = __gen_e_acsl_strlen((char const *)empty_str);
+ tmp_1 = __e_acsl_builtin_strlen((char const *)empty_str);
len = tmp_1 != (size_t)0;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
@@ -407,7 +388,7 @@ int main(int argc, char const **argv)
pid_t pid_0 = __gen_e_acsl_fork();
if (! pid_0) {
size_t tmp_3;
- tmp_3 = __gen_e_acsl_strlen((char const *)heap_str);
+ tmp_3 = __e_acsl_builtin_strlen((char const *)heap_str);
len = tmp_3 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
@@ -424,7 +405,7 @@ int main(int argc, char const **argv)
pid_t pid_1 = __gen_e_acsl_fork();
if (! pid_1) {
size_t tmp_5;
- tmp_5 = __gen_e_acsl_strlen((char const *)(stack_str));
+ tmp_5 = __e_acsl_builtin_strlen((char const *)(stack_str));
len = tmp_5 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
@@ -441,7 +422,7 @@ int main(int argc, char const **argv)
pid_t pid_2 = __gen_e_acsl_fork();
if (! pid_2) {
size_t tmp_7;
- tmp_7 = __gen_e_acsl_strlen((char const *)const_str);
+ tmp_7 = __e_acsl_builtin_strlen((char const *)const_str);
len = tmp_7 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
@@ -460,7 +441,7 @@ int main(int argc, char const **argv)
pid_t pid_3 = __gen_e_acsl_fork();
if (! pid_3) {
size_t tmp_9;
- tmp_9 = __gen_e_acsl_strlen((char const *)heap_str);
+ tmp_9 = __e_acsl_builtin_strlen((char const *)heap_str);
len = tmp_9 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
@@ -477,7 +458,7 @@ int main(int argc, char const **argv)
pid_t pid_4 = __gen_e_acsl_fork();
if (! pid_4) {
size_t tmp_11;
- tmp_11 = __gen_e_acsl_strlen((char const *)(stack_str));
+ tmp_11 = __e_acsl_builtin_strlen((char const *)(stack_str));
len = tmp_11 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
@@ -495,7 +476,7 @@ int main(int argc, char const **argv)
pid_t pid_5 = __gen_e_acsl_fork();
if (! pid_5) {
size_t tmp_13;
- tmp_13 = __gen_e_acsl_strlen((char const *)heap_str);
+ tmp_13 = __e_acsl_builtin_strlen((char const *)heap_str);
len = tmp_13 != (size_t)7;
if (len) __gen_e_acsl_abort();
__gen_e_acsl_exit(0);
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
index c671cb08c98861ff4f19e9bb3975242b6eadd4c7..cf30aa9d16ac57ed095e1a94371f345ed07b6467 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
@@ -8,79 +8,6 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strcat':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strncat':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:432: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:427: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:433: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:441: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
- Some assumes clauses could not be translated.
- Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:430: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:437: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:437: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:411: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:412: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:413: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:410: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:416: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:419: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:420: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
@@ -102,5 +29,3 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/unistd.h:859: Warning:
function __gen_e_acsl_fork: postcondition 'result_ok_child_or_error' got status unknown.
-[eva:alarm] FRAMAC_SHARE/libc/string.h:416: Warning:
- function __gen_e_acsl_strcat: postcondition 'sum_of_lengths' got status unknown.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
index f6cbb2f80f2b420d8c1f639511a592fe4f85adec..0b3334f947372e5176288fef98afcaff4892b581 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
@@ -14,12 +14,6 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strcmp':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strncmp':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `strdup':
the generated program may miss memory instrumentation
if there are memory-related annotations.
@@ -49,32 +43,6 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:480: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:147: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:148: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:147: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:150: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:140: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:140: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:143: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
index b36d6936026e912519fc77c972b7cbd084fb1fce..8825987199ec9197f0dde125be642354da7b9bfc 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
@@ -8,12 +8,6 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strncpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `strdup':
the generated program may miss memory instrumentation
if there are memory-related annotations.
@@ -43,49 +37,6 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:480: 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 construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:366: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning:
- Some assumes clauses could not be translated.
- Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:376: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:354: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:355: Warning:
- E-ACSL construct `logic functions performing read accesses'
- 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:354: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:360: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
index b1dce3cca73734a26bbe419c6e8ebece8913c525..77c57316bb0d811d79a914934545aae5a9efa4cc 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
@@ -11,9 +11,6 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] Warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
[e-acsl] Warning: annotating undefined function `strdup':
the generated program may miss memory instrumentation
if there are memory-related annotations.
@@ -43,16 +40,6 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:480: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:128: Warning:
- E-ACSL construct `logic functions with labels' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:128: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:130: Warning:
- E-ACSL construct `logic functions performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/unistd.h:856: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.