CONTRACTS: Dynamic frames for loop contracts#7541

Merged

qinheping merged 10 commits intodiffblue:developfrom

qinheping:loop-contracts-dfcc

May 11, 2023

Commits on May 10, 2023

CONTRACTS: pointer predicates now use dfcc_cfg_infot
Remi Delmas
committed
CONTRACTS: avoid circular dependency between classes
Remi Delmas
committed
CONTRACTS: fix missing source location
Remi Delmas
committed
CONTRACTS: add loop contracts support in DFCC
Remi Delmas
committed
CONTRACTS: update loop tests for DFCC
Remi Delmas
committed
CONTRACTS: loop normal form tests for DFCC
Remi Delmas
committed
CONTRACTS: new test with ternary assignment LHS
Remi Delmas
committed
CONTRACTS: test combination of loop contracts and recursive functions
Remi Delmas
committed
CONTRACTS: deduplicate tests
Remi Delmas
committed
fix missing file doc
Remi Delmas
committed