Repository navigation
Can we remove "assertion failed" from successful assertions? #189
Description
When viewing a CBMC trace from RMC, a user might see something like this:
[main.assertion.1] line 28 assertion failed: std_string == \"1\": FAILURE
[main.assertion.2] line 30 assertion failed: weird_string == \"w\": SUCCESS
The top assertion is failing and the bottom is provably true, but both have assertion failed. I think this is just an artifact of how Rust proper prints assertions; it would be nice to remove this for CBMC usability.
Activity
adpaco commentedon Jun 11, 2021
Yes, I think these come specifically from
compiler/rustc_middle/src/mir/mod.rs.It is true that it may be confusing at times but RMC has nothing to do with this: the assertion text comes from MIR, the verification output comes from CBMC.