diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-12 19:18:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
| commit | b4130798bd428ad3586baa17b0f991018854997a (patch) | |
| tree | 7330a228071a119a60a0fcb0fe9448d7f8262de6 /common | |
| parent | 659c06eb4fabce59751476ddeb2e065759f19765 (diff) | |
| download | compcert-kvx-b4130798bd428ad3586baa17b0f991018854997a.tar.gz compcert-kvx-b4130798bd428ad3586baa17b0f991018854997a.zip | |
Asmgenproof0: add predicate exec_straight0
This is a variant of exec_straight where it is allowed to take zero steps.
In other words, exec_straight0 is the "star" relation, while exec_straight
is the "plus" relation.
In the end we need "plus" relations in simulation diagrams, to show
the absence of stuttering. But the "star" relation exec_straight0 is
useful to reason about code fragments that are always preceded or
followed by at least one instruction.
Diffstat (limited to 'common')
0 files changed, 0 insertions, 0 deletions