diff --git a/ethers-solc/src/artifacts/mod.rs b/ethers-solc/src/artifacts/mod.rs index 94806f9c..a90b0962 100644 --- a/ethers-solc/src/artifacts/mod.rs +++ b/ethers-solc/src/artifacts/mod.rs @@ -1018,6 +1018,8 @@ pub struct ModelCheckerSettings { pub timeout: Option, #[serde(skip_serializing_if = "Option::is_none")] pub targets: Option>, + #[serde(skip_serializing_if = "Option::is_none")] + pub invariants: Option>, } /// 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 { + 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)] pub struct Compiler { pub version: String, diff --git a/ethers-solc/tests/project.rs b/ethers-solc/tests/project.rs index 1b754273..3cc8c97e 100644 --- a/ethers-solc/tests/project.rs +++ b/ethers-solc/tests/project.rs @@ -1610,6 +1610,7 @@ fn can_compile_model_checker_sample() { engine: Some(CHC), targets: None, timeout: Some(10000), + invariants: None, }); let compiled = project.compile().unwrap();