Xia Li-yao
Xia Li-yao
CI uses the `--creusot-contracts` option which was accidentally left unimplemented. This implements it.
It would be nice if why3find came back online soon...
> I would like `result` to be accessed with a special syntax which would not conflict with identifiers, like `res!` or so.
They appear in code generated by the `#[test]` macro (so this would help solve #1265). ```rust extern crate creusot_contracts; fn foo() {} struct Test(fn()); fn example1() -> Test { Test(foo)...
If crate B uses a `const` from crate A, then borrows in the body of the `const` will not be resolved. This breaks soundness because this also omits type invariant...
#1684 is a hack to avoid the crash (issue #1683) but it would be nice to know what is going on exactly. If it is a rustc bug maybe it...
The opacity check (`opacity.rs`) is implemented using `visit_term` which never calls `visit_pattern` (a warning about this appears when upgrading the toolchain to a new nightly). Fixing that causes the following...
From discussion at #1565, the way we currently use the trait solver via `codegen_select_candidate` is not ideal because (1) we lose information in case of ambiguity (2) we need access...
It is currently not possible to override the default `collect` implementation: - The signature `fn collect` must have a `B: ::std::iter::FromIterator` bound - But the extern specs for this method...