Bloated MIR due to panic code in standard library #2835
Description
Proposed change:
Reconsider the way in which panic code is handled.
For example, when an assert statement is added, the panic call is ignored. This, however, is not the case when there are panic calls in standard library functions that are used in a verified program.
Motivation:
See the attached example, which is a variant of the switchInt example from Kani's tests directory.
The use of iterator pulls in standard library code that calls the panic function. It seems that due to that, a lot of code that is irrelevant for verification. This causes the internal go-to representation in CBMC to include a lot of irrelevant information. This may hinder performance.
main1.rs.zip