Automatic tests for CPA-witness2test
There are currently no automatic tests for CPA-w2t (scripts/cpa_witness2test.py
).
Tests should be written for the different supported memsafety
properties
as well as for unreach-call
with target functions reach_error
, __VERIFIER_error
and some additional, arbitrary target function.
Both small unit tests and some integration tests may be useful.