Merge latest changes from develop to Security Scanner Support

Author: NathanJPhillips

.travis.yml

@@ -160,6 +160,8 @@ install:
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src boost-download" &&
     eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C src/ansi-c library_check" &&
+    eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" &&

CHANGELOG

@@ -10,6 +10,7 @@
 * GOTO-INSTRUMENT: New option --remove-function-body
 * GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
   --no-system-headers
+* GOTO-INSTRUMENT: dump-c can output the generated environment via --harness
 
 
 5.7

appveyor.yml

@@ -109,6 +109,7 @@ test_script:
     rmdir /s /q cbmc-java\classpath1
     rmdir /s /q cbmc-java\jar-file3
     rmdir /s /q cbmc-java\tableswitch2
+    rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
 
     make test

regression/Makefile

@@ -1,10 +1,12 @@
 DIRS = ansi-c \
        cbmc \
-       cpp \
+       cbmc-cover \
        cbmc-java \
        cbmc-java-inheritance \
+       cpp \
        goto-analyzer \
        goto-diff \
+       goto-gcc \
        goto-instrument \
        goto-instrument-typedef \
        invariants \
@@ -13,9 +15,14 @@ DIRS = ansi-c \
        test-script \
        # Empty last line
 
-
+# Check for the existence of $dir. Tests under goto-gcc cannot be run on
+# Windows, so appveyor.yml unlinks the entire directory under Windows.
 test:
-	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
+	@for dir in $(DIRS); do \
+	  if [ -d "$$dir" ]; then \
+	    $(MAKE) -C "$$dir" test || exit 1; \
+	  fi; \
+	done;
 
 clean:
 	@for dir in *; do \

regression/ansi-c/Union_Padding1/main.c

@@ -62,6 +62,33 @@ STATIC_ASSERT(sizeof(union some_union4)==3);
 
 #endif
 
+#ifdef _MSC_VER
+
+union some_union5
+{
+  int i;
+};
+
+STATIC_ASSERT(__alignof(union some_union5)==1);
+
+#else
+
+union some_union5
+{
+  int i;
+};
+
+union some_union6
+{
+  int i;
+} __attribute__((__packed__));
+
+// Packing may affect alignment
+STATIC_ASSERT(_Alignof(union some_union5)==4);
+STATIC_ASSERT(_Alignof(union some_union6)==1);
+
+#endif
+
 int main()
 {
 }

regression/ansi-c/Union_Padding2/main.c

@@ -0,0 +1,34 @@
+static unsigned bar()
+{
+  unsigned r;
+  return r;
+}
+
+#ifdef _MSC_VER
+
+static void foo()
+{
+}
+
+#else
+
+static void foo()
+{
+ unsigned len=bar();
+ struct {
+   int a;
+   union {
+     int s;
+     unsigned char b[len];
+   } __attribute__ (( packed )) S;
+   int c;
+ } __attribute__ (( packed )) *l;
+}
+
+#endif
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/ansi-c/Union_Padding2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/linker_script_start+end/main.c

@@ -0,0 +1,12 @@
+extern char src_start[];
+extern char src_end[];
+extern char dst_start[];
+
+void *memcpy(void *dest, void *src, unsigned n){
+  return (void *)0;
+}
+
+int main(){
+  memcpy(dst_start, src_start, (unsigned)src_end - (unsigned)src_start);
+  return 0;
+}

regression/ansi-c/linker_script_start+end/script.ld

@@ -0,0 +1,22 @@
+MEMORY {
+  RAM : ORIGIN = 0x0, LENGTH = 25M
+}
+
+SECTIONS
+{
+  /* GCC insists on having these */
+  .note.gnu.build-id : { } > RAM
+  .text : { } > RAM
+
+  .src_section : {
+    src_start = .;
+    *(.text*)
+    src_end = .;
+  } > RAM
+
+  .dst_section : {
+    dst_start = .;
+    *(.text*)
+    dst_end = .;
+  } > RAM
+}

regression/ansi-c/linker_script_start+end/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+-o out.gb -T script.ld -nostdlib
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+Tesing the functionality of goto-cc's linker script parsing
+functionality, ensuring that it can get the values of symbols that are
+defined in linker scripts.
+
+This test ensures that goto-cc and ls-parse can:
+
+- get the value of a symbol whose value indicates the start of a section;
+- get the value of a symbol whose value indicates the end of a section.

regression/ansi-c/linker_script_start+size/main.c

@@ -0,0 +1,12 @@
+extern char src_start[];
+extern char src_size[];
+extern char dst_start[];
+
+void *memcpy(void *dest, void *src, unsigned n){
+  return (void *)0;
+}
+
+int main(){
+  memcpy(dst_start, src_start, (unsigned)src_size);
+  return 0;
+}

regression/ansi-c/linker_script_start+size/script.ld

@@ -0,0 +1,25 @@
+
+MEMORY {
+  RAM : ORIGIN = 0x0, LENGTH = 25M
+}
+
+SECTIONS
+{
+  /* GCC insists on having these */
+  .note.gnu.build-id : { } > RAM
+  .text : { } > RAM
+
+  .src_section : {
+    src_start = .;
+    *(.text*)
+    src_end = .;
+  } > RAM
+
+  src_size = src_end - src_start;
+
+  .dst_section : {
+    dst_start = .;
+    *(.text*)
+    dst_end = .;
+  } > RAM
+}

