cprover
c_preprocess.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "c_preprocess.h"
10 
11 #include <cstdio>
12 #include <cstdlib>
13 #include <cstring>
14 
15 #if defined(__linux__) || \
16  defined(__FreeBSD_kernel__) || \
17  defined(__GNU__) || \
18  defined(__unix__) || \
19  defined(__CYGWIN__) || \
20  defined(__MACH__)
21 #include <unistd.h>
22 #endif
23 
24 #include <fstream>
25 
26 #include <util/c_types.h>
27 #include <util/config.h>
28 #include <util/message.h>
29 #include <util/tempfile.h>
30 #include <util/unicode.h>
31 #include <util/arith_tools.h>
32 #include <util/std_types.h>
33 #include <util/prefix.h>
34 
35 #define GCC_DEFINES_16 \
36  " -D__INT_MAX__=32767"\
37  " -D__CHAR_BIT__=8"\
38  " -D__SCHAR_MAX__=127"\
39  " -D__SHRT_MAX__=32767"\
40  " -D__INT32_TYPE__=long"\
41  " -D__LONG_LONG_MAX__=2147483647L"\
42  " -D__LONG_MAX__=2147483647" \
43  " -D__SIZE_TYPE__=\"unsigned int\""\
44  " -D__PTRDIFF_TYPE__=int"\
45  " -D__WINT_TYPE__=\"unsigned int\""\
46  " -D__INTMAX_TYPE__=\"long long int\""\
47  " -D__UINTMAX_TYPE__=\"long long unsigned int\""\
48  " -D__INTPTR_TYPE__=\"int\""\
49  " -D__UINTPTR_TYPE__=\"unsigned int\""
50 
51 #define GCC_DEFINES_32 \
52  " -D__INT_MAX__=2147483647"\
53  " -D__CHAR_BIT__=8"\
54  " -D__SCHAR_MAX__=127"\
55  " -D__SHRT_MAX__=32767"\
56  " -D__INT32_TYPE__=int"\
57  " -D__LONG_LONG_MAX__=9223372036854775807LL"\
58  " -D__LONG_MAX__=2147483647L" \
59  " -D__SIZE_TYPE__=\"long unsigned int\""\
60  " -D__PTRDIFF_TYPE__=int"\
61  " -D__WINT_TYPE__=\"unsigned int\""\
62  " -D__INTMAX_TYPE__=\"long long int\""\
63  " -D__UINTMAX_TYPE__=\"long long unsigned int\""\
64  " -D__INTPTR_TYPE__=\"long int\""\
65  " -D__UINTPTR_TYPE__=\"long unsigned int\""
66 
67 #define GCC_DEFINES_LP64 \
68  " -D__INT_MAX__=2147483647"\
69  " -D__CHAR_BIT__=8"\
70  " -D__SCHAR_MAX__=127"\
71  " -D__SHRT_MAX__=32767"\
72  " -D__INT32_TYPE__=int"\
73  " -D__LONG_LONG_MAX__=9223372036854775807LL"\
74  " -D__LONG_MAX__=9223372036854775807L"\
75  " -D__SIZE_TYPE__=\"long unsigned int\""\
76  " -D__PTRDIFF_TYPE__=long"\
77  " -D__WINT_TYPE__=\"unsigned int\""\
78  " -D__INTMAX_TYPE__=\"long int\""\
79  " -D__UINTMAX_TYPE__=\"long unsigned int\""\
80  " -D__INTPTR_TYPE__=\"long int\""\
81  " -D__UINTPTR_TYPE__=\"long unsigned int\""
82 
83 #define GCC_DEFINES_LLP64 \
84  " -D__INT_MAX__=2147483647"\
85  " -D__CHAR_BIT__=8"\
86  " -D__SCHAR_MAX__=127"\
87  " -D__SHRT_MAX__=32767"\
88  " -D__INT32_TYPE__=int"\
89  " -D__LONG_LONG_MAX__=9223372036854775807LL"\
90  " -D__LONG_MAX__=2147483647"\
91  " -D__SIZE_TYPE__=\"long long unsigned int\""\
92  " -D__PTRDIFF_TYPE__=\"long long\""\
93  " -D__WINT_TYPE__=\"unsigned int\""\
94  " -D__INTMAX_TYPE__=\"long long int\""\
95  " -D__UINTMAX_TYPE__=\"long long unsigned int\""\
96  " -D__INTPTR_TYPE__=\"long long int\""\
97  " -D__UINTPTR_TYPE__=\"long long unsigned int\""
98 
100 static std::string type_max(const typet &src)
101 {
102  if(src.id()==ID_signedbv)
103  return integer2string(
104  power(2, to_signedbv_type(src).get_width()-1)-1);
105  else if(src.id()==ID_unsignedbv)
106  return integer2string(
107  power(2, to_unsignedbv_type(src).get_width()-1)-1);
108  else
109  assert(false);
110 }
111 
113 static std::string shell_quote(const std::string &src)
114 {
115  #ifdef _WIN32
116  // first check if quoting is needed at all
117 
118  if(src.find(' ')==std::string::npos &&
119  src.find('"')==std::string::npos &&
120  src.find('&')==std::string::npos &&
121  src.find('|')==std::string::npos &&
122  src.find('(')==std::string::npos &&
123  src.find(')')==std::string::npos &&
124  src.find('<')==std::string::npos &&
125  src.find('>')==std::string::npos &&
126  src.find('^')==std::string::npos)
127  {
128  // seems fine -- return as is
129  return src;
130  }
131 
132  std::string result;
133 
134  result+='"';
135 
136  for(const char ch : src)
137  {
138  if(ch=='"')
139  result+='"'; // quotes are doubled
140  result+=ch;
141  }
142 
143  result+='"';
144 
145  return result;
146 
147  #else
148 
149  // first check if quoting is needed at all
150 
151  if(src.find(' ')==std::string::npos &&
152  src.find('"')==std::string::npos &&
153  src.find('*')==std::string::npos &&
154  src.find('$')==std::string::npos &&
155  src.find('\\')==std::string::npos &&
156  src.find('?')==std::string::npos &&
157  src.find('&')==std::string::npos &&
158  src.find('|')==std::string::npos &&
159  src.find('>')==std::string::npos &&
160  src.find('<')==std::string::npos &&
161  src.find('^')==std::string::npos &&
162  src.find('\'')==std::string::npos)
163  {
164  // seems fine -- return as is
165  return src;
166  }
167 
168  std::string result;
169 
170  // the single quotes catch everything but themselves!
171  result+='\'';
172 
173  for(const char ch : src)
174  {
175  if(ch=='\'')
176  result+="'\\''";
177  result+=ch;
178  }
179 
180  result+='\'';
181 
182  return result;
183  #endif
184 }
185 
186 static void error_parse_line(
187  const std::string &line,
188  bool warning_only,
189  messaget &message)
190 {
191  std::string error_msg=line;
192  source_locationt saved_error_location;
193 
194  if(has_prefix(line, "file "))
195  {
196  const char *tptr=line.c_str();
197  int state=0;
198  std::string file, line_no, column, _error_msg, function;
199 
200  tptr+=5;
201 
202  char previous=0;
203 
204  while(*tptr!=0)
205  {
206  if(strncmp(tptr, " line ", 6)==0 && state!=4)
207  {
208  state=1;
209  tptr+=6;
210  continue;
211  }
212  else if(strncmp(tptr, " column ", 8)==0 && state!=4)
213  {
214  state=2;
215  tptr+=8;
216  continue;
217  }
218  else if(strncmp(tptr, " function ", 10)==0 && state!=4)
219  {
220  state=3;
221  tptr+=10;
222  continue;
223  }
224  else if(*tptr==':' && state!=4)
225  {
226  if(tptr[1]==' ' && previous!=':')
227  {
228  state=4;
229  tptr++;
230  while(*tptr==' ') tptr++;
231  continue;
232  }
233  }
234 
235  if(state==0) // file
236  file+=*tptr;
237  else if(state==1) // line number
238  line_no+=*tptr;
239  else if(state==2) // column
240  column+=*tptr;
241  else if(state==3) // function
242  function+=*tptr;
243  else if(state==4) // error message
244  _error_msg+=*tptr;
245 
246  previous=*tptr;
247 
248  tptr++;
249  }
250 
251  if(state==4)
252  {
253  saved_error_location.set_file(file);
254  saved_error_location.set_function(function);
255  saved_error_location.set_line(line_no);
256  saved_error_location.set_column(column);
257  error_msg=_error_msg;
258  }
259  }
260  else if(has_prefix(line, "In file included from "))
261  {
262  }
263  else
264  {
265  const char *tptr=line.c_str();
266  int state=0;
267  std::string file, line_no;
268 
269  while(*tptr!=0)
270  {
271  if(state==0)
272  {
273  if(*tptr==':')
274  state++;
275  else
276  file+=*tptr;
277  }
278  else if(state==1)
279  {
280  if(*tptr==':')
281  state++;
282  else if(isdigit(*tptr))
283  line_no+=*tptr;
284  else
285  state=3;
286  }
287 
288  tptr++;
289  }
290 
291  if(state==2)
292  {
293  saved_error_location.set_file(file);
294  saved_error_location.set_function("");
295  saved_error_location.set_line(line_no);
296  saved_error_location.set_column("");
297  }
298  }
299 
301  warning_only ? message.warning() : message.error();
302  m.source_location=saved_error_location;
303  m << error_msg << messaget::eom;
304 }
305 
306 static void error_parse(
307  std::istream &errors,
308  bool warning_only,
309  messaget &message)
310 {
311  std::string line;
312 
313  while(std::getline(errors, line))
314  error_parse_line(line, warning_only, message);
315 }
316 
319  std::istream &instream,
320  std::ostream &outstream,
321  message_handlert &message_handler)
322 {
323  temporary_filet tmp_file("tmp.stdin", ".c");
324 
325  std::ofstream tmp(tmp_file());
326 
327  if(!tmp)
328  {
329  messaget message(message_handler);
330  message.error() << "failed to open temporary file" << messaget::eom;
331  return true; // error
332  }
333 
334  tmp << instream.rdbuf(); // copy
335 
336  tmp.close(); // flush
337 
338  bool result=c_preprocess(tmp_file(), outstream, message_handler);
339 
340  return result;
341 }
342 
344 static bool is_dot_i_file(const std::string &path)
345 {
346  const char *ext=strrchr(path.c_str(), '.');
347  if(ext==nullptr)
348  return false;
349  if(std::string(ext)==".i" ||
350  std::string(ext)==".ii")
351  return true;
352  return false;
353 }
354 
357  const std::string &, std::ostream &, message_handlert &);
358 bool c_preprocess_arm(
359  const std::string &, std::ostream &, message_handlert &);
361  const std::string &,
362  std::ostream &,
365 bool c_preprocess_none(
366  const std::string &, std::ostream &, message_handlert &);
368  const std::string &, std::ostream &, message_handlert &);
369 
371  const std::string &path,
372  std::ostream &outstream,
373  message_handlert &message_handler)
374 {
375  switch(config.ansi_c.preprocessor)
376  {
378  return c_preprocess_codewarrior(path, outstream, message_handler);
379 
381  return
383  path, outstream, message_handler, config.ansi_c.preprocessor);
384 
386  return
388  path, outstream, message_handler, config.ansi_c.preprocessor);
389 
391  return c_preprocess_visual_studio(path, outstream, message_handler);
392 
394  return c_preprocess_arm(path, outstream, message_handler);
395 
397  return c_preprocess_none(path, outstream, message_handler);
398  }
399 
400  // not reached
401  return true;
402 }
403 
406  const std::string &file,
407  std::ostream &outstream,
408  message_handlert &message_handler)
409 {
410  // check extension
411  if(is_dot_i_file(file))
412  return c_preprocess_none(file, outstream, message_handler);
413 
414  messaget message(message_handler);
415 
416  // use Visual Studio's CL
417 
418  std::string stderr_file=get_temporary_file("tmp.stderr", "");
419  std::string command_file_name=get_temporary_file("tmp.cl-cmd", "");
420 
421  {
422  std::ofstream command_file(command_file_name);
423 
424  // This marks the file as UTF-8, which Visual Studio
425  // understands.
426  command_file << char(0xef) << char(0xbb) << char(0xbf);
427 
428  command_file << "/nologo" << "\n";
429  command_file << "/E" << "\n";
430  command_file << "/D__CPROVER__" << "\n";
431  command_file << "/D__WORDSIZE=" << config.ansi_c.pointer_width << "\n";
432 
433  if(config.ansi_c.pointer_width==64)
434  {
435  command_file << "\"/D__PTRDIFF_TYPE__=long long int\"" << "\n";
436  // yes, both _WIN32 and _WIN64 get defined
437  command_file << "/D_WIN64" << "\n";
438  }
439  else
440  {
441  command_file << "/D__PTRDIFF_TYPE__=int" << "\n";
442  command_file << "/U_WIN64" << "\n";
443  }
444 
446  command_file << "/J" << "\n"; // This causes _CHAR_UNSIGNED to be defined
447 
448  // Standard Defines, ANSI9899 6.10.8
449  command_file << "/D__STDC_VERSION__=199901L" << "\n";
450  command_file << "/D__STDC_IEC_559__=1" << "\n";
451  command_file << "/D__STDC_IEC_559_COMPLEX__=1" << "\n";
452  command_file << "/D__STDC_ISO_10646__=1" << "\n";
453 
454  for(const auto &define : config.ansi_c.defines)
455  command_file << "/D" << shell_quote(define) << "\n";
456 
457  for(const auto &include_path : config.ansi_c.include_paths)
458  command_file << "/I" << shell_quote(include_path) << "\n";
459 
460  for(const auto &include_file : config.ansi_c.include_files)
461  command_file << "/FI" << shell_quote(include_file) << "\n";
462 
463  // Finally, the file to be preprocessed
464  // (this is already in UTF-8).
465  command_file << shell_quote(file) << "\n";
466  }
467 
468  std::string tmpi=get_temporary_file("tmp.cl", "");
469 
470  std::string command="CL @\""+command_file_name+"\"";
471  command+=" > \""+tmpi+"\"";
472  command+=" 2> \""+stderr_file+"\"";
473 
474  // _popen isn't very reliable on WIN32
475  // that's why we use system()
476  int result=system(command.c_str());
477 
478  std::ifstream instream(tmpi);
479 
480  if(!instream)
481  {
482  unlink(tmpi.c_str());
483  unlink(stderr_file.c_str());
484  unlink(command_file_name.c_str());
485  message.error() << "CL Preprocessing failed (open failed)"
486  << messaget::eom;
487  return true;
488  }
489 
490  outstream << instream.rdbuf(); // copy
491 
492  instream.close();
493  unlink(tmpi.c_str());
494  unlink(command_file_name.c_str());
495 
496  // errors/warnings
497  std::ifstream stderr_stream(stderr_file);
498  error_parse(stderr_stream, result==0, message);
499 
500  unlink(stderr_file.c_str());
501 
502  if(result!=0)
503  {
504  message.error() << "CL Preprocessing failed" << messaget::eom;
505  return true;
506  }
507 
508  return false;
509 }
510 
513  std::istream &instream,
514  std::ostream &outstream)
515 {
516  // CodeWarrior prepends some header to the file,
517  // marked with '#' signs.
518  // We skip over it.
519  //
520  // CodeWarrior has an ugly way of marking lines, e.g.:
521  //
522  // /* #line 1 "__ppc_eabi_init.cpp" /* stack depth 0 */
523  //
524  // We remove the initial '/* ' prefix
525 
526  std::string line;
527 
528  while(instream)
529  {
530  std::getline(instream, line);
531 
532  if(line.size()>=2 &&
533  line[0]=='#' && (line[1]=='#' || line[1]==' ' || line[1]=='\t'))
534  {
535  // skip the line!
536  }
537  else if(line.size()>=3 &&
538  line[0]=='/' && line[1]=='*' && line[2]==' ')
539  {
540  outstream << line.c_str()+3 << "\n"; // strip the '/* '
541  }
542  else
543  outstream << line << "\n";
544  }
545 }
546 
549  const std::string &file,
550  std::ostream &outstream,
551  message_handlert &message_handler)
552 {
553  // check extension
554  if(is_dot_i_file(file))
555  return c_preprocess_none(file, outstream, message_handler);
556 
557  // preprocessing
558  messaget message(message_handler);
559 
560  std::string stderr_file=get_temporary_file("tmp.stderr", "");
561 
562  std::string command;
563 
564  command="mwcceppc -E -P -D__CPROVER__ -ppopt line -ppopt full";
565 
566  for(const auto &define : config.ansi_c.defines)
567  command+=" -D"+shell_quote(define);
568 
569  for(const auto &include_path : config.ansi_c.include_paths)
570  command+=" -I"+shell_quote(include_path);
571 
572  for(const auto &include_file : config.ansi_c.include_files)
573  command+=" -include "+shell_quote(include_file);
574 
575  for(const auto &opt : config.ansi_c.preprocessor_options)
576  command+=" "+opt;
577 
578  int result;
579 
580  std::string tmpi=get_temporary_file("tmp.cl", "");
581  command+=" \""+file+"\"";
582  command+=" -o \""+tmpi+"\"";
583  command+=" 2> \""+stderr_file+"\"";
584 
585  result=system(command.c_str());
586 
587  std::ifstream stream_i(tmpi);
588 
589  if(stream_i)
590  {
591  postprocess_codewarrior(stream_i, outstream);
592 
593  stream_i.close();
594  unlink(tmpi.c_str());
595  }
596  else
597  {
598  unlink(tmpi.c_str());
599  unlink(stderr_file.c_str());
600  message.error() << "Preprocessing failed (fopen failed)"
601  << messaget::eom;
602  return true;
603  }
604 
605  // errors/warnings
606  std::ifstream stderr_stream(stderr_file);
607  error_parse(stderr_stream, result==0, message);
608 
609  unlink(stderr_file.c_str());
610 
611  if(result!=0)
612  {
613  message.error() << "Preprocessing failed" << messaget::eom;
614  return true;
615  }
616 
617  return false;
618 }
619 
622  const std::string &file,
623  std::ostream &outstream,
624  message_handlert &message_handler,
625  configt::ansi_ct::preprocessort preprocessor)
626 {
627  // check extension
628  if(is_dot_i_file(file))
629  return c_preprocess_none(file, outstream, message_handler);
630 
631  // preprocessing
632  messaget message(message_handler);
633 
634  std::string stderr_file=get_temporary_file("tmp.stderr", "");
635 
636  std::string command;
637 
639  command="clang";
640  else
641  command="gcc";
642 
643  command +=" -E -undef -D__CPROVER__";
644 
645  command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
646 
647  command+=" -D__DBL_MIN_EXP__=\"(-1021)\"";
648  command+=" -D__FLT_MIN__=1.17549435e-38F";
649  command+=" -D__DEC64_SUBNORMAL_MIN__=0.000000000000001E-383DD";
650  command+=" -D__CHAR_BIT__=8";
651  command+=" -D__DBL_DENORM_MIN__=4.9406564584124654e-324";
652  command+=" -D__FLT_EVAL_METHOD__=0";
653  command+=" -D__DBL_MIN_10_EXP__=\"(-307)\"";
654  command+=" -D__FINITE_MATH_ONLY__=0";
655  command+=" -D__DEC64_MAX_EXP__=384";
656  command+=" -D__SHRT_MAX__=32767";
657  command+=" -D__LDBL_MAX__=1.18973149535723176502e+4932L";
658  command+=" -D__DEC32_EPSILON__=1E-6DF";
659  command+=" -D__SCHAR_MAX__=127";
660  command+=" -D__USER_LABEL_PREFIX__=_";
661  command+=" -D__DEC64_MIN_EXP__=\"(-383)\"";
662  command+=" -D__DBL_DIG__=15";
663  command+=" -D__FLT_EPSILON__=1.19209290e-7F";
664  command+=" -D__LDBL_MIN__=3.36210314311209350626e-4932L";
665  command+=" -D__DEC32_MAX__=9.999999E96DF";
666  command+=" -D__DECIMAL_DIG__=21";
667  command+=" -D__LDBL_HAS_QUIET_NAN__=1";
668  command+=" -D__DYNAMIC__=1";
669  command+=" -D__GNUC__=4";
670  command+=" -D__FLT_HAS_DENORM__=1";
671  command+=" -D__DBL_MAX__=1.7976931348623157e+308";
672  command+=" -D__DBL_HAS_INFINITY__=1";
673  command+=" -D__DEC32_MIN_EXP__=\"(-95)\"";
674  command+=" -D__LDBL_HAS_DENORM__=1";
675  command+=" -D__DEC32_MIN__=1E-95DF";
676  command+=" -D__DBL_MAX_EXP__=1024";
677  command+=" -D__DEC128_EPSILON__=1E-33DL";
678  command+=" -D__SSE2_MATH__=1";
679  command+=" -D__GXX_ABI_VERSION=1002";
680  command+=" -D__FLT_MIN_EXP__=\"(-125)\"";
681  command+=" -D__DBL_MIN__=2.2250738585072014e-308";
682  command+=" -D__DBL_HAS_QUIET_NAN__=1";
683  command+=" -D__DEC128_MIN__=1E-6143DL";
684  command+=" -D__REGISTER_PREFIX__=";
685  command+=" -D__DBL_HAS_DENORM__=1";
686  command+=" -D__DEC_EVAL_METHOD__=2";
687  command+=" -D__DEC128_MAX__=9.999999999999999999999999999999999E6144DL";
688  command+=" -D__FLT_MANT_DIG__=24";
689  command+=" -D__DEC64_EPSILON__=1E-15DD";
690  command+=" -D__DEC128_MIN_EXP__=\"(-6143)\"";
691  command+=" -D__DEC32_SUBNORMAL_MIN__=0.000001E-95DF";
692  command+=" -D__FLT_RADIX__=2";
693  command+=" -D__LDBL_EPSILON__=1.08420217248550443401e-19L";
694  command+=" -D__k8=1";
695  command+=" -D__LDBL_DIG__=18";
696  command+=" -D__FLT_HAS_QUIET_NAN__=1";
697  command+=" -D__FLT_MAX_10_EXP__=38";
698  command+=" -D__FLT_HAS_INFINITY__=1";
699  command+=" -D__DEC64_MAX__=9.999999999999999E384DD";
700  command+=" -D__DEC64_MANT_DIG__=16";
701  command+=" -D__DEC32_MAX_EXP__=96";
702  // NOLINTNEXTLINE(whitespace/line_length)
703  command+=" -D__DEC128_SUBNORMAL_MIN__=0.000000000000000000000000000000001E-6143DL";
704  command+=" -D__LDBL_MANT_DIG__=64";
705  command+=" -D__CONSTANT_CFSTRINGS__=1";
706  command+=" -D__DEC32_MANT_DIG__=7";
707  command+=" -D__k8__=1";
708  command+=" -D__pic__=2";
709  command+=" -D__FLT_DIG__=6";
710  command+=" -D__FLT_MAX_EXP__=128";
711  // command+=" -D__BLOCKS__=1";
712  command+=" -D__DBL_MANT_DIG__=53";
713  command+=" -D__DEC64_MIN__=1E-383DD";
714  command+=" -D__LDBL_MIN_EXP__=\"(-16381)\"";
715  command+=" -D__LDBL_MAX_EXP__=16384";
716  command+=" -D__LDBL_MAX_10_EXP__=4932";
717  command+=" -D__DBL_EPSILON__=2.2204460492503131e-16";
718  command+=" -D__GNUC_PATCHLEVEL__=1";
719  command+=" -D__LDBL_HAS_INFINITY__=1";
720  command+=" -D__INTMAX_MAX__=9223372036854775807L";
721  command+=" -D__FLT_DENORM_MIN__=1.40129846e-45F";
722  command+=" -D__PIC__=2";
723  command+=" -D__FLT_MAX__=3.40282347e+38F";
724  command+=" -D__FLT_MIN_10_EXP__=\"(-37)\"";
725  command+=" -D__DEC128_MAX_EXP__=6144";
726  command+=" -D__GNUC_MINOR__=2";
727  command+=" -D__DBL_MAX_10_EXP__=308";
728  command+=" -D__LDBL_DENORM_MIN__=3.64519953188247460253e-4951L";
729  command+=" -D__DEC128_MANT_DIG__=34";
730  command+=" -D__LDBL_MIN_10_EXP__=\"(-4931)\"";
731 
733  {
734  command+=" -D_Noreturn=\"__attribute__((__noreturn__))\"";
735  command+=" -D__llvm__";
736  command+=" -D__clang__";
737  }
738 
739  if(config.ansi_c.int_width==16)
740  command+=GCC_DEFINES_16;
741  else if(config.ansi_c.int_width==32)
742  {
743  if(config.ansi_c.pointer_width==64)
744  {
746  command+=GCC_DEFINES_LLP64; // Windows, for instance
747  else
748  command+=GCC_DEFINES_LP64;
749  }
750  else
751  command+=GCC_DEFINES_32;
752  }
753 
754  // The width of wchar_t depends on the OS!
755  {
756  command+=" -D__WCHAR_MAX__="+type_max(wchar_t_type());
757 
758  std::string sig=config.ansi_c.wchar_t_is_unsigned?"unsigned":"signed";
759 
761  command+=" -D__WCHAR_TYPE__=\""+sig+" short int\"";
763  command+=" -D__WCHAR_TYPE__=\""+sig+" int\"";
765  command+=" -D__WCHAR_TYPE__=\""+sig+" long int\"";
767  command+=" -D__WCHAR_TYPE__=\""+sig+" char\"";
768  else
769  assert(false);
770  }
771 
773  command+=" -D __CHAR_UNSIGNED__"; // gcc
774 
775  switch(config.ansi_c.os)
776  {
778  command+=" -Dlinux -D__linux -D__linux__ -D__gnu_linux__";
779  command+=" -Dunix -D__unix -D__unix__";
780  command+=" -D__USE_UNIX98";
781  break;
782 
784  command+=" -D__APPLE__ -D__MACH__";
785  // needs to be __APPLE_CPP__ for C++
786  command+=" -D__APPLE_CC__";
787  break;
788 
790  command+=" -D _WIN32";
791 
793  command+=" -D _M_IX86=Blend";
794 
795  if(config.ansi_c.arch=="x86_64")
796  command+=" -D _WIN64"; // yes, both _WIN32 and _WIN64 get defined
797 
799  command+=" -D _CHAR_UNSIGNED"; // This is Visual Studio
800  break;
801 
803  command+=" -nostdinc"; // make sure we don't mess with the system library
804  break;
805 
806  default:
807  assert(false);
808  }
809 
810  // Standard Defines, ANSI9899 6.10.8
811  switch(config.ansi_c.c_standard)
812  {
814  break; // __STDC_VERSION__ is not defined
815 
817  command += " -D __STDC_VERSION__=199901L";
818  break;
819 
821  command += " -D __STDC_VERSION__=201112L";
822  break;
823  }
824 
825  command += " -D __STDC_IEC_559__=1";
826  command += " -D __STDC_IEC_559_COMPLEX__=1";
827  command += " -D __STDC_ISO_10646__=1";
828 
829  for(const auto &define : config.ansi_c.defines)
830  command+=" -D"+shell_quote(define);
831 
832  for(const auto &include_path : config.ansi_c.include_paths)
833  command+=" -I"+shell_quote(include_path);
834 
835  for(const auto &include_file : config.ansi_c.include_files)
836  command+=" -include "+shell_quote(include_file);
837 
838  for(const auto &opt : config.ansi_c.preprocessor_options)
839  command+=" "+opt;
840 
841  int result;
842 
843  #if 0
844  // the following forces the mode
845  switch(config.ansi_c.mode)
846  {
847  case configt::ansi_ct::flavourt::GCC_C: command+=" -x c"; break;
848  case configt::ansi_ct::flavourt::GCC_CPP: command+=" -x c++"; break;
849  default:
850  {
851  }
852  }
853  #endif
854 
855  #ifdef _WIN32
856  std::string tmpi=get_temporary_file("tmp.gcc", "");
857  command+=" \""+file+"\"";
858  command+=" -o \""+tmpi+"\"";
859  command+=" 2> \""+stderr_file+"\"";
860 
861  // _popen isn't very reliable on WIN32
862  // that's why we use system() and a temporary file
863  result=system(command.c_str());
864 
865  std::ifstream instream(tmpi);
866 
867  // errors/warnings
868  std::ifstream stderr_stream(stderr_file);
869  error_parse(stderr_stream, result==0, message);
870 
871  unlink(stderr_file.c_str());
872 
873  if(instream)
874  {
875  outstream << instream.rdbuf();
876  instream.close();
877  unlink(tmpi.c_str());
878  }
879  else
880  {
881  unlink(tmpi.c_str());
882  message.error() << "GCC preprocessing failed (open failed)"
883  << messaget::eom;
884  result=1;
885  }
886  #else
887  command+=" \""+file+"\"";
888  command+=" 2> \""+stderr_file+"\"";
889 
890  FILE *stream=popen(command.c_str(), "r");
891 
892  if(stream!=nullptr)
893  {
894  int ch;
895  while((ch=fgetc(stream))!=EOF)
896  outstream << (unsigned char)ch;
897 
898  result=pclose(stream);
899  }
900  else
901  {
902  message.error() << "GCC preprocessing failed (popen failed)"
903  << messaget::eom;
904  result=1;
905  }
906 
907  // errors/warnings
908  std::ifstream stderr_stream(stderr_file);
909  error_parse(stderr_stream, result==0, message);
910 
911  unlink(stderr_file.c_str());
912 
913  #endif
914 
915  if(result!=0)
916  {
917  message.error() << "GCC preprocessing failed" << messaget::eom;
918  return true;
919  }
920 
921  return false;
922 }
923 
926  const std::string &file,
927  std::ostream &outstream,
928  message_handlert &message_handler)
929 {
930  // check extension
931  if(is_dot_i_file(file))
932  return c_preprocess_none(file, outstream, message_handler);
933 
934  // preprocessing using armcc
935  messaget message(message_handler);
936 
937  std::string stderr_file=get_temporary_file("tmp.stderr", "");
938 
939  std::string command;
940 
941  command="armcc -E -D__CPROVER__";
942 
943 // command+=" -D__sizeof_int="+std::to_string(config.ansi_c.int_width/8);
944 // command+=" -D__sizeof_long="+std::to_string(config.ansi_c.long_int_width/8);
945 // command+=" -D__sizeof_ptr="+std::to_string(config.ansi_c.pointer_width/8);
946  // command+=" -D__EDG_VERSION__=308";
947  // command+=" -D__EDG__";
948 // command+=" -D__CC_ARM=1";
949  // command+=" -D__ARMCC_VERSION=410000";
950 // command+=" -D__arm__";
951 
952 // if(config.ansi_c.endianness==configt::ansi_ct::IS_BIG_ENDIAN)
953 // command+=" -D__BIG_ENDIAN";
954 
955 // if(config.ansi_c.char_is_unsigned)
956 // command+=" -D__CHAR_UNSIGNED__";
957 
959  {
960  command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
961 
962  if(config.ansi_c.int_width==16)
963  command+=GCC_DEFINES_16;
964  else if(config.ansi_c.int_width==32)
965  command+=GCC_DEFINES_32;
966  else if(config.ansi_c.int_width==64)
967  command+=GCC_DEFINES_LP64;
968  }
969 
970  // Standard Defines, ANSI9899 6.10.8
971  command+=" -D__STDC__";
972  // command+=" -D__STDC_VERSION__=199901L";
973 
974  for(const auto &define : config.ansi_c.defines)
975  command+=" "+shell_quote("-D"+define);
976 
977  for(const auto &include_path : config.ansi_c.include_paths)
978  command+=" "+shell_quote("-I"+include_path);
979 
980  int result;
981 
982  #ifdef _WIN32
983  std::string tmpi=get_temporary_file("tmp.cl", "");
984  command+=" \""+file+"\"";
985  command+=" > \""+tmpi+"\"";
986  command+=" 2> \""+stderr_file+"\"";
987 
988  // _popen isn't very reliable on WIN32
989  // that's why we use system() and a temporary file
990  result=system(command.c_str());
991 
992  std::ifstream instream(tmpi);
993 
994  if(!instream)
995  {
996  outstream << instream.rdbuf(); // copy
997  instream.close();
998  unlink(tmpi.c_str());
999  }
1000  else
1001  {
1002  unlink(tmpi.c_str());
1003  unlink(stderr_file.c_str());
1004  message.error() << "ARMCC preprocessing failed (fopen failed)"
1005  << messaget::eom;
1006  return true;
1007  }
1008  #else
1009  command+=" \""+file+"\"";
1010  command+=" 2> \""+stderr_file+"\"";
1011 
1012  FILE *stream=popen(command.c_str(), "r");
1013 
1014  if(stream!=nullptr)
1015  {
1016  int ch;
1017  while((ch=fgetc(stream))!=EOF)
1018  outstream << (unsigned char)ch;
1019 
1020  result=pclose(stream);
1021  }
1022  else
1023  {
1024  unlink(stderr_file.c_str());
1025  message.error() << "ARMCC preprocessing failed (popen failed)"
1026  << messaget::eom;
1027  return true;
1028  }
1029  #endif
1030 
1031  // errors/warnings
1032  std::ifstream stderr_stream(stderr_file);
1033  error_parse(stderr_stream, result==0, message);
1034 
1035  unlink(stderr_file.c_str());
1036 
1037  if(result!=0)
1038  {
1039  message.error() << "ARMCC preprocessing failed" << messaget::eom;
1040  return true;
1041  }
1042 
1043  return false;
1044 }
1045 
1048  const std::string &file,
1049  std::ostream &outstream,
1050  message_handlert &message_handler)
1051 {
1052  #ifdef _MSC_VER
1053  std::ifstream infile(widen(file));
1054  #else
1055  std::ifstream infile(file);
1056  #endif
1057 
1058  if(!infile)
1059  {
1060  messaget message(message_handler);
1061  message.error() << "failed to open `" << file << "'" << messaget::eom;
1062  return true;
1063  }
1064 
1066  {
1067  // special treatment for "/* #line"
1068  postprocess_codewarrior(infile, outstream);
1069  }
1070  else
1071  {
1072  char ch;
1073 
1074  while(infile.read(&ch, 1))
1075  outstream << ch;
1076  }
1077 
1078  return false;
1079 }
1080 
1082 const char c_test_program[]=
1083  "#include <stdlib.h>\n"
1084  "\n"
1085  "int main() { }\n";
1086 
1088 {
1089  std::ostringstream out;
1090  std::istringstream in(c_test_program);
1091 
1092  return c_preprocess(in, out, message_handler);
1093 }
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
bool c_preprocess_visual_studio(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
struct configt::ansi_ct ansi_c
void set_function(const irep_idt &function)
bool c_preprocess_codewarrior(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
unsigned int_width
Definition: config.h:30
#define GCC_DEFINES_16
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
std::wstring widen(const char *s)
Definition: unicode.cpp:56
static std::string shell_quote(const std::string &src)
quote a string for bash and CMD
std::list< std::string > defines
Definition: config.h:111
unsigned short_int_width
Definition: config.h:34
unsigned char_width
Definition: config.h:33
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
preprocessort preprocessor
Definition: config.h:109
unsigned wchar_t_width
Definition: config.h:40
const irep_idt & id() const
Definition: irep.h:189
std::list< std::string > include_files
Definition: config.h:115
bool c_preprocess_gcc_clang(const std::string &, std::ostream &, message_handlert &, configt::ansi_ct::preprocessort)
ANSI-C preprocessing.
flavourt mode
Definition: config.h:105
static bool is_dot_i_file(const std::string &path)
ANSI-C preprocessing.
source_locationt source_location
Definition: message.h:175
void set_file(const irep_idt &file)
#define GCC_DEFINES_LP64
bool c_preprocess_arm(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
void set_line(const irep_idt &line)
irep_idt arch
Definition: config.h:83
void set_column(const irep_idt &column)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
bool char_is_unsigned
Definition: config.h:43
void postprocess_codewarrior(std::istream &instream, std::ostream &outstream)
post-processing specifically for CodeWarrior
static std::string type_max(const typet &src)
produce a string with the maximum value of a given type
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
enum configt::ansi_ct::c_standardt c_standard
bool test_c_preprocessor(message_handlert &message_handler)
bitvector_typet wchar_t_type()
Definition: c_types.cpp:148
const char c_test_program[]
tests ANSI-C preprocessing
API to type classes.
static void error_parse(std::istream &errors, bool warning_only, messaget &message)
#define GCC_DEFINES_LLP64
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
Definition: tempfile.cpp:87
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
static void error_parse_line(const std::string &line, bool warning_only, messaget &message)
mstreamt & error()
Definition: message.h:223
unsigned long_int_width
Definition: config.h:31
bool wchar_t_is_unsigned
Definition: config.h:43
unsigned pointer_width
Definition: config.h:36
std::list< std::string > preprocessor_options
Definition: config.h:113
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
#define GCC_DEFINES_32
bool c_preprocess_none(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
std::list< std::string > include_paths
Definition: config.h:114
Definition: kdev_t.h:19