diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle index c3e129c735e51c8931c704fd34b2b71e7c26cbb3..8e21a5839c9ad6af6a30335d8452cad0233b17a5 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle @@ -1,6 +1,8 @@ [e-acsl] beginning translation. [e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_nstring because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:284: Warning: + E-ACSL construct `labeled \valid_read' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning: E-ACSL construct `logic functions or predicates performing read accesses' diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle index aacd127bce378a5ddba8a647e7037b3eb04e679d..a33ac7b284bde4a5fa2360f566b232758a18102e 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle @@ -9,10 +9,14 @@ E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle index 180520653f74553d5bf54704909ad132cdbedb7b..23aaebecb39a3031654d59684ee79c701659ffab 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle @@ -19,13 +19,18 @@ [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: Some assumes clauses could not be translated. @@ -36,9 +41,12 @@ [e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning: +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning: diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle index 82dd3516a25051fa56208f746f8fb9f3393b1df3..4d60df21bef6e71b55d35f9d70e3f0a80081b3b3 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle @@ -14,13 +14,18 @@ [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: Some assumes clauses could not be translated. @@ -31,9 +36,12 @@ [e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning: +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning: diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle index 2c826d7c60a6c436bd933ff1224eb6994d5f085e..08078ac2fc031bffaaa0258a46f0b6d74806cc7f 100644 --- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle +++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle @@ -17,13 +17,18 @@ [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning: Some assumes clauses could not be translated. @@ -34,9 +39,12 @@ [e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. -[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning: +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning: diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle index 7ea32d04a840db852dfa49087dfe4c53929d64ae..1dfe0498bed0112fac1d2f66b88acc3283fc62d6 100644 --- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle +++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle @@ -46,7 +46,10 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:484: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:483: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle index 7ea32d04a840db852dfa49087dfe4c53929d64ae..1dfe0498bed0112fac1d2f66b88acc3283fc62d6 100644 --- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle +++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle @@ -46,7 +46,10 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:484: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:483: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. diff --git a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle index ab3b47adbce2287a98ec04fdc931609b0c526c45..7becfbbc7834eb8af9c7dc3946ae0b88d8d1a0b0 100644 --- a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle +++ b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle @@ -1,4 +1,6 @@ [e-acsl] beginning translation. +[e-acsl] functions_contiki.c:27: Warning: + no assigns clause generated for function length because pointers as arguments is not yet supported [e-acsl] functions_contiki.c:27: Warning: E-ACSL construct `logic functions with labels' is not yet supported. Ignoring annotation. 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 81d4fa06f45a8688ea85ac8c638930365601d0c3..1eaec8a8f39741aa8937f21524340247e6280696 100644 --- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle +++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle @@ -21,7 +21,10 @@ the generated program may miss memory instrumentation if there are memory-related annotations. [e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning: E-ACSL construct `logic functions or predicates performing read accesses' @@ -39,7 +42,8 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:173: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:176: Warning: E-ACSL construct `datacons' is not yet supported. Ignoring annotation. @@ -56,7 +60,8 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:180: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:181: Warning: E-ACSL construct @@ -66,7 +71,8 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle index 96af966113561ba992b41632cec3373bcb51b18c..7b2ac7b3ecfaaee74530b636fd6fe37f6ab863e8 100644 --- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle +++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle @@ -9,10 +9,14 @@ E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:150: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:151: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdio.h:149: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. 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 009670d149431e5e85ab761f5e00bc24266578b2..673b705e2c742c0cc5a1f353cf2b6fb2f9771c51 100644 --- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle +++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle @@ -1,5 +1,7 @@ [e-acsl] beginning translation. [e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning: + no assigns clause generated for function valid_or_empty because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/string.h:49: Warning: E-ACSL construct `predicates with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning: @@ -11,6 +13,8 @@ E-ACSL construct `predicates with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:121: 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:52: Warning: E-ACSL construct `predicates with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning: diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle index 17287256d000087ec770a71077c33f99fe4eb014..67886b4500ae16bb187e07dbbe1e3b244bd84636 100644 --- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle +++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle @@ -1,15 +1,24 @@ [e-acsl] beginning translation. [e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_nstring because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:284: Warning: + E-ACSL construct `labeled \valid_read' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning: E-ACSL construct `logic functions or predicates performing read accesses' @@ -40,10 +49,12 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:424: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning: E-ACSL construct `logic functions or predicates performing read accesses' @@ -65,7 +76,7 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `labeled \valid_read' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning: E-ACSL construct `logic functions or predicates performing read accesses' @@ -90,7 +101,8 @@ is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning: E-ACSL construct `logic functions or predicates performing read accesses' diff --git a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle index 3243990e03e4a383f2437a0bc3a1af4d4eecb198..411c0b7ba798d3afe689edf886fe08f7a6ca47b5 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle @@ -3,7 +3,10 @@ the generated program may miss memory instrumentation if there are memory-related annotations. [e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle index 9116a25386a2230fcd07d7d92fa9fc5c86bfc55f..ee68e8606cdbd0d90a5f6ca011b556bb39421112 100644 --- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle @@ -5,10 +5,12 @@ [e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:710: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:717: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:700: Warning: Some assumes clauses could not be translated. diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle index 7782e4d751012aa9caf256ce468ad0ff2e56eb57..1c9dd482c25fd5d5c7013fb3714d6bc6e97cca56 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle +++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle @@ -3,7 +3,10 @@ the generated program may miss memory instrumentation if there are memory-related annotations. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:521: Warning: - E-ACSL construct `predicates with labels' is not yet supported. + no assigns clause generated for function valid_read_string because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning: + E-ACSL construct `logic functions or predicates performing read accesses' + is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/stdlib.h:520: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. 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 d7c3cd0d2e1d9b317764e8d378e42554002fb2dd..9106573e05febb9ac0e542e9402eeab84e00c929 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 @@ -1,5 +1,7 @@ [e-acsl] beginning translation. [e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning: + no assigns clause generated for function valid_or_empty because pointers as arguments is not yet supported +[e-acsl] FRAMAC_SHARE/libc/string.h:49: Warning: E-ACSL construct `predicates with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning: @@ -11,6 +13,8 @@ E-ACSL construct `predicates with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:96: 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:52: Warning: E-ACSL construct `predicates with labels' is not yet supported. Ignoring annotation. [e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning: