goto-cc: get gcc version

appveyor.yml

@@ -74,6 +74,7 @@ test_script:
     rmdir /s /q ansi-c\Universal_characters1
     rmdir /s /q ansi-c\function_return1
     rmdir /s /q ansi-c\gcc_attributes7
+    rmdir /s /q ansi-c\gcc_version1
     rmdir /s /q ansi-c\struct6
     rmdir /s /q ansi-c\struct7
     rmdir /s /q cbmc\Malloc23

regression/ansi-c/float_constant1/main.c

@@ -12,7 +12,7 @@ STATIC_ASSERT(0X.0p+1f == 0);
 
 // 32-bit, 64-bit and 128-bit constants, GCC proper only,
 // clang doesn't have it
-#if defined(__GNUC__) && !defined(__clang__)
+#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 7
 STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
 STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));

regression/ansi-c/gcc_types_compatible_p1/main.c

@@ -67,8 +67,8 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
 STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
 STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
 
-#ifndef __clang__
 // clang doesn't have these
+#if !defined(__clang__) && __GNUC__ >= 7
 #if defined(__x86_64__) || defined(__i386__)
 STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128));
 #endif
@@ -95,16 +95,19 @@ STATIC_ASSERT(!__builtin_types_compatible_p(long int, int));
 STATIC_ASSERT(!__builtin_types_compatible_p(long long int, long int));
 STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
 
-#ifndef __clang__
+STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
+
 // clang doesn't have these
+#if !defined(__clang__)
+#if __GNUC__ >= 7
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
 STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
+#endif
 STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
 STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));
-STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
 #endif
 #endif
 

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

@@ -0,0 +1,4 @@
+#!/bin/sh
+
+gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $*
+

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

@@ -0,0 +1,4 @@
+#!/bin/sh
+
+gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $*
+

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

@@ -0,0 +1,2 @@
+typedef double _Float64;
+

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

@@ -0,0 +1,2 @@
+_Float64 some_var;
+

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

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

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

@@ -0,0 +1,7 @@
+CORE
+gcc-7.c
+--native-compiler ./fake-gcc-7
+^EXIT=0$
+^SIGNAL=0$
+--
+^CONVERSION ERROR$

regression/cbmc/ts18661_typedefs/main.c

@@ -1,9 +1,18 @@
+#if defined(__clang__)
+#elif defined(__GNUC__)
+#if __GNUC__ >= 7
+#define HAS_FLOATN
+#endif
+#endif
+
+#ifndef HAS_FLOATN
 typedef float _Float32;
 typedef double _Float32x;
 typedef double _Float64;
 typedef long double _Float64x;
 typedef long double _Float128;
 typedef long double _Float128x;
+#endif
 
 int main(int argc, char** argv) {
 }

src/ansi-c/ansi_c_convert_type.cpp

@@ -346,22 +346,9 @@ void ansi_c_convert_typet::write(typet &type)
        gcc_float64_cnt+gcc_float64x_cnt+
        gcc_float128_cnt+gcc_float128x_cnt>=2)
     {
-      // Temporary workaround for our glibc versions that try to define TS 18661
-      // types (for example, typedef float _Float32). This can be removed once
-      // upgrade cbmc's GCC support to at least 7.0 (when glibc will expect us
-      // to provide these types natively), or disable parsing them ourselves
-      // when our preprocessor stage claims support <7.0.
-      if(c_storage_spec.is_typedef)
-      {
-        warning().source_location = source_location;
-        warning() << "ignoring typedef for TS 18661 (_FloatNNx) type. If you need these, try using goto-cc instead." << eom;
-      }
-      else
-      {
-        error().source_location=source_location;
-        error() << "conflicting type modifiers" << eom;
-        throw 0;
-      }
+      error().source_location=source_location;
+      error() << "conflicting type modifiers" << eom;
+      throw 0;
     }
 
     // _not_ the same as float, double, long double

src/ansi-c/ansi_c_language.cpp

@@ -75,6 +75,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.in=&codestr;
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
+  ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_parser.cpp98=false; // it's not C++
   ansi_c_parser.cpp11=false; // it's not C++
   ansi_c_parser.mode=config.ansi_c.mode;
@@ -196,6 +197,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.in=&i_preprocessed;
   ansi_c_parser.set_message_handler(get_message_handler());
   ansi_c_parser.mode=config.ansi_c.mode;
