diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:23:17 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:23:17 +0200 |
| commit | 2836e342c9129027dd864dfb215deabec15c5ff9 (patch) | |
| tree | e01f73be0e25b97c77991bf6689d6c77435fe727 /test/monniaux/minisat | |
| parent | 07247055911bc1a436e469a3114649d3bb317d73 (diff) | |
| download | compcert-kvx-2836e342c9129027dd864dfb215deabec15c5ff9.tar.gz compcert-kvx-2836e342c9129027dd864dfb215deabec15c5ff9.zip | |
Makefile etcZ
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 15 | ||||
| l--------- | test/monniaux/minisat/cycles.h | 1 |
2 files changed, 11 insertions, 5 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index 08283c8a..c5f68fe8 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -7,29 +7,34 @@ PROFILING_DAT=compcert_profiling.dat EXECUTE=k1-cluster -- EXAMPLE=sudoku.sat -ALL=minisat.ccomp minisat.branch_linearize minisat.profiled minisat.gcc-O3 minisat.gcc-O3.profiled +ALL=minisat.ccomp minisat.branch_linearize minisat.profiled minisat.gcc-O3 minisat.gcc-O3.profiled minisat.gcc-O3.profile-arcs minisat.profile-arcs all: $(ALL) minisat.ccomp: $(CFILES) $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS) +minisat.profile-arcs: $(CFILES) + $(CCOMP) $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) + minisat.gcc-O3: $(CFILES) $(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS) minisat.gcc-O3.profile-arcs: $(CFILES) $(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) -$(GCDAFILES): minisat.gcc-O3.profile-arcs +gcda: minisat.gcc-O3.profile-arcs $(EXECUTE) $< $(EXAMPLE) +$(GCDAFILES): gcda + minisat.gcc-O3.profiled: $(CFILES) $(GCDAFILES) $(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS) minisat.branch_linearize: $(CFILES) - $(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@ $(LIBS) + $(CCOMP) $(CCOMPFLAGS) -ftracelinearize $(CFILES) -o $@ $(LIBS) -$(PROFILING_DAT): minisat.profile_arcs +$(PROFILING_DAT): minisat.profile-arcs -rm -f $(PROFILING_DAT) $(EXECUTE) $< $(EXAMPLE) @@ -39,4 +44,4 @@ minisat.profiled: $(CFILES) $(PROFILING_DAT) clean: -rm -f $(ALL) $(PROFILING_DAT) $(GCDAFILES) -.PHONY: clean +.PHONY: clean gcda diff --git a/test/monniaux/minisat/cycles.h b/test/monniaux/minisat/cycles.h new file mode 120000 index 00000000..84e54d21 --- /dev/null +++ b/test/monniaux/minisat/cycles.h @@ -0,0 +1 @@ +../cycles.h
\ No newline at end of file |