Skip to Content.
Sympa Menu

sm-commit - [SM-Commit] GIT changes to master grimoire by Ismael Luceno (a69aef9a1bc6347c576939855604e8b60646ab18)

sm-commit AT lists.ibiblio.org

Subject: Source Mage code commit list

List archive

Chronological Thread  
  • From: Ismael Luceno <scm AT sourcemage.org>
  • To: sm-commit AT lists.ibiblio.org
  • Subject: [SM-Commit] GIT changes to master grimoire by Ismael Luceno (a69aef9a1bc6347c576939855604e8b60646ab18)
  • Date: Mon, 13 Apr 2020 16:41:59 +0000

GIT changes to master grimoire by Ismael Luceno <ismael AT sourcemage.org>:

ChangeLog | 3 +++
devel/cbmc/BUILD | 2 ++
devel/cbmc/DEPENDS | 4 ++++
devel/cbmc/DETAILS | 20 ++++++++++++++++++++
devel/cbmc/HISTORY | 2 ++
devel/cbmc/INSTALL | 1 +
devel/cbmc/PRE_BUILD | 3 +++
7 files changed, 35 insertions(+)

New commits:
commit a69aef9a1bc6347c576939855604e8b60646ab18
Author: Ismael Luceno <ismael AT sourcemage.org>
Commit: Ismael Luceno <ismael AT sourcemage.org>

cbmc: new spell, C Bounded Model Checker

diff --git a/ChangeLog b/ChangeLog
index e3ec75e..10826ff 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,6 @@
+2020-04-13 Ismael Luceno <ismael AT sourcemage.org>
+ * devel/cbmc: new spell, C Bounded Model Checker
+
2020-04-11 Florian Franzmann <siflfran AT hawo.stw.uni-erlangen.de>
* video/libva-utils: new spell, diagnostic utils for libva

diff --git a/devel/cbmc/BUILD b/devel/cbmc/BUILD
new file mode 100755
index 0000000..9a8d0b3
--- /dev/null
+++ b/devel/cbmc/BUILD
@@ -0,0 +1,2 @@
+make_single &&
+cmake_build
diff --git a/devel/cbmc/DEPENDS b/devel/cbmc/DEPENDS
new file mode 100755
index 0000000..8a5d482
--- /dev/null
+++ b/devel/cbmc/DEPENDS
@@ -0,0 +1,4 @@
+optional_depends JAVA \
+ '-DWITH_JBMC=on' \
+ '-DWITH_JBMC=off' \
+ 'to build JBMC (Bounded Model Checker for Java)'
diff --git a/devel/cbmc/DETAILS b/devel/cbmc/DETAILS
new file mode 100755
index 0000000..f26dae1
--- /dev/null
+++ b/devel/cbmc/DETAILS
@@ -0,0 +1,20 @@
+ SPELL=cbmc
+ VERSION=5.12
+ SOURCE="$SPELL-$VERSION.tar.gz"
+ SOURCE_URL[0]=https://github.com/diffblue/cbmc/archive/$SOURCE
+
SOURCE_HASH=sha512:b72599faae391722210e88f61634e794240c87d5ed8566746aeb894f86df1cdcb80661945a3b1e706ef4116a13846145143b58ca75577342bc288784c91b21b5
+SOURCE_DIRECTORY="$BUILD_DIRECTORY/cbmc-cbmc-$VERSION"
+ WEB_SITE="http://www.cprover.org/cbmc";
+ LICENSE[0]=BSD-4
+ ENTERED=20200413
+ SHORT="C Bounded Model Checker"
+cat << EOF
+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. It allows verifying 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.
+EOF
diff --git a/devel/cbmc/HISTORY b/devel/cbmc/HISTORY
new file mode 100644
index 0000000..e72cb23
--- /dev/null
+++ b/devel/cbmc/HISTORY
@@ -0,0 +1,2 @@
+2020-04-13 Ismael Luceno <ismael AT sourcemage.org>
+ * BUILD, DEPENDS, DETAILS, INSTALL, PRE_BUILD: spell created
diff --git a/devel/cbmc/INSTALL b/devel/cbmc/INSTALL
new file mode 100755
index 0000000..157bcdc
--- /dev/null
+++ b/devel/cbmc/INSTALL
@@ -0,0 +1 @@
+cmake_install
diff --git a/devel/cbmc/PRE_BUILD b/devel/cbmc/PRE_BUILD
new file mode 100755
index 0000000..d53b7b5
--- /dev/null
+++ b/devel/cbmc/PRE_BUILD
@@ -0,0 +1,3 @@
+default_pre_build &&
+cd "$SOURCE_DIRECTORY" &&
+sedit '/^ *set(CMAKE_CXX_FLAGS /{s/ -Werror[^ ]*//}' CMakeLists.txt



  • [SM-Commit] GIT changes to master grimoire by Ismael Luceno (a69aef9a1bc6347c576939855604e8b60646ab18), Ismael Luceno, 04/13/2020

Archive powered by MHonArc 2.6.24.

Top of Page