CONTRACTS: Dynamic frame condition checking#6887

Closed

remi-delmas-3000 wants to merge 20 commits intodiffblue:developfrom

remi-delmas-3000:contracts-dfcc

Commits on Sep 22, 2022

CONTRACTS: Front-end extensions for assigns clauses and frees clauses.
Remi Delmas
committed
CONTRACTS: Front-end: frees clause improvements
Remi Delmas
committed
CONTRACTS: Front-end extension: add `__CPROVER_is_freshr`
Remi Delmas
committed
CONTRACTS: Add class `dfcc_utilst` for DFCC utility methods.
Remi Delmas
committed
CONTRACTS: Add library functions for dynamic frames
Remi Delmas
committed
CONTRACTS: Add `dfcc_contract_modet` and `dfcc_contract_handlert`.
Remi Delmas
committed
CONTRACTS: Map built-in predicate calls to their contract implem.
Remi Delmas
committed
CONTRACTS: Add class `goto_program_cfg_infot`.
Remi Delmas
committed
CONTRACTS: Add class `dfcc_instrumentt` to instrument goto
Remi Delmas
committed
CONTRACTS: Adds the `dfcc_spec_functionst` class.
Remi Delmas
committed
CONTRACTS: Add the `dfcc_dsl_contract_functionst` class.
Remi Delmas
committed
dfcc_dsl_contract_functionst fixes
Remi Delmas
committed
CONTRACTS: Add the `dfcc_dsl_wrapper_programt` class.
Remi Delmas
committed
CONTRACTS: Add the `dfcc_dsl_contract_handlert` class.
Remi Delmas
committed
CONTRACTS: Add the `dfcc_swap_and_wrapt class`.
Remi Delmas
committed
dfcc_swap_and_wrap fixes
Remi Delmas
committed
CONTRACTS: Add class `dfcct`, the main class for
Remi Delmas
committed
CONTRACTS: add the `--dfcc` switch to the goto-instrument CLI interface
Remi Delmas
committed
CONTACTS: update regression test suite for DFCC
Remi Delmas
committed
developer doc for contracts with dynamic frames
Remi Delmas
committed