Enumerative loop invariant synthesizers. More...
#include <enumerative_loop_invariant_synthesizer.h>
Inheritance diagram for enumerative_loop_invariant_synthesizert: Collaboration diagram for enumerative_loop_invariant_synthesizert:Public Member Functions | |
| enumerative_loop_invariant_synthesizert (const goto_modelt &goto_model, messaget &log) | |
| invariant_mapt | synthesize_all () override |
| This synthesizer guarantees that, with the synthesized loop invariants, all checks in the annotated GOTO program pass. More... | |
| exprt | synthesize (loop_idt loop_id) override |
Synthesize loop invariant for a specified loop in the goto_model. More... | |
| Public Member Functions inherited from loop_invariant_synthesizer_baset | |
| loop_invariant_synthesizer_baset (const goto_modelt &goto_model, messaget &log) | |
| virtual | ~loop_invariant_synthesizer_baset ()=default |
Private Member Functions | |
| void | init_candidates () |
| Initialize invariants as true for all unannotated loops. More... | |
Private Attributes | |
| invariant_mapt | invariant_candiate_map |
Additional Inherited Members | |
| Protected Attributes inherited from loop_invariant_synthesizer_baset | |
| const goto_modelt & | goto_model |
| messaget & | log |
Detailed Description
Enumerative loop invariant synthesizers.
It is designed for goto_model containing only checks instrumented by goto-instrument with the --pointer-check flag. When other checks present, it will just enumerate candidates and check if they are valid.
Definition at line 28 of file enumerative_loop_invariant_synthesizer.h.
Constructor & Destructor Documentation
◆ enumerative_loop_invariant_synthesizert()
|
inline |
Definition at line 32 of file enumerative_loop_invariant_synthesizer.h.
Member Function Documentation
◆ init_candidates()
|
private |
Initialize invariants as true for all unannotated loops.
Definition at line 14 of file enumerative_loop_invariant_synthesizer.cpp.
◆ synthesize()
Synthesize loop invariant for a specified loop in the goto_model.
Implements loop_invariant_synthesizer_baset.
Definition at line 48 of file enumerative_loop_invariant_synthesizer.cpp.
◆ synthesize_all()
|
overridevirtual |
This synthesizer guarantees that, with the synthesized loop invariants, all checks in the annotated GOTO program pass.
Implements loop_invariant_synthesizer_baset.
Definition at line 39 of file enumerative_loop_invariant_synthesizer.cpp.
Member Data Documentation
◆ invariant_candiate_map
|
private |
Definition at line 48 of file enumerative_loop_invariant_synthesizer.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp
