distributed_verification/db.rs
1use crate::{BoxStr, InstKind, MacroBacktrace, ProofKind};
2use serde::{Deserialize, Serialize};
3
4/// All information for a function stored in db.
5#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord, Hash)]
6pub struct DbFunction {
7 // A file path where src lies.
8 // The path is stripped with pwd or sysroot prefix.
9 pub file: String,
10
11 /// Function name.
12 pub name: String,
13
14 /// A hash considering recursive calls.
15 pub hash: BoxStr,
16
17 /// A hash only computed from direct calls.
18 pub hash_direct: BoxStr,
19
20 /// InstanceKind, but normal Item is represented as None.
21 pub inst_kind: Option<InstKind>,
22
23 /// Potential kani proof kind: standard or contract.
24 /// This tool will never identify if a function is an auto harness.
25 pub proof_kind: Option<ProofKind>,
26
27 /// Attributes are attached the function, but it seems that attributes
28 /// and function must be separated to query.
29 pub attrs: Vec<String>,
30
31 /// Source that a stable_mir span points to.
32 pub src: String,
33
34 /// The count of macro backtraces.
35 pub macro_backtrace_len: usize,
36
37 /// For a function that is generated through macros.
38 pub macro_backtrace: Vec<MacroBacktrace>,
39
40 /// The count of callees recursively traversed.
41 pub callees_len: usize,
42
43 /// Recurisve callees where the string refers to recursive hash of the function.
44 pub callees: Vec<BoxStr>,
45}