Основні моменти релізу Halmos v0.3.0! (Коротке нагадування: Halmos — це інструмент для символьного тестування байт-коду EVM, який чудово взаємодіє з проектами ливарного виробництва та підтримує кілька розв'язувачів SMT) 1. Ми (нарешті) додали підтримку інваріантного тестування зі збереженням стану

2. звіти про покриття (просто запустіть з --coverage), а потім або згенеруйте результат, або візуалізуйте його в VSCode

3. Флеймографи Дещо дивний, але цікавий спосіб візуалізувати інваріантну тестову кампанію. Просто запустіть з --flamegraph

5. Краща підтримка розв'язувача before: --solver-command "yices-smt2 --smt2-model-format" після: --solver yices before: --solver-command "bitwuzla --produce-models --abstraction" після: --solver bitwuzla-abs

6. Дружба закінчилася на Z3, YICES тепер вирішує за замовчуванням (тому вам навіть не потрібно казати '--solver yices', щоб насолодитися перевагами)

7. Підтримка SOLX Якщо ви не знаєте, що таке Solx, @PatrickAlphaC вам допоможе

8. Додані чит-коди ENV* і випадкові*, всього 3 мільйони. Дякуємо @Jayakumar2812 за внесок!

9. Круті індикатори прогресу з майбутнього

Ось і все! Отримайте його зараз: Встановлення уф-інструменту --Python 3.13 Halmos