CONTRACTS: ensure at most one predicate per pointer#8577

Open

remi-delmas-3000 wants to merge 3 commits intodiffblue:developfrom remi-delmas-3000:contracts-ptr-pred-ctx

+938-405

Commits on Jan 25, 2025

CONTRACTS: separation checks using nondet demonic variable
Remi Delmas
committed
CONTRACTS: at most one predicate occurence per pointer
Remi Delmas
committed
Refresh memory predicate documentation, add paragraph about using pointer predicates in disjunctions.
Remi Delmas
committed