#235 adds the test src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs, which has this chunk:
let dest_slice : &[u8] = from_raw_parts(dest, l);
let dest_as_str : &str= str::from_utf8(dest_slice).unwrap();
assert!(dest_as_str.len() == l);
With failures verification with:
[...copy_empty_string_by_intrinsic.assertion.2] line 1035 unreachable code: FAILURE
[...copy_empty_string_by_intrinsic.assertion.1] line 1037 a panicking function std::result::unwrap_failed is invoked: FAILURE
[...copy_string.assertion.2] line 28 assertion failed: dest_as_str.len() == l: FAILURE
#235 adds the test
src/test/cbmc/Strings/copy_empty_string_by_intrinsic_fixme.rs, which has this chunk:With failures verification with: