Add DDVerify models and benchmarks

ddverify/.gitignore

@@ -0,0 +1,16 @@
+# ddverify binary
+bin/ddverify
+
+# ddverify outputs
+__main.c
+compile
+ddv_satabs
+ddv_cbmc
+.ddv_output_*
+.claim_out_*
+
+# compilation outputs
+*.o
+
+# goblint confs
+!goblint

ddverify/awk/convert_satabs_output

@@ -0,0 +1,5 @@
+BEGIN {foundclaim = 0;}
+/^Claim*/ {foundclaim = 1; claim = NR; n = length($2) - 1; str = substr($2, 1, n); print str}
+(NR == claim + 1) && (foundclaim == 1) {print $2 "\n" $4}
+(NR == claim + 2) && (foundclaim == 1) {print substr($0, 3)}		
+(NR == claim + 3) && (foundclaim == 1) {print substr($0, 3) "\n"}

ddverify/awk/get_number_of_iteration

@@ -0,0 +1,3 @@
+BEGIN {}
+/Iterations:/ {print $2}
+(foundline == 1) && (NR == linenr + 1) {print $2}

ddverify/awk/get_time_result

@@ -0,0 +1,3 @@
+BEGIN {foundline = 0; linenr = 0; ORS = "";}
+/^VERIFICATION SUCCESSFUL*/ {foundline = 1; linenr = NR;}
+(foundline == 1) && (NR == linenr + 1) {print $2}

ddverify/awk/get_too_many_iterations_result

@@ -0,0 +1,6 @@
+BEGIN {foundline = 0; linenr = 0; ORS = "";}
+/^Too many iterations, giving up.*/ {foundline = 1; linenr = NR}
+(foundline == 1) && (NR == linenr + 2) {print $2, $4, $6, $9, $11, " "}
+(foundline == 1) && (NR == linenr + 3) {print $2, " "}
+(foundline == 1) && (NR == linenr + 4) {print $2, "\n"}
+

ddverify/awk/get_verification_result

@@ -0,0 +1,6 @@
+BEGIN {foundline = 0; linenr = 0; ORS = "";}
+/VERIFICATION/ {print $2, "\t"; foundline = 1; linenr = NR}
+(foundline == 1) && (NR == linenr + 1) {print $2, $4, $6, $9, $11, " "}
+(foundline == 1) && (NR == linenr + 2) {print $2, " "}
+(foundline == 1) && (NR == linenr + 3) {print $2, "\n"}
+

ddverify/awk/parse_dd_file

@@ -0,0 +1,3 @@
+/^[ ]*module_init\(*\)*/ {print "MODULE_INIT\n" $1}
+/^[ ]*module_exit\(*\)*/ {print "MODULE_EXIT\n" $1}
+/^[ ]*#include*/ {print "INCLUDE\n" $2}

ddverify/bin/LICENSE

@@ -0,0 +1,40 @@
+(C) 2001-2008, Daniel Kroening, ETH Zurich,
+Edmund Clarke, Computer Science Department, Carnegie Mellon University
+
+All rights reserved. Redistribution and use in source and binary forms, with
+or without modification, are permitted provided that the following
+conditions are met:
+
+  1. Redistributions of source code must retain the above copyright
+     notice, this list of conditions and the following disclaimer.
+
+  2. Redistributions in binary form must reproduce the above copyright
+     notice, this list of conditions and the following disclaimer in the
+     documentation and/or other materials provided with the distribution.
+
+  3. All advertising materials mentioning features or use of this software
+     must display the following acknowledgement:
+
+     This product includes software developed by Daniel Kroening,
+     ETH Zurich and Edmund Clarke, Computer Science Department,
+     Carnegie Mellon University.
+
+  4. Neither the name of the University nor the names of its contributors
+     may be used to endorse or promote products derived from this software
+     without specific prior written permission.
+
+  5. We must be notified by email at [email protected] after you install
+     the program for any purpose.
+
+
+THIS SOFTWARE IS PROVIDED BY THE UNIVERSITIES AND CONTRIBUTORS `AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGE.