diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-01 10:16:05 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-05 13:53:16 +0200 |
| commit | 108d60c059949e34c07719cb3ce38b8c62d27e0d (patch) | |
| tree | 450494edca954f8d4f4a593c8b95ef0c08c4eec6 /backend/ValueAnalysis.v | |
| parent | e8dc5a7222dbb81306883e4f19eb5b0c33b0d5e0 (diff) | |
| download | compcert-108d60c059949e34c07719cb3ce38b8c62d27e0d.tar.gz compcert-108d60c059949e34c07719cb3ce38b8c62d27e0d.zip | |
Recognize more if-then-else statements that can be if-converted
Ignore debug statements that could have prevented the recognition
of a simple assignment.
Since debug statements can formally get stuck, revise the simulation
diagram to use the "eventually" modality.
Diffstat (limited to 'backend/ValueAnalysis.v')
0 files changed, 0 insertions, 0 deletions