Source Mage code commit list

[Ismael Luceno <scm AT sourcemage.org>]

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