search

project-oak / rust-verification-tools

RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
https://project-oak.github.io/rust-verification-tools/
Apache License 2.0
274 stars 37 forks source link

Add --replace-backend-flags to cargo-verify #118

Closed fshaked closed 3 years ago

fshaked commented 3 years ago

Also add Handlebar templates to --backend-flags.

fshaked commented 3 years ago

@alastairreid, note that --replace-backend-flags doesn't pass Opt::args to the verified program, because there is no simple way to do it (will need a handlebar template that expands to Vec, or something like that). The user should pass those through --backend-flags instead, if she uses --replace-backend-flags.

alastairreid commented 3 years ago

Just before I dive into the code...

Passing args to the program is a really useful capability - it's fundamental for finding bugs in standalone programs like uutils/coreutils. So I would really not like to lose that capability.

alastairreid commented 3 years ago

Following on from my previous comment... If this changes how arguments are passed to programs, does this require a change to scripts/regression-tests or do those tests (especially of demos/simple/argv) still pass?

fshaked commented 3 years ago

If this changes how arguments are passed to programs, does this require a change to scripts/regression-tests or do those tests (especially of demos/simple/argv) still pass?

This PR doesn't change anything if you don't use --replace-backend-flags on the command line. So script/regression-tests should be unaffected.

I will add to regression-tests something that uses --replace-backend-flags.