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 /lib/Readconfig.mll | |
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 'lib/Readconfig.mll')
0 files changed, 0 insertions, 0 deletions