@@ -6,7 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com
66
77\*******************************************************************/
88
9-
9+ # include < fstream >
1010#include < iostream>
1111#include < string>
1212
@@ -15,50 +15,65 @@ bool has_prefix(const std::string &s, const std::string &prefix)
1515 return std::string (s, 0 , prefix.size ())==prefix;
1616}
1717
18- int main ( )
18+ static void convert_line ( const std::string &line, bool first )
1919{
20- std::string line;
21- bool first=true ;
20+ if (has_prefix (line, " /* FUNCTION: " ))
21+ {
22+ if (!first)
23+ std::cout << " },\n " ;
2224
23- std::cout << " {\n " ;
25+ std::string function = std::string (line, 13 , std::string::npos);
26+ std::size_t pos = function.find (' ' );
27+ if (pos != std::string::npos)
28+ function = std::string (function, 0 , pos);
2429
25- while (getline (std::cin, line))
30+ std::cout << " { \" " << function << " \" ,\n " ;
31+ std::cout << " \" #line 1 \\\" <builtin-library-" << function
32+ << " >\\\"\\ n\"\n " ;
33+ }
34+ else if (!first)
2635 {
27- if (has_prefix (line, " /* FUNCTION: " ))
36+ std::cout << " \" " ;
37+
38+ for (unsigned i = 0 ; i < line.size (); i++)
2839 {
29- if (first)
30- first=false ;
40+ const char ch = line[i];
41+ if (ch == ' \\ ' )
42+ std::cout << " \\\\ " ;
43+ else if (ch == ' "' )
44+ std::cout << " \\\" " ;
45+ else if (ch == ' \r ' || ch == ' \n ' )
46+ {
47+ }
3148 else
32- std::cout << " },\n " ;
49+ std::cout << ch;
50+ }
3351
34- std::string function=std::string (line, 13 , std::string::npos);
35- std::size_t pos=function.find (' ' );
36- if (pos!=std::string::npos)
37- function=std::string (function, 0 , pos);
52+ std::cout << " \\ n\"\n " ;
53+ }
54+ }
3855
39- std::cout << " { \" " << function << " \" ,\n " ;
40- std::cout << " \" #line 1 \\\" <builtin-library-"
41- << function << " >\\\"\\ n\"\n " ;
42- }
43- else if (!first)
44- {
45- std::cout << " \" " ;
56+ int main (int argc, char *argv[])
57+ {
58+ std::string line;
59+ bool first = true ;
4660
47- for (unsigned i=0 ; i<line.size (); i++)
48- {
49- const char ch=line[i];
50- if (ch==' \\ ' )
51- std::cout << " \\\\ " ;
52- else if (ch==' "' )
53- std::cout << " \\\" " ;
54- else if (ch==' \r ' || ch==' \n ' )
55- {
56- }
57- else
58- std::cout << ch;
59- }
61+ std::cout << " {\n " ;
62+
63+ for (int i = 1 ; i < argc; ++i)
64+ {
65+ std::ifstream input_file (argv[i]);
66+
67+ if (!input_file)
68+ {
69+ std::cerr << " Failed to open " << argv[i] << ' \n ' ;
70+ return 1 ;
71+ }
6072
61- std::cout << " \\ n\"\n " ;
73+ while (getline (input_file, line))
74+ {
75+ convert_line (line, first);
76+ first = false ;
6277 }
6378 }
6479
@@ -68,4 +83,6 @@ int main()
6883 std::cout <<
6984 " { 0, 0 }\n "
7085 " }" ;
86+
87+ return 0 ;
7188}
0 commit comments