diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle index 6ea6f74635e3967de6c3b6d100e358da724b2b46..61c1a73899c027eb2f8c8723e43d98904a83659c 100644 --- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle @@ -46,9 +46,13 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:196: Warning: - E-ACSL construct `datacons' is not yet supported. Ignoring annotation. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:204: Warning: - E-ACSL construct `datacons' is not yet supported. Ignoring annotation. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:192: Warning: Some assumes clauses could not be translated. Ignoring complete and disjoint behaviors annotations. diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle index d6ab15b134feef6c04847d8603b2d0b999f4f181..66d16674c03c91bd18f51a25b836c0cfc23e445f 100644 --- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle +++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle @@ -7,7 +7,9 @@ E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning: - E-ACSL construct `datacons' is not yet supported. Ignoring annotation. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:138: Warning: no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/string.h:137: Warning: diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle index c9851298903b4367411d8b16bb63c8b09e3a5e65..4e14e33da388847b5440e474374c1e29322cfdaa 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle @@ -7,7 +7,9 @@ E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning: - E-ACSL construct `datacons' is not yet supported. Ignoring annotation. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. + Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning: no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported [e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning: