|
4 | 4 | //! This file contains functions related to codegenning MIR functions into gotoc |
5 | 5 |
|
6 | 6 | use crate::codegen_cprover_gotoc::GotocCtx; |
7 | | -use crate::kani_middle::attributes::{extract_harness_attributes, is_test_harness_closure}; |
8 | 7 | use cbmc::goto_program::{Expr, Stmt, Symbol}; |
9 | 8 | use cbmc::InternString; |
10 | | -use kani_metadata::{HarnessAttributes, HarnessMetadata}; |
11 | 9 | use rustc_middle::mir::traversal::reverse_postorder; |
12 | 10 | use rustc_middle::mir::{Body, HasLocalDecls, Local}; |
13 | 11 | use rustc_middle::ty::{self, Instance}; |
@@ -89,9 +87,6 @@ impl<'tcx> GotocCtx<'tcx> { |
89 | 87 | let stmts = self.current_fn_mut().extract_block(); |
90 | 88 | let body = Stmt::block(stmts, loc); |
91 | 89 | self.symbol_table.update_fn_declaration_with_definition(&name, body); |
92 | | - |
93 | | - self.record_kani_attributes(); |
94 | | - self.record_test_harness_metadata(); |
95 | 90 | } |
96 | 91 | self.reset_current_fn(); |
97 | 92 | } |
@@ -244,50 +239,4 @@ impl<'tcx> GotocCtx<'tcx> { |
244 | 239 | }); |
245 | 240 | self.reset_current_fn(); |
246 | 241 | } |
247 | | - |
248 | | - /// We record test harness information in kani-metadata, just like we record |
249 | | - /// proof harness information. This is used to support e.g. cargo-kani assess. |
250 | | - /// |
251 | | - /// Note that we do not actually spot the function that was annotated by `#[test]` |
252 | | - /// but instead the closure that gets put into the "test description" that macro |
253 | | - /// expands into. (See comment below) This ends up being preferrable, actually, |
254 | | - /// as it add asserts for tests that return `Result` types. |
255 | | - fn record_test_harness_metadata(&mut self) { |
256 | | - let def_id = self.current_fn().instance().def_id(); |
257 | | - if is_test_harness_closure(self.tcx, def_id) { |
258 | | - self.test_harnesses.push(self.generate_metadata(None)) |
259 | | - } |
260 | | - } |
261 | | - |
262 | | - /// This updates the goto context with any information that should be accumulated from a function's |
263 | | - /// attributes. |
264 | | - /// |
265 | | - /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here) |
266 | | - fn record_kani_attributes(&mut self) { |
267 | | - let def_id = self.current_fn().instance().def_id(); |
268 | | - let attributes = extract_harness_attributes(self.tcx, def_id); |
269 | | - if attributes.is_some() { |
270 | | - self.proof_harnesses.push(self.generate_metadata(attributes)); |
271 | | - } |
272 | | - } |
273 | | - |
274 | | - /// Create the default proof harness for the current function |
275 | | - fn generate_metadata(&self, attributes: Option<HarnessAttributes>) -> HarnessMetadata { |
276 | | - let current_fn = self.current_fn(); |
277 | | - let pretty_name = current_fn.readable_name().to_owned(); |
278 | | - let mangled_name = current_fn.name(); |
279 | | - let loc = self.codegen_span(¤t_fn.mir().span); |
280 | | - |
281 | | - HarnessMetadata { |
282 | | - pretty_name, |
283 | | - mangled_name, |
284 | | - crate_name: current_fn.krate(), |
285 | | - original_file: loc.filename().unwrap(), |
286 | | - original_start_line: loc.start_line().unwrap() as usize, |
287 | | - original_end_line: loc.end_line().unwrap() as usize, |
288 | | - attributes: attributes.unwrap_or_default(), |
289 | | - // We record the actual path after codegen before we dump the metadata into a file. |
290 | | - goto_file: None, |
291 | | - } |
292 | | - } |
293 | 242 | } |
0 commit comments