Creates a single Prusti assertion from the input and returns it.
(&mut self)
| 90 | } |
| 91 | /// Creates a single Prusti assertion from the input and returns it. |
| 92 | pub fn extract_assertion(&mut self) -> syn::Result<AssertionWithoutId> { |
| 93 | if self.tokens.is_empty() { |
| 94 | Ok(AssertionWithoutId { |
| 95 | kind: Box::new(common::AssertionKind::And(vec![])) |
| 96 | }) |
| 97 | } else { |
| 98 | if let Some(span) = self.contains_both_and_or(&self.tokens) { |
| 99 | return Err(self.error_ambiguous_expression(span)); |
| 100 | } |
| 101 | |
| 102 | let expr = self.parse_prusti()?; |
| 103 | if self.pop().is_some() { |
| 104 | Err(self.error_unexpected()) |
| 105 | } else { |
| 106 | Ok(expr) |
| 107 | } |
| 108 | } |
| 109 | } |
| 110 | /// Create a pledge from the input |
| 111 | pub fn extract_pledge(&mut self) -> syn::Result<PledgeWithoutId> { |
| 112 | let pledge = self.parse_pledge()?; |
no test coverage detected