Merge branch 'master' of github.com:diffblue/cbmc

Author: kroening

appveyor.yml

@@ -75,6 +75,10 @@ test_script:
     cat goto-instrument-typedef/chain.sh || true
 
     rem HACK disable failing tests
+    rmdir /s /q ansi-c\arch_flags_mcpu_bad
+    rmdir /s /q ansi-c\arch_flags_mcpu_good
+    rmdir /s /q ansi-c\arch_flags_mthumb_bad
+    rmdir /s /q ansi-c\arch_flags_mthumb_good
     rmdir /s /q ansi-c\Forward_Declaration2
     rmdir /s /q ansi-c\Incomplete_Type1
     rmdir /s /q ansi-c\Union_Padding1

regression/Makefile

@@ -12,3 +12,10 @@ DIRS = ansi-c \
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
+
+clean:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			$(MAKE) -C "$$dir" clean; \
+		fi; \
+	done;

regression/ansi-c/arch_flags_mcpu_bad/object.intel

@@ -0,0 +1 @@
+int foo() { return 3; }

regression/ansi-c/arch_flags_mcpu_bad/preproc.i

@@ -0,0 +1 @@
+int bar(){ return 9; }

regression/ansi-c/arch_flags_mcpu_bad/source.c

@@ -0,0 +1,20 @@
+CORE
+preproc.i
+-mcpu=cortex-a15 -o linked-object.gb object.intel
+^EXIT=(64|1)$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+This tests the -mcpu=cortex=a15 flag that should activate ARM-32 mode.
+The object file 'object.intel' was compiled from 'source.c' with goto-cc
+on a 64-bit platform:
+
+  goto-cc -c source.c
+
+preproc.i is already pre-processed so that it can be linked in without
+needing to invoke a pre-processor from a cross-compile toolchain on your
+local machine. Linking it together with the Intel object file, while
+passing -mcpu=cortex-a15 on the command line, should fail because
+-mcpu=cortex-a15 implies that we're trying to make an ARM executable.

regression/ansi-c/arch_flags_mcpu_bad/test.desc

@@ -0,0 +1 @@
+int foo() { return 3; }

regression/ansi-c/arch_flags_mcpu_good/object.arm

@@ -0,0 +1 @@
+int bar(){ return 9; }

regression/ansi-c/arch_flags_mcpu_good/preproc.i

@@ -0,0 +1,20 @@
+CORE
+preproc.i
+-mcpu=cortex-a15 -o linked-object.gb object.arm
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+This tests the -mcpu=cortex-a15 flag that should activate ARM-32 mode.
+The object file 'object.arm' was compiled from 'source.c' with goto-cc
+along with an ARM cross-compiler on a 64-bit platform with the following
+command line:
+
+  goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
+
+preproc.i is already pre-processed so that it can be linked in without
+needing to invoke a pre-processor from a cross-compile toolchain on your
+local machine. Linking it together with the ARM object file, while
+passing -mcpu=cortex-a15 on the command line, should succeed.