regression/ansi-c/linker_script_start+size/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+-o out.gb -T script.ld -nostdlib
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+Tesing the functionality of goto-cc's linker script parsing
+functionality, ensuring that it can get the values of symbols that are
+defined in linker scripts.
+
+This test ensures that goto-cc and ls-parse can:
+
+- get the value of a symbol whose value indicates the start of a section;
+- get the value of a symbol whose value indicates the size of a section,
+  and whose value has been generated through a basic arithmetic
+  expression in the linker script.

regression/ansi-c/linker_script_symbol-only/main.c

@@ -0,0 +1,6 @@
+extern char sym[];
+
+int main(){
+  int foo = (int)sym;
+  return 0;
+}

regression/ansi-c/linker_script_symbol-only/script.ld

@@ -0,0 +1,15 @@
+MEMORY {
+  RAM : ORIGIN = 0x0, LENGTH = 25M
+}
+
+SECTIONS
+{
+  /* GCC insists on having these */
+  .note.gnu.build-id : { } > RAM
+  .text : { } > RAM
+
+  .src_section : {
+    sym = .;
+    *(.text*)
+  } > RAM
+}

regression/ansi-c/linker_script_symbol-only/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+-o out.gb -T script.ld -nostdlib
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+Tesing the functionality of goto-cc's linker script parsing
+functionality, ensuring that it can get the values of symbols that are
+defined in linker scripts.
+
+This test ensures that goto-cc and ls-parse can get the value of a
+symbol whose value indicates the start of a section.

regression/cbmc-cover/assertion1/main.c

@@ -5,6 +5,7 @@ int main()
   __CPROVER_input("input1", input1);
   __CPROVER_input("input2", input2);
 
+  // assert() is platform-dependent and changes set of coverage goals
   __CPROVER_assert(!input1, "");
 
   if(input1)

regression/cbmc-cover/assertion1/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover assertion
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 8 function main: SATISFIED$
-^\[main.coverage.2\] file main.c line 12 function main: SATISFIED$
+^\[main.coverage.1\] file main.c line 9 function main: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc-cover/branch1/test.desc

@@ -3,12 +3,12 @@ main.c
 --cover branch
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 3 function main function main entry point: SATISFIED$
-^\[main.coverage.2\] file main.c line 8 function main function main block 1 branch false: SATISFIED$
-^\[main.coverage.3\] file main.c line 8 function main function main block 1 branch true: SATISFIED$
-^\[main.coverage.4\] file main.c line 10 function main function main block 2 branch false: FAILED$
-^\[main.coverage.5\] file main.c line 10 function main function main block 2 branch true: SATISFIED$
-^\[main.coverage.6\] file main.c line 16 function main function main block 4 branch false: SATISFIED$
-^\[main.coverage.7\] file main.c line 16 function main function main block 4 branch true: SATISFIED$
+^\[main.coverage.1\] file main.c line 3 function main entry point: SATISFIED$
+^\[main.coverage.2\] file main.c line 8 function main block 1 branch false: SATISFIED$
+^\[main.coverage.3\] file main.c line 8 function main block 1 branch true: SATISFIED$
+^\[main.coverage.4\] file main.c line 10 function main block 2 branch false: FAILED$
+^\[main.coverage.5\] file main.c line 10 function main block 2 branch true: SATISFIED$
+^\[main.coverage.6\] file main.c line 16 function main block 4 branch false: SATISFIED$
+^\[main.coverage.7\] file main.c line 16 function main block 4 branch true: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc-cover/branch2/test.desc

@@ -3,8 +3,8 @@ main.c
 --cover branch --unwind 2
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 5 function main function main entry point: SATISFIED$
-^\[main.coverage.2\] file main.c line 6 function main function main block .* branch false: SATISFIED$
-^\[main.coverage.3\] file main.c line 6 function main function main block .* branch true: SATISFIED$
+^\[main.coverage.1\] file main.c line 5 function main entry point: SATISFIED$
+^\[main.coverage.2\] file main.c line 6 function main block .* branch false: SATISFIED$
+^\[main.coverage.3\] file main.c line 6 function main block .* branch true: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc-cover/branch3/main.c

@@ -1,4 +1,3 @@
-#include <assert.h>
 #include <stdio.h>
 
 int main()

regression/cbmc-cover/branch3/test.desc

@@ -3,6 +3,6 @@ main.c
 --cover branch --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 23 of 23 covered \(100.0%\)$
+^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring

regression/cbmc-cover/built-ins2/test.desc

@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 4 covered
+^\*\* .* of .* covered \(100.0%\)
 --
 ^warning: ignoring
 ^\[.*<builtin-library-

regression/cbmc-cover/cover1/main.c

@@ -14,5 +14,6 @@ int main()
   }
 
   // should not produce a goal
+  // assert() is platform-dependent and changes set of coverage goals
   __CPROVER_assert(input1, "");
 }

regression/cbmc-cover/inlining1/test.desc

@@ -3,9 +3,9 @@ main.c
 --cover branch
 ^EXIT=0$
 ^SIGNAL=0$
-^\[my_func.coverage.1\] file main.c line 3 function my_func function my_func block 1 branch false: SATISFIED$
-^\[my_func.coverage.2\] file main.c line 3 function my_func function my_func block 1 branch true: FAILED$
-^\[my_func.coverage.3\] file main.c line 3 function my_func function my_func block 2 branch false: FAILED$
-^\[my_func.coverage.4\] file main.c line 3 function my_func function my_func block 2 branch true: SATISFIED$
+^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
+^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
+^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
+^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
 --
 ^warning: ignoring

regression/cbmc-cover/location11/main.c

@@ -1,5 +1,3 @@
-#include <assert.h>
-
 int myfunc(int x, int y)
 {
   int z = x + y;