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}