Xavier Denis
Xavier Denis
if a crate contains extra executables in `src/bin/foo.rs` `cargo creusot` will also attempt to verify them and there is no way to disable this behavior. Using `trusted` is insufficient as...
`cargo creusot` attempts to compile build.rs scripts and often doesn't like what it finds.
Adds parser support for ranges like `0..10` and also adds an instance of `IndexLogic` for `Seq` that uses that to call `subsequence`. This should make sequence heavy specifications _much_ nicer...
the following program crashes ``` extern crate creusot_contracts; use creusot_contracts::*; struct X(Vec); impl X { pub fn foo() -> Self { let mut v: Vec = (0..10).map_inv(|_, _| None).collect(); X(v)...
We currently have a hard requirement where we must dynamically link against the same version of `rustc_driver` that was used to build `cargo creusot` at each invocation. Unfortunately if they...
Extracted from #656, we need to add an `assume` construct, which could also be used in `invariant` for `for` loops.
We like to use `ExternSpec` to strengthen the predicates associated to trait methods. This works pretty well for methods of traits which do not have additional generic parameters, but completely...
I'm just trying out `drom` for a small project and wanted to open an issue with the various problems / issues I'm encountering. I hope this will be useful for...
Some form of tta-expansion should probably be done... Right now there's a bug where if a function is defined like: ``` a :: b -> b -> b fn a()...