999a2e3391
Port by Simon Mages (maintainer) with input from Jan Klemkow, sthen@ and myself. ok sthen@ DESCR: CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. It also supports SystemC using Scoot, and has experimental support for Java Bytecode. CBMC verifies array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check C and C++ for consistency with other languages, such as Verilog. The verification is performed by unwinding the loops in the program and passing the resulting equation to a decision procedure. While CBMC is aimed for embedded software, it also supports dynamic memory allocation using malloc and new. CBMC comes with a built-in solver for bit-vector formulas that is based on MiniSat. As an alternative, CBMC has featured support for external SMT solvers. Recommended solvers are (in no particular order) Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be installed separately and have different licensing conditions.
34 lines
1.2 KiB
Plaintext
34 lines
1.2 KiB
Plaintext
$OpenBSD: patch-src_common,v 1.1.1.1 2016/10/23 00:13:10 jca Exp $
|
|
--- src/common.orig Sat Aug 20 14:08:13 2016
|
|
+++ src/common Fri Oct 14 16:29:34 2016
|
|
@@ -9,6 +9,8 @@ else ifeq ($(uname),Darwin)
|
|
BUILD_ENV_ := OSX
|
|
else ifeq ($(uname),FreeBSD)
|
|
BUILD_ENV_ := FreeBSD
|
|
+else ifeq ($(uname),OpenBSD)
|
|
+ BUILD_ENV_ := OpenBSD
|
|
else ifeq ($(filter-out MINGW32_%, $(uname)),)
|
|
BUILD_ENV_ := MinGW
|
|
else ifeq ($(filter-out CYGWIN_%, $(uname)),)
|
|
@@ -20,7 +22,7 @@ else
|
|
BUILD_ENV_ := $(BUILD_ENV)
|
|
endif
|
|
|
|
-ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
|
|
+ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD OpenBSD,$(BUILD_ENV_)),)
|
|
# Linux-ish
|
|
LIBEXT = .a
|
|
OBJEXT = .o
|
|
@@ -59,6 +61,11 @@ ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
|
|
else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
|
|
CP_CXXFLAGS +=
|
|
LINKLIB = ar rcT $@ $^
|
|
+ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
|
|
+ LINKNATIVE = $(HOSTCXX) -o $@ $^
|
|
+else ifeq ($(filter-out OpenBSD,$(BUILD_ENV_)),)
|
|
+ CP_CXXFLAGS +=
|
|
+ LINKLIB = ar rc $@ $^
|
|
LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
|
|
LINKNATIVE = $(HOSTCXX) -o $@ $^
|
|
ifeq ($(origin CC),default)
|