Merge pull request diffblue#271 from diffblue/smowton/merge_develop_2…

…017_11_16

Merge latest cbmc-develop

CMakeLists.txt

@@ -44,3 +44,49 @@ if(${enable_cbmc_tests})
 endif()
 add_subdirectory(unit)
 add_subdirectory(regression)
+
+set_target_properties(
+    analyses
+    ansi-c
+    assembler
+    big-int
+    cbmc
+    cbmc-lib
+    clobber
+    clobber-lib
+    cpp
+    driver
+    goto-analyzer
+    goto-analyzer-lib
+    goto-cc
+    goto-cc-lib
+    goto-diff
+    goto-diff-lib
+    goto-instrument
+    goto-instrument-lib
+    goto-programs
+    goto-symex
+    java_bytecode
+    jbmc
+    jbmc-lib
+    jsil
+    json
+    langapi
+    linking
+    miniBDD
+    miniz
+    mmcc
+    pointer-analysis
+    solvers
+    string_utils
+    test-bigint
+    testing-utils
+    unit
+    util
+    xml
+
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)

CODEOWNERS

@@ -1,36 +1,57 @@
 # These owners will be the default owners for everything in the repo.
-*       @kroening @tautschnig @peterschrammel
+*       @kroening @tautschnig @peterschrammel @smowton @chrisr-diffblue
 
-src/java_bytecode/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
-src/jbmc/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
-src/miniz/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli
+# These files should rarely change
 
-src/ansi-c/ @marek-trtik @kroening @tautschnig
+src/big-int/ @kroening
+src/ansi-c/ @kroening @tautschnig
+src/assembler/ @kroening @tautschnig
+src/goto-cc/ @kroening @tautschnig
+src/linking/ @kroening @tautschnig
+src/memory-models/ @kroening @tautschnig
+src/goto-symex/ @kroening @tautschnig @peterschrammel
+src/json/ @kroening @tautschnig @peterschrammel
+src/langapi/ @kroening @tautschnig @peterschrammel
+src/xmllang/ @kroening @tautschnig @peterschrammel
+src/nonstd/ @smowton @peterschrammel
+src/solvers/cvc @martin-cs @kroening
+src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
+src/solvers/floatbv @martin-cs @kroening
+src/solvers/miniBDD @tautschnig @kroening
+src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
+src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
+src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
+src/miniz/ @smowton @mgudemann @peterschrammel
 
-src/cpp/ @marek-trtik @kroening @tautschnig
 
-CMakeLists.txt @reuk @thk123
+# These files change frequently and changes are high-risk
 
-cmake/ @reuk @thk123
+src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
+src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
+src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
+src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
+src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
+src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
+src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
 
-src/solvers/ @martin-cs @romainbrenguier @antlechner @kroening
 
-src/analyses/ @martin-cs @peterschrammel @thk123 @marek-trtik @NathanJPhillips
+# These files change frequently and changes are medium-risk
 
-src/pointer-analysis/ @martin-cs @peterschrammel @thk123 @marek-trtik 
+src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
+src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
+src/goto-diff/ @tautschnig @peterschrammel
+src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+src/cpp/ @kroening @tautschnig @peterschrammel
 
-src/goto-analyzer/ @martin-cs @peterschrammel @thk123 @marek-trtik 
 
-src/goto-instrument/ @martin-cs @peterschrammel @thk123 @marek-trtik  
-
-src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik  
-
-src/linking/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik  
+# These files change frequently and changes are low-risk
 
 unit/ @diffblue/cbmc-developers
-
 regression/ @diffblue/cbmc-developers
 
-.travis.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
-appveyor.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
+CMakeLists.txt @reuk @chrisr-diffblue
+cmake/ @reuk @chrisr-diffblue
 
+scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
+.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
+appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel

appveyor.yml

@@ -83,6 +83,7 @@ test_script:
     rmdir /s /q cbmc\byte_update7
     rmdir /s /q cbmc\pipe1
     rmdir /s /q cbmc\unsigned___int128
+    rmdir /s /q cbmc-cpp
     rmdir /s /q cpp\Decltype1
     rmdir /s /q cpp\Decltype2
     rmdir /s /q cpp\Function_Overloading1

regression/CMakeLists.txt

@@ -1,12 +1,9 @@
-set(CMAKE_CXX_STANDARD 11)
-set(CMAKE_CXX_STANDARD_REQUIRED true)
-
 set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
 
 macro(add_test_pl_profile name cmdline flag profile)
     add_test(
         NAME "${name}-${profile}"
-        COMMAND ${test_pl_path} -c ${cmdline} ${flag}
+        COMMAND ${test_pl_path} -p -c ${cmdline} ${flag}
         WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
@@ -25,15 +22,21 @@ endmacro(add_test_pl_tests)
 
 add_subdirectory(ansi-c)
 add_subdirectory(cbmc)
+add_subdirectory(cbmc-cover)
+add_subdirectory(cbmc-cpp)
 add_subdirectory(cbmc-java)
 add_subdirectory(cbmc-java-inheritance)
 add_subdirectory(cpp)
 add_subdirectory(goto-analyzer)
+add_subdirectory(goto-analyzer-taint)
 add_subdirectory(goto-cc-cbmc)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-diff)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-instrument-typedef)
