mark tests that are meant for goto-gcc only

appveyor.yml

@@ -64,15 +64,9 @@ test_script:
 - cmd: |
     cd regression
     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\Universal_characters1
-    rmdir /s /q ansi-c\gcc_attributes7
-    rmdir /s /q ansi-c\gcc_version1
     rmdir /s /q cbmc\Malloc23
     rmdir /s /q cbmc\byte_update2
     rmdir /s /q cbmc\byte_update3

buildspec-windows.yml

@@ -28,14 +28,8 @@ phases:
       - |
         cd regression
         # HACK disable failing tests
-        Remove-Item ansi-c\arch_flags_mcpu_bad -Force -Recurse
-        Remove-Item ansi-c\arch_flags_mcpu_good -Force -Recurse
-        Remove-Item ansi-c\arch_flags_mthumb_bad -Force -Recurse
-        Remove-Item ansi-c\arch_flags_mthumb_good -Force -Recurse
         Remove-Item ansi-c\Forward_Declaration2 -Force -Recurse
         Remove-Item ansi-c\Incomplete_Type1 -Force -Recurse
-        Remove-Item ansi-c\gcc_attributes7 -Force -Recurse
-        Remove-Item ansi-c\gcc_version1 -Force -Recurse
         Remove-Item cbmc\Malloc23 -Force -Recurse
         Remove-Item cbmc\byte_update2 -Force -Recurse
         Remove-Item cbmc\byte_update3 -Force -Recurse

regression/ansi-c/Makefile

@@ -4,7 +4,7 @@ include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	exe=../../../src/goto-cc/goto-cl
+	exe=../../../src/goto-cc/goto-cl -X gcc-only
 else
 	exe=../../../src/goto-cc/goto-cc
 endif

regression/ansi-c/arch_flags_mcpu_bad/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 preproc.i
 -mcpu=cortex-a15 -o linked-object.gb object.intel
 ^EXIT=(64|1)$

regression/ansi-c/arch_flags_mcpu_good/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 preproc.i
 -mcpu=cortex-a15 -o linked-object.gb object.arm
 ^EXIT=0$

regression/ansi-c/arch_flags_mthumb_bad/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 preproc.i
 -mthumb -o linked-object.gb object.intel
 ^EXIT=(64|1)$

regression/ansi-c/arch_flags_mthumb_good/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 preproc.i
 -mthumb -o linked-object.gb object.arm
 ^EXIT=0$

regression/ansi-c/gcc___auto_type1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes10/main.c

@@ -2,15 +2,17 @@
   int array##__LINE__[(condition) ? 1 : -1]
 
 #ifdef __GNUC__
+#ifndef __clang__
 
-int  x   __attribute__ ((__vector_size__ (12), __may_alias__));
+int  x   __attribute__ ((__vector_size__ (16), __may_alias__));
 int  x2   __attribute__ ((__may_alias__));
-int  x3   __attribute__ ((__may_alias__, __vector_size__ (12)));
+int  x3   __attribute__ ((__may_alias__, __vector_size__ (16)));
 
-STATIC_ASSERT(sizeof(x)==12);
+STATIC_ASSERT(sizeof(x)==16);
 STATIC_ASSERT(sizeof(x2)==sizeof(int));
-STATIC_ASSERT(sizeof(x3)==12);
+STATIC_ASSERT(sizeof(x3)==16);
 
+#endif
 #endif
 
 int main(int argc, char* argv[])

regression/ansi-c/gcc_attributes10/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes11/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes12/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes13/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes5/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes7/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.i
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes8/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_attributes9/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtin_constant_p1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtins1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtins2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtins3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtins4/main.c

@@ -2,23 +2,29 @@
 
 #define STATIC_ASSERT(a) int __dummy__[(a)?1:-1]
 
-struct { int i; } s;
+struct { int i; _Bool bit_field : 1; } s;
 union { int i; } u;
 enum { Econst } e;
 int a[10];
 
-STATIC_ASSERT(__builtin_classify_type(*(void *)0)==0);
 STATIC_ASSERT(__builtin_classify_type((int)0)==1);
