attempted to read from stolen value: rustc_middle::thir::Thir

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.

GNU Lesser General Public License v2.1

1.15k stars 50 forks source link

attempted to read from stolen value: rustc_middle::thir::Thir #940

Open Kixunil opened 9 months ago

Kixunil commented 9 months ago

I tired running creusot from master (eb3d2c05080e47c01546e19d348722817f2aa42e) and got this error:

thread 'rustc' panicked at creusot/src/ctx.rs:395:25:
attempted to read from stolen value: rustc_middle::thir::Thir

xldenis commented 9 months ago

can you provide the program you attempted to run it on and the specific command you used?

Kixunil commented 8 months ago

I did it in a disposable VM which I already killed :) But the code is too large anyway.

Basically I was trying to prove that this type is correct: https://github.com/rust-bitcoin/rust-bitcoin/blob/4544f5d3c2b7b3babac499a25f1053064636d7b2/bitcoin/src/pow.rs#L322

I added ensures(result.to_be_bytes() == a) on top of from_be_bytes and analogous for LE, moved build.rs to avoid failures and ran cargo creusot.