diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 12:53:19 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-16 12:53:19 +0000 |
| commit | 1fe28ba1ec3dd0657b121c4a911ee1cb046bab09 (patch) | |
| tree | 7f3b22fade6b3d7b7871624aa0ccf4ef52a10e84 /extraction | |
| parent | f8d59bccd57fd53b55de5e9dd96fbc1af150951a (diff) | |
Distinguish two kinds of nonterminating behaviors: silent divergence
and reactive divergence. As a consequence:
- Removed the Enilinf constructor from traceinf (values of traceinf
type are always infinite traces).
- Traces are now uniquely defined.
- Adapted proofs big step -> small step for Clight and Cminor accordingly.
- Strengthened results in driver/Complements accordingly.
- Added common/Determinism to collect generic results about
deterministic semantics.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'extraction')
0 files changed, 0 insertions, 0 deletions