Skip to content

Commit f295ed8

Browse files
committed
Move {json,xml}(source_locationt) to {json,xml}_irep.{h,cpp}
This prepares the move of {json,xml}_expr.{h,cpp} to goto-programs to remove the dependency of util on langapi.
1 parent 387834c commit f295ed8

28 files changed

+88
-104
lines changed

src/analyses/custom_bitvector_analysis.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/expr_util.h>
1515
#include <util/simplify_expr.h>
1616
#include <util/string_constant.h>
17-
#include <util/xml_expr.h>
17+
#include <util/xml_irep.h>
1818

1919
#include <langapi/language_util.h>
2020

src/analyses/dependence_graph.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,7 @@ Date: August 2013
1717
#include <cassert>
1818

1919
#include <util/container_utils.h>
20-
#include <util/json.h>
21-
#include <util/json_expr.h>
20+
#include <util/json_irep.h>
2221

2322
#include "goto_rw.h"
2423

src/cbmc/bmc_cover.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,11 @@ Author: Daniel Kroening, [email protected]
1616

1717
#include <goto-checker/bmc_util.h>
1818

19-
#include <util/xml.h>
20-
#include <util/xml_expr.h>
2119
#include <util/json.h>
22-
#include <util/json_stream.h>
2320
#include <util/json_expr.h>
21+
#include <util/json_stream.h>
22+
#include <util/xml_expr.h>
23+
#include <util/xml_irep.h>
2424

2525
#include <solvers/prop/cover_goals.h>
2626
#include <solvers/prop/literal_expr.h>

src/cbmc/fault_localization.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,12 @@ Author: Peter Schrammel
1313

1414
#include <chrono>
1515

16-
#include <util/threeval.h>
1716
#include <util/arith_tools.h>
18-
#include <util/symbol.h>
19-
#include <util/std_expr.h>
2017
#include <util/message.h>
21-
#include <util/xml_expr.h>
18+
#include <util/std_expr.h>
19+
#include <util/symbol.h>
20+
#include <util/threeval.h>
21+
#include <util/xml_irep.h>
2222

2323
#include <solvers/prop/minimize.h>
2424
#include <solvers/prop/literal_expr.h>

src/goto-analyzer/static_verifier.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ Author: Martin Brain, [email protected]
88

99
#include "static_verifier.h"
1010

11-
#include <util/json_expr.h>
11+
#include <util/json_irep.h>
1212
#include <util/message.h>
1313
#include <util/namespace.h>
1414
#include <util/options.h>

src/goto-analyzer/unreachable_instructions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Date: April 2016
1414
#include "unreachable_instructions.h"
1515

1616
#include <util/file_util.h>
17-
#include <util/json_expr.h>
17+
#include <util/json_irep.h>
1818
#include <util/options.h>
1919
#include <util/xml.h>
2020

src/goto-diff/goto_diff_base.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Author: Peter Schrammel
1111

1212
#include "goto_diff.h"
1313

14-
#include <util/json_expr.h>
14+
#include <util/json_irep.h>
1515
#include <util/options.h>
1616

1717
#include <goto-programs/goto_model.h>

src/goto-instrument/unwind.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
1616
#include "unwindset.h"
1717

1818
#include <util/json.h>
19-
#include <util/json_expr.h>
2019
#include <goto-programs/goto_model.h>
2120

2221
class goto_modelt;

src/goto-programs/goto_inline_class.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/message.h>
1616
#include <util/json.h>
17-
#include <util/json_expr.h>
1817

1918
#include "goto_functions.h"
2019

src/goto-programs/json_goto_trace.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,12 @@ Author: Daniel Kroening
1414
#include "json_goto_trace.h"
1515
#include "goto_trace.h"
1616

17-
#include <util/json_expr.h>
18-
#include <util/json.h>
19-
#include <util/json_stream.h>
17+
#include <langapi/language_util.h>
2018
#include <util/arith_tools.h>
2119
#include <util/config.h>
2220
#include <util/invariant.h>
21+
#include <util/json_expr.h>
2322
#include <util/simplify_expr.h>
24-
#include <util/json_irep.h>
25-
#include <langapi/language_util.h>
2623

