Skip to content

Commit 61ec7fc

Browse files
authored
Merge pull request diffblue#2331 from diffblue/arch_flags_tests
mark tests that are meant for goto-gcc only
2 parents 2796025 + 8b2fc41 commit 61ec7fc

File tree

39 files changed

+80
-71
lines changed

39 files changed

+80
-71
lines changed

appveyor.yml

-6
Original file line numberDiff line numberDiff line change
@@ -64,15 +64,9 @@ test_script:
6464
- cmd: |
6565
cd regression
6666
rem HACK disable failing tests
67-
rmdir /s /q ansi-c\arch_flags_mcpu_bad
68-
rmdir /s /q ansi-c\arch_flags_mcpu_good
69-
rmdir /s /q ansi-c\arch_flags_mthumb_bad
70-
rmdir /s /q ansi-c\arch_flags_mthumb_good
7167
rmdir /s /q ansi-c\Forward_Declaration2
7268
rmdir /s /q ansi-c\Incomplete_Type1
7369
rmdir /s /q ansi-c\Universal_characters1
74-
rmdir /s /q ansi-c\gcc_attributes7
75-
rmdir /s /q ansi-c\gcc_version1
7670
rmdir /s /q cbmc\Malloc23
7771
rmdir /s /q cbmc\byte_update2
7872
rmdir /s /q cbmc\byte_update3

buildspec-windows.yml

-6
Original file line numberDiff line numberDiff line change
@@ -28,14 +28,8 @@ phases:
2828
- |
2929
cd regression
3030
# HACK disable failing tests
31-
Remove-Item ansi-c\arch_flags_mcpu_bad -Force -Recurse
32-
Remove-Item ansi-c\arch_flags_mcpu_good -Force -Recurse
33-
Remove-Item ansi-c\arch_flags_mthumb_bad -Force -Recurse
34-
Remove-Item ansi-c\arch_flags_mthumb_good -Force -Recurse
3531
Remove-Item ansi-c\Forward_Declaration2 -Force -Recurse
3632
Remove-Item ansi-c\Incomplete_Type1 -Force -Recurse
37-
Remove-Item ansi-c\gcc_attributes7 -Force -Recurse
38-
Remove-Item ansi-c\gcc_version1 -Force -Recurse
3933
Remove-Item cbmc\Malloc23 -Force -Recurse
4034
Remove-Item cbmc\byte_update2 -Force -Recurse
4135
Remove-Item cbmc\byte_update3 -Force -Recurse

regression/ansi-c/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ include ../../src/config.inc
44
include ../../src/common
55

66
ifeq ($(BUILD_ENV_),MSVC)
7-
exe=../../../src/goto-cc/goto-cl
7+
exe=../../../src/goto-cc/goto-cl -X gcc-only
88
else
99
exe=../../../src/goto-cc/goto-cc
1010
endif

regression/ansi-c/arch_flags_mcpu_bad/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
preproc.i
33
-mcpu=cortex-a15 -o linked-object.gb object.intel
44
^EXIT=(64|1)$

regression/ansi-c/arch_flags_mcpu_good/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
preproc.i
33
-mcpu=cortex-a15 -o linked-object.gb object.arm
44
^EXIT=0$

regression/ansi-c/arch_flags_mthumb_bad/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
preproc.i
33
-mthumb -o linked-object.gb object.intel
44
^EXIT=(64|1)$

regression/ansi-c/arch_flags_mthumb_good/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
preproc.i
33
-mthumb -o linked-object.gb object.arm
44
^EXIT=0$

regression/ansi-c/gcc___auto_type1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes10/main.c

+6-4
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,17 @@
22
int array##__LINE__[(condition) ? 1 : -1]
33

44
#ifdef __GNUC__
5+
#ifndef __clang__
56

6-
int x __attribute__ ((__vector_size__ (12), __may_alias__));
7+
int x __attribute__ ((__vector_size__ (16), __may_alias__));
78
int x2 __attribute__ ((__may_alias__));
8-
int x3 __attribute__ ((__may_alias__, __vector_size__ (12)));
9+
int x3 __attribute__ ((__may_alias__, __vector_size__ (16)));
910

10-
STATIC_ASSERT(sizeof(x)==12);
11+
STATIC_ASSERT(sizeof(x)==16);
1112
STATIC_ASSERT(sizeof(x2)==sizeof(int));
12-
STATIC_ASSERT(sizeof(x3)==12);
13+
STATIC_ASSERT(sizeof(x3)==16);
1314

15+
#endif
1416
#endif
1517

1618
int main(int argc, char* argv[])

regression/ansi-c/gcc_attributes10/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes11/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes12/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes13/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.i
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes8/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes9/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtin_constant_p1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtins1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtins2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtins3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtins4/main.c

+10-4
Original file line numberDiff line numberDiff line change
@@ -2,23 +2,29 @@
22

33
#define STATIC_ASSERT(a) int __dummy__[(a)?1:-1]
44

5-
struct { int i; } s;
5+
struct { int i; _Bool bit_field : 1; } s;
66
union { int i; } u;
77
enum { Econst } e;
88
int a[10];
99