+  ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
   ansi_c_scanner_init();
 
   bool result=ansi_c_parser.parse();

src/ansi-c/ansi_c_parser.h

@@ -35,7 +35,8 @@ class ansi_c_parsert:public parsert
     mode(modet::NONE),
     cpp98(false),
     cpp11(false),
-    for_has_scope(false)
+    for_has_scope(false),
+    ts_18661_3_Floatn_types(false)
   {
   }
 
@@ -77,6 +78,9 @@ class ansi_c_parsert:public parsert
   // in C99 and upwards, for(;;) has a scope
   bool for_has_scope;
 
+  // ISO/IEC TS 18661-3:2015
+  bool ts_18661_3_Floatn_types;
+
   typedef ansi_c_identifiert identifiert;
   typedef ansi_c_scopet scopet;
 

src/ansi-c/scanner.l

@@ -459,36 +459,31 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"_Float16"      { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float16"      { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT16; }
                   else
                     return make_identifier();
                 }
 
-"_Float32"      { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float32"      { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT32; }
                   else
                     return make_identifier();
                 }
 
-"_Float32x"     { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float32x"     { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT32X; }
                   else
                     return make_identifier();
                 }
 
-"_Float64"      { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float64"      { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT64; }
                   else
                     return make_identifier();
                 }
 
-"_Float64x"     { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float64x"     { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT64X; }
                   else
                     return make_identifier();
@@ -501,16 +496,20 @@ void ansi_c_scanner_init()
                     return make_identifier();
                 }
 
-"__float128" |
-"_Float128"     { // clang doesn't have it
+"__float128"    { // clang doesn't have it
                   if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();
                 }
 
-"_Float128x"    { // clang doesn't have it
-                  if(PARSER.mode==configt::ansi_ct::flavourt::GCC)
+"_Float128"     { if(PARSER.ts_18661_3_Floatn_types)
+                  { loc(); return TOK_GCC_FLOAT128; }
+                  else
+                    return make_identifier();
+                }
+
+"_Float128x"    { if(PARSER.ts_18661_3_Floatn_types)
                   { loc(); return TOK_GCC_FLOAT128X; }
                   else
                     return make_identifier();

src/cpp/cpp_parser.cpp

@@ -24,6 +24,7 @@ bool cpp_parsert::parse()
   ansi_c_parser.cpp11=
     config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP11 ||
     config.cpp.cpp_standard==configt::cppt::cpp_standardt::CPP14;
+  ansi_c_parser.ts_18661_3_Floatn_types=false;
   ansi_c_parser.in=in;
   ansi_c_parser.mode=mode;
   ansi_c_parser.set_file(get_file());

src/goto-cc/Makefile

@@ -8,6 +8,7 @@ SRC = armcc_cmdline.cpp \
       cw_mode.cpp \
       gcc_cmdline.cpp \
       gcc_mode.cpp \
+      gcc_version.cpp \
       goto_cc_cmdline.cpp \
       goto_cc_languages.cpp \
       goto_cc_main.cpp \

src/goto-cc/as_mode.cpp

@@ -267,7 +267,7 @@ int as_modet::run_as()
   std::cout << '\n';
   #endif
 
-  return run(new_argv[0], new_argv, cmdline.stdin_file, "");
+  return run(new_argv[0], new_argv, cmdline.stdin_file);
 }
 
 int as_modet::as_hybrid_binary()
@@ -314,7 +314,7 @@ int as_modet::as_hybrid_binary()
     objcopy_argv.push_back("--remove-section=goto-cc");
     objcopy_argv.push_back(output_file);
 
-    result=run(objcopy_argv[0], objcopy_argv, "", "");
+    result = run(objcopy_argv[0], objcopy_argv);
   }
 
   if(result==0)
@@ -327,7 +327,7 @@ int as_modet::as_hybrid_binary()
     objcopy_argv.push_back("goto-cc="+saved);
     objcopy_argv.push_back(output_file);
 
-    result=run(objcopy_argv[0], objcopy_argv, "", "");
+    result = run(objcopy_argv[0], objcopy_argv);
   }
 
   int remove_result=remove(saved.c_str());
@@ -354,7 +354,7 @@ int as_modet::as_hybrid_binary()
     lipo_argv.push_back("-output");
     lipo_argv.push_back(output_file);
 
