Skip to content

Commit bd241b6

Browse files
author
Ubuntu
committed
Static compile
1 parent a8fe19a commit bd241b6

File tree

6 files changed

+49
-31
lines changed

6 files changed

+49
-31
lines changed

‎src/dpa/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ include ../makefile.include
22

33
ifeq ($(STATIC_DPA), 1)
44
CXX += -static-libstdc++ -static-libgcc -static
5-
LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
5+
# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
66
LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
77
else
88
LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl

‎src/makefile.include

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,8 @@ endif
5050
GPP=g++ -std=c++17
5151

5252
#### flags
53-
CFLAG_OPT = -g -O3
53+
#CFLAG_OPT = -g -O3
54+
CFLAG_OPT = -O3
5455

5556
#### includes
5657
INCLUDE_DIRS =
@@ -59,7 +60,8 @@ CFLAGS_INC = $(INCLUDE_DIRS)
5960
CFLAGS = -c $(CFLAGS_INC) $(CFLAG_OPT)
6061

6162
#### optional flags
62-
FLAG_PG = -pg
63+
#FLAG_PG = -pg
64+
FLAG_PG =
6365

6466
#### link flags
6567
LINK_FLAGS = $(CFLAG_OPT)

‎src/reach/Makefile

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,18 @@
11
include ../makefile.include
22

3-
CFLAGS += -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label
3+
CFLAGS += -fPIC -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label
44

55
ifeq ($(STATIC_REA), 1)
66
CXX += -static-libstdc++ -static-libgcc -static
7-
LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
7+
# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
88
LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
99
else
1010
LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl
1111
endif
1212

1313
ifeq ($(ENABLE_Y2), 1)
1414
Y2_DIR = $(DEPS)/yices2
15-
Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a
15+
Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a $(STATIC_GMPXX) $(STATIC_GMP)
1616
INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include
1717
LINKLIBS += $(Y2_LIB)
1818
CFLAGS += -D_Y2
@@ -38,11 +38,15 @@ endif
3838

3939
ifeq ($(ENABLE_M5), 1)
4040
MSAT_DIR = $(DEPS)/mathsat
41-
MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a # $(STATIC_GMPXX) $(STATIC_GMP)
41+
MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a $(STATIC_GMPXX) $(STATIC_GMP)
4242
INCLUDE += -I$(MSAT_DIR)/include
4343
LINKLIBS += $(MSAT_LIB)
4444
CFLAGS += -D_M5
4545
endif
46+
ifeq ($(CONFIG_M5), 1)
47+
CFLAGS += -DBACKEND_M5
48+
REACH_SUFFIX = m5
49+
endif
4650

4751
ifeq ($(ENABLE_Z3), 1)
4852
Z3_DIR = $(DEPS)/z3

‎src/reach/reach_backend.h

Lines changed: 23 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,23 @@
2626
/// Configurations
2727
/// Note: Only one of the below flag should be enabled
2828

29+
// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries
2930
// #define BACKEND_Y2 // Yices 2 for all queries
3031
// #define BACKEND_BT // Boolector for all queries
31-
// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries
32+
// #define BACKEND_MT // MathSAT 5 for all queries
33+
3234

33-
// Use Y2 backend for all abstract queries
35+
/// Config: BACKEND_Y2BT
36+
#ifdef BACKEND_Y2BT
37+
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
38+
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
39+
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
40+
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
41+
#define SOLVER_CORE y2_API // Solver for getting unsat core
42+
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core
43+
44+
#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
45+
#endif
3446

3547
/// Config: BACKEND_Y2
3648
#ifdef BACKEND_Y2
@@ -56,16 +68,16 @@
5668
#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
5769
#endif
5870

59-
/// Config: BACKEND_Y2BT
60-
#ifdef BACKEND_Y2BT
61-
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
62-
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
63-
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
64-
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
65-
#define SOLVER_CORE y2_API // Solver for getting unsat core
66-
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core
71+
/// Config: BACKEND_M5
72+
#ifdef BACKEND_M5
73+
#define SOLVER_CTI m5_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
74+
#define SOLVER_REACH m5_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
75+
#define SOLVER_CONTAIN m5_API // Solver for checking if frame restriction global
76+
#define SOLVER_AB m5_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
77+
#define SOLVER_CORE m5_API // Solver for getting unsat core
78+
#define SOLVER_MUS m5_API // Solver for getting minimal unsat core
6779

68-
#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
80+
#define SOLVER_BV m5_API // Solver for concrete / bit-vector queries
6981
#endif
7082

7183

‎src/vwn/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ LINKLIBS =
88

99
ifeq ($(STATIC_VWN), 1)
1010
CXX += -static-libstdc++ -static-libgcc -static
11-
LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
11+
# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64
1212
LINK_FLAGS += -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive
1313
LINKLIBS += $(STATIC_GMPXX) $(STATIC_GMP)
1414
else

‎workers.txt

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
1-
python3 avr.py --split
1+
python3 avr.py --backend y2 --split
22
python3 avr.py --kind --abstract sa --backend bt
3-
python3 avr.py --kind --abstract sa --split
4-
python3 avr.py --abstract sa --backend bt
3+
python3 avr.py --kind --abstract sa --backend y2 --split
54
python3 avr.py --abstract sa
6-
python3 avr.py
75
python3 avr.py --bmc --abstract sa --backend bt --split
8-
python3 avr.py --bmc --abstract sa+heavy
9-
python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
10-
python3 avr.py --abstract sa4 --split --forward 1 --interpol 1
11-
python3 avr.py --abstract sa+heavy --backend bt --split
6+
python3 avr.py
7+
python3 avr.py --abstract sa8 --level 5 --granularity 3 --forward 1 --interpol 1
8+
python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1
9+
python3 avr.py --split --level 0
10+
python3 avr.py --abstract sa8 --backend y2 --split --interpol 1
1211
python3 avr.py --kind --abstract sa --backend bt --split
13-
python3 avr.py --abstract sa8 --split --interpol 1
14-
python3 avr.py --abstract sa16 --split --forward 1 --backend bt
15-
python3 avr.py --abstract sa32 --backend bt --level 0 --granularity 3
16-
python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1
12+
python3 avr.py --bmc --abstract sa --backend y2
13+
python3 avr.py --abstract sa --backend bt
14+
python3 avr.py --abstract sa+heavy
15+
python3 avr.py --bmc --abstract sa+heavy --backend bt
16+
python3 avr.py --kind --abstract sa+heavy --backend bt

0 commit comments

Comments
 (0)