Closed nchong-at-aws closed 1 year ago
This also fails:
pub fn main() {
assert!("2021".parse::<u32>().unwrap() == 2021);
}
Experiment with switching to running goto-instrument
with --generate-function-body assert-false-assume-false
.
We should also replace the call to the function with codegen_unimplemented so that we get a proper error message on what is unsupported.
@zhassan-aws Do you mind adding taking a look at this one while you are looking into adding compiler warnings to codegen_unimplemented? Thanks
Summarizing a discussion from Friday 4/8:
"2021".parse::<u32>()
, the failure is due to a missing definition for an std
function, which is caused by Kani not linking the standard library.Check 3: _ZN4core3num60_$LT$impl$u20$core..str..traits..FromStr$u20$for$u20$u32$GT$8from_str17hbdfd7c3b5dc0b1b5E.assertion.1
- Status: FAILURE
- Description: "assertion false"
- Location: Unknown File in function _ZN4core3num60_$LT$impl$u20$core..str..traits..FromStr$u20$for$u20$u32$GT$8from_str17hbdfd7c3b5dc0b1b5E
std
crate when compiling a file/package, or including the symtab/goto binary of the std
crate in the Kani release package--reachability-slice
or via implementing our own linker/slicer) to aggressively prune the code that gets analyzed (much more than what is pruned by CBMC's --drop-unused-functions
).I believe this issue has been fixed by the MIR Linker (#1588). The following test has been added to our regression to ensure we can correctly handle parse
function.
Unfortunately, I wasn't able to run the original test from this issue in a reasonable time. The test no longer fail, but symbolic execution is just taking too long. Maybe we should create a different issue to track the performance part of it.
I tried this code, which is a slightly modified example from the proptest book (https://altsysrq.github.io/proptest-book/proptest/getting-started.html):
using the following command line invocation:
with RMC version: a728d8d41a15c3c71795351b23eddd4ce8b54cc9
I expected to see this happen: VERIFICATION SUCCESSFUL
Instead, this happened: VERIFICATION FAILED