[herd] Delay errors and warning until after filtering by model. #686
Conversation
maranget
force-pushed
the
herd-delay-more
branch
from
b187f4e to
cbe3b61
Compare
|
I guess this PR is an answer to PR #684 and issue #646. After digging in old code, I tend to think that errors have never been delayed that far for no specific reason. More precisely, commit 94dd2ac introduced the (unsolved) equations, including I am tempted to merge this PR. |
| @@ -2,7 +2,7 @@ | |||
| (* the diy toolsuite *) | |||
| (* *) | |||
| (* Jade Alglave, University College London, UK. *) | |||
| (* Luc Maranget, INRIA Paris-Rocquencourt, France. *) | |||
There was a problem hiding this comment.
You might want to revert this before merging.
| @@ -1117,7 +1117,7 @@ let match_reg_events es = | |||
| PP.show_es_rfm test es rfm ; | |||
| prerr_endline "Unsolvable system" | |||
| end ; | |||
| assert (rfmap_is_cyclic es rfm); | |||
| assert (true || rfmap_is_cyclic es rfm); | |||
There was a problem hiding this comment.
should we remove this assert, or did you it intentionally?
There was a problem hiding this comment.
I'd like to keep the assert as it was before, thanks for your acute eye.
maranget
force-pushed
the
herd-delay-more
branch
from
cbe3b61 to
2da38eb
Compare
|
LGTM. Out of curiousity: what prompts the change in the unit tests? (Specifically, the need to specify the "DontCheckMixed" variant.) |
|
Hi @artkhyzha. The tests contain (at least!) two fatal errors: (1) the masking attempt of a symbolic locations and (2) accesses of different sizes of the same location. Before this PR the specific error about illegal masking was raised at the end of the second solving phase and error (1) was found first. After this PR the checking of (1) has moved beyond the point where (2) is checked (point (2) is after equation solving, while (1) is after model application). However it is possible to disable the checking of (2), with |
|
Ah, I see, thank you for the explanation! |
maranget
force-pushed
the
herd-delay-more
branch
from
2da38eb to
3ec6bc2
Compare
That way errors and warning from execution candidates rejected by the model do not show up. Some test error output changed for mundane reasons, they are updated as part of this commit.
maranget
force-pushed
the
herd-delay-more
branch
from
3ec6bc2 to
eb991db
Compare
|
Merged, thanks @relokin, @artkhyzha |
[herd] Delay errors and warning until after filtering by model. That way errors and warning from execution candidates rejected by the model do not show up.
That way errors and warning from execution candidates rejected by the model do not show up.