Skip to content
Snippets Groups Projects
Commit 2491fba9 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[e-acsl] update error message in oracle

- these tests do not use anymore datacons, another error is thus triggered
parent 90dc6fc6
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
......@@ -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:
......
......@@ -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:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment