diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-15 11:13:11 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2021-01-13 14:45:05 +0100 |
| commit | e16f5d1de08bb0c3ac561c2ea6a98f49ed8f49d5 (patch) | |
| tree | 92cb8fbf813f773779d13da9194adf86700a195f /powerpc | |
| parent | bbf3b4140f4263cdcb7dcb9c9a32c8c7651818d8 (diff) | |
| download | compcert-kvx-e16f5d1de08bb0c3ac561c2ea6a98f49ed8f49d5.tar.gz compcert-kvx-e16f5d1de08bb0c3ac561c2ea6a98f49ed8f49d5.zip | |
Revised correctness proof for record_goto
We used to define an instrumented version record_goto' that also
builds the measure f, prove it correct, then show equivalence with
record_goto.
The new proofs make do without the instrumented version. They prove
strong existence of the measure, as in
`{ f | branch_map_correct (record_goto fn) f}`.
Diffstat (limited to 'powerpc')
0 files changed, 0 insertions, 0 deletions