GaloisInc / crucible

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

`crucible-mir`: Report line number when MIR `Assert` fails #1139

Open spernsteiner opened 9 months ago

spernsteiner commented 9 months ago

When overflow checking is enabled (the default for debug builds), rustc emits MIR TerminatorKind::Assert to assert that overflow did not occur. Currently, our translation of Assert only reports the message from the MIR, which will be something generic like "attempted to add with overflow". It would be helpful to also provide the line number or other source information so the user can more easily identify which operation it was that overflowed.