goto-synthesizer: correctly configure the C front-end

goto-synthesizer will eventually invoke code that parses C code (for
example, the model library), which in turn requires correct
configuration to support _Float16. (For other tools this was previously
done in b2b2734.)

Author: tautschnig

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -16,6 +16,7 @@ Author: Qinheping Hu
 #include <goto-programs/set_properties.h>
 #include <goto-programs/write_goto_binary.h>
 
+#include <ansi-c/gcc_version.h>
 #include <goto-instrument/contracts/contracts.h>
 #include <goto-instrument/nondet_volatile.h>
 
@@ -52,6 +53,14 @@ int goto_synthesizer_parse_optionst::doit()
   if(result_get_goto_program != CPROVER_EXIT_SUCCESS)
     return result_get_goto_program;
 
+  // configure gcc, if required -- get_goto_program will have set the config
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
+
   // Synthesize loop invariants and annotate them into `goto_model`
   enumerative_loop_contracts_synthesizert synthesizer(goto_model, log);
   const auto &invariant_map = synthesizer.synthesize_all();