Creusot errors with "unsupported type" on functions returning impl FnMut

[jhaye]

The project I'm attempting to use Creusot for uses nom for parsing. The crate has many functions which have the return type impl FnMut(I) -> IResult<I, O, E>. An example of this is all_consuming(…), .

Creusot fails with the following error:

error[creusot]: unsupported type impl FnMut(I)-> std::result::Result<(I, O), nom::Err<E>>
   --> ~/.cargo/registry/src/github.com-1ecc6299db9ec823/nom-7.1.1/src/combinator/mod.rs:382:1
    |
382 | / pub fn all_consuming<I, O, E: ParseError<I>, F>(mut f: F) -> impl FnMut(I) -> IResult<I, O, E>
383 | | where
384 | |   I: InputLength,
385 | |   F: Parser<I, O, E>,
    | |_____________________^

[xldenis]

Indeed, I haven't thought about how to integrate impl Trait into Creusot, though I don't think it is necessarily so difficult. What are you expecting to prove? I imagine that working with nom in proofs will be quite challenging since it's a large complex library without specifications.

[jhaye]

I'm trying to get it to compile with Creusot first. This is a side project of mine which I want to use to gauge Creusot's ability to integrate with an existing code base. It's a quasi copy of the Berkley parser. If this is not supported yet, I can just discard the input parsing of the program and see if I can prove that it doesn't crash without them and then move on from there.

[xldenis]

You can mark functions as #[trusted] to tell creusot to skip them. This will still translate the signatures but should be used for parts of the code that can't / shouldn't be verified (like a parser)