diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:09:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:09:21 +0200 |
| commit | 112beeee204d4a06b8c39e9554255261365f3fed (patch) | |
| tree | f434c8fa997b4ea00b4ea62494af1937fb67fe66 /test/monniaux/minisat | |
| parent | 3907d3d6029a7d867f5be2c0434a44eeca1d9e46 (diff) | |
| download | compcert-kvx-112beeee204d4a06b8c39e9554255261365f3fed.tar.gz compcert-kvx-112beeee204d4a06b8c39e9554255261365f3fed.zip | |
Makefile for profiling
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled new file mode 100644 index 00000000..febac0d5 --- /dev/null +++ b/test/monniaux/minisat/Makefile.profiled @@ -0,0 +1,21 @@ +CFILES=main.c solver.c ../clock.c +CCOMP=../../../ccomp +CCOMPFLAGS= +PROFILING_DAT=compcert_profiling.dat +EXECUTE=k1-cluster -- +EXAMPLE=sudoku.sat + +all: minisat.ccomp minisat.branch_linearize minisat.profiled + +minisat.ccomp: $(CFILES) + $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ + +minisat.branch_linearize: $(CFILES) + $(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@ + +$(PROFILING_DAT): minisat.profile_arcs + -rm -f $(PROFILING_DAT) + $(EXECUTE) $< $(EXAMPLE) + +minisat.profiled: $(CFILES) $(PROFILING_DAT) + $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@ |