search

AeneasVerif / aeneas

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

Aeneas still generate `as` variable names even though they are reserved keywords #210

Closed RaitoBezarius closed 4 months ago

RaitoBezarius commented 4 months ago

Repro: https://github.com/RaitoBezarius/avl-verification/tree/avl

Things like:

let as ← AVLTreeSet.insert_rebalance_left_loop T OrdInst self.root

are still generated so far, even after https://github.com/AeneasVerif/aeneas/pull/146.

RaitoBezarius commented 3 months ago

Still an issue in https://github.com/AeneasVerif/aeneas/commit/3f07bf067fe725c2bc60b12139ff9cba13375c6a (main).

sonmarcho commented 3 months ago

Triggered by the AVL trees?

sonmarcho commented 3 months ago

(if yes I can reopen the issue)

RaitoBezarius commented 3 months ago

Argh, that might be related to me messing up my version of Charon/Aeneas actually, please ignore.