Skip to content

Commit 8ebb169

Browse files
author
Vojtech Forejt
committed
Add source location to JSON output.
Without this commit, the JSON output will miss source locations of messages. Compare the following plaintext output from cbmc: ``` file My.java line 8 function java::My.doIt:()V: no identifier for function parameter ``` with the JSON output for the same input file and parameters ``` { "messageText": "no identifier for function parameter", "messageType": "ERROR" } ``` With this commit, the JSON output will be something like ``` { "messageText": "no identifier for function parameter", "messageType": "ERROR" "sourceLocation": { "bytecodeIndex": "2" "file": "My.java", "function": "java::My.doIt:()V", "line": "8" } } ``` This should make debugging of errors easier.
1 parent 6d1be13 commit 8ebb169

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed

src/memory-models/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ SRC = mm2cpp.cpp \
99
OBJ += ../big-int/big-int$(LIBEXT) \
1010
../ansi-c/ansi-c$(LIBEXT) \
1111
../linking/linking$(LIBEXT) \
12+
../langapi/langapi$(LIBEXT) \
1213
../util/util$(LIBEXT)
1314

1415
INCLUDES= -I ..

src/util/ui_message.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include "xml.h"
1515
#include "json.h"
1616
#include "xml_expr.h"
17+
#include "json_expr.h"
1718
#include "cout_message.h"
1819
#include "cmdline.h"
1920

@@ -219,11 +220,9 @@ void ui_message_handlert::json_ui_msg(
219220

220221
json_objectt result;
221222

222-
#if 0
223223
if(location.is_not_nil() &&
224224
!location.get_file().empty())
225-
result.new_element(xml(location));
226-
#endif
225+
result["sourceLocation"] = json(location);
227226

228227
result["messageType"] = json_stringt(type);
229228
result["messageText"] = json_stringt(msg1);

0 commit comments

Comments
 (0)