prusti_specs/
spec_attribute_kind.rs

1use std::convert::TryFrom;
2
3/// This type identifies one of the procedural macro attributes of Prusti
4#[derive(PartialEq, Eq, Copy, Clone, Debug, PartialOrd, Ord)]
5pub enum SpecAttributeKind {
6    /// All type specifications that alter its type must be processed before
7    /// PrintCounterexample. Currently this only applies to Model.
8    Model = 0,
9    Requires = 1,
10    Ensures = 2,
11    AfterExpiry = 3,
12    AssertOnExpiry = 4,
13    Pure = 5,
14    Trusted = 6,
15    Predicate = 7,
16    Invariant = 8,
17    RefineSpec = 9,
18    Terminates = 10,
19    PrintCounterexample = 11,
20    Verified = 12,
21}
22
23impl TryFrom<String> for SpecAttributeKind {
24    type Error = String;
25
26    fn try_from(name: String) -> Result<Self, Self::Error> {
27        match name.as_str() {
28            "requires" => Ok(SpecAttributeKind::Requires),
29            "ensures" => Ok(SpecAttributeKind::Ensures),
30            "after_expiry" => Ok(SpecAttributeKind::AfterExpiry),
31            "assert_on_expiry" => Ok(SpecAttributeKind::AssertOnExpiry),
32            "pure" => Ok(SpecAttributeKind::Pure),
33            "trusted" => Ok(SpecAttributeKind::Trusted),
34            "predicate" => Ok(SpecAttributeKind::Predicate),
35            "invariant" => Ok(SpecAttributeKind::Invariant),
36            "refine_spec" => Ok(SpecAttributeKind::RefineSpec),
37            "model" => Ok(SpecAttributeKind::Model),
38            "print_counterexample" => Ok(SpecAttributeKind::PrintCounterexample),
39            "verified" => Ok(SpecAttributeKind::Verified),
40            _ => Err(name),
41        }
42    }
43}
prusti_specs/spec_attribute_kind.rs

prusti_specs/
spec_attribute_kind.rs
