Enable encode_unsigned_num_constraint by default (viperproject#1281)

* Addresses viperproject#1215

* Skip memchr crate

* Add more tests

* Removed unneeded environment variable

* Skip failing crates

* Fix typo

* Skip failing crates

* Temporarily disable fail_fast

* Switch from native-tls to rustls

* Re-enable skipped crates

* Skip failing crates

* Skip failing crates

* disable failing crate

* Re-enable fail_fast

* Print errors with Display

* Disable encode_unsigned_num_constraints

* Fix typo in environment variable

* Remove unnecessairy compile flags

prusti-tests/tests/compiletest.rs

@@ -124,7 +124,6 @@ fn run_no_verification(group_name: &str, filter: &Option<String>) {
 fn run_verification_base(group_name: &str, filter: &Option<String>) {
     let _temporary_env_vars = (
         TemporaryEnvVar::set("PRUSTI_FULL_COMPILATION", "true"),
-        TemporaryEnvVar::set("PRUSTI_ENCODE_UNSIGNED_NUM_CONSTRAINT", "true"),
         TemporaryEnvVar::set("PRUSTI_QUIET", "true"),
     );
 

prusti-tests/tests/verify/pass/issues/issue-1215-1.rs

@@ -0,0 +1,9 @@
+use prusti_contracts::*;
+
+fn main() {}
+
+// #[requires(0 <= i)] // This should not be needed, if encode_unsigned_num_constraint=true is the default
+#[requires(i < s.len())]
+fn _test(s: &[i64], i: usize) -> i64 {
+    s[i]
+}

prusti-tests/tests/verify/pass/issues/issue-1215-2.rs

@@ -0,0 +1,28 @@
+#![allow(unused_comparisons)]
+use prusti_contracts::*;
+
+fn main() {}
+
+fn _test_u8(x: u8) {
+    prusti_assert!(x >= 0);
+}
+
+fn _test_u16(x: u16) {
+    prusti_assert!(x >= 0);
+}
+
+fn _test_u32(x: u32) {
+    prusti_assert!(x >= 0);
+}
+
+fn _test_u64(x: u64) {
+    prusti_assert!(x >= 0);
+}
+
+fn _test_u128(x: u128) {
+    prusti_assert!(x >= 0);
+}
+
+fn _test_usize(x: usize) {
+    prusti_assert!(x >= 0);
+}

prusti-utils/src/config.rs

@@ -79,7 +79,7 @@ lazy_static::lazy_static! {
         settings.set_default("check_foldunfold_state", false).unwrap();
         settings.set_default("check_overflows", true).unwrap();
         settings.set_default("check_panics", true).unwrap();
-        settings.set_default("encode_unsigned_num_constraint", false).unwrap();
+        settings.set_default("encode_unsigned_num_constraint", true).unwrap();
         settings.set_default("encode_bitvectors", false).unwrap();
         settings.set_default("simplify_encoding", true).unwrap();
         settings.set_default("log", "").unwrap();

test-crates/src/main.rs

@@ -204,7 +204,7 @@ fn main() -> Result<(), Box<dyn Error>> {
         java_home: Some(guest_java_home.clone()),
     };
 
-    info!("Crate a new workspace...");
+    info!("Create a new workspace...");
     // `Error: Compat { error: SandboxImagePullFailed(ExecutionFailed(ExitStatus(unix_wait_status(256)))) }` if
     // docker daemon isn't running
     let workspace = WorkspaceBuilder::new(workspace_path, "prusti-test-crates").init()?;
@@ -279,7 +279,7 @@ fn main() -> Result<(), Box<dyn Error>> {
             });
 
             if let Err(err) = build_status {
-                warn!("Error: {:?}", err);
+                warn!("Error: {}", err);
                 warn!("Output:\n{}", storage);
 
                 // Report the failure
@@ -323,6 +323,7 @@ fn main() -> Result<(), Box<dyn Error>> {
                         .env("PRUSTI_LOG_DIR", "/tmp/prusti_log")
                         .env("PRUSTI_CHECK_PANICS", "false")
                         .env("PRUSTI_CHECK_OVERFLOWS", "false")
+                        .env("PRUSTI_ENCODE_UNSIGNED_NUM_CONSTRAINT", "false")
                         // Do not report errors for unsupported language features
                         .env("PRUSTI_SKIP_UNSUPPORTED_FEATURES", "true");
                     match test_kind {
@@ -344,7 +345,7 @@ fn main() -> Result<(), Box<dyn Error>> {
             });
 
             if let Err(err) = verification_status {
-                error!("Error: {:?}", err);
+                error!("Error: {}", err);
                 error!("Output:\n{}", storage);
 
                 // Report the failure