Skip to content

Commit 6d5e446

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#2240 from diffblue/get-gcc-version
goto-cc: get gcc version
2 parents b618d94 + 78794e2 commit 6d5e446

25 files changed

+306
-81
lines changed

‎appveyor.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@ test_script:
7474
rmdir /s /q ansi-c\Universal_characters1
7575
rmdir /s /q ansi-c\function_return1
7676
rmdir /s /q ansi-c\gcc_attributes7
77+
rmdir /s /q ansi-c\gcc_version1
7778
rmdir /s /q ansi-c\struct6
7879
rmdir /s /q ansi-c\struct7
7980
rmdir /s /q cbmc\Malloc23

‎regression/ansi-c/float_constant1/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ STATIC_ASSERT(0X.0p+1f == 0);
1212

1313
// 32-bit, 64-bit and 128-bit constants, GCC proper only,
1414
// clang doesn't have it
15-
#if defined(__GNUC__) && !defined(__clang__)
15+
#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 7
1616
STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
1717
STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
1818
STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));

‎regression/ansi-c/gcc_types_compatible_p1/main.c

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -67,8 +67,8 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
6767
STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
6868
STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
6969

70-
#ifndef __clang__
7170
// clang doesn't have these
71+
#if !defined(__clang__) && __GNUC__ >= 7
7272
#if defined(__x86_64__) || defined(__i386__)
7373
STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128));
7474
#endif
@@ -95,16 +95,19 @@ STATIC_ASSERT(!__builtin_types_compatible_p(long int, int));
9595
STATIC_ASSERT(!__builtin_types_compatible_p(long long int, long int));
9696
STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
9797

98-
#ifndef __clang__
98+
STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
99+
99100
// clang doesn't have these
101+
#if !defined(__clang__)
102+
#if __GNUC__ >= 7
100103
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
101104
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
102105
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
103106
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
107+
#endif
104108
STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
105109
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
106110
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));
107-
STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
108111
#endif
109112
#endif
110113

‎regression/ansi-c/gcc_version1/fake-gcc-4

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
#!/bin/sh
2+
3+
gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $*
4+

‎regression/ansi-c/gcc_version1/fake-gcc-7

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
#!/bin/sh
2+
3+
gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $*
4+

‎regression/ansi-c/gcc_version1/gcc-4.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
typedef double _Float64;
2+

‎regression/ansi-c/gcc_version1/gcc-7.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
_Float64 some_var;
2+

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
gcc-4.c
3+
--native-compiler ./fake-gcc-4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^CONVERSION ERROR$

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
gcc-7.c
3+
--native-compiler ./fake-gcc-7
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^CONVERSION ERROR$

‎regression/cbmc/ts18661_typedefs/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,18 @@
1+
#if defined(__clang__)
2+
#elif defined(__GNUC__)
3+
#if __GNUC__ >= 7
4+
#define HAS_FLOATN
5+
#endif
6+
#endif
7+
8+
#ifndef HAS_FLOATN
19
typedef float _Float32;
210
typedef double _Float32x;
311
typedef double _Float64;
412
typedef long double _Float64x;
513
typedef long double _Float128;
614
typedef long double _Float128x;
15+
#endif
716

817
int main(int argc, char** argv) {
918
}

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -346,22 +346,9 @@ void ansi_c_convert_typet::write(typet &type)
346346
gcc_float64_cnt+gcc_float64x_cnt+
347347
gcc_float128_cnt+gcc_float128x_cnt>=2)
348348
{
349-
// Temporary workaround for our glibc versions that try to define TS 18661
350-
// types (for example, typedef float _Float32). This can be removed once
351-
// upgrade cbmc's GCC support to at least 7.0 (when glibc will expect us
352-
// to provide these types natively), or disable parsing them ourselves
353-
// when our preprocessor stage claims support <7.0.
354-
if(c_storage_spec.is_typedef)
355-
{
356-
warning().source_location = source_location;
357-
warning() << "ignoring typedef for TS 18661 (_FloatNNx) type. If you need these, try using goto-cc instead." << eom;
358-
}
359-
else
360-
{
361-
error().source_location=source_location;
362-
error() << "conflicting type modifiers" << eom;
363-
throw 0;
364-
}
349+
error().source_location=source_location;
350+
error() << "conflicting type modifiers" << eom;
351+
throw 0;
365352
}
366353

367354
// _not_ the same as float, double, long double

