search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
629 stars 42 forks source link

crux-mir tests throw away information #1229

Open sauclovian-g opened 1 month ago

sauclovian-g commented 1 month ago

I had some problems running the crux-mir tests (now solved) that revealed the following points:

  1. Even once you persuade cabal to let you run the test harness by hand, there's no way to get that program to print the subprogram invocations (of mir-json) that it attempts. A -v option would be appropriate, probably.
  2. The test program throws away stderr when it runs mir-json, so if mir-json fails it's impossible to tell why. The actual problem I was having was that the rust invocations inside mir-json were failing, but the errors they printed were being lost. Test infrastructure should not under any circumstances throw away output of things that fail -- otherwise you have no hope of being able to diagnose the failure.