Skip to content

Commit 29e1def

Browse files
Update goto-checker docs
w.r.t. cover goals verifier
1 parent 5a31e59 commit 29e1def

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/goto-checker/README.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,11 @@ There are the following variants of goto verifiers at the moment:
6262
\ref all_properties_verifier_with_trace_storaget,
6363
\ref all_properties_verifiert does not require to store any traces.
6464
A trace ends at a violated property.
65+
* \ref cover_goals_verifiert : Determines the status of all properties,
66+
but full traces with potentially several failing properties
67+
(e.g. coverage goals) are kept.
68+
The reporting uses 'goals' rather than 'property' terminology. I.e.
69+
a failing property means 'success' and a passing property 'failed'.
6570

6671
There are the following variants of incremental goto checkers at the moment:
6772
* \ref multi_path_symex_checkert : The default mode of goto-symex. It explores

0 commit comments

Comments
 (0)