-    result=run(lipo_argv[0], lipo_argv, "", "");
+    result = run(lipo_argv[0], lipo_argv);
   }
 
   int remove_result=remove(saved.c_str());

src/goto-cc/gcc_mode.cpp

@@ -336,16 +336,26 @@ int gcc_modet::doit()
     base_name=="bcc" ||
     base_name.find("goto-bcc")!=std::string::npos;
 
+  // if we are gcc or bcc, then get the version number
+  gcc_version.get(native_tool_name);
+
   if((cmdline.isset('v') && cmdline.have_infile_arg()) ||
      (cmdline.isset("version") && !produce_hybrid_binary))
   {
     // "-v" a) prints the version and b) increases verbosity.
     // Compilation continues, don't exit!
 
     if(act_as_bcc)
-      std::cout << "bcc: version 0.16.17 (goto-cc " CBMC_VERSION ")\n";
+      std::cout << "bcc: version " << gcc_version
+                << " (goto-cc " CBMC_VERSION ")\n";
     else
-      std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n";
+    {
+      if(gcc_version.flavor == gcc_versiont::flavort::CLANG)
+        std::cout << "clang version " << gcc_version
+                  << " (goto-cc " CBMC_VERSION ")\n";
+      else
+        std::cout << "gcc (goto-cc " CBMC_VERSION ") " << gcc_version << '\n';
+    }
   }
 
   compilet compiler(cmdline,
@@ -359,11 +369,17 @@ int gcc_modet::doit()
     if(produce_hybrid_binary)
       return run_gcc(compiler);
 
-    std::cout << '\n' <<
-      "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" <<
-      "CBMC version: " CBMC_VERSION << '\n' <<
-      "Architecture: " << config.this_architecture() << '\n' <<
-      "OS: " << config.this_operating_system() << '\n';
+    std::cout
+      << '\n'
+      << "Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
+      << "CBMC version: " CBMC_VERSION << '\n'
+      << "Architecture: " << config.this_architecture() << '\n'
+      << "OS: " << config.this_operating_system() << '\n';
+
+    if(gcc_version.flavor == gcc_versiont::flavort::CLANG)
+      std::cout << "clang: " << gcc_version << '\n';
+    else
+      std::cout << "gcc: " << gcc_version << '\n';
 
     return EX_OK; // Exit!
   }
@@ -381,7 +397,7 @@ int gcc_modet::doit()
     if(cmdline.isset("dumpmachine"))
       std::cout << config.this_architecture() << '\n';
     else if(cmdline.isset("dumpversion"))
-      std::cout << "3.4.4\n";
+      std::cout << gcc_version << '\n';
 
     // we don't have any meaningful output for the other options, and GCC
     // doesn't necessarily produce non-empty output either
@@ -509,6 +525,11 @@ int gcc_modet::doit()
   if(cmdline.isset("-fsingle-precision-constant"))
     config.ansi_c.single_precision_constant=true;
 
+  // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
+  if(gcc_version.flavor==gcc_versiont::flavort::GCC &&
+     gcc_version.is_at_least(7))
+    config.ansi_c.ts_18661_3_Floatn_types=true;
+
   // -fshort-double makes double the same as float
   if(cmdline.isset("fshort-double"))
     config.ansi_c.double_width=config.ansi_c.single_width;
@@ -831,7 +852,7 @@ int gcc_modet::run_gcc(const compilet &compiler)
     debug() << " " << new_argv[i];
   debug() << eom;
 
-  return run(new_argv[0], new_argv, cmdline.stdin_file, "");
+  return run(new_argv[0], new_argv, cmdline.stdin_file);
 }
 
 int gcc_modet::gcc_hybrid_binary(compilet &compiler)

src/goto-cc/gcc_mode.h

@@ -15,6 +15,7 @@ Date: June 2006
 #define CPROVER_GOTO_CC_GCC_MODE_H
 
 #include "compile.h"
+#include "gcc_version.h"
 #include "goto_cc_mode.h"
 
 #include <util/cout_message.h>
@@ -61,6 +62,8 @@ class gcc_modet:public goto_cc_modet
     const compilet &compiler);
 
   static bool needs_preprocessing(const std::string &);
+
+  gcc_versiont gcc_version;
 };
 
 #endif // CPROVER_GOTO_CC_GCC_MODE_H