Skip to content

Commit c065104

Browse files
committed
test: split standard and contract proofs since kind is supported
1 parent 8ee870d commit c065104

File tree

1 file changed

+10
-13
lines changed

1 file changed

+10
-13
lines changed

tests/kani_list.rs

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use distributed_verification::KaniList;
1+
use distributed_verification::{KaniList, Kind};
22
use std::{collections::HashMap, process::Command};
33

44
mod utils;
@@ -58,15 +58,15 @@ fn merge(list: &KaniList, v_ser_fun: &[SerFunction]) {
5858
let map: HashMap<_, _> = v_ser_fun
5959
.iter()
6060
.enumerate()
61-
.map(|(idx, f)| ((&*f.func.file, &*f.func.name), idx))
61+
.map(|(idx, f)| ((&*f.func.file, &*f.func.name), (idx, f.kind)))
6262
.collect();
6363

6464
// check all standard proofs are in distributed-verification json
6565
for (path, proofs) in &list.standard_harnesses {
6666
for proof in proofs {
6767
let key = (path.as_str(), proof.as_str());
68-
let idx = map.get(&key).unwrap();
69-
dbg!(idx);
68+
let val = map.get(&key).unwrap();
69+
dbg!(val);
7070
}
7171
}
7272

@@ -79,15 +79,12 @@ fn merge(list: &KaniList, v_ser_fun: &[SerFunction]) {
7979
}
8080
}
8181

82-
// douoble check
83-
for &(path, proof) in map.keys() {
84-
// FIXME: split standard and contract proofs if kind supported
85-
match list.standard_harnesses.get(path) {
86-
Some(set) => _ = set.get(proof).unwrap(),
87-
None => match list.contract_harnesses.get(path) {
88-
Some(set) => _ = set.get(proof).unwrap(),
89-
None => panic!("{path} {proof} does not exist"),
90-
},
82+
// double check
83+
for (&(path, proof), &(_, kind)) in &map {
84+
let harnesses = match kind {
85+
Kind::Standard => &list.standard_harnesses[path],
86+
Kind::Contract => &list.contract_harnesses[path],
9187
};
88+
_ = harnesses.get(proof).unwrap();
9289
}
9390
}

0 commit comments

Comments
 (0)