add configure_gcc for version-specific gcc properties

Author: Daniel Kroening

src/ansi-c/gcc_version.cpp

@@ -142,3 +142,23 @@ std::ostream &operator<<(std::ostream &out, const gcc_versiont &v)
 {
   return out << v.v_major << '.' << v.v_minor << '.' << v.v_patchlevel;
 }
+
+void configure_gcc(const gcc_versiont &gcc_version)
+{
+  // 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;
+  }
+
+  const auto gcc_float128_minor_version =
+    config.ansi_c.arch == "x86_64" ? 3u : 5u;
+
+  // __float128 exists (as a typedef) since gcc 4.5 everywhere,
+  // and since 4.3 on x86_64
+  config.ansi_c.gcc__float128_type =
+    gcc_version.flavor == gcc_versiont::flavort::GCC &&
+    gcc_version.is_at_least(4u, gcc_float128_minor_version);
+}

src/ansi-c/gcc_version.h

@@ -50,6 +50,8 @@ class gcc_versiont
   }
 };
 
+void configure_gcc(const gcc_versiont &);
+
 std::ostream &operator<<(std::ostream &, const gcc_versiont &);
 
 #endif

src/cbmc/cbmc_parse_options.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_preprocess.h>
 #include <ansi-c/cprover_library.h>
+#include <ansi-c/gcc_version.h>
 
 #include <assembler/remove_asm.h>
 
@@ -490,6 +491,14 @@ int cbmc_parse_optionst::doit()
 
   register_languages();
 
+  // configure gcc, if required
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
+
   if(cmdline.isset("test-preprocessor"))
     return test_c_preprocessor(ui_message_handler)
              ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED

src/goto-cc/gcc_mode.cpp

@@ -531,24 +531,13 @@ 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;
-
-  const auto gcc_float128_minor_version =
-    config.ansi_c.arch == "x86_64" ? 3u : 5u;
-
-  // __float128 exists (as a typedef) since gcc 4.5 everywhere,
-  // and since 4.3 on x86_64
-  config.ansi_c.gcc__float128_type =
-    gcc_version.flavor == gcc_versiont::flavort::GCC &&
-    gcc_version.is_at_least(4u, gcc_float128_minor_version);
-
   // -fshort-double makes double the same as float
   if(cmdline.isset("fshort-double"))
     config.ansi_c.double_width=config.ansi_c.single_width;
 
+  // configure version-specific gcc settings
+  configure_gcc(gcc_version);
+
   switch(compiler.mode)
   {
   case compilet::LINK_LIBRARY: