1- #![ allow( dead_code) ]
1+ #![ allow( dead_code, clippy :: result_large_err ) ]
22
33extern crate rustc_driver;
44extern crate rustc_errors;
@@ -54,7 +54,6 @@ pub struct TestErr {
5454 pub json_output : Option < serde_json:: Value > , // captured when `--output-json` is used
5555}
5656
57- #[ allow( dead_code) ]
5857pub fn verify_files (
5958 name : & str ,
6059 files : impl IntoIterator < Item = ( String , String ) > ,
@@ -66,10 +65,9 @@ pub fn verify_files(
6665
6766use std:: { cell:: RefCell , path} ;
6867thread_local ! {
69- pub static THREAD_LOCAL_TEST_NAME : RefCell <Option <String >> = RefCell :: new( None ) ;
68+ pub static THREAD_LOCAL_TEST_NAME : RefCell <Option <String >> = const { RefCell :: new( None ) } ;
7069}
7170
72- #[ allow( dead_code) ]
7371pub fn verify_files_vstd (
7472 name : & str ,
7573 files : impl IntoIterator < Item = ( String , String ) > ,
@@ -80,7 +78,6 @@ pub fn verify_files_vstd(
8078 verify_files_vstd_all_diags ( name, files, entry_file, import_vstd, options) . map ( |_| ( ) )
8179}
8280
83- #[ allow( dead_code) ]
8481pub fn verify_files_vstd_all_diags (
8582 name : & str ,
8683 files : impl IntoIterator < Item = ( String , String ) > ,
@@ -597,7 +594,6 @@ pub fn run_cargo_with_target(
597594 run
598595}
599596
600- #[ allow( dead_code) ]
601597pub const FEATURE_PRELUDE : & str = crate :: common:: code_str! {
602598 // If we're using the pre-macro-expanded vstd lib, then it might have
603599 // some macro-internal stuff in it, and rustc needs this option in order to accept it.
@@ -621,13 +617,11 @@ pub const FEATURE_PRELUDE: &str = crate::common::code_str! {
621617 #![ feature( const_destruct) ]
622618} ;
623619
624- #[ allow( dead_code) ]
625620pub const USE_PRELUDE : & str = crate :: common:: code_str! {
626621 use verus_builtin:: * ;
627622 use verus_builtin_macros:: * ;
628623} ;
629624
630- #[ allow( dead_code) ]
631625pub fn verify_one_file ( name : & str , code : String , options : & [ & str ] ) -> Result < TestErr , TestErr > {
632626 let mut options: Vec < _ > = options. into_iter ( ) . map ( |x| * x) . collect ( ) ;
633627 let mut no_prelude = false ;
@@ -791,14 +785,10 @@ pub fn relevant_error_span(err: &Vec<DiagnosticSpan>) -> &DiagnosticSpan {
791785 } ) {
792786 return e;
793787 }
794- err. iter ( )
795- . filter ( |e| e. label != Some ( vir:: def:: THIS_PRE_FAILED . to_string ( ) ) )
796- . next ( )
797- . expect ( "span" )
788+ err. iter ( ) . find ( |e| e. label != Some ( vir:: def:: THIS_PRE_FAILED . to_string ( ) ) ) . expect ( "span" )
798789}
799790
800791/// Assert that one verification failure happened on source lines containing the string "FAILS".
801- #[ allow( dead_code) ]
802792pub fn assert_one_fails ( err : TestErr ) {
803793 assert_eq ! ( err. errors. len( ) , 1 ) ;
804794 assert ! (
@@ -812,7 +802,6 @@ pub fn assert_one_fails(err: TestErr) {
812802
813803/// When this testcase has ONE verification failure,
814804/// assert that all spans are properly reported (All spans are respoinsible to the verification failure)
815- #[ allow( dead_code) ]
816805pub fn assert_expand_fails ( err : TestErr , span_count : usize ) {
817806 assert_fails ( err. clone ( ) , 1 ) ;
818807
@@ -825,7 +814,6 @@ pub fn assert_expand_fails(err: TestErr, span_count: usize) {
825814}
826815
827816/// Assert that `count` verification failures happened on source lines containin the string "FAILS".
828- #[ allow( dead_code) ]
829817pub fn assert_fails ( err : TestErr , count : usize ) {
830818 assert_eq ! ( err. errors. len( ) , count) ;
831819 for c in 0 ..count {
@@ -839,20 +827,17 @@ pub fn assert_fails(err: TestErr, count: usize) {
839827 }
840828}
841829
842- #[ allow( dead_code) ]
843830pub fn assert_vir_error_msg ( err : TestErr , expected_msg : & str ) {
844831 assert_eq ! ( err. errors. len( ) , 1 ) ;
845832 assert ! ( err. errors[ 0 ] . code. is_none( ) ) ; // thus likely a VIR error
846833 assert ! ( err. errors[ 0 ] . message. contains( expected_msg) ) ;
847834}
848835
849- #[ allow( dead_code) ]
850836pub fn assert_any_vir_error_msg ( err : TestErr , expected_msg : & str ) {
851837 assert ! ( err. errors. iter( ) . all( |x| x. code. is_none( ) ) ) ; // thus likely a VIR error
852838 assert ! ( err. errors. iter( ) . any( |x| x. message. contains( expected_msg) ) ) ;
853839}
854840
855- #[ allow( dead_code) ]
856841pub fn assert_vir_error_msgs ( err : TestErr , expected_msgs : & [ & str ] ) {
857842 assert ! ( err. errors. len( ) == expected_msgs. len( ) ) ;
858843 assert ! ( err. errors. iter( ) . all( |x| x. code. is_none( ) ) ) ; // thus likely a VIR error
@@ -861,20 +846,17 @@ pub fn assert_vir_error_msgs(err: TestErr, expected_msgs: &[&str]) {
861846 }
862847}
863848
864- #[ allow( dead_code) ]
865849pub fn assert_custom_attr_error_msg ( err : TestErr , expected_msg : & str ) {
866850 assert ! (
867851 err. errors. iter( ) . any( |x| x. message. contains( "custom attribute panicked" )
868852 && x. rendered. contains( expected_msg) )
869853 ) ;
870854}
871855
872- #[ allow( dead_code) ]
873856pub fn assert_help_error_msg ( err : TestErr , expected_msg : & str ) {
874857 assert ! ( err. errors. iter( ) . any( |x| x. rendered. contains( expected_msg) ) ) ;
875858}
876859
877- #[ allow( dead_code) ]
878860pub fn assert_help_error_msgs ( err : TestErr , expected_msgs : & [ & str ] ) {
879861 assert ! (
880862 expected_msgs
@@ -883,7 +865,6 @@ pub fn assert_help_error_msgs(err: TestErr, expected_msgs: &[&str]) {
883865 ) ;
884866}
885867
886- #[ allow( dead_code) ]
887868pub fn assert_rust_error_msg ( err : TestErr , expected_msg : & str ) {
888869 assert_eq ! ( err. errors. len( ) , 1 ) ;
889870 let error_re = regex:: Regex :: new ( r"^E[0-9]{4}$" ) . unwrap ( ) ;
@@ -896,14 +877,11 @@ pub fn assert_rust_error_msg(err: TestErr, expected_msg: &str) {
896877 assert ! ( err. errors[ 0 ] . message. contains( expected_msg) ) ;
897878}
898879
899- #[ allow( dead_code) ]
900- pub fn assert_rust_error_msg_skip_spec_msgs ( err : TestErr , expected_msg : & str ) {
901- let mut err = err;
902- err. errors = err. errors . into_iter ( ) . filter ( |e| !e. message . contains ( "(Verus spec" ) ) . collect ( ) ;
880+ pub fn assert_rust_error_msg_skip_spec_msgs ( mut err : TestErr , expected_msg : & str ) {
881+ err. errors . retain ( |e| !e. message . contains ( "(Verus spec" ) ) ;
903882 assert_rust_error_msg ( err, expected_msg)
904883}
905884
906- #[ allow( dead_code) ]
907885pub fn assert_rust_error_msgs ( err : TestErr , expected_msgs : & [ & str ] ) {
908886 assert_eq ! ( err. errors. len( ) , expected_msgs. len( ) ) ;
909887 let error_re = regex:: Regex :: new ( r"^E[0-9]{4}$" ) . unwrap ( ) ;
@@ -918,7 +896,6 @@ pub fn assert_rust_error_msgs(err: TestErr, expected_msgs: &[&str]) {
918896 }
919897}
920898
921- #[ allow( dead_code) ]
922899pub fn assert_rust_error_msg_all ( err : TestErr , expected_msg : & str ) {
923900 assert ! ( err. errors. len( ) >= 1 ) ;
924901 let error_re = regex:: Regex :: new ( r"^E[0-9]{4}$" ) . unwrap ( ) ;
@@ -928,7 +905,6 @@ pub fn assert_rust_error_msg_all(err: TestErr, expected_msg: &str) {
928905 }
929906}
930907
931- #[ allow( dead_code) ]
932908pub fn assert_rust_error_msg_any ( err : TestErr , expected_msg : & str ) {
933909 assert ! ( err. errors. len( ) >= 1 ) ;
934910 let error_re = regex:: Regex :: new ( r"^E[0-9]{4}$" ) . unwrap ( ) ;
@@ -942,7 +918,6 @@ pub fn assert_rust_error_msg_any(err: TestErr, expected_msg: &str) {
942918 assert ! ( found) ;
943919}
944920
945- #[ allow( dead_code) ]
946921pub fn assert_spans_contain ( err : & Diagnostic , needle : & str ) {
947922 assert ! (
948923 err. spans
@@ -952,7 +927,6 @@ pub fn assert_spans_contain(err: &Diagnostic, needle: &str) {
952927 ) ;
953928}
954929
955- #[ allow( dead_code) ]
956930pub fn assert_fails_bv ( err : TestErr , fail32 : bool , fail64 : bool ) {
957931 assert_eq ! ( err. errors. len( ) , ( if fail32 { 1 } else { 0 } ) + ( if fail64 { 1 } else { 0 } ) ) ;
958932 if fail32 {
@@ -964,29 +938,22 @@ pub fn assert_fails_bv(err: TestErr, fail32: bool, fail64: bool) {
964938 }
965939}
966940
967- #[ allow( dead_code) ]
968941pub fn assert_fails_bv_32bit ( err : TestErr ) {
969942 assert_fails_bv ( err, true , false ) ;
970943}
971944
972- #[ allow( dead_code) ]
973945pub fn assert_fails_bv_64bit ( err : TestErr ) {
974946 assert_fails_bv ( err, false , true ) ;
975947}
976948
977- #[ allow( dead_code) ]
978949pub fn assert_fails_bv_32bit_64bit ( err : TestErr ) {
979950 assert_fails_bv ( err, true , true ) ;
980951}
981952
982953pub fn typ_inv_relevant_error_span ( err : & Vec < DiagnosticSpan > ) -> & DiagnosticSpan {
983- err. iter ( )
984- . filter ( |e| e. label != Some ( "type invariant declared here" . to_string ( ) ) )
985- . next ( )
986- . expect ( "span" )
954+ err. iter ( ) . find ( |e| e. label != Some ( "type invariant declared here" . to_string ( ) ) ) . expect ( "span" )
987955}
988956
989- #[ allow( dead_code) ]
990957pub fn assert_has_recommends_failure ( err : TestErr ) {
991958 assert ! ( err. errors. len( ) > 0 ) ;
992959 let mut found_rec_failure = false ;
@@ -999,7 +966,6 @@ pub fn assert_has_recommends_failure(err: TestErr) {
999966 assert ! ( found_rec_failure) ;
1000967}
1001968
1002- #[ allow( dead_code) ]
1003969pub fn assert_fails_type_invariant_error ( err : TestErr , count : usize ) {
1004970 assert_eq ! ( err. errors. len( ) , count) ;
1005971 for c in 0 ..count {
0 commit comments