2724
/// Convert an ASSERT goto_trace step.
2825
/// \param [out] json_failure: The JSON object that

src/goto-programs/json_goto_trace.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,10 @@ Date: November 2005
1616

1717
#include "goto_trace.h"
1818

19+
#include <util/invariant.h>
1920
#include <util/json.h>
21+
#include <util/json_irep.h>
2022
#include <util/json_stream.h>
21-
#include <util/json_expr.h>
22-
#include <util/invariant.h>
2323

2424
/// This is structure is here to facilitate
2525
/// passing arguments to the conversion

src/goto-programs/loop_ids.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <iostream>
1515

16-
#include <util/xml.h>
17-
#include <util/xml_expr.h>
18-
#include <util/json.h>
19-
#include <util/json_expr.h>
16+
#include <util/json_irep.h>
17+
#include <util/xml_irep.h>
2018

2119
void show_loop_ids(
2220
ui_message_handlert::uit ui,

src/goto-programs/show_goto_functions.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,6 @@ Author: Peter Schrammel
1313

1414
#include <util/xml.h>
1515
#include <util/json.h>
16-
#include <util/json_expr.h>
17-
#include <util/xml_expr.h>
1816
#include <util/cprover_prefix.h>
1917
#include <util/prefix.h>
2018

src/goto-programs/show_goto_functions_json.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Thomas Kiley
1414
#include <iostream>
1515
#include <sstream>
1616

17-
#include <util/json_expr.h>
1817
#include <util/json_irep.h>
1918
#include <util/cprover_prefix.h>
2019
#include <util/prefix.h>

src/goto-programs/show_goto_functions_xml.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ Author: Thomas Kiley
1414
#include <iostream>
1515
#include <sstream>
1616

17-
#include <util/xml_expr.h>
1817
#include <util/cprover_prefix.h>
1918
#include <util/prefix.h>
19+
#include <util/xml_irep.h>
2020

2121
#include <langapi/language_util.h>
2222

src/goto-programs/show_properties.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <iostream>
1515

16-
#include <util/xml.h>
17-
#include <util/xml_expr.h>
18-
#include <util/json.h>
19-
#include <util/json_expr.h>
16+
#include <util/json_irep.h>
17+
#include <util/xml_irep.h>
2018

2119
#include <langapi/language_util.h>
2220

src/goto-programs/xml_goto_trace.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,9 @@ Author: Daniel Kroening
1515

1616
#include <cassert>
1717

18-
#include <util/xml_expr.h>
1918
#include <util/symbol.h>
19+
#include <util/xml_expr.h>
20+
#include <util/xml_irep.h>
2021

2122
#include <langapi/language_util.h>
2223

src/goto-symex/show_vcc.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,7 @@ Author: Daniel Kroening, [email protected]
2020

2121
#include <util/exception_utils.h>
2222
#include <util/format_expr.h>
23-
#include <util/json.h>
24-
#include <util/json_expr.h>
23+
#include <util/json_irep.h>
2524
#include <util/ui_message.h>
2625

2726
void show_vcc_plain(

src/pointer-analysis/value_set_analysis.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,9 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "value_set_analysis.h"
1313

14-
#include <util/prefix.h>
1514
#include <util/cprover_prefix.h>
16-
#include <util/xml_expr.h>
17-
#include <util/xml.h>
15+
#include <util/prefix.h>
16+
#include <util/xml_irep.h>
1817

1918
#include <langapi/language_util.h>
2019

src/util/json_expr.cpp

Lines changed: 0 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -84,31 +84,6 @@ static exprt simplify_json_expr(
8484
return src;
8585
}
8686

87-
json_objectt json(const source_locationt &location)
88-
{
89-
json_objectt result;
90-
91-
if(!location.get_working_directory().empty())
92-
result["workingDirectory"] = json_stringt(location.get_working_directory());
93-
94-
if(!location.get_file().empty())
95-
result["file"] = json_stringt(location.get_file());
96-
97-
if(!location.get_line().empty())
98-
result["line"] = json_stringt(location.get_line());
99-
100-
if(!location.get_column().empty())
101-
result["column"] = json_stringt(location.get_column());
102-
103-
if(!location.get_function().empty())
104-
result["function"] = json_stringt(location.get_function());
105-
106-
if(!location.get_java_bytecode_index().empty())
107-
result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
108-
109-
return result;
110-
}
111-
11287
/// Output a CBMC type in json.
11388
/// The `mode` argument is used to correctly report types.
11489
/// \param type: a type

src/util/json_expr.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Peter Schrammel
1515
#include "json.h"
1616
#include "irep.h"
1717

18-
class source_locationt;
1918
class typet;
2019
class exprt;
2120
class namespacet;
@@ -30,6 +29,4 @@ json_objectt json(
3029
const namespacet &,
3130
const irep_idt &mode);
3231

33-
json_objectt json(const source_locationt &);
34-
3532
#endif // CPROVER_UTIL_JSON_EXPR_H

src/util/json_irep.cpp

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,3 +137,28 @@ irept json_irept::convert_from_json(const jsont &in) const
137137

138138
return out;
139139
}
140+
141+
json_objectt json(const source_locationt &location)
142+
{
143+
json_objectt result;
144+
145+
if(!location.get_working_directory().empty())
146+
result["workingDirectory"] = json_stringt(location.get_working_directory());
147+
148+
if(!location.get_file().empty())
149+
result["file"] = json_stringt(location.get_file());
150+
151+
if(!location.get_line().empty())
152+
result["line"] = json_stringt(location.get_line());
153+
154+
if(!location.get_column().empty())
155+
result["column"] = json_stringt(location.get_column());
156+
157+
if(!location.get_function().empty())
158+
result["function"] = json_stringt(location.get_function());
159+
160+
if(!location.get_java_bytecode_index().empty())
161+
result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
162+
163+
return result;
164+
}

src/util/json_irep.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ Author: Thomas Kiley, [email protected]
1313
#define CPROVER_UTIL_JSON_IREP_H
1414

1515
#include "irep.h"
16+
#include "json.h"
1617

17-
class jsont;
18-
class json_objectt;
18+
class source_locationt;
1919

2020
class json_irept
2121
{
@@ -38,4 +38,6 @@ class json_irept
3838
bool include_comments;
3939
};
4040

41+
json_objectt json(const source_locationt &);
42+
4143
#endif // CPROVER_UTIL_JSON_IREP_H

src/util/ui_message.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,10 @@ Author: Daniel Kroening, [email protected]
1212
#include <iostream>
1313

1414
#include "cmdline.h"
15-
#include "json.h"
16-
#include "json_expr.h"
15+
#include "json_irep.h"
1716
#include "json_stream.h"
1817
#include "make_unique.h"
19-
#include "xml.h"
20-
#include "xml_expr.h"
18+
#include "xml_irep.h"
2119

2220
ui_message_handlert::ui_message_handlert(
2321
message_handlert *_message_handler,

src/util/xml_expr.cpp

Lines changed: 0 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -23,31 +23,6 @@ Author: Daniel Kroening
2323
#include "std_expr.h"
2424
#include "xml.h"
2525

26-
xmlt xml(const source_locationt &location)
27-
{
28-
xmlt result;
29-
30-
result.name="location";
31-
32-
if(!location.get_working_directory().empty())
33-
result.set_attribute(
34-
"working-directory", id2string(location.get_working_directory()));
35-
36-
if(!location.get_file().empty())
37-
result.set_attribute("file", id2string(location.get_file()));
38-
39-
if(!location.get_line().empty())
40-
result.set_attribute("line", id2string(location.get_line()));
41-
42-
if(!location.get_column().empty())
43-
result.set_attribute("column", id2string(location.get_column()));
44-
45-
if(!location.get_function().empty())
46-
result.set_attribute("function", id2string(location.get_function()));
47-
48-
return result;
49-
}
50-
5126
xmlt xml(
5227
const typet &type,
5328
const namespacet &ns)

src/util/xml_expr.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include "xml.h"
1414

15-
class source_locationt;
1615
class typet;
1716
class exprt;
1817
class namespacet;
@@ -25,6 +24,4 @@ xmlt xml(
2524
const typet &,
2625
const namespacet &);
2726

28-
xmlt xml(const source_locationt &);
29-
3027
#endif // CPROVER_UTIL_XML_EXPR_H

0 commit comments

Comments
 (0)