Convert implicit Rust assertions into smack assertions without including the crate

smackers / smack

SMACK Software Verifier and Verification Toolchain

http://smackers.github.io

Other

432 stars 82 forks source link

Convert implicit Rust assertions into smack assertions without including the crate #739

Open keram88 opened 3 years ago

keram88 commented 3 years ago

Currently the following:

fn main() {
    assert!(0==1);
}

will pass in SMACK because this generates an assertion failure in the standard library. This should require checking for the symbols generated from here to convert into the relevant __VERIFIER_assert call.