Comp kind

COMPILING

@@ -1,6 +1,6 @@
-2LS 0.4
+2LS 0.5
 
 ./install.sh
 
-The executable is src/summarizer/2ls
+The executable is src/2ls/2ls
 

README.md

@@ -0,0 +1,21 @@
+[![Build Status][build_img]][travis]
+
+About
+=====
+
+2LS is a verification tool for C programs. It is built upon the
+CPROVER framework ([cprover.org](http://www.cprover.org)), which
+supports C89, C99, most of C11 and most compiler extensions provided
+by gcc and Visual Studio. It allows verifying array bounds (buffer
+overflows), pointer safety, exceptions, user-specified assertions, and
+termination properties.  The analysis is performed by template-based
+predicate synthesis and abstraction refinements techniques.
+
+For more information see [cprover.org](http://www.cprover.org/2LS).
+
+License
+=======
+4-clause BSD license, see `LICENSE` file.
+
+[build_img]: https://travis-ci.org/diffblue/2ls.svg?branch=master
+[travis]: https://travis-ci.org/diffblue/2ls

install.sh

@@ -1,13 +1,33 @@
-git clone https://github.com/diffblue/cbmc
+#!/bin/bash
+
+CBMC_REPO=https://github.com/peterschrammel/cbmc
+CBMC_VERSION=d95e7da28018fd315b04a1201d5b7cfe8195cbc6
+
+if [ "$1" != "" ]
+then
+  COMPILER="$1"
+fi
+
+git clone $CBMC_REPO
 cd cbmc
 CBMC=`pwd`
-git checkout e4a5a611f569c72f97c0e099e56a827c9a55d2aa
-cd src
-make minisat2-download
-make
-cd ../../src
+git checkout $CBMC_VERSION
+make -C src minisat2-download
+if [ "$COMPILER" != "" ]
+then
+  make -C src CXX=$COMPILER
+else
+  make -C src
+fi
+
+cd ../src
 cp config.inc.template config.inc
 sed -i.bak "s#CBMC = ~/my-cbmc#CBMC = $CBMC#g" config.inc
-make
+if [ "$COMPILER" != "" ]
+then
+  make CXX=$COMPILER
+else
+  make
+fi
 cd ..
-echo "The executable is src/summarizer/2ls"
+echo "The executable is src/2ls/2ls"

regression/interprocedural/Makefile

@@ -3,10 +3,10 @@ default: tests.log
 FLAGS = --verbosity 10
 
 test:
-	@../test.pl -c "../../../src/summarizer/2ls $(FLAGS)"
+	@../test.pl -c "../../../src/2ls/2ls $(FLAGS)"
 
 tests.log: ../test.pl
-	@../test.pl -c "../../../src/summarizer/2ls $(FLAGS)"
+	@../test.pl -c "../../../src/2ls/2ls $(FLAGS)"
 
 show:
 	@for dir in *; do \

regression/interprocedural/contextsensitive1/main.c

@@ -1,17 +1,17 @@
-
-int sign(int x) 
-{ 
-  if(x>0) return 1;
-  else if (x==0) return 0;
-  return -1;
-}
-
-void main()
-{
-  int x = 1;
-  int y = sign(x);
-  x = -x;
-  int z = sign(x);
-  assert(-1<=y && y<=1 && -1<=z && z<=1);
-}
-
+
+int sign(int x) 
+{ 
+  if(x>0) return 1;
+  else if (x==0) return 0;
+  return -1;
+}
+
+void main()
+{
+  int x = 1;
+  int y = sign(x);
+  x = -x;
+  int z = sign(x);
+  assert(-1<=y && y<=1 && -1<=z && z<=1);
+}
+

regression/interprocedural/contextsensitive2/main.c

@@ -1,28 +1,28 @@
-
-int sign(int x) 
-{ 
-  if(x>0) return 1;
-  else if (x==0) return 0;
-  return -1;
-}
-
-int do1(int x)
-{
-  return sign(x);
-}
-
-int do2(int x)
-{
-  return sign(x);
-}
-
-void main()
-{
-  int x = 1;
-  int y = do1(x);
-  assert(y==1);
-  x = -x;
-  int z = do2(x);
-  assert(-1<=z && z<=1);
-}
-
+
+int sign(int x) 
+{ 
+  if(x>0) return 1;
+  else if (x==0) return 0;
+  return -1;
+}
+
+int do1(int x)
+{
+  return sign(x);
+}
+
+int do2(int x)
+{
+  return sign(x);
+}
+
+void main()
+{
+  int x = 1;
+  int y = do1(x);
+  assert(y==1);
+  x = -x;
+  int z = do2(x);
+  assert(-1<=z && z<=1);
+}
+

regression/interprocedural/contextsensitive3/main.c

@@ -1,28 +1,28 @@
-
-int sign(int x) 
-{ 
-  if(x>0) return 1;
-  else if (x==0) return 0;
-  return -1;
-}
-
-int do1(int x)
-{
-  return sign(x);
-}
-
-int do2(int x)
-{
-  return sign(x);
-}
-
-void main()
-{
-  int x = 1;
-  int y = do2(x);
-  assert(y==1);
-  x = -x;
-  int z = do1(x);
-  assert(-1<=z && z<=1);
-}
-
+
+int sign(int x) 
+{ 
+  if(x>0) return 1;
+  else if (x==0) return 0;
+  return -1;
+}
+
+int do1(int x)
+{
+  return sign(x);
+}
+
+int do2(int x)
+{
+  return sign(x);
+}
+
+void main()
+{
+  int x = 1;
+  int y = do2(x);
+  assert(y==1);
+  x = -x;
+  int z = do1(x);
+  assert(-1<=z && z<=1);
+}
+

regression/interprocedural/contextsensitive4/main.c

@@ -1,29 +1,29 @@
-
-int x = 1;
-
-int sign(int x) 
-{ 
-  if(x>0) return 1;
-  else if (x==0) return 0;
-  return -1;
-}
-
-int do1(int x)
-{
-  return sign(x);
-}
-
-int do2(int x)
-{
-  return sign(x);
-}
-
-void main()
-{
-  int y = do1(x);
-  assert(y==1);
-  x = -x;
-  int z = do2(x);
-  assert(-1<=z && z<=1);
-}
-
+
+int x = 1;
+
+int sign(int x) 
+{ 
+  if(x>0) return 1;
+  else if (x==0) return 0;
+  return -1;
+}
+
+int do1(int x)
+{
+  return sign(x);
+}
+
+int do2(int x)
+{
+  return sign(x);
+}
+
+void main()
+{
+  int y = do1(x);
+  assert(y==1);
+  x = -x;
+  int z = do2(x);
+  assert(-1<=z && z<=1);
+}
+

regression/interprocedural/contextsensitive5/main.c

@@ -1,15 +1,15 @@
-#include <stdlib.h>
-
-void foo(int* x) 
-{ 
-  assert(x!=NULL);
-  *x = 0;
-}
-
-void main()
-{
-  int x;
-  int *y = &x;
-  foo(y);
-}
-
+#include <stdlib.h>
+
+void foo(int* x) 
+{ 
+  assert(x!=NULL);
+  *x = 0;
+}
+
+void main()
+{
+  int x;
+  int *y = &x;
+  foo(y);
+}
+

regression/interprocedural/contextsensitive6/main.c

@@ -1,12 +1,12 @@
-
-void foo(int x) 
-{ 
-  assert(x!=0);
-}
-
-void main()
-{
-  int x = 1;
-  foo(x);
-}
-
+
+void foo(int x) 
+{ 
+  assert(x!=0);
+}
+
+void main()
+{
+  int x = 1;
+  foo(x);
+}
+