Create testing setup

prusti-encoder/Cargo.toml

@@ -18,6 +18,8 @@ task-encoder = { path = "../task-encoder" }
 vir = { path = "../vir" }
 tracing = { path = "../tracing" }
 
+backtrace-on-stack-overflow = { git = "https://github.com/Pistonight/backtrace-on-stack-overflow", branch = "feature/limit_stack_size" }
+
 [package.metadata.rust-analyzer]
 # This crate uses #[feature(rustc_private)]
 rustc_private = true

prusti-encoder/src/lib.rs

@@ -27,6 +27,7 @@ pub fn test_entrypoint<'tcx>(
     def_spec: prusti_interface::specs::typed::DefSpecificationMap,
 ) -> request::RequestWithContext {
     vir::init_vcx(vir::VirCtxt::new(tcx, body, def_spec));
+    unsafe { backtrace_on_stack_overflow::enable() };
 
     // TODO: this should be a "crate" encoder, which will deps.require all the methods in the crate
 

prusti-tests/tests/harnesses/compiletest.rs

@@ -78,6 +78,7 @@ fn run_prusti_tests(
         config
     };
 
+    /*
     // UI
     {
         let config = prusti_config(format!("tests/{group_name}/ui"));
@@ -94,6 +95,7 @@ fn run_prusti_tests(
         ));
         run_tests(config)?;
     }
+    */
 
     // pass
     {
@@ -176,10 +178,11 @@ pub(crate) fn run() {
     let server_address = spawn_server_thread();
     env::set_var("PRUSTI_SERVER_ADDRESS", server_address.to_string());
 
+    /*
     // Run (temporary) tests specific to Prusti v2.
     println!("[v2]");
     run_verification_no_overflow("v2");
-    /*
+
         let save_verification_cache =
             || match ureq::post(&format!("http://{server_address}/save")).call() {
                 Ok(response) => {
@@ -198,10 +201,13 @@ pub(crate) fn run() {
         // Test the type-checking of specifications. This doesn't run the verifier.
         println!("[typecheck]");
         run_no_verification("typecheck");
+    */
 
-        // Test the verifier.
-        println!("[verify]");
-        run_verification_no_overflow("verify");
+    // Test the verifier.
+    println!("[verify]");
+    run_verification_no_overflow("verify");
+
+    /*
         save_verification_cache();
 
         // Test the verifier with overflow checks enabled.

prusti/src/verifier.rs

@@ -89,6 +89,7 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) {
             //         || (config::skip_unsupported_features()
             //             && config::allow_unreachable_unsupported_code())
             // );
+            std::process::exit(1);
         }
 
         //let verification_result =