aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/minisat/Makefile.profiled
blob: febac0d5cc635f03aba1121b92d66a542b56ceb7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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 $@