CBMC
Loading...
Searching...
No Matches
json_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JSON symbol deserialization
4
5Author: Chris Smowton, chris.smowton@diffblue.com
6
7\*******************************************************************/
8
9#include "json_symbol.h"
10
12#include <util/expr.h>
13#include <util/json_irep.h>
15#include <util/type.h>
16
21static const std::string &
22try_get_string(const jsont &in, const std::string &key)
23{
24 if(!in.is_string())
26 "symbol_from_json: expected string for key '" + key + "'");
27 return in.value;
28}
29
34static bool try_get_bool(const jsont &in, const std::string &key)
35{
36 if(!(in.is_true() || in.is_false()))
38 "symbol_from_json: expected bool for key '" + key + "'");
39 return in.is_true();
40}
41
46{
47 if(!in.is_object())
48 throw deserialization_exceptiont("symbol_from_json takes an object");
49 symbolt result;
51 for(const auto &kv : to_json_object(in))
52 {
53 if(kv.first == "type")
54 {
55 irept irep = json2irep.convert_from_json(kv.second);
56 result.type = static_cast<typet &>(irep);
57 }
58 else if(kv.first == "value")
59 {
60 irept irep = json2irep.convert_from_json(kv.second);
61 result.value = static_cast<exprt &>(irep);
62 }
63 else if(kv.first == "location")
64 {
65 irept irep = json2irep.convert_from_json(kv.second);
66 result.location = static_cast<source_locationt &>(irep);
67 }
68 else if(kv.first == "name")
69 result.name = try_get_string(kv.second, "name");
70 else if(kv.first == "module")
71 result.module = try_get_string(kv.second, "module");
72 else if(kv.first == "baseName")
73 result.base_name = try_get_string(kv.second, "baseName");
74 else if(kv.first == "mode")
75 result.mode = try_get_string(kv.second, "mode");
76 else if(kv.first == "prettyName")
77 result.pretty_name = try_get_string(kv.second, "prettyName");
78 else if(kv.first == "isType")
79 result.is_type = try_get_bool(kv.second, "isType");
80 else if(kv.first == "isMacro")
81 result.is_macro = try_get_bool(kv.second, "isMacro");
82 else if(kv.first == "isExported")
83 result.is_exported = try_get_bool(kv.second, "isExported");
84 else if(kv.first == "isInput")
85 result.is_input = try_get_bool(kv.second, "isInput");
86 else if(kv.first == "isOutput")
87 result.is_output = try_get_bool(kv.second, "isOutput");
88 else if(kv.first == "isStateVar")
89 result.is_state_var = try_get_bool(kv.second, "isStateVar");
90 else if(kv.first == "isProperty")
91 result.is_property = try_get_bool(kv.second, "isProperty");
92 else if(kv.first == "isStaticLifetime")
93 result.is_static_lifetime = try_get_bool(kv.second, "isStaticLifetime");
94 else if(kv.first == "isThreadLocal")
95 result.is_thread_local = try_get_bool(kv.second, "isThreadLocal");
96 else if(kv.first == "isLvalue")
97 result.is_lvalue = try_get_bool(kv.second, "isLvalue");
98 else if(kv.first == "isFileLocal")
99 result.is_file_local = try_get_bool(kv.second, "isFileLocal");
100 else if(kv.first == "isExtern")
101 result.is_extern = try_get_bool(kv.second, "isExtern");
102 else if(kv.first == "isVolatile")
103 result.is_volatile = try_get_bool(kv.second, "isVolatile");
104 else if(kv.first == "isParameter")
105 result.is_parameter = try_get_bool(kv.second, "isParameter");
106 else if(kv.first == "isAuxiliary")
107 result.is_auxiliary = try_get_bool(kv.second, "isAuxiliary");
108 else if(kv.first == "isWeak")
109 result.is_weak = try_get_bool(kv.second, "isWeak");
110 else if(kv.first == "prettyType")
111 {
112 } // ignore
113 else if(kv.first == "prettyValue")
114 {
115 } // ignore
116 else
118 "symbol_from_json: unexpected key '" + kv.first + "'");
119 }
120
121 return result;
122}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Base class for all expressions.
Definition expr.h:56
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
Definition json.h:27
bool is_false() const
Definition json.h:76
std::string value
Definition json.h:132
bool is_string() const
Definition json.h:46
bool is_true() const
Definition json.h:71
bool is_object() const
Definition json.h:56
Symbol table entry.
Definition symbol.h:28
bool is_auxiliary
Definition symbol.h:77
bool is_volatile
Definition symbol.h:75
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_file_local
Definition symbol.h:73
bool is_static_lifetime
Definition symbol.h:70
bool is_property
Definition symbol.h:67
bool is_parameter
Definition symbol.h:76
bool is_thread_local
Definition symbol.h:71
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
bool is_state_var
Definition symbol.h:66
bool is_output
Definition symbol.h:65
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:78
irep_idt name
The unique identifier.
Definition symbol.h:40
bool is_exported
Definition symbol.h:63
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
bool is_lvalue
Definition symbol.h:72
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
bool is_input
Definition symbol.h:64
The type of an expression, extends irept.
Definition type.h:29
json_objectt & to_json_object(jsont &json)
Definition json.h:442
static bool try_get_bool(const jsont &in, const std::string &key)
Return boolean value for a given key if present in the json object.
symbolt symbol_from_json(const jsont &in)
Deserialise a json object to a symbolt.
static const std::string & try_get_string(const jsont &in, const std::string &key)
Return string value for a given key if present in the json object.
Defines typet, type_with_subtypet and type_with_subtypest.