Skip to content

Commit dd7db5a

Browse files
author
thk123
committed
Move invariant out of if
The full_lhs_value should have a non-nil value regardless of whether the identifier exists in the namespace.
1 parent 205ec36 commit dd7db5a

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

src/goto-programs/json_goto_trace.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,10 @@ void convert_decl(
118118
const symbolt *symbol;
119119
irep_idt base_name, display_name;
120120

121+
DATA_INVARIANT(
122+
step.full_lhs_value.is_not_nil(),
123+
"full_lhs_value in assignment must not be nil");
124+
121125
if(!ns.lookup(identifier, symbol))
122126
{
123127
base_name = symbol->base_name;
@@ -132,9 +136,6 @@ void convert_decl(
132136
}
133137
else
134138
{
135-
DATA_INVARIANT(
136-
step.full_lhs_value.is_not_nil(),
137-
"full_lhs_value in assignment must not be nil");
138139
full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
139140
}
140141

0 commit comments

Comments
 (0)