diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:29:09 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:29:09 +0200 |
| commit | fc01a94d6be690b37e6de9490a2809f1c9fd71ca (patch) | |
| tree | eebcc54c5c45e02cf4cc55777f5dd0093fb98c02 /test/monniaux/minisat | |
| parent | 2836e342c9129027dd864dfb215deabec15c5ff9 (diff) | |
| download | compcert-kvx-fc01a94d6be690b37e6de9490a2809f1c9fd71ca.tar.gz compcert-kvx-fc01a94d6be690b37e6de9490a2809f1c9fd71ca.zip | |
Makefile...
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index c5f68fe8..abd63d32 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -5,43 +5,49 @@ GCC=k1-cos-gcc LIBS=-lm PROFILING_DAT=compcert_profiling.dat EXECUTE=k1-cluster -- +EXECUTE_CYCLES=k1-cluster --cycle-based -- EXAMPLE=sudoku.sat -ALL=minisat.ccomp minisat.branch_linearize minisat.profiled minisat.gcc-O3 minisat.gcc-O3.profiled minisat.gcc-O3.profile-arcs minisat.profile-arcs +ALL=minisat.ccomp.log minisat.branch_linearize.log minisat.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log all: $(ALL) -minisat.ccomp: $(CFILES) +minisat.ccomp.exe: $(CFILES) $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS) -minisat.profile-arcs: $(CFILES) +minisat.ccomp.profile-arcs.exe: $(CFILES) $(CCOMP) $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) -minisat.gcc-O3: $(CFILES) +minisat.gcc-O3.exe: $(CFILES) $(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS) -minisat.gcc-O3.profile-arcs: $(CFILES) +minisat.gcc-O3.profile-arcs.exe: $(CFILES) $(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) -gcda: minisat.gcc-O3.profile-arcs +gcda: minisat.gcc-O3.profile-arcs.exe $(EXECUTE) $< $(EXAMPLE) $(GCDAFILES): gcda -minisat.gcc-O3.profiled: $(CFILES) $(GCDAFILES) +minisat.gcc-O3.profiled.exe: $(CFILES) $(GCDAFILES) $(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS) -minisat.branch_linearize: $(CFILES) +minisat.ccomp.trace_linearize.exe: $(CFILES) $(CCOMP) $(CCOMPFLAGS) -ftracelinearize $(CFILES) -o $@ $(LIBS) -$(PROFILING_DAT): minisat.profile-arcs +$(PROFILING_DAT): minisat.ccomp.profile-arcs.exe -rm -f $(PROFILING_DAT) $(EXECUTE) $< $(EXAMPLE) -minisat.profiled: $(CFILES) $(PROFILING_DAT) - $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@ $(LIBS) +minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT) + $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS) + +%.log : %.exe + $(EXECUTE_CYCLES) $< $(EXAMPLE) 2>&1 | tee $@ clean: -rm -f $(ALL) $(PROFILING_DAT) $(GCDAFILES) .PHONY: clean gcda + +.SECONDARY: |