@@ -13,7 +13,6 @@ use crate::header::TestProps;
13
13
use crate :: json;
14
14
use crate :: read2:: read2;
15
15
use crate :: util:: logv;
16
- use regex:: Regex ;
17
16
18
17
use std:: env;
19
18
use std:: fs:: { self , create_dir_all} ;
@@ -222,43 +221,19 @@ impl<'test> TestCx<'test> {
222
221
/// message is printed to stdout if the verification result is not expected.
223
222
fn verify ( & self ) {
224
223
let proc_res = self . run_kani ( ) ;
225
- // If the test file contains expected failures in some locations, ensure
226
- // that verification does indeed fail in those locations
227
- if proc_res. stdout . contains ( "EXPECTED FAIL" ) {
228
- let lines = TestCx :: verify_expect_fail ( & proc_res. stdout ) ;
229
- if !lines. is_empty ( ) {
230
- self . fatal_proc_rec (
231
- & format ! ( "test failed: expected failure in lines {lines:?}, got success" ) ,
232
- & proc_res,
233
- )
234
- }
235
- } else {
236
- // The code above depends too much on the exact string output of
237
- // Kani. If the output of Kani changes in the future, the check below
238
- // will (hopefully) force some tests to fail and remind us to
239
- // update the code above as well.
240
- if fs:: read_to_string ( & self . testpaths . file ) . unwrap ( ) . contains ( "__VERIFIER_expect_fail" )
241
- {
242
- self . fatal_proc_rec (
243
- "found call to `__VERIFIER_expect_fail` with no corresponding \
244
- \" EXPECTED FAIL\" in Kani's output",
245
- & proc_res,
246
- )
247
- }
248
- // Print an error if the verification result is not expected.
249
- if self . props . kani_panic_step == Some ( KaniFailStep :: Verify ) {
250
- if proc_res. status . success ( ) {
251
- self . fatal_proc_rec (
252
- "test failed: expected verification failure, got success" ,
253
- & proc_res,
254
- ) ;
255
- }
256
- } else if !proc_res. status . success ( ) {
224
+ // Print an error if the verification result is not expected.
225
+ if self . props . kani_panic_step == Some ( KaniFailStep :: Verify ) {
226
+ if proc_res. status . success ( ) {
257
227
self . fatal_proc_rec (
258
- "test failed: expected verification success , got failure " ,
228
+ "test failed: expected verification failure , got success " ,
259
229
& proc_res,
260
230
) ;
261
231
}
232
+ } else if !proc_res. status . success ( ) {
233
+ self . fatal_proc_rec (
234
+ "test failed: expected verification success, got failure" ,
235
+ & proc_res,
236
+ ) ;
262
237
}
263
238
}
264
239
@@ -279,18 +254,6 @@ impl<'test> TestCx<'test> {
279
254
}
280
255
}
281
256
282
- /// If the test file contains expected failures in some locations, ensure
283
- /// that verification does not succeed in those locations.
284
- fn verify_expect_fail ( str : & str ) -> Vec < usize > {
285
- let re = Regex :: new ( r"line ([0-9]+) EXPECTED FAIL: SUCCESS" ) . unwrap ( ) ;
286
- let mut lines = vec ! [ ] ;
287
- for m in re. captures_iter ( str) {
288
- let num = m. get ( 1 ) . unwrap ( ) . as_str ( ) . parse ( ) . unwrap ( ) ;
289
- lines. push ( num) ;
290
- }
291
- lines
292
- }
293
-
294
257
/// Runs cargo-kani on the function specified by the stem of `self.testpaths.file`.
295
258
/// The `test` parameter controls whether to specify `--tests` to `cargo kani`.
296
259
/// An error message is printed to stdout if verification output does not
0 commit comments