CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
lispirep.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#include "lispirep.h"
11
12#include "irep.h"
13#include "lispexpr.h"
14
15void lisp2irep(const lispexprt &src, irept &dest)
16{
17 dest.make_nil();
18
19 if(src.type!=lispexprt::List || src.empty())
20 return;
21
22 dest.id(src[0].value);
23
24 for(std::size_t i=1; i<src.size(); i++)
25 if(!src[i].is_nil())
26 {
27 const std::string &name=src[i].value;
28 i++;
29
30 if(i<src.size())
31 {
32 irept sub;
33 lisp2irep(src[i], sub);
34
35 if(name.empty())
36 dest.move_to_sub(sub);
37 else
38 dest.move_to_named_sub(name, sub);
39 }
40 }
41}
42
43void irep2lisp(const irept &src, lispexprt &dest)
44{
45 dest.clear();
46 dest.value.clear();
48
49 const std::size_t named_sub_size = src.get_named_sub().size();
50 dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);
51
52 lispexprt id;
54 id.value=src.id_string();
55 dest.push_back(id);
56
57 // reserve objects for extra performance
58
59 for(const auto &irep : src.get_sub())
60 {
61 lispexprt name;
63 name.value.clear();
64 dest.push_back(name);
65
66 lispexprt sub;
67
68 irep2lisp(irep, sub);
69 dest.push_back(sub);
70 }
71
72 for(const auto &irep_entry : src.get_named_sub())
73 {
74 lispexprt name;
76 name.value = id2string(irep_entry.first);
77 dest.push_back(name);
78
79 lispexprt sub;
80
81 irep2lisp(irep_entry.second, sub);
82 dest.push_back(sub);
83 }
84
85 lispexprt nil;
87 nil.value="nil";
88
89 dest.push_back(nil);
90}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
void move_to_named_sub(const irep_idt &name, irept &irep)
Definition irep.cpp:26
const std::string & id_string() const
Definition irep.h:391
subt & get_sub()
Definition irep.h:448
void make_nil()
Definition irep.h:446
void move_to_sub(irept &irep)
Definition irep.cpp:35
const irep_idt & id() const
Definition irep.h:388
named_subt & get_named_sub()
Definition irep.h:450
lispsymbolt value
Definition lispexpr.h:77
enum lispexprt::@7 type
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
void lisp2irep(const lispexprt &src, irept &dest)
Definition lispirep.cpp:15
void irep2lisp(const irept &src, lispexprt &dest)
Definition lispirep.cpp:43