Merge pull request #1354 from NathanJPhillips/merge-develop-to-sss

Merge develop to security scanner support

Author: smowton

.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.