unbound type symbol 'opaque_ptr' in why3 ide

[nishanthkarthik]

Hi! I built creusot by following the steps at https://github.com/creusot-rs/creusot and created an empty rust project with the same toolchain version to test a contract. When I run cargo creusot, I see an mlcfg file generated but this is not loaded by the why3 ide

I am using the ide script from the repo root.

Unrecognized source format `mlcfg`
File "../ghostptrtoken_test-bin.mlcfg", line 67, characters 39-49: unbound type symbol 'opaque_ptr'

The prelude pointed to by the ide script does point to a type in prelude.mlw.

The snippet I'm trying to use to test creusot contract is

use creusot_contracts::*;
use creusot_contracts::ghost_ptr::GhostPtrToken;
use ::std::ops::Deref;
use ::std::ptr::null;

fn main() {
    let mut tok = GhostPtrToken::new();
    let b = Box::new(1);
    let p = tok.ptr_from_box(b);
    let mut r = tok.ptr_to_box(p);
    *r += 5;
}

[Armael]

Hi! I'm not a Creusot expert, but from what I can see this error is the result of the ide script malfunctioning.
What you can do, instead of using the script, is to use the cargo creusot why3 ide command to launch the why3 IDE on your code.
Unfortunately the current instructions in the README do not mention it, and I plan to fix that really soon (the ide script will then only be used when working on the creusot testsuite).

Using cargo creusot why3 ide I was able to launch the why3 ide on your code and have the proofs go through!

NB: there's currently a bug with cargo creusot why3 ide (#943) where cargo won't launch the IDE if the mlcfg is "up to date"... So you need to make some changes to the source file then launch cargo creusot why3 ide. It's also on my list to try to fix this.