diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-28 13:36:57 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-28 13:36:57 +0100 |
| commit | 0541343719a382bce51619839344652d73453f37 (patch) | |
| tree | d609aa4f144a8516c5befaeb109133749ee38417 | |
| parent | ae18d304656aced623fcef6a7eb6f22ec9abaca8 (diff) | |
| download | compcert-kvx-0541343719a382bce51619839344652d73453f37.tar.gz compcert-kvx-0541343719a382bce51619839344652d73453f37.zip | |
some more inline
| -rw-r--r-- | test/monniaux/picosat-965/picosat.c | 20 | ||||
| -rw-r--r-- | test/monniaux/rules.mk | 5 |
2 files changed, 13 insertions, 12 deletions
diff --git a/test/monniaux/picosat-965/picosat.c b/test/monniaux/picosat-965/picosat.c index ac7003bf..21442f44 100644 --- a/test/monniaux/picosat-965/picosat.c +++ b/test/monniaux/picosat-965/picosat.c @@ -4553,7 +4553,7 @@ force (PS * ps, Cls * c) assign_forced (ps, forced, reason); } -static void +static INLINE void inc_lreduce (PS * ps) { #ifdef STATS @@ -4813,7 +4813,7 @@ collect_clauses (PS * ps) return res; } -static int +static INLINE int need_to_reduce (PS * ps) { return ps->nlclauses >= reduce_limit_on_lclauses (ps); @@ -4977,7 +4977,7 @@ assign_decision (PS * ps, Lit * lit) #ifndef NFL -static int +static INLINE int lit_has_binary_clauses (PS * ps, Lit * lit) { #ifdef NO_BINARY_CLAUSES @@ -5000,7 +5000,7 @@ flbcp (PS * ps) #endif } -inline static int +inline static INLINE int cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b) { (void) ps; @@ -5637,7 +5637,7 @@ init_reduce (PS * ps) ps->prefix, ps->prefix, ps->lreduce, ps->prefix); } -static unsigned +static INLINE unsigned rng (PS * ps) { unsigned res = ps->srng; @@ -6431,25 +6431,25 @@ reset_assumptions (PS * ps) ps->adecidelevel = 0; } -static void +static INLINE void check_ready (PS * ps) { ABORTIF (!ps || ps->state == RESET, "API usage: uninitialized"); } -static void +static INLINE void check_sat_state (PS * ps) { ABORTIF (ps->state != SAT, "API usage: expected to be in SAT state"); } -static void +static INLINE void check_unsat_state (PS * ps) { ABORTIF (ps->state != UNSAT, "API usage: expected to be in UNSAT state"); } -static void +static INLINE void check_sat_or_unsat_or_unknown_state (PS * ps) { ABORTIF (ps->state != SAT && ps->state != UNSAT && ps->state != UNKNOWN, @@ -6527,7 +6527,7 @@ enter (PS * ps) ps->entered = picosat_time_stamp (); } -static void +static INLINE void leave (PS * ps) { assert (ps->nentered); diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index eec216bd..fcd6ed0a 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -10,6 +10,7 @@ K1C_CCOMP = ../../../ccomp K1C_CCOMPFLAGS=-O3 -Wall -Wno-c11-extensions -fno-unprototyped # -fpostpass-ilp EXECUTE=k1-cluster --syscall=libstd_scalls.so -- +EXECUTE_CYCLES=k1-cluster --syscall=libstd_scalls.so --cycle-based -- %.gcc.host.o : %.gcc.host.s $(CC) $(CFLAGS) -c -o $@ $< @@ -48,7 +49,7 @@ EXECUTE=k1-cluster --syscall=libstd_scalls.so -- $(CCOMP) $(CCOMPFLAGS) $+ -o $@ %.k1c.out : %.k1c - k1-cluster --cycle-based -- $< |tee $@ + $(EXECUTE_CYCLES) $< $(EXECUTE_ARGS) |tee $@ %.host.out : %.host - ./$< |tee $@ + ./$< $(EXECUTE_ARGS) |tee $@ |