Skip to content
Snippets Groups Projects
Commit c70ccbbe authored by Andre Maroneze's avatar Andre Maroneze Committed by Virgile Prevosto
Browse files

[Eva] improve message for check of invalid properties

parent aceb64d1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/value/engine/transfer_logic.ml
+ 1
− 1
View file @ c70ccbbe
...@@ -629,7 +629,7 @@ module Make ...@@ -629,7 +629,7 @@ module Make
"valid" "valid"
| Alarmset.False, `True -> | Alarmset.False, `True ->
change_status Property_status.False_if_reachable; change_status Property_status.False_if_reachable;
"invalid (stopping propagation)" "invalid" ^ (if reduce then " (stopping propagation)" else "")
| Alarmset.False, `Unknown -> | Alarmset.False, `Unknown ->
change_status Property_status.False_if_reachable; change_status Property_status.False_if_reachable;
"invalid" "invalid"
......
tests/value/oracle/logic.res.oracle
+ 1
− 2
View file @ c70ccbbe
...@@ -253,8 +253,7 @@ ...@@ -253,8 +253,7 @@
[eva:alarm] tests/value/logic.c:301: Warning: assertion got status unknown. [eva:alarm] tests/value/logic.c:301: Warning: assertion got status unknown.
[eva:alarm] tests/value/logic.c:303: Warning: [eva:alarm] tests/value/logic.c:303: Warning:
assertion got status invalid (stopping propagation). assertion got status invalid (stopping propagation).
[eva:alarm] tests/value/logic.c:306: Warning: [eva:alarm] tests/value/logic.c:306: Warning: check got status invalid.
check got status invalid (stopping propagation).
[eva] tests/value/logic.c:307: Frama_C_show_each_reachable: {42} [eva] tests/value/logic.c:307: Frama_C_show_each_reachable: {42}
[eva] Recording results for check_and_assert [eva] Recording results for check_and_assert
[eva] Done for function check_and_assert [eva] Done for function check_and_assert
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment