Merge pull request #439 from Nadrieril/fully-analyze

charon-pin

@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-821fe7c71300e00c23e47ae97de1e8dc4ac91f9d
+5651efc286dcee58e8e96be869980a40a26af95c

tests/src/borrow-check-negative.borrow-check.out

@@ -1,15 +1,15 @@
 [Info ] Imported: tests/llbc/borrow_check_negative.llbc
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 23:12-23:14
+Source: 'tests/src/borrow-check-negative.rs', lines 24:12-24:14
 [Error] Can't end abstraction 8 as it is set as non-endable
-Source: 'tests/src/borrow-check-negative.rs', lines 26:0-32:1
+Source: 'tests/src/borrow-check-negative.rs', lines 27:0-33:1
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 40:4-40:11
+Source: 'tests/src/borrow-check-negative.rs', lines 41:4-41:11
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 49:12-49:14
+Source: 'tests/src/borrow-check-negative.rs', lines 50:12-50:14
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 63:12-63:17
+Source: 'tests/src/borrow-check-negative.rs', lines 64:12-64:17
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 78:12-78:17
+Source: 'tests/src/borrow-check-negative.rs', lines 79:12-79:17
 [Error] Can not apply a projection to the ⊥ value
-Source: 'tests/src/borrow-check-negative.rs', lines 89:12-89:15
+Source: 'tests/src/borrow-check-negative.rs', lines 90:12-90:15

tests/src/borrow-check-negative.rs

@@ -1,3 +1,4 @@
+//@ charon-args=--skip-borrowck
 //@ [!borrow-check] skip
 //@ [borrow-check] known-failure
 // Some negative tests for borrow checking

tests/src/loops-borrow-check-negative.borrow-check.out

@@ -1,3 +1,3 @@
 [Info ] Imported: tests/llbc/loops_borrow_check_negative.llbc
 [Error] Can't end abstraction 16 as it is set as non-endable
-Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-28:1
+Source: 'tests/src/loops-borrow-check-negative.rs', lines 19:0-29:1

tests/src/loops-borrow-check-negative.rs

@@ -1,3 +1,4 @@
+//@ charon-args=--skip-borrowck
 //@ [!borrow-check] skip
 //@ [borrow-check] known-failure
 

tests/test_runner/run_test.ml

@@ -116,6 +116,9 @@ let run_charon (env : runner_env) (case : Input.t) =
         [
           env.charon_path;
           "--no-cargo";
+          "--rustc-flag=--crate-type=rlib";
+          "--rustc-flag=--allow=unused";
+          "--rustc-flag=--allow=non_snake_case";
           "--hide-marker-traits";
           "--input";
           case.path;
@@ -146,6 +149,7 @@ let run_charon (env : runner_env) (case : Input.t) =
           [
             env.charon_path;
             "--hide-marker-traits";
+            "--rustc-flag=--allow=unused";
             "--dest";
             Filename_unix.realpath env.llbc_dir;
           ]