utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
51 stars 24 forks source link

`expectedError` and console output #1201

Open pieter-bos opened 1 month ago

pieter-bos commented 1 month ago

I've had some trouble in the past explaining that expectedError is a testing fixture yet also causes the error to be "inverted" in the console output. That is: an example that should fail contains some expectedError declaration, and therefore outputs nothing. I think it's more intuitive that this marker is only treated as an inverting error in the testing framework, but leaves the console output alone for didactic purposes.

bobismijnnaam commented 1 month ago

Possibly the error output could be modified with "expected error", to be clear that this is a succesful failure :)