From e2a92c7827eda1d7c7aaa8c140c432aca4c3f99a Mon Sep 17 00:00:00 2001 From: Thibaut Benjamin <thibaut.benjamin@gmail.com> Date: Mon, 3 Oct 2022 17:47:01 +0200 Subject: [PATCH] [e-acsl] update oracles --- .../tests/bts/oracle/bts2252.res.oracle | 4 ++- .../bts/oracle/issue-eacsl-40.res.oracle | 8 ++++-- .../tests/builtin/oracle/strcmp.res.oracle | 18 ++++++++---- .../tests/builtin/oracle/strcpy.res.oracle | 18 ++++++++---- .../tests/builtin/oracle/strlen.res.oracle | 18 ++++++++---- .../oracle/parallel_threads.res.oracle | 5 +++- .../oracle/threads_debug.res.oracle | 5 +++- .../oracle/functions_contiki.res.oracle | 2 ++ .../tests/format/oracle/printf.res.oracle | 14 +++++++--- .../e-acsl/tests/libc/oracle/file.res.oracle | 8 ++++-- .../e-acsl/tests/libc/oracle/mem.res.oracle | 4 +++ .../e-acsl/tests/libc/oracle/str.res.oracle | 28 +++++++++++++------ .../tests/memory/oracle/mainargs.res.oracle | 5 +++- .../tests/memory/oracle/memalign.res.oracle | 6 ++-- .../tests/temporal/oracle/t_getenv.res.oracle | 5 +++- .../tests/temporal/oracle/t_memcpy.res.oracle | 4 +++ 16 files changed, 114 insertions(+), 38 deletions(-) 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 c3e129c735e..8e21a5839c9 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 aacd127bce3..a33ac7b284b 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 180520653f7..23aaebecb39 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 82dd3516a25..4d60df21bef 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 2c826d7c60a..08078ac2fc0 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 7ea32d04a84..1dfe0498bed 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 7ea32d04a84..1dfe0498bed 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 ab3b47adbce..7becfbbc783 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 81d4fa06f45..1eaec8a8f39 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 96af9661135..7b2ac7b3ecf 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 009670d1494..673b705e2c7 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 17287256d00..67886b4500a 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 3243990e03e..411c0b7ba79 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 9116a25386a..ee68e8606cd 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 7782e4d7510..1c9dd482c25 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 d7c3cd0d2e1..9106573e05f 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: -- GitLab