diff options
| -rw-r--r-- | .depend | 118 | ||||
| -rw-r--r-- | Makefile | 17 | ||||
| -rw-r--r-- | cfrontend/Cminorgen.v (renamed from backend/Cminorgen.v) | 0 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v (renamed from backend/Cminorgenproof.v) | 0 | ||||
| -rw-r--r-- | cfrontend/Csharpminor.v (renamed from backend/Csharpminor.v) | 0 | ||||
| -rw-r--r-- | common/AST.v (renamed from backend/AST.v) | 0 | ||||
| -rw-r--r-- | common/Events.v (renamed from backend/Events.v) | 0 | ||||
| -rw-r--r-- | common/Globalenvs.v (renamed from backend/Globalenvs.v) | 0 | ||||
| -rw-r--r-- | common/Main.v (renamed from backend/Main.v) | 0 | ||||
| -rw-r--r-- | common/Mem.v (renamed from backend/Mem.v) | 0 | ||||
| -rw-r--r-- | common/Values.v (renamed from backend/Values.v) | 0 | ||||
| -rw-r--r-- | extraction/Makefile | 2 |
12 files changed, 70 insertions, 67 deletions
@@ -9,64 +9,64 @@ lib/Iteration.vo: lib/Iteration.v lib/Coqlib.vo lib/Integers.vo: lib/Integers.v lib/Coqlib.vo lib/Floats.vo: lib/Floats.v lib/Integers.vo lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo -backend/AST.vo: backend/AST.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo -backend/Values.vo: backend/Values.v lib/Coqlib.vo backend/AST.vo lib/Integers.vo lib/Floats.vo -backend/Mem.vo: backend/Mem.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo -backend/Events.vo: backend/Events.v lib/Coqlib.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo -backend/Globalenvs.vo: backend/Globalenvs.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo -backend/Op.vo: backend/Op.v lib/Coqlib.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo -backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Events.vo backend/Values.vo backend/Mem.vo backend/Op.vo backend/Globalenvs.vo -backend/Cmconstr.vo: backend/Cmconstr.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Op.vo backend/Globalenvs.vo backend/Cminor.vo -backend/Cmconstrproof.vo: backend/Cmconstrproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Op.vo backend/Globalenvs.vo backend/Cminor.vo backend/Cmconstr.vo -backend/Csharpminor.vo: backend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo -backend/Cminorgen.vo: backend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo lib/Integers.vo backend/Mem.vo backend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo -backend/Cminorgenproof.vo: backend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo backend/Cminorgen.vo backend/Cmconstrproof.vo -backend/Registers.vo: backend/Registers.v lib/Coqlib.vo backend/AST.vo lib/Maps.vo lib/Sets.vo -backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo -backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo -backend/RTLgenproof1.vo: backend/RTLgenproof1.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo -backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof1.vo -backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Globalenvs.vo backend/Values.vo backend/Mem.vo lib/Integers.vo backend/Events.vo +common/AST.vo: common/AST.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo +common/Events.vo: common/Events.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo +common/Globalenvs.vo: common/Globalenvs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo +common/Mem.vo: common/Mem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo +common/Values.vo: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo +common/Main.vo: common/Main.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo backend/PPC.vo cfrontend/Cminorgen.vo backend/RTLgen.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Stacking.vo backend/PPCgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/Cminorgenproof.vo backend/RTLgenproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2mach.vo backend/PPCgenproof.vo +backend/Op.vo: backend/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo +backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Mem.vo backend/Op.vo common/Globalenvs.vo +backend/Cmconstr.vo: backend/Cmconstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo backend/Op.vo common/Globalenvs.vo backend/Cminor.vo +backend/Cmconstrproof.vo: backend/Cmconstrproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo backend/Op.vo common/Globalenvs.vo backend/Cminor.vo backend/Cmconstr.vo +backend/Registers.vo: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Sets.vo +backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo +backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo +backend/RTLgenproof1.vo: backend/RTLgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo +backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof1.vo +backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo common/Globalenvs.vo common/Values.vo common/Mem.vo lib/Integers.vo common/Events.vo backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo -backend/Constprop.vo: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo -backend/Constpropproof.vo: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Constprop.vo -backend/CSE.vo: backend/CSE.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo -backend/CSEproof.vo: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo -backend/Locations.vo: backend/Locations.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo -backend/Conventions.vo: backend/Conventions.v lib/Coqlib.vo backend/AST.vo backend/Locations.vo -backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo -backend/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/Constprop.vo: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo +backend/Constpropproof.vo: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Constprop.vo +backend/CSE.vo: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo +backend/CSEproof.vo: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo +backend/Locations.vo: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo +backend/Conventions.vo: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo +backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo +backend/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo -backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo -backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo -backend/Parallelmove.vo: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo backend/Values.vo backend/Events.vo backend/AST.vo backend/Locations.vo backend/Conventions.vo -backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Parallelmove.vo backend/LTL.vo -backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Parallelmove.vo backend/Allocation.vo backend/LTL.vo -backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Parallelmove.vo -backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo -backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo -backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo -backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo -backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo backend/AST.vo backend/Values.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Kildall.vo lib/Lattice.vo -backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo lib/Lattice.vo -backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Conventions.vo -backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo -backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Mem.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo -backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Mem.vo lib/Integers.vo backend/Values.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo -backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Conventions.vo -backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Op.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Locations.vo backend/Mach.vo backend/Machabstr.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Stacking.vo -backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo backend/AST.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Stacking.vo backend/Stackingproof.vo -backend/Machabstr2mach.vo: backend/Machabstr2mach.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Machabstr.vo backend/Mach.vo backend/Machtyping.vo backend/Stackingproof.vo -backend/PPC.vo: backend/PPC.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo -backend/PPCgen.vo: backend/PPCgen.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/PPC.vo -backend/PPCgenproof1.vo: backend/PPCgenproof1.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/Conventions.vo -backend/PPCgenproof.vo: backend/PPCgenproof.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/PPCgenproof1.vo -backend/Main.vo: backend/Main.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo backend/Values.vo backend/Csharpminor.vo backend/Cminor.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo backend/PPC.vo backend/Cminorgen.vo backend/RTLgen.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Stacking.vo backend/PPCgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Machtyping.vo backend/Cminorgenproof.vo backend/RTLgenproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2mach.vo backend/PPCgenproof.vo -cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo backend/AST.vo -cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/Values.vo backend/AST.vo backend/Mem.vo backend/Events.vo backend/Globalenvs.vo cfrontend/Csyntax.vo -cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo backend/AST.vo cfrontend/Csyntax.vo -cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo backend/AST.vo cfrontend/Csyntax.vo backend/Csharpminor.vo -cfrontend/Cshmgenproof1.vo: cfrontend/Cshmgenproof1.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/AST.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo backend/Csharpminor.vo cfrontend/Cshmgen.vo -cfrontend/Cshmgenproof2.vo: cfrontend/Cshmgenproof2.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/AST.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo backend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo -cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo backend/AST.vo backend/Values.vo backend/Events.vo backend/Mem.vo backend/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo backend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo cfrontend/Cshmgenproof2.vo +backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo +backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo +backend/Parallelmove.vo: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo +backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Parallelmove.vo backend/LTL.vo +backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Parallelmove.vo backend/Allocation.vo backend/LTL.vo +backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Parallelmove.vo +backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo +backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo +backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo +backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo +backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo common/AST.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Kildall.vo lib/Lattice.vo +backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo lib/Lattice.vo +backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Conventions.vo +backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo +backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo +backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo +backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Conventions.vo +backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo backend/Op.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Locations.vo backend/Mach.vo backend/Machabstr.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Stacking.vo +backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Stacking.vo backend/Stackingproof.vo +backend/Machabstr2mach.vo: backend/Machabstr2mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Machabstr.vo backend/Mach.vo backend/Machtyping.vo backend/Stackingproof.vo +backend/PPC.vo: backend/PPC.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo +backend/PPCgen.vo: backend/PPCgen.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/PPC.vo +backend/PPCgenproof1.vo: backend/PPCgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/Conventions.vo +backend/PPCgenproof.vo: backend/PPCgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/PPC.vo backend/PPCgen.vo backend/PPCgenproof1.vo +cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/AST.vo +cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo +cfrontend/Ctyping.vo: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo cfrontend/Csyntax.vo +cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csharpminor.vo +cfrontend/Cshmgenproof1.vo: cfrontend/Cshmgenproof1.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo +cfrontend/Cshmgenproof2.vo: cfrontend/Cshmgenproof2.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo +cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo cfrontend/Cshmgenproof2.vo +cfrontend/Csharpminor.vo: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo +cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo common/AST.vo lib/Integers.vo common/Mem.vo cfrontend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo +cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo cfrontend/Cminorgen.vo backend/Cmconstrproof.vo @@ -2,19 +2,22 @@ COQC=coqc $(INCLUDES) COQDEP=coqdep $(INCLUDES) COQDOC=coqdoc -INCLUDES=-I lib -I backend -I cfrontend +INCLUDES=-I lib -I common -I backend -I cfrontend # Files in lib/ LIB=Coqlib.v Maps.v Sets.v union_find.v Inclusion.v Lattice.v Ordered.v \ Iteration.v Integers.v Floats.v Parmov.v +# Files in common/ + +COMMON=AST.v Events.v Globalenvs.v Mem.v Values.v Main.v + # Files in backend/ -BACKEND=AST.v Values.v Mem.v Events.v Globalenvs.v \ +BACKEND=\ Op.v Cminor.v \ Cmconstr.v Cmconstrproof.v \ - Csharpminor.v Cminorgen.v Cminorgenproof.v \ Registers.v RTL.v \ RTLgen.v RTLgenproof1.v RTLgenproof.v \ RTLtyping.v \ @@ -31,17 +34,17 @@ BACKEND=AST.v Values.v Mem.v Events.v Globalenvs.v \ Mach.v Machabstr.v Machtyping.v \ Stacking.v Stackingproof.v Stackingtyping.v \ Machabstr2mach.v \ - PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v \ - Main.v + PPC.v PPCgen.v PPCgenproof1.v PPCgenproof.v # Files in cfrontend/ CFRONTEND=Csyntax.v Csem.v Ctyping.v Cshmgen.v \ - Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v + Cshmgenproof1.v Cshmgenproof2.v Cshmgenproof3.v \ + Csharpminor.v Cminorgen.v Cminorgenproof.v # All source files -FILES=$(LIB:%=lib/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%) +FILES=$(LIB:%=lib/%) $(COMMON:%=common/%) $(BACKEND:%=backend/%) $(CFRONTEND:%=cfrontend/%) FLATFILES=$(LIB) $(BACKEND) $(CFRONTEND) diff --git a/backend/Cminorgen.v b/cfrontend/Cminorgen.v index 4c611b4..4c611b4 100644 --- a/backend/Cminorgen.v +++ b/cfrontend/Cminorgen.v diff --git a/backend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 7820095..7820095 100644 --- a/backend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v diff --git a/backend/Csharpminor.v b/cfrontend/Csharpminor.v index 246ebf5..246ebf5 100644 --- a/backend/Csharpminor.v +++ b/cfrontend/Csharpminor.v diff --git a/backend/AST.v b/common/AST.v index 1342bef..1342bef 100644 --- a/backend/AST.v +++ b/common/AST.v diff --git a/backend/Events.v b/common/Events.v index a0559fd..a0559fd 100644 --- a/backend/Events.v +++ b/common/Events.v diff --git a/backend/Globalenvs.v b/common/Globalenvs.v index 036fd8f..036fd8f 100644 --- a/backend/Globalenvs.v +++ b/common/Globalenvs.v diff --git a/backend/Main.v b/common/Main.v index 95dc4e6..95dc4e6 100644 --- a/backend/Main.v +++ b/common/Main.v diff --git a/backend/Mem.v b/common/Mem.v index 7af696e..7af696e 100644 --- a/backend/Mem.v +++ b/common/Mem.v diff --git a/backend/Values.v b/common/Values.v index aa59e04..aa59e04 100644 --- a/backend/Values.v +++ b/common/Values.v diff --git a/extraction/Makefile b/extraction/Makefile index 6ae8e35..04878c7 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -32,7 +32,7 @@ OCAMLC=ocamlc -g $(CAMLINCL) OCAMLOPT=ocamlopt $(CAMLINCL) OCAMLDEP=ocamldep $(CAMLINCL) -COQINCL=-I ../lib -I ../backend +COQINCL=-I ../lib -I ../common -I ../backend -I ../cfrontend COQEXEC=coqtop $(COQINCL) -batch -load-vernac-source ../ccomp: $(FILES:.ml=.cmo) |