feat(ethers-solc): extend model checker setting field (#2123)
This commit is contained in:
parent
b08c1e29b8
commit
060e145ea2
|
@ -1018,6 +1018,8 @@ pub struct ModelCheckerSettings {
|
||||||
pub timeout: Option<u32>,
|
pub timeout: Option<u32>,
|
||||||
#[serde(skip_serializing_if = "Option::is_none")]
|
#[serde(skip_serializing_if = "Option::is_none")]
|
||||||
pub targets: Option<Vec<ModelCheckerTarget>>,
|
pub targets: Option<Vec<ModelCheckerTarget>>,
|
||||||
|
#[serde(skip_serializing_if = "Option::is_none")]
|
||||||
|
pub invariants: Option<Vec<ModelCheckerInvariant>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Which model checker engine to run.
|
/// Which model checker engine to run.
|
||||||
|
@ -1104,6 +1106,36 @@ impl FromStr for ModelCheckerTarget {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Which model checker invariants to check.
|
||||||
|
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
|
||||||
|
#[serde(rename_all = "camelCase")]
|
||||||
|
pub enum ModelCheckerInvariant {
|
||||||
|
Contract,
|
||||||
|
Reentrancy,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl fmt::Display for ModelCheckerInvariant {
|
||||||
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
|
let string = match self {
|
||||||
|
ModelCheckerInvariant::Contract => "contract",
|
||||||
|
ModelCheckerInvariant::Reentrancy => "reentrancy",
|
||||||
|
};
|
||||||
|
write!(f, "{string}")
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl FromStr for ModelCheckerInvariant {
|
||||||
|
type Err = String;
|
||||||
|
|
||||||
|
fn from_str(s: &str) -> Result<Self, Self::Err> {
|
||||||
|
match s {
|
||||||
|
"contract" => Ok(ModelCheckerInvariant::Contract),
|
||||||
|
"reentrancy" => Ok(ModelCheckerInvariant::Reentrancy),
|
||||||
|
s => Err(format!("Unknown model checker invariant: {s}")),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
|
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
|
||||||
pub struct Compiler {
|
pub struct Compiler {
|
||||||
pub version: String,
|
pub version: String,
|
||||||
|
|
|
@ -1610,6 +1610,7 @@ fn can_compile_model_checker_sample() {
|
||||||
engine: Some(CHC),
|
engine: Some(CHC),
|
||||||
targets: None,
|
targets: None,
|
||||||
timeout: Some(10000),
|
timeout: Some(10000),
|
||||||
|
invariants: None,
|
||||||
});
|
});
|
||||||
let compiled = project.compile().unwrap();
|
let compiled = project.compile().unwrap();
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue