Skip to content

Commit 03388f3

Browse files
committed
feat: define KaniList for parsing the json output of kani list
1 parent 967230e commit 03388f3

File tree

3 files changed

+30
-1
lines changed

3 files changed

+30
-1
lines changed

Cargo.lock

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ edition = "2024"
77
clap = { version = "4.5.35", features = ["derive"] }
88
serde = { version = "1", features = ["derive"] }
99
serde_json = { version = "1", features = ["preserve_order"] }
10-
indexmap = "2.9.0"
10+
indexmap = { version = "2.9.0", features = ["serde"] }
1111

1212
# error handling
1313
eyre = "0.6"

src/lib.rs

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
use indexmap::{IndexMap, IndexSet};
12
use serde::{Deserialize, Serialize};
23

34
/// A Rust funtion with its file source, attributes, and raw function content.
@@ -83,3 +84,30 @@ pub fn kani_path() -> String {
8384
assert!(std::fs::exists(&path).unwrap());
8485
path
8586
}
87+
88+
/// Output of `kani list` command.
89+
#[derive(Debug, Serialize, Deserialize, Clone)]
90+
#[serde(rename_all = "kebab-case")]
91+
pub struct KaniList {
92+
pub kani_version: String,
93+
pub file_version: String,
94+
pub standard_harnesses: IndexMap<String, IndexSet<String>>,
95+
pub contract_harnesses: IndexMap<String, IndexSet<String>>,
96+
pub contracts: IndexSet<ContractedFunction>,
97+
pub totals: Total,
98+
}
99+
100+
#[derive(Debug, Serialize, Deserialize, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
101+
pub struct ContractedFunction {
102+
pub function: String,
103+
pub file: String,
104+
pub harnesses: Vec<String>,
105+
}
106+
107+
#[derive(Debug, Serialize, Deserialize, Clone)]
108+
#[serde(rename_all = "kebab-case")]
109+
pub struct Total {
110+
pub standard_harnesses: usize,
111+
pub contract_harnesses: usize,
112+
pub functions_under_contract: usize,
113+
}

0 commit comments

Comments
 (0)