Skip to content

Commit caf96d8

Browse files
committed
Re-use C type conversion in C++ front-end
This avoids duplicating code and the need to update code in two places to add new features.
1 parent b1c89bd commit caf96d8

File tree

12 files changed

+133
-354
lines changed

12 files changed

+133
-354
lines changed

regression/ansi-c/always_inline5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only broken-test-c++-front-end
1+
CORE gcc-only test-c++-front-end
22
main.c
33

44
^EXIT=0$

regression/ansi-c/gcc_attributes3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE gcc-only broken-test-c++-front-end
1+
CORE gcc-only test-c++-front-end
22
main.c
33

44
^EXIT=0$
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#ifdef __GNUC__
2+
3+
const char *__attribute__((weak)) bar();
4+
#endif
5+
6+
int main()
7+
{
8+
#ifdef __GNUC__
9+
return bar() != 0;
10+
#else
11+
return 0
12+
#endif
13+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.cpp
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -589,6 +589,13 @@ void ansi_c_convert_typet::write(typet &type)
589589
}
590590
}
591591

592+
build_type_with_subtype(type);
593+
set_attributes(type);
594+
}
595+
596+
/// Build a vector or complex type with \p type as subtype.
597+
void ansi_c_convert_typet::build_type_with_subtype(typet &type) const
598+
{
592599
if(vector_size.is_not_nil())
593600
{
594601
type_with_subtypet new_type(ID_frontend_vector, type);
@@ -604,7 +611,11 @@ void ansi_c_convert_typet::write(typet &type)
604611
new_type.add_source_location()=source_location;
605612
type.swap(new_type);
606613
}
614+
}
607615

616+
/// Add qualifiers and GCC attributes onto \p type.
617+
void ansi_c_convert_typet::set_attributes(typet &type) const
618+
{
608619
if(gcc_attribute_mode.is_not_nil())
609620
{
610621
typet new_type=gcc_attribute_mode;

src/ansi-c/ansi_c_convert_type.h

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,8 @@ class ansi_c_convert_typet:public messaget
5151
// qualifiers
5252
c_qualifierst c_qualifiers;
5353

54-
void read(const typet &type);
55-
void write(typet &type);
54+
virtual void read(const typet &type);
55+
virtual void write(typet &type);
5656

5757
source_locationt source_location;
5858

@@ -64,7 +64,7 @@ class ansi_c_convert_typet:public messaget
6464
{
6565
}
6666

67-
void clear()
67+
virtual void clear()
6868
{
6969
unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt=
7070
long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt=
@@ -90,7 +90,9 @@ class ansi_c_convert_typet:public messaget
9090
}
9191

9292
protected:
93-
void read_rec(const typet &type);
93+
virtual void read_rec(const typet &type);
94+
virtual void build_type_with_subtype(typet &type) const;
95+
virtual void set_attributes(typet &type) const;
9496
};
9597

9698
#endif // CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H

0 commit comments

Comments
 (0)