Skip to content

Commit 49526f7

Browse files
Replace asserts
1 parent df5aa96 commit 49526f7

File tree

1 file changed

+7
-4
lines changed

1 file changed

+7
-4
lines changed

src/goto-programs/json_goto_trace.cpp

+7-4
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,10 @@ Author: Daniel Kroening
1313

1414
#include "json_goto_trace.h"
1515

16-
#include <cassert>
17-
1816
#include <util/json_expr.h>
1917
#include <util/arith_tools.h>
2018
#include <util/config.h>
19+
#include <util/invariant.h>
2120

2221
#include <langapi/language_util.h>
2322

@@ -194,7 +193,9 @@ void convert(
194193
std::string value_string, binary_string, type_string, full_lhs_string;
195194
json_objectt full_lhs_value;
196195

197-
assert(step.full_lhs.is_not_nil());
196+
DATA_INVARIANT(
197+
step.full_lhs.is_not_nil(),
198+
"full_lhs in assignment must not be nil");
198199
exprt simplified=simplify_array_access(step.full_lhs);
199200
full_lhs_string=from_expr(ns, identifier, simplified);
200201

@@ -214,7 +215,9 @@ void convert(
214215
}
215216
else
216217
{
217-
assert(step.full_lhs_value.is_not_nil());
218+
DATA_INVARIANT(
219+
step.full_lhs_value.is_not_nil(),
220+
"full_lhs_value in assignment must not be nil");
218221
full_lhs_value=json(step.full_lhs_value, ns);
219222
}
220223

0 commit comments

Comments
 (0)