Skip to content

Commit 7c76ca9

Browse files
committed
XPR: handle no-offset separately
1 parent e1f6616 commit 7c76ca9

2 files changed

Lines changed: 10 additions & 1 deletion

File tree

chb/app/CHVersion.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
chbversion: str = "0.3.0-20260105"
1+
chbversion: str = "0.3.0-20260122"

chb/invariants/XXprUtil.py

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -449,6 +449,8 @@ def memory_variable_to_lval_expression(
449449
offset = cast("VMemoryOffsetFieldOffset", offset)
450450
astoffset: AST.ASTOffset = field_offset_to_ast_offset(
451451
offset, xdata, iaddr, astree, anonymous=anonymous)
452+
elif offset.is_no_offset:
453+
astoffset = nooffset
452454
elif offset.is_array_index_offset:
453455
offset = cast("VMemoryOffsetArrayIndexOffset", offset)
454456
astoffset = array_offset_to_ast_offset(
@@ -460,6 +462,11 @@ def memory_variable_to_lval_expression(
460462
return astree.mk_memref_expr(
461463
astbase, offset=astoffset, anonymous=anonymous)
462464

465+
elif offset.is_no_offset:
466+
astlval = xvariable_to_ast_def_lval_expression(
467+
base.basevar, xdata, iaddr, astree, anonymous=anonymous)
468+
return astree.mk_memref_expr(astlval, anonymous=anonymous)
469+
463470
elif (
464471
offset.is_field_offset
465472
or offset.is_array_index_offset
@@ -1952,6 +1959,8 @@ def basevar_variable_to_ast_lval(
19521959
offset = cast("VMemoryOffsetArrayIndexOffset", offset)
19531960
astoffset = array_offset_to_ast_offset(
19541961
offset, xdata, iaddr, astree, anonymous=anonymous)
1962+
elif offset.is_no_offset:
1963+
astoffset = nooffset
19551964
elif offset.is_constant_value_offset:
19561965
astoffset = astree.mk_scalar_index_offset(offset.offsetvalue())
19571966
else:

0 commit comments

Comments
 (0)