Useful error message for non-terminating symbolic execution?

GaloisInc / saw-script

The SAW scripting language.

BSD 3-Clause "New" or "Revised" License

433 stars 63 forks source link

Useful error message for non-terminating symbolic execution? #56

Open atomb opened 8 years ago

atomb commented 8 years ago

Various examples fail to symbolically terminate in various simulators. Sometimes the JSS and LSS engines fail to terminate. Sometimes, especially when simulating Cryptol, the symbolic backends to SAWCore can fail to terminate. Is there a way we can give useful feedback that it seems like simulation is failing to terminate? The saw-script integration test test0000 demonstrates this on a recursive term from Cryptol when using the ABC backend.

atomb commented 3 years ago

Crucible now has an option for simulator timeouts, and we should make that available in SAW.