‎src/ansi-c/ansi_c_language.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ bool ansi_c_languaget::parse(
7575
ansi_c_parser.in=&codestr;
7676
ansi_c_parser.set_message_handler(get_message_handler());
7777
ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
78+
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
7879
ansi_c_parser.cpp98=false; // it's not C++
7980
ansi_c_parser.cpp11=false; // it's not C++
8081
ansi_c_parser.mode=config.ansi_c.mode;
@@ -196,6 +197,7 @@ bool ansi_c_languaget::to_expr(
196197
ansi_c_parser.in=&i_preprocessed;
197198
ansi_c_parser.set_message_handler(get_message_handler());
198199
ansi_c_parser.mode=config.ansi_c.mode;
200+
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
199201
ansi_c_scanner_init();
200202

201203
bool result=ansi_c_parser.parse();

‎src/ansi-c/ansi_c_parser.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert
3535
mode(modet::NONE),
3636
cpp98(false),
3737
cpp11(false),
38-
for_has_scope(false)
38+
for_has_scope(false),
39+
ts_18661_3_Floatn_types(false)
3940
{
4041
}
4142

@@ -77,6 +78,9 @@ class ansi_c_parsert:public parsert
7778
// in C99 and upwards, for(;;) has a scope
7879
bool for_has_scope;
7980

81+
// ISO/IEC TS 18661-3:2015
82+
bool ts_18661_3_Floatn_types;
83+
8084
typedef ansi_c_identifiert identifiert;
8185
typedef ansi_c_scopet scopet;
8286

‎src/ansi-c/scanner.l

Lines changed: 13 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -459,36 +459,31 @@ void ansi_c_scanner_init()
459459
return make_identifier();
460460
}
461461

462-
"_Float16" { // clang doesn't have it
463-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
462+
"_Float16" { if(PARSER.ts_18661_3_Floatn_types)
464463
{ loc(); return TOK_GCC_FLOAT16; }
465464
else
466465
return make_identifier();
467466
}
468467

469-
"_Float32" { // clang doesn't have it
470-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
468+
"_Float32" { if(PARSER.ts_18661_3_Floatn_types)
471469
{ loc(); return TOK_GCC_FLOAT32; }
472470
else
473471
return make_identifier();
474472
}
475473

476-
"_Float32x" { // clang doesn't have it
477-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
474+
"_Float32x" { if(PARSER.ts_18661_3_Floatn_types)
478475
{ loc(); return TOK_GCC_FLOAT32X; }
479476
else
480477
return make_identifier();
481478
}
482479

483-
"_Float64" { // clang doesn't have it
484-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
480+
"_Float64" { if(PARSER.ts_18661_3_Floatn_types)
485481
{ loc(); return TOK_GCC_FLOAT64; }
486482
else
487483
return make_identifier();
488484
}
489485

490-
"_Float64x" { // clang doesn't have it
491-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
486+
"_Float64x" { if(PARSER.ts_18661_3_Floatn_types)
492487
{ loc(); return TOK_GCC_FLOAT64X; }
493488
else
494489
return make_identifier();
@@ -501,16 +496,20 @@ void ansi_c_scanner_init()
501496
return make_identifier();
502497
}
503498

504-
"__float128" |
505-
"_Float128" { // clang doesn't have it
499+
"__float128" { // clang doesn't have it
506500
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
507501
{ loc(); return TOK_GCC_FLOAT128; }
508502
else
509503
return make_identifier();
510504
}
511505

512-
"_Float128x" { // clang doesn't have it
513-
if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
506+
"_Float128" { if(PARSER.ts_18661_3_Floatn_types)
507+
{ loc(); return TOK_GCC_FLOAT128; }
508+
else
509+
return make_identifier();
510+
}
511+
512+
"_Float128x" { if(PARSER.ts_18661_3_Floatn_types)
514513
{ loc(); return TOK_GCC_FLOAT128X; }
515514
else
516515
return make_identifier();

‎src/cpp/cpp_parser.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ bool cpp_parsert::parse()
2424
ansi_c_parser.cpp11=
2525
config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP11 ||
2626
config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP14;
27+
ansi_c_parser.ts_18661_3_Floatn_types=false;
2728
ansi_c_parser.in=in;
2829
ansi_c_parser.mode=mode;
2930
ansi_c_parser.set_file(get_file());

‎src/goto-cc/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ SRC = armcc_cmdline.cpp \
88
cw_mode.cpp \
99
gcc_cmdline.cpp \
1010
gcc_mode.cpp \
11+
gcc_version.cpp \
1112
goto_cc_cmdline.cpp \
1213
goto_cc_languages.cpp \
1314
goto_cc_main.cpp \

‎src/goto-cc/as_mode.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ int as_modet::run_as()
267267
std::cout << '\n';
268268
#endif
269269

270-
return run(new_argv[0], new_argv, cmdline.stdin_file, "");
270+
return run(new_argv[0], new_argv, cmdline.stdin_file);
271271
}
272272

273273
int as_modet::as_hybrid_binary()
@@ -314,7 +314,7 @@ int as_modet::as_hybrid_binary()
314314
objcopy_argv.push_back("--remove-section=goto-cc");
315315
objcopy_argv.push_back(output_file);
316316

317-
result=run(objcopy_argv[0], objcopy_argv, "", "");
317+
result = run(objcopy_argv[0], objcopy_argv);
318318
}
319319

320320
if(result==0)
@@ -327,7 +327,7 @@ int as_modet::as_hybrid_binary()
327327
objcopy_argv.push_back("goto-cc="+saved);
328328
objcopy_argv.push_back(output_file);
329329

330-
result=run(objcopy_argv[0], objcopy_argv, "", "");
330+
result = run(objcopy_argv[0], objcopy_argv);
331331
}
332332

333333
int remove_result=remove(saved.c_str());
@@ -354,7 +354,7 @@ int as_modet::as_hybrid_binary()
354354
lipo_argv.push_back("-output");
355355
lipo_argv.push_back(output_file);
356356

357-
result=run(lipo_argv[0], lipo_argv, "", "");
357+
result = run(lipo_argv[0], lipo_argv);
358358
}
359359

360360
int remove_result=remove(saved.c_str());

‎src/goto-cc/gcc_mode.cpp

Lines changed: 30 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -336,16 +336,26 @@ int gcc_modet::doit()
336336
base_name=="bcc" ||
337337
base_name.find("goto-bcc")!=std::string::npos;
338338

339+
// if we are gcc or bcc, then get the version number
340+
gcc_version.get(native_tool_name);
341+
339342
if((cmdline.isset('v') && cmdline.have_infile_arg()) ||
340343
(cmdline.isset("version") && !produce_hybrid_binary))
341344
{
342345
// "-v" a) prints the version and b) increases verbosity.
343346
// Compilation continues, don't exit!
344347

345348
if(act_as_bcc)
346-
std::cout << "bcc: version 0.16.17 (goto-cc " CBMC_VERSION ")\n";
349+
std::cout << "bcc: version " << gcc_version
350+
<< " (goto-cc " CBMC_VERSION ")\n";
347351
else
348-
std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n";
352+
{
353+
if(gcc_version.flavor == gcc_versiont::flavort::CLANG)
354+
std::cout << "clang version " << gcc_version
355+
<< " (goto-cc " CBMC_VERSION ")\n";
356+
else
357+
std::cout << "gcc (goto-cc " CBMC_VERSION ") " << gcc_version << '\n';
358+
}
349359
}
350360

351361
compilet compiler(cmdline,
@@ -359,11 +369,17 @@ int gcc_modet::doit()
359369
if(produce_hybrid_binary)
360370
return run_gcc(compiler);
361371

362-
std::cout << '\n' <<
363-
"Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" <<
364-
"CBMC version: " CBMC_VERSION << '\n' <<
365-
"Architecture: " << config.this_architecture() << '\n' <<
366-
"OS: " << config.this_operating_system() << '\n';
372+
std::cout
373+
<< '\n'
374+
<< "Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
375+
<< "CBMC version: " CBMC_VERSION << '\n'
376+
<< "Architecture: " << config.this_architecture() << '\n'
377+
<< "OS: " << config.this_operating_system() << '\n';
378+
379+
if(gcc_version.flavor == gcc_versiont::flavort::CLANG)
380+
std::cout << "clang: " << gcc_version << '\n';
381+
else
382+
std::cout << "gcc: " << gcc_version << '\n';
367383

368384
return EX_OK; // Exit!
369385
}
@@ -381,7 +397,7 @@ int gcc_modet::doit()
381397
if(cmdline.isset("dumpmachine"))
382398
std::cout << config.this_architecture() << '\n';
383399
else if(cmdline.isset("dumpversion"))
384-
std::cout << "3.4.4\n";
400+
std::cout << gcc_version << '\n';
385401

386402
// we don't have any meaningful output for the other options, and GCC
387403
// doesn't necessarily produce non-empty output either
@@ -509,6 +525,11 @@ int gcc_modet::doit()
509525
if(cmdline.isset("-fsingle-precision-constant"))
510526
config.ansi_c.single_precision_constant=true;
511527

528+
// ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
529+
if(gcc_version.flavor==gcc_versiont::flavort::GCC &&
530+
gcc_version.is_at_least(7))
531+
config.ansi_c.ts_18661_3_Floatn_types=true;
532+
512533
// -fshort-double makes double the same as float
513534
if(cmdline.isset("fshort-double"))
514535
config.ansi_c.double_width=config.ansi_c.single_width;
@@ -831,7 +852,7 @@ int gcc_modet::run_gcc(const compilet &compiler)
831852
debug() << " " << new_argv[i];
832853
debug() << eom;
833854

834-
return run(new_argv[0], new_argv, cmdline.stdin_file, "");
855+
return run(new_argv[0], new_argv, cmdline.stdin_file);
835856
}
836857

837858
int gcc_modet::gcc_hybrid_binary(compilet &compiler)

‎src/goto-cc/gcc_mode.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Date: June 2006
1515
#define CPROVER_GOTO_CC_GCC_MODE_H
1616

1717
#include "compile.h"
18+
#include "gcc_version.h"
1819
#include "goto_cc_mode.h"
1920

2021
#include <util/cout_message.h>
@@ -61,6 +62,8 @@ class gcc_modet:public goto_cc_modet
6162
const compilet &compiler);
6263

6364
static bool needs_preprocessing(const std::string &);
65+
66+
gcc_versiont gcc_version;
6467
};
6568

6669
#endif // CPROVER_GOTO_CC_GCC_MODE_H

0 commit comments

Comments
 (0)