update sessions

creusot-contracts/src/lib.rs

@@ -203,7 +203,9 @@ mod macros {
     /// This means you cannot `#[open]` a body which refers to a `pub(crate)` symbol.
     pub use creusot_contracts_dummy::open;
 
-    pub use creusot_contracts_proc::Resolve;
+    pub use creusot_contracts_dummy::DeepModel;
+
+    pub use creusot_contracts_dummy::Resolve;
 }
 
 #[cfg(creusot)]
@@ -249,7 +251,6 @@ pub mod resolve;
 pub mod util;
 pub mod well_founded;
 
-pub use macros::*;
 // We add some common things at the root of the creusot-contracts library
 pub use crate::{
     logic::{IndexLogic as _, Int, OrdLogic, Seq},
@@ -296,7 +297,3 @@ macro_rules! vec {
     );
     ($($x:expr,)*) => (vec![$($x),*])
 }
-
-// #[logic]
-// #[open]
-// pub fn foo() -> bool { true }

creusot-contracts/src/logic/int.rs

@@ -4,6 +4,7 @@ use crate::{
 };
 
 #[cfg_attr(creusot, rustc_diagnostic_item = "creusot_int", creusot::builtins = "prelude.Int.int")]
+#[allow(dead_code)]
 pub struct Int(*mut ());
 
 impl Int {

creusot/src/callbacks.rs

@@ -2,7 +2,7 @@ use rustc_borrowck::consumers::{BodyWithBorrowckFacts, ConsumerOptions};
 use rustc_driver::{Callbacks, Compilation};
 use rustc_hir::def_id::LocalDefId;
 use rustc_interface::{interface::Compiler, Config, Queries};
-use rustc_middle::{mir::dump_mir, ty::TyCtxt};
+use rustc_middle::ty::TyCtxt;
 
 use std::{cell::RefCell, collections::HashMap, thread_local};
 

creusot/src/cleanup_spec_closures.rs

@@ -159,7 +159,8 @@ pub fn remove_ghost_closures<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) {
             let Rvalue::Aggregate(box AggregateKind::Closure(def_id, _), _) = rhs else {
                 return;
             };
-            if util::is_no_translate(self.tcx, *def_id) || util::is_snapshot_closure(self.tcx, *def_id)
+            if util::is_no_translate(self.tcx, *def_id)
+                || util::is_snapshot_closure(self.tcx, *def_id)
             {
                 statement.kind = StatementKind::Nop
             }

creusot/src/translation/fmir.rs

@@ -8,8 +8,6 @@ use rustc_middle::{
 use rustc_span::{Span, Symbol};
 use rustc_target::abi::VariantIdx;
 
-pub use rustc_span::DUMMY_SP;
-
 #[derive(Clone, Debug)]
 pub struct Place<'tcx> {
     pub(crate) local: Symbol,

creusot/tests/should_fail/array.stderr

@@ -10,7 +10,7 @@ error: Unsupported expression: Repeat
 13 | #[requires([0; 4] == x)]
    |            ^^^^^^
 
-error[creusot]: internal error
+error: internal error
 
 error: aborting due to 3 previous errors
 

creusot/tests/should_fail/bad_borrow.stderr

@@ -9,6 +9,6 @@ error[E0499]: cannot borrow `x` as mutable more than once at a time
 6 |     *a += *b;
   |     -------- first borrow later used here
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 
 For more information about this error, try `rustc --explain E0499`.

creusot/tests/should_fail/bad_law.stderr

@@ -1,10 +1,10 @@
-error[creusot]: Laws cannot have additional generic parameters
+error: Laws cannot have additional generic parameters
  --> bad_law.rs:6:5
   |
 6 |     fn my_law<T>(x: T);
   |     ^^^^^^^^^^^^^^^^^^^
 
-error[creusot]: Expected `my_law` to be a logic function as specified by the trait declaration
+error: Expected `my_law` to be a logic function as specified by the trait declaration
   --> bad_law.rs:10:5
    |
 10 |     fn my_law<T>(_: T) {}

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

@@ -17,12 +17,18 @@ module Core_Ptr_Unique_Unique_Type
     | C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't)
 
 end
-module Alloc_RawVec_RawVec_Type
+module Alloc_RawVec_Cap_Type
   use prelude.UIntSize
   use prelude.Int
+  type t_cap  =
+    | C_Cap usize
+
+end
+module Alloc_RawVec_RawVec_Type
+  use Alloc_RawVec_Cap_Type as Alloc_RawVec_Cap_Type
   use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
   type t_rawvec 't 'a =
-    | C_RawVec (Core_Ptr_Unique_Unique_Type.t_unique 't) usize 'a
+    | C_RawVec (Core_Ptr_Unique_Unique_Type.t_unique 't) (Alloc_RawVec_Cap_Type.t_cap) 'a
 
 end
 module Alloc_Vec_Vec_Type

creusot/tests/should_fail/bug/211.stderr

@@ -5,22 +5,22 @@ error[E0004]: non-exhaustive patterns: `E::B` and `E::C` not covered
    |           ^^^ patterns `E::B` and `E::C` not covered
    |
 note: `E` defined here
-  --> 211.rs:3:5
+  --> 211.rs:1:10
    |
 1  | pub enum E {
-   |          -
+   |          ^
 2  |     A,
 3  |     B,
-   |     ^ not covered
+   |     - not covered
 4  |     C,
-   |     ^ not covered
+   |     - not covered
    = note: the matched value is of type `E`
 help: ensure that all possible cases are being handled by adding a match arm with a wildcard pattern, a match arm with multiple or-patterns as shown, or multiple match arms
    |
 11 ~         E::A => {},
 12 +         E::B | E::C => todo!()
    |
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 
 For more information about this error, try `rustc --explain E0004`.

creusot/tests/should_fail/bug/436_0.stderr

@@ -1,8 +1,8 @@
-error[creusot]: called prophetic logic function "prophecy" in logic context
+error: called Logic { prophetic: true } function in Logic { prophetic: false } context "prophecy"
   --> 436_0.rs:15:23
    |
 15 |     b.g = snapshot! { prophecy(b) + 1i32 };
    |                       ^^^^^^^^
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 

creusot/tests/should_fail/bug/436_1.stderr

@@ -1,10 +1,10 @@
-error[creusot]: called prophetic logic function "creusot_contracts::__stubs::fin" in logic context
+error: called Logic { prophetic: true } function in Logic { prophetic: false } context "creusot_contracts::__stubs::fin"
   --> 436_1.rs:10:5
    |
 10 |     pearlite! { *(^x).g }
    |     ^^^^^^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 

creusot/tests/should_fail/bug/436_2.stderr

@@ -1,8 +1,8 @@
-error[creusot]: Illegal use of the Snapshot type
+error: Illegal use of the Snapshot type
  --> 436_2.rs:6:10
   |
 6 |     Some(Snapshot<&'a mut Bad<'a>>),
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 

creusot/tests/should_fail/bug/603.stderr

@@ -15,7 +15,7 @@ error[E0277]: the trait bound `VecMap<K, V>: creusot_contracts::Default` is not
              usize
            and 22 others
 
-error[creusot]: error above
+error: error above
 
 error: aborting due to 2 previous errors
 

creusot/tests/should_fail/bug/borrowed_ghost.stderr

@@ -1,10 +1,10 @@
-error[creusot]: Use of borrowed variable x
+error: Use of borrowed variable x
  --> borrowed_ghost.rs:7:10
   |
 7 |     *r = snapshot! { !x.inner() }; // r = (snapshot (not (inner x)), x)
   |          ^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the macro `snapshot` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 

creusot/tests/should_fail/bug/specialize.mlcfg

@@ -17,12 +17,18 @@ module Core_Ptr_Unique_Unique_Type
     | C_Unique (Core_Ptr_NonNull_NonNull_Type.t_nonnull 't) (Core_Marker_PhantomData_Type.t_phantomdata 't)
 
 end
-module Alloc_RawVec_RawVec_Type
+module Alloc_RawVec_Cap_Type
   use prelude.UIntSize
   use prelude.Int
+  type t_cap  =
+    | C_Cap usize
+
+end
+module Alloc_RawVec_RawVec_Type
+  use Alloc_RawVec_Cap_Type as Alloc_RawVec_Cap_Type
   use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
   type t_rawvec 't 'a =
-    | C_RawVec (Core_Ptr_Unique_Unique_Type.t_unique 't) usize 'a
+    | C_RawVec (Core_Ptr_Unique_Unique_Type.t_unique 't) (Alloc_RawVec_Cap_Type.t_cap) 'a
 
 end
 module Alloc_Vec_Vec_Type

creusot/tests/should_fail/builtin_with_contract.stderr

@@ -6,11 +6,11 @@ warning: function `builtin_with_contract` is never used
   |
   = note: `#[warn(dead_code)]` on by default
 
-error[creusot]: cannot specify both `creusot::builtins` and a contract on the same definition
+error: cannot specify both `creusot::builtins` and a contract on the same definition
  --> builtin_with_contract.rs:7:1
   |
 7 | fn builtin_with_contract() {}
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: aborting due to previous error; 1 warning emitted
+error: aborting due to 1 previous error; 1 warning emitted
 

creusot/tests/should_fail/cycle.stderr

@@ -6,11 +6,11 @@ warning: unused import: `creusot_contracts::*`
   |
   = note: `#[warn(unused_imports)]` on by default
 
-error[creusot]: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[fa28]::f))}, {Item(DefId(0:6 ~ cycle[fa28]::g))}, {Item(DefId(0:5 ~ cycle[fa28]::f))}]
+error: encountered a cycle during translation: [{Item(DefId(0:5 ~ cycle[4e30]::f))}, {Item(DefId(0:6 ~ cycle[4e30]::g))}, {Item(DefId(0:5 ~ cycle[4e30]::f))}]
  --> cycle.rs:4:1
   |
 4 | pub fn f() {
   | ^^^^^^^^^^
 
-error: aborting due to previous error; 1 warning emitted
+error: aborting due to 1 previous error; 1 warning emitted
 

creusot/tests/should_fail/ghost_mapping.stderr

@@ -1,12 +1,12 @@
-error[creusot]: called prophetic logic function "creusot_contracts::__stubs::fin" in logic context
+error: called Logic { prophetic: true } function in Logic { prophetic: false } context "creusot_contracts::__stubs::fin"
   --> ghost_mapping.rs:11:5
    |
 11 |     pearlite! { |_| ^x }
    |     ^^^^^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error[creusot]: called prophetic logic function "creusot_contracts::__stubs::fin" in logic context
+error: called Logic { prophetic: true } function in Logic { prophetic: false } context "creusot_contracts::__stubs::fin"
   --> ghost_mapping.rs:21:5
    |
 21 |     pearlite! { forall<_x:Int> ^y == 1i32 }

creusot/tests/should_fail/impure_functions.stderr

@@ -1,10 +1,10 @@
-error[creusot]: called program function "std::vec::Vec::<T, A>::len" in logic context
+error: called Program function in Logic { prophetic: false } context "std::vec::Vec::<T, A>::len"
  --> impure_functions.rs:6:19
   |
 6 |     pearlite! { v.len()@ }
   |                   ^^^
 
-error[creusot]: called logic function "x" in program context
+error: called Logic { prophetic: false } function in Program context "x"
   --> impure_functions.rs:10:13
    |
 10 |     let _ = x(&Vec::<()>::new());

creusot/tests/should_fail/inexhaustive_match.stderr

@@ -5,19 +5,19 @@ error[E0004]: non-exhaustive patterns: `Option::Some(_)` not covered
   |           ^ pattern `Option::Some(_)` not covered
   |
 note: `Option<()>` defined here
- --> inexhaustive_match.rs:2:5
+ --> inexhaustive_match.rs:1:6
   |
 1 | enum Option<T> {
-  |      ------
+  |      ^^^^^^
 2 |     Some(T),
-  |     ^^^^ not covered
+  |     ---- not covered
   = note: the matched value is of type `Option<()>`
 help: ensure that all possible cases are being handled by adding a match arm with a wildcard pattern or an explicit pattern as shown
   |
 9 ~         None => (),
 10~         Option::Some(_) => todo!(),
   |
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 
 For more information about this error, try `rustc --explain E0004`.

creusot/tests/should_fail/infinite_size.stderr

@@ -12,6 +12,6 @@ help: insert some indirection (e.g., a `Box`, `Rc`, or `&`) to break the cycle
 2 ~ struct Tree2(Box<Node2>);
   |
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 
 For more information about this error, try `rustc --explain E0072`.

creusot/tests/should_fail/logic_prophetic_impl.stderr

@@ -1,8 +1,8 @@
-error[creusot]: Expected `f` to be a logic function as specified by the trait declaration
+error: Expected `f` to be a logic function as specified by the trait declaration
   --> logic_prophetic_impl.rs:11:5
    |
 11 |     fn f() {
    |     ^^^^^^
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 

creusot/tests/should_fail/non_bool_assertion.stderr

@@ -4,7 +4,7 @@ error[E0308]: mismatched types
 5 |     proof_assert! { 1 };
   |                     ^ expected `bool`, found `Int`
 
-error[creusot]: internal error
+error: internal error
 
 error: aborting due to 2 previous errors
 

creusot/tests/should_fail/opaque.stderr

@@ -1,8 +1,8 @@
-error[creusot]: Cannot make `"x::priv_symbol"` transparent in `"x::bad"` as it would call a less-visible item.
+error: Cannot make `"x::priv_symbol"` transparent in `"x::bad"` as it would call a less-visible item.
   --> opaque.rs:17:9
    |
 17 |         priv_symbol()
    |         ^^^^^^^^^^^^^
 
-error: aborting due to previous error
+error: aborting due to 1 previous error
 

creusot/tests/should_fail/result_param.stderr

@@ -6,11 +6,11 @@ warning: function `result_arg` is never used
   |
   = note: `#[warn(dead_code)]` on by default
 
-error[creusot]: `result` is not allowed as a parameter name
+error: `result` is not allowed as a parameter name
  --> result_param.rs:6:15
   |
 6 | fn result_arg(result: u32) {}
   |               ^^^^^^
 
-error: aborting due to previous error; 1 warning emitted
+error: aborting due to 1 previous error; 1 warning emitted
 

creusot/tests/should_fail/trait_item_types_mismatch.stderr

@@ -1,10 +1,10 @@
-error[creusot]: Expected implementation of trait `Trusted` for `()` to be marked as `#[trusted]`
+error: Expected implementation of trait `Trusted` for `()` to be marked as `#[trusted]`
  --> trait_item_types_mismatch.rs:7:1
   |
 7 | impl Trusted for () {}
   | ^^^^^^^^^^^^^^^^^^^
 
-error[creusot]: Expected `my_predicate` to be a predicate as specified by the trait declaration
+error: Expected `my_predicate` to be a predicate as specified by the trait declaration
   --> trait_item_types_mismatch.rs:17:5
    |
 17 |     fn my_predicate() -> bool {

creusot/tests/should_fail/unsafe.stderr

@@ -6,14 +6,14 @@ warning: unused import: `std::*`
   |
   = note: `#[warn(unused_imports)]` on by default
 
-error[E0133]: call to unsafe function is unsafe and requires unsafe function or block
+error[E0133]: call to unsafe function `evil` is unsafe and requires unsafe function or block
  --> unsafe.rs:8:5
   |
 8 |     evil();
   |     ^^^^^^ call to unsafe function
   |
   = note: consult the function's documentation for information on how to avoid undefined behavior
 
-error: aborting due to previous error; 1 warning emitted
+error: aborting due to 1 previous error; 1 warning emitted
 
 For more information about this error, try `rustc --explain E0133`.

creusot/tests/should_fail/unsupported_binary_operations.stderr

@@ -18,11 +18,11 @@ warning: function `bit_xor` is never used
 11 | fn bit_xor(a: u32, b: u32) -> u32 {
    |    ^^^^^^^
 
-error[creusot]: bitwise operations are currently unsupported
+error: bitwise operations are currently unsupported
  --> unsupported_binary_operations.rs:4:5
   |
 4 |     a & b
   |     ^^^^^
 
-error: aborting due to previous error; 3 warnings emitted
+error: aborting due to 1 previous error; 3 warnings emitted