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 /doc/style.css | |
parent | 659c06eb4fabce59751476ddeb2e065759f19765 (diff) | |
download | compcert-b4130798bd428ad3586baa17b0f991018854997a.tar.gz compcert-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 'doc/style.css')
0 files changed, 0 insertions, 0 deletions