To test either the Free PCS or the Coupling Graph implementation, check out this branch and then use the following commands:
To try the FreePCS (owned stuff only) using the following command:
./x.py run --bin prusti-rustc -- --edition=2021 -Z dump_mir_dataflow -Ptest_free_pcs=true ./path/to/rust/file.rs
and make sure to put the following in the .rs file:
#![feature(core_intrinsics, rustc_attrs)] // At the top of the file
#[rustc_mir(borrowck_graphviz_postflow="log/analysis/foo/foo.dot")] // Above any fn you want to dump info on
fn foo( ... ) { ... }
Which will create a log/analysis/foo/free_pcs_foo.dot file (along with others from the compiler analyses)
To try out the Coupling Graph (borrows only), use the following:
./x.py run --bin prusti-rustc -- --edition=2021 -Z dump_mir_dataflow -Ptest_coupling_graph=true ./path/to/rust/file.rs
Which will dump the graphs under log/coupling (a combined .dot with all the graphs lives under log/coupling/all.dot). While looking at those, it can be useful to open e.g. log/analysis/foo/borrows_foo.dot in parallel to inspect the CFG.
To test either the Free PCS or the Coupling Graph implementation, check out this branch and then use the following commands:
To try the FreePCS (owned stuff only) using the following command:
and make sure to put the following in the
.rs
file:Which will create a
log/analysis/foo/free_pcs_foo.dot
file (along with others from the compiler analyses)To try out the Coupling Graph (borrows only), use the following:
Which will dump the graphs under
log/coupling
(a combined .dot with all the graphs lives underlog/coupling/all.dot
). While looking at those, it can be useful to open e.g.log/analysis/foo/borrows_foo.dot
in parallel to inspect the CFG.TODO: