Skip to content
Snippets Groups Projects
Commit d8810a08 authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] fix oracle

parent 14bff652
Branches stable/copper
Tags 0.7
No related merge requests found
...@@ -24,10 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time ...@@ -24,10 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid. tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown. tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown. tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
......
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