diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-19 14:02:13 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-19 14:02:13 +0100 |
| commit | 293e792b47dc725f4e4ed4eb73dd47eef6ca04c5 (patch) | |
| tree | 9b125135c39b534957516f7df4ac71a2886fa0d1 /Makefile | |
| parent | 3ecf782231a8d8113f26b69f09ca43cf8a68b00f (diff) | |
| download | compcert-kvx-293e792b47dc725f4e4ed4eb73dd47eef6ca04c5.tar.gz compcert-kvx-293e792b47dc725f4e4ed4eb73dd47eef6ca04c5.zip | |
Asmgenproof1 pas sur kvx
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -122,9 +122,13 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ - Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v Asmaux.v \ + Asm.v Asmgen.v Asmgenproof0.v Asmgenproof.v Asmaux.v \ $(BACKENDLIB) +ifneq ($(ARCH), "kvx") + BACKEND += Asmgenproof1.v +endif + # C front-end modules (in cfrontend/) CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ |