Xavier Denis comments

Results 113 comments of


Xavier Denis

Using pearlite! in a regular Rust function should probably error

``` use rustc_hir::def_id::DefId; use rustc_lint::{LateContext, LateLintPass, LintContext}; use rustc_session::{declare_tool_lint, impl_lint_pass}; use rustc_span::{ExpnData, ExpnId, Span}; use crate::util; declare_tool_lint! { /// Blah Blah pub creusot::PEARLITE, Forbid, "checks for valid usages of the...

Using pearlite! in a regular Rust function should probably error

Today, we don't forbid the actual macro, but any call to a logical symbol will raise an error. I'm going to close this for now.

Make it possible to hide the body of public logic function

Fixed through the addition of opacity and the `#[open(..)]` annotation.

Not useful error message: "call expression requires function"

I just had an idea: we can use a lint to check this !

Specifications on logic functions and predicates which use `exists`/`forall` cause a Why3 error

Fixed.

Error when user forgets to use `pearlite!`

We now provide an error message when logical symbols are used outside of `pearlite!` contexts.

Underscore as the last character of a logic function has the potential to cause Why3 errors

Fixed.

Support macro invocations in pearlite terms.

We've settled on only allowing whitelisted macros for now (`proof_assert`).

Support macro invocations in pearlite terms.

> The problem being that arbitrary macros could allow writing non-pearlite code in pearlite context. I don't really consider this a problem we need to defend against. They wouldn't be...

Deriving `PartialEq` is not supported for enums with more than one variant.

Should be supported now that we have a `PartialEq` derive.