10-
STATIC_ASSERT(__builtin_classify_type(*(void *)0)==0);
1110
STATIC_ASSERT(__builtin_classify_type((int)0)==1);
12-
STATIC_ASSERT(__builtin_classify_type(e)==3);
11+
STATIC_ASSERT(__builtin_classify_type((char)0)==1);
12+
STATIC_ASSERT(__builtin_classify_type(e)==1);
13+
#ifndef __clang__
14+
STATIC_ASSERT(__builtin_classify_type((_Bool)0)==1);
15+
STATIC_ASSERT(__builtin_classify_type(s.bit_field)==1);
16+
#else
1317
STATIC_ASSERT(__builtin_classify_type((_Bool)0)==4);
18+
STATIC_ASSERT(__builtin_classify_type(s.bit_field)==4);
19+
#endif
1420
STATIC_ASSERT(__builtin_classify_type((int *)0)==5);
1521
STATIC_ASSERT(__builtin_classify_type(1.0)==8);
1622
STATIC_ASSERT(__builtin_classify_type(*(0?(void *)0:(double *)0))==8);
1723
STATIC_ASSERT(__builtin_classify_type(*(0?(double *)0:(void *)0))==8);
1824
STATIC_ASSERT(__builtin_classify_type((_Complex double)0)==9);
1925
STATIC_ASSERT(__builtin_classify_type(s)==12);
2026
STATIC_ASSERT(__builtin_classify_type(u)==13);
21-
STATIC_ASSERT(__builtin_classify_type(a)==14);
27+
STATIC_ASSERT(__builtin_classify_type(a)==5);
2228

2329
#endif
2430

regression/ansi-c/gcc_builtins4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtins5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_builtins6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_types_compatible_p1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_types_compatible_p2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_types_compatible_p3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_types_compatible_p4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_vector1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
main.c
33

44
^EXIT=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
gcc-4.c
33
--native-compiler ./fake-gcc-4
44
^EXIT=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
gcc-5.c
33
--native-compiler ./fake-gcc-5
44
^EXIT=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE gcc-only
22
gcc-7.c
33
--native-compiler ./fake-gcc-7
44
^EXIT=0$

src/ansi-c/c_typecheck_expr.cpp

+30-17
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/arith_tools.h>
1717
#include <util/base_type.h>
1818
#include <util/c_types.h>
19+
#include <util/config.h>
1920
#include <util/cprover_prefix.h>
2021
#include <util/ieee_float.h>
2122
#include <util/pointer_offset_size.h>
@@ -2581,7 +2582,7 @@ exprt c_typecheck_baset::do_special_functions(
25812582
}
25822583
else if(identifier=="__builtin_classify_type")
25832584
{
2584-
// This is a gcc extension that produces an integer
2585+
// This is a gcc/clang extension that produces an integer
25852586
// constant for the type of the argument expression.
25862587
if(expr.arguments().size()!=1)
25872588
{
@@ -2594,22 +2595,34 @@ exprt c_typecheck_baset::do_special_functions(
25942595

25952596
// The value doesn't matter at all, we only care about the type.
25962597
// Need to sync with typeclass.h.
2597-
const typet &type=follow(object.type());
2598-
2599-
unsigned type_number=
2600-
type.id()==ID_empty?0:
2601-
type.id()==ID_c_enum_tag?3:
2602-
(type.id()==ID_bool || type.id()==ID_c_bool)?4:
2603-
type.id()==ID_pointer?5:
2604-
type.id()==ID_floatbv?8:
2605-
(type.id()==ID_complex && type.subtype().id()==ID_floatbv)?9:
2606-
type.id()==ID_struct?12:
2607-
type.id()==ID_union?13:
2608-
type.id()==ID_array?14:
2609-
1; // int, short
2610-
2611-
// clang returns 15 for the three 'char' types,
2612-
// gcc treats these as 'int'
2598+
typet type = follow(object.type());
2599+
2600+
// use underlying type for bit fields
2601+
if(type.id() == ID_c_bit_field)
2602+
type = to_c_bit_field_type(type).subtype();
2603+
2604+
unsigned type_number;
2605+
2606+
if(type.id() == ID_bool || type.id() == ID_c_bool)
2607+
{
2608+
// clang returns 4 for _Bool, gcc treats these as 'int'.
2609+
type_number =
2610+
config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG
2611+
? 4
2612+
: 1;
2613+
}
2614+
else
2615+
{
2616+
type_number =
2617+
type.id() == ID_empty ? 0
2618+
: (type.id() == ID_bool || type.id() == ID_c_bool) ? 4
2619+
: (type.id() == ID_pointer || type.id() == ID_array) ? 5
2620+
: type.id() == ID_floatbv ? 8
2621+
: (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ? 9
2622+
: type.id() == ID_struct ? 12
2623+
: type.id() == ID_union ? 13
2624+
: 1; // int, short, char, enum_tag
2625+
}
26132626

26142627
exprt tmp=from_integer(type_number, expr.type());
26152628
tmp.add_source_location()=source_location;

0 commit comments

Comments
 (0)