Generate contracts of dependencies as assertions#3802

Merged

carolynzech merged 19 commits intomodel-checking:mainfrom

carolynzech:contracts-as-assertions

Jan 9, 2025

Commits on Dec 28, 2024

replace ClosureType with ContractMode (to be consistent with kani-compiler)
Carolyn Zech
committed
move split_for_remembers to shared.rs; remove unused variants
Carolyn Zech
committed

Commits on Dec 29, 2024

add ContractMode for assertions to library/kani_macros
Carolyn Zech
committed
add option to use Assert ContractMode
Carolyn Zech
committed

Commits on Dec 30, 2024

tests
Carolyn Zech
committed
documentation
Carolyn Zech
committed
tweak comment
Carolyn Zech
committed
doc nits
Carolyn Zech
committed

Commits on Dec 31, 2024

Merge branch 'main' of github.com:model-checking/kani into contracts-as-assertions
Carolyn Zech
committed
wrap body in a closure
Carolyn Zech
committed
simplify tests to reduce runner load
Carolyn Zech
committed
add loops test
Carolyn Zech
committed
update docs to reflect body wrapper closure
Carolyn Zech
committed

Commits on Jan 2, 2025

Apply suggestions from code review

Carolyn Zech
and
zhassan-aws
authored
clarify tests
Carolyn Zech
committed

Commits on Jan 7, 2025

make asserting contracts the default
Carolyn Zech
committed
add simple precedence test
Carolyn Zech
committed
clap nits
Carolyn Zech
authored

Commits on Jan 8, 2025

Merge branch 'main' into contracts-as-assertions
Carolyn Zech
authored