Generate statements for checking the given loop invariant.
(
&mut self,
spec_id: untyped::SpecificationId,
assertion: untyped::Assertion,
)
| 135 | |
| 136 | /// Generate statements for checking the given loop invariant. |
| 137 | pub fn generate_spec_loop( |
| 138 | &mut self, |
| 139 | spec_id: untyped::SpecificationId, |
| 140 | assertion: untyped::Assertion, |
| 141 | ) -> TokenStream { |
| 142 | let mut statements = TokenStream::new(); |
| 143 | assertion.encode_type_check(&mut statements); |
| 144 | let spec_id_str = spec_id.to_string(); |
| 145 | let assertion_json = crate::specifications::json::to_json_string(&assertion); |
| 146 | let callsite_span = Span::call_site(); |
| 147 | quote_spanned! {callsite_span=> |
| 148 | #[allow(unused_must_use, unused_variables)] |
| 149 | { |
| 150 | #[prusti::spec_only] |
| 151 | #[prusti::loop_body_invariant_spec] |
| 152 | #[prusti::spec_id = #spec_id_str] |
| 153 | #[prusti::assertion = #assertion_json] |
| 154 | || { |
| 155 | #statements |
| 156 | }; |
| 157 | } |
| 158 | } |
| 159 | } |
| 160 | |
| 161 | /// Generate statements for checking a closure specification. |
| 162 | /// TODO: arguments, result (types are typically not known yet after parsing...) |
nothing calls this directly
no test coverage detected