Skip to content
Snippets Groups Projects
Commit 29224cbe authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Remove contraction in warning message

parent ce509e3d
No related branches found
No related tags found
No related merge requests found
...@@ -595,7 +595,7 @@ let check_complete_and_disjoint kf kinstr env contract = ...@@ -595,7 +595,7 @@ let check_complete_and_disjoint kf kinstr env contract =
Cil.CurrentLoc.set contract.location; Cil.CurrentLoc.set contract.location;
Options.warning Options.warning
~current:true ~current:true
"@[Some assumes clauses couldn't be translated.@ Ignoring complete and \ "@[Some assumes clauses could not be translated.@ Ignoring complete and \
disjoint behaviors annotations.@]"; disjoint behaviors annotations.@]";
env env
end end
......
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
...@@ -37,7 +37,7 @@ ...@@ -37,7 +37,7 @@
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
...@@ -55,7 +55,7 @@ ...@@ -55,7 +55,7 @@
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:365: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:471: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
...@@ -60,7 +60,7 @@ ...@@ -60,7 +60,7 @@
E-ACSL construct `logic functions with labels' is not yet supported. E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning: [e-acsl] FRAMAC_SHARE/libc/string.h:160: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
...@@ -11,7 +11,7 @@ ...@@ -11,7 +11,7 @@
E-ACSL construct `predicate performing read accesses' is not yet supported. E-ACSL construct `predicate performing read accesses' is not yet supported.
Ignoring annotation. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: [e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
Some assumes clauses couldn't be translated. Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations. Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning: [e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported. E-ACSL construct `assigns clause in behavior' is not yet supported.
......
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