Generate a dummy function for checking the given precondition, postcondition or predicate. `spec_type` should be either `"pre"`, `"post"` or `"pred"`.
(
&mut self,
spec_type: SpecItemType,
spec_id: untyped::SpecificationId,
assertion: untyped::Assertion,
item: &untyped::AnyFnItem,
)
| 93 | /// |
| 94 | /// `spec_type` should be either `"pre"`, `"post"` or `"pred"`. |
| 95 | pub fn generate_spec_item_fn( |
| 96 | &mut self, |
| 97 | spec_type: SpecItemType, |
| 98 | spec_id: untyped::SpecificationId, |
| 99 | assertion: untyped::Assertion, |
| 100 | item: &untyped::AnyFnItem, |
| 101 | ) -> syn::Result<syn::Item> { |
| 102 | if let Some(span) = self.check_contains_keyword_in_params(item, "result") { |
| 103 | return Err(syn::Error::new( |
| 104 | span, |
| 105 | "it is not allowed to use the keyword `result` as a function argument".to_string(), |
| 106 | )); |
| 107 | } |
| 108 | let item_span = item.span(); |
| 109 | let item_name = syn::Ident::new( |
| 110 | &format!("prusti_{}_item_{}_{}", spec_type, item.sig().ident, spec_id), |
| 111 | item_span, |
| 112 | ); |
| 113 | let mut statements = TokenStream::new(); |
| 114 | assertion.encode_type_check(&mut statements); |
| 115 | let spec_id_str = spec_id.to_string(); |
| 116 | let assertion_json = crate::specifications::json::to_json_string(&assertion); |
| 117 | |
| 118 | let mut spec_item: syn::ItemFn = parse_quote_spanned! {item_span=> |
| 119 | #[allow(unused_must_use, unused_variables, dead_code)] |
| 120 | #[prusti::spec_only] |
| 121 | #[prusti::spec_id = #spec_id_str] |
| 122 | #[prusti::assertion = #assertion_json] |
| 123 | fn #item_name() { |
| 124 | #statements |
| 125 | } |
| 126 | }; |
| 127 | spec_item.sig.generics = item.sig().generics.clone(); |
| 128 | spec_item.sig.inputs = item.sig().inputs.clone(); |
| 129 | if spec_type == SpecItemType::Postcondition { |
| 130 | let fn_arg = self.generate_result_arg(item); |
| 131 | spec_item.sig.inputs.push(fn_arg); |
| 132 | } |
| 133 | Ok(syn::Item::Fn(spec_item)) |
| 134 | } |
| 135 | |
| 136 | /// Generate statements for checking the given loop invariant. |
| 137 | pub fn generate_spec_loop( |
nothing calls this directly
no test coverage detected