Commit 0ce0f79
committed
Turn verbose Kani run into JSON
Given a run of Kani on the standard library with `--verbose` (and,
typically, `autoharness`) enabled this produces a machine-processable
JSON result via
```
python3 log_parser.py \
--kani-list-file kani-list.json \
--analysis-results-dir std_lib_analysis/results/ \
verification.log -o results.json
```
where each entry in the resulting JSON array is of the form
```
{
"thread_id": int,
"result": {
"harness": string,
"is_autoharness": bool,
"autoharness_result": string,
"with_contract": bool,
"crate": string,
"function": string,
"function_safeness": string,
"file_name": string,
"n_failed_properties": int,
"n_total_properties": int,
"result": string,
"time": string,
"output": array
}
}
```
With the help of `jq` one can then conveniently compute various metrics,
e.g.,
```
jq 'map(select(.result.result == "SUCCESSFUL" and
.result.is_autoharness == true and
.result.crate == "core" and
.result.function_safeness == "unsafe" and
.result.with_contract == true)) | length' results.json
```
to find the number of successfully-verified contracts of unsafe
functions in crate `core` that were verified using automatically
generated harnesses.1 parent 659982c commit 0ce0f79
1 file changed
+403
-0
lines changed
0 commit comments