+if(NOT WIN32)
+  add_subdirectory(goto-gcc)
+endif()
 add_subdirectory(invariants)
 add_subdirectory(jbmc-strings)
 add_subdirectory(strings)

regression/Makefile

@@ -1,6 +1,7 @@
 DIRS = ansi-c \
        cbmc \
        cbmc-cover \
+       cbmc-cpp \
        cbmc-java \
        cbmc-java-inheritance \
        cpp \

regression/ansi-c/Makefile

@@ -10,16 +10,10 @@ else
 endif
 
 test:
-	@if ! ../test.pl -c $(exe) ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c $(exe)
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c $(exe) ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c $(exe)
 
 show:
 	@for dir in *; do \

regression/cbmc-cover/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-cover/Makefile

@@ -1,16 +1,10 @@
 default: tests.log
 
 test:
-	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c ../../../src/cbmc/cbmc
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c ../../../src/cbmc/cbmc
 
 show:
 	@for dir in *; do \

regression/cbmc-cpp/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-cpp/FunctionParam1/main.cpp

@@ -0,0 +1,12 @@
+#include <assert.h>
+int x;
+
+void g(int i){
+  x=i;
+}
+
+int main() {
+  g(3);
+  assert(x==3);
+}
+

regression/cbmc-cpp/FunctionParam1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-cpp/MethodParam1/main.cpp

@@ -0,0 +1,18 @@
+#include <assert.h>
+unsigned x;
+
+class ct {
+  void f(int i) {
+    x=x+i;
+  }
+};
+
+int main() {
+  unsigned r;
+  x=r%3;
+  ct c;
+  c.f(2);
+  assert(x<4);
+  assert(x<5);
+}
+

regression/cbmc-cpp/MethodParam1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.cpp
+
+instance is SATISFIABLE$
+instance is UNSATISFIABLE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-cpp/union2/main.cpp

@@ -1,3 +1,4 @@
+#include <assert.h>
 struct A
 {
   union

regression/cbmc-java-inheritance/Makefile

@@ -1,16 +1,10 @@
 default: tests.log
 
 test:
-	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c ../../../src/jbmc/jbmc
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/cbmc-java/Makefile

@@ -1,16 +1,10 @@
 default: tests.log
 
 test:
-	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c ../../../src/jbmc/jbmc
 
 tests.log: ../test.pl
-	@if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \
-		../failed-tests-printer.pl ; \
-		exit 1 ; \
-	fi
+	@../test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/cbmc-java/classpath2/test.desc

@@ -1,6 +1,6 @@
 CORE
 jarfile3.class
---function jarfile3.f --java-cp-include-files "jarfile3\.class"
+--function jarfile3.f --java-cp-include-files 'jarfile3\.class'
 ^EXIT=10$
 ^SIGNAL=0$
 .*SUCCESS$

regression/cbmc-java/divide_by_zero/DivideByZero.java

@@ -0,0 +1,6 @@
+public class DivideByZero {
+    public static void main(String args[]) {
+        int i=0;
+        int j=10/i;
+    }
+}

regression/cbmc-java/divide_by_zero/test.desc

@@ -0,0 +1,9 @@
+CORE
+DivideByZero.class
+
+^EXIT=10$
+^SIGNAL=0$
+Denominator should be nonzero: FAILURE
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/function1/test.desc

@@ -1,6 +1,6 @@
 CORE
 Main.class
---function "Other.fail:()V"
+--function 'Other.fail:()V'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-java/function2/test.desc

@@ -1,6 +1,6 @@
 CORE
 Main.class
---function "D.fail:()V"
+--function 'D.fail:()V'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-java/function3/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Main.class
---function "A.dummy:()V"
+--function 'A.dummy:()V'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/function4/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Main.class
---function "Other.fail"
+--function 'Other.fail'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/generic_class_bound1/Gn.java

@@ -0,0 +1,15 @@
+interface A{}
+interface B{}
+interface C{}
+interface L<T> extends A,B,C{}
+
+public class Gn<T extends L<? extends B>>{
+	Gn<?> ex1;
+	public void foo1(Gn<?> ex1){
+		if(ex1 != null)
+		this.ex1 = ex1;
+	}
+	public static void main(String[] args) {
+		System.out.println("ddfsdf");
+	}
+}