Run tests using why3find

creusot-dev-config/src/lib.rs

@@ -6,21 +6,33 @@ use std::{path::PathBuf, process::Command};
 
 pub struct Paths {
     pub why3: PathBuf,
+    pub why3find: PathBuf,
     pub why3_config: PathBuf,
 }
 
 /// Fails if the config could not be loaded
 pub fn paths() -> anyhow::Result<Paths> {
     let paths = creusot_setup::status_for_creusot()?;
-    Ok(Paths { why3: paths.why3_path, why3_config: paths.why3_config })
+    Ok(Paths {
+        why3: paths.why3_path,
+        why3find: paths.why3find_path,
+        why3_config: paths.why3_config,
+    })
 }
 
 /// Returns a command to invoke why3 (passing it the path to its configuration
 /// file if needed).
 /// Fails if the config could not be loaded
 pub fn why3_command() -> anyhow::Result<Command> {
     let p = paths()?;
-    let mut cmd = Command::new(p.why3.clone());
+    let mut cmd = Command::new(p.why3);
     cmd.arg("-C").arg(p.why3_config);
     Ok(cmd)
 }
+
+pub fn why3find_command() -> anyhow::Result<Command> {
+    let p = paths()?;
+    let mut cmd = Command::new(p.why3find);
+    cmd.env("WHY3CONFIG", p.why3_config);
+    Ok(cmd)
+}

creusot-setup/src/lib.rs

@@ -157,6 +157,7 @@ pub fn status() -> anyhow::Result<()> {
 
 pub struct CreusotFlags {
     pub why3_path: PathBuf,
+    pub why3find_path: PathBuf,
     pub why3_config: PathBuf,
 }
 
@@ -187,6 +188,7 @@ pub fn status_for_creusot() -> anyhow::Result<CreusotFlags> {
             }
             Ok(CreusotFlags {
                 why3_path: cfg.why3.path.to_path_buf(),
+                why3find_path: cfg.why3find.path.to_path_buf(),
                 why3_config: paths.why3_config_file,
             })
         }

creusot/tests/should_fail/bug/01_resolve_unsoundness.rs

@@ -1,3 +1,4 @@
+// WHY3PROVE
 extern crate creusot_contracts;
 
 use creusot_contracts::*;

creusot/tests/should_fail/bug/1204.rs

@@ -1,3 +1,4 @@
+// WHY3PROVE
 extern crate creusot_contracts;
 use creusot_contracts::*;
 

creusot/tests/should_fail/bug/1204.stderr

@@ -1,26 +1,26 @@
 warning: function cannot return without recursing
- --> 1204.rs:7:1
+ --> 1204.rs:8:1
   |
-7 | fn evil(x: Int) -> Int {
+8 | fn evil(x: Int) -> Int {
   | ^^^^^^^^^^^^^^^^^^^^^^ cannot return without recursing
-8 |     evil(-x) + 1
+9 |     evil(-x) + 1
   |     -------- recursive call site
   |
   = help: a `loop` may express intention better if this is on purpose
   = note: `#[warn(unconditional_recursion)]` on by default
 
 warning: function `evil` is never used
- --> 1204.rs:7:4
+ --> 1204.rs:8:4
   |
-7 | fn evil(x: Int) -> Int {
+8 | fn evil(x: Int) -> Int {
   |    ^^^^
   |
   = note: `#[warn(dead_code)]` on by default
 
 warning: function `wrong` is never used
-  --> 1204.rs:13:4
+  --> 1204.rs:14:4
    |
-13 | fn wrong() {
+14 | fn wrong() {
    |    ^^^^^
 
 warning: 3 warnings emitted

creusot/tests/should_fail/bug/222.rs

@@ -1,4 +1,4 @@
-// SHOULD_PROVE Z3 NO_SPLIT
+// WHY3PROVE SHOULD_PROVE Z3 NO_SPLIT
 extern crate creusot_contracts;
 use creusot_contracts::{logic::Int, *};
 

creusot/tests/should_fail/bug/492.rs

@@ -1,3 +1,4 @@
+// WHY3PROVE
 extern crate creusot_contracts;
 use creusot_contracts::*;
 

creusot/tests/should_fail/bug/692.rs

@@ -1,3 +1,4 @@
+// WHY3PROVE
 extern crate creusot_contracts;
 use creusot_contracts::*;
 

creusot/tests/should_fail/bug/695.rs

@@ -1,3 +1,4 @@
+// WHY3PROVE
 extern crate creusot_contracts;
 use creusot_contracts::*;
 

creusot/tests/should_fail/bug/869.rs

@@ -1,3 +1,4 @@
+// WHY3PROVE
 extern crate creusot_contracts;
 use creusot_contracts::*;