draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Add comparative tests to sample_binaries/user_func_specs #288

Closed gltrost closed 3 years ago

gltrost commented 3 years ago

Currently, the flag --user-func-specs is only tested in the single-program case, but not in the comparative case. This branch adds two tests, sub_spec_3/run_wp_comp.sh and sub_spec_1/run_wp_1.sh to the comparative test, where adding the --user-func-specs flag changes a SAT result to an UNSAT result in both new cases.