diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:08:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-04 15:08:29 +0000 |
| commit | 73729d23ac13275c0d28d23bc1b1f6056104e5d9 (patch) | |
| tree | e3044ce75edb30377bd8c87356b7617eba5ed223 /Makefile | |
| parent | c79434827bf2bd71f857f4471f7bbf381fddd189 (diff) | |
Fusion de la branche "traces":
- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 18 |
1 files changed, 11 insertions, 7 deletions
@@ -2,16 +2,16 @@ COQC=coqc $(INCLUDES) COQDEP=coqdep $(INCLUDES) COQDOC=coqdoc -INCLUDES=-I lib -I backend +INCLUDES=-I lib -I backend -I cfrontend # Files in lib/ LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \ - Integers.v Floats.v + Iteration.v Integers.v Floats.v Parmov.v # Files in backend/ -BACKEND=AST.v Values.v Mem.v Globalenvs.v \ +BACKEND=AST.v Values.v Mem.v Events.v Globalenvs.v \ Op.v Cminor.v \ Cmconstr.v Cmconstrproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v \ @@ -24,8 +24,7 @@ BACKEND=AST.v Values.v Mem.v Globalenvs.v \ Locations.v Conventions.v LTL.v LTLtyping.v \ InterfGraph.v Coloring.v Coloringproof.v \ Parallelmove.v Allocation.v \ - Allocproof_aux.v Allocproof.v \ - Alloctyping_aux.v Alloctyping.v \ + Allocproof.v Alloctyping.v \ Tunneling.v Tunnelingproof.v Tunnelingtyping.v \ Linear.v Lineartyping.v \ Linearize.v Linearizeproof.v Linearizetyping.v \ @@ -35,11 +34,16 @@ BACKEND=AST.v Values.v Mem.v Globalenvs.v \ PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v \ Main.v +# Files in cfrontend/ + +CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \ + Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v + # All source files -FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%) +FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%) -FLATFILES=$(LIB) $(BACKEND) +FLATFILES=$(LIB) $(BACKEND) $(CFRONTEND) proof: $(FILES:.v=.vo) |