-STATIC_ASSERT(__builtin_classify_type(e)==3);
+STATIC_ASSERT(__builtin_classify_type((char)0)==1);
+STATIC_ASSERT(__builtin_classify_type(e)==1);
+#ifndef __clang__
+STATIC_ASSERT(__builtin_classify_type((_Bool)0)==1);
+STATIC_ASSERT(__builtin_classify_type(s.bit_field)==1);
+#else
 STATIC_ASSERT(__builtin_classify_type((_Bool)0)==4);
+STATIC_ASSERT(__builtin_classify_type(s.bit_field)==4);
+#endif
 STATIC_ASSERT(__builtin_classify_type((int *)0)==5);
 STATIC_ASSERT(__builtin_classify_type(1.0)==8);
 STATIC_ASSERT(__builtin_classify_type(*(0?(void *)0:(double *)0))==8);
 STATIC_ASSERT(__builtin_classify_type(*(0?(double *)0:(void *)0))==8);
 STATIC_ASSERT(__builtin_classify_type((_Complex double)0)==9);
 STATIC_ASSERT(__builtin_classify_type(s)==12);
 STATIC_ASSERT(__builtin_classify_type(u)==13);
-STATIC_ASSERT(__builtin_classify_type(a)==14);
+STATIC_ASSERT(__builtin_classify_type(a)==5);
 
 #endif
 

regression/ansi-c/gcc_builtins4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtins5/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_builtins6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_types_compatible_p1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_types_compatible_p2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_types_compatible_p3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_types_compatible_p4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_vector1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 main.c
 
 ^EXIT=0$

regression/ansi-c/gcc_version1/test-gcc-4.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 gcc-4.c
 --native-compiler ./fake-gcc-4
 ^EXIT=0$

regression/ansi-c/gcc_version1/test-gcc-5.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 gcc-5.c
 --native-compiler ./fake-gcc-5
 ^EXIT=0$

regression/ansi-c/gcc_version1/test-gcc-7.desc

@@ -1,4 +1,4 @@
-CORE
+CORE gcc-only
 gcc-7.c
 --native-compiler ./fake-gcc-7
 ^EXIT=0$

src/ansi-c/c_typecheck_expr.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/base_type.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
@@ -2581,7 +2582,7 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier=="__builtin_classify_type")
   {
-    // This is a gcc extension that produces an integer
+    // This is a gcc/clang extension that produces an integer
     // constant for the type of the argument expression.
     if(expr.arguments().size()!=1)
     {
@@ -2594,22 +2595,34 @@ exprt c_typecheck_baset::do_special_functions(
 
     // The value doesn't matter at all, we only care about the type.
     // Need to sync with typeclass.h.
-    const typet &type=follow(object.type());
-
-    unsigned type_number=
-      type.id()==ID_empty?0:
-      type.id()==ID_c_enum_tag?3:
-      (type.id()==ID_bool || type.id()==ID_c_bool)?4:
-      type.id()==ID_pointer?5:
-      type.id()==ID_floatbv?8:
-      (type.id()==ID_complex && type.subtype().id()==ID_floatbv)?9:
-      type.id()==ID_struct?12:
-      type.id()==ID_union?13:
-      type.id()==ID_array?14:
-      1; // int, short
-
-    // clang returns 15 for the three 'char' types,
-    // gcc treats these as 'int'
+    typet type = follow(object.type());
+
+    // use underlying type for bit fields
+    if(type.id() == ID_c_bit_field)
+      type = to_c_bit_field_type(type).subtype();
+
+    unsigned type_number;
+
+    if(type.id() == ID_bool || type.id() == ID_c_bool)
+    {
+      // clang returns 4 for _Bool, gcc treats these as 'int'.
+      type_number =
+        config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG
+          ? 4
+          : 1;
+    }
+    else
+    {
+      type_number =
+          type.id() == ID_empty ? 0
+        : (type.id() == ID_bool || type.id() == ID_c_bool) ? 4
+        : (type.id() == ID_pointer || type.id() == ID_array) ? 5
+        : type.id() == ID_floatbv ? 8
+        : (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ? 9
+        : type.id() == ID_struct ? 12
+        : type.id() == ID_union ? 13
+        : 1; // int, short, char, enum_tag
+    }
 
     exprt tmp=from_integer(type_number, expr.type());
     tmp.add_source_location()=source_location;