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 /Makefile | |
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 'Makefile')
-rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -41,7 +41,7 @@ LIB=Coqlib.v Maps.v Lattice.v Ordered.v \ # Parts common to the front-ends and the back-end (in common/) COMMON=Errors.v AST.v Events.v Globalenvs.v Mem.v Values.v \ - Smallstep.v Switch.v + Smallstep.v Determinism.v Switch.v # Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) |