Skip to content

Migrate loop contracts to dynamic frames in CBMC #2155

Closed
@remi-delmas-3000

Description

@remi-delmas-3000

Proposed change:
Migrate loop contract transformation from src/goto-instrument/contracts/contracts.cpp to ``src/goto-instrument/contracts/dynamic-frames/dfcc.cpp`

Motivation:
Extend the new contract contract system complete by including loop contracts.

Metadata

Metadata

Labels

[C] InternalTracks some internal work. I.e.: Users should not be affected.

Type

No type

Projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions