search

AeneasVerif / aeneas

A verification toolchain for Rust programs
Apache License 2.0
186 stars 15 forks source link

Trait overriding from the libstd is not supported #133

Closed RaitoBezarius closed 6 months ago

RaitoBezarius commented 6 months ago

If I use the libstd's order machinery, I can obtain:

❯ nix run github:aeneasverif/aeneas -L -- -backend lean avl_verification.llbc
[Info ] Imported: avl_verification.llbc
[Error] Overriding trait provided methods in trait implementations is not supported yet (overriden methods: lt, le, ge, gt)
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cmp.rs', lines 1357:12-1370:13

Reproducer: https://github.com/RaitoBezarius/avl-verification/tree/rust-avl-std

cc @Nadrieril

Nadrieril commented 6 months ago

I'm on it! Duplicate of https://github.com/AeneasVerif/aeneas/issues/70.