CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
converter.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include <fstream> // IWYU pragma: keep
10#include <iostream>
11#include <string>
12
13bool has_prefix(const std::string &s, const std::string &prefix)
14{
15 return std::string(s, 0, prefix.size())==prefix;
16}
17
18static void convert_line(const std::string &line, bool first)
19{
20 if(has_prefix(line, "/* FUNCTION: "))
21 {
22 if(!first)
23 std::cout << "},\n";
24
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);
29
30 std::cout << "{ \"" << function << "\",\n";
31 std::cout << " \"#line 1 \\\"<builtin-library-" << function
32 << ">\\\"\\n\"\n";
33 }
34 else if(!first)
35 {
36 std::cout << " \"";
37
38 for(unsigned i = 0; i < line.size(); i++)
39 {
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 }
48 else
49 std::cout << ch;
50 }
51
52 std::cout << "\\n\"\n";
53 }
54}
55
56int main(int argc, char *argv[])
57{
58 std::string line;
59 bool first = true;
60
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 }
72
73 while(getline(input_file, line))
74 {
75 convert_line(line, first);
76 first = false;
77 }
78 }
79
80 if(!first)
81 std::cout << "},\n";
82
83 std::cout <<
84 "{ 0, 0 }\n"
85 "}";
86
87 return 0;
88}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
static void convert_line(const std::string &line, bool first)
Definition converter.cpp:18
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
int main()
Definition example.cpp:18
literalt pos(literalt a)
Definition literal.h:194