Skip to content

Commit b854f4c

Browse files
committed
XPR: add support for startof
1 parent 2304753 commit b854f4c

File tree

1 file changed

+7
-1
lines changed

1 file changed

+7
-1
lines changed

chb/invariants/XXprUtil.py

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1372,7 +1372,13 @@ def xmemory_dereference_lval(
13721372
xaddr = xxpr_to_ast_def_expr(address, xdata, iaddr, astree)
13731373
if xaddr.is_ast_binary_op:
13741374
xaddr = cast(AST.ASTBinaryOp, xaddr)
1375-
if xaddr.exp1.is_ast_lval_expr:
1375+
if xaddr.exp1.is_ast_startof:
1376+
xalval = cast(AST.ASTStartOf, xaddr.exp1)
1377+
astoffset = astree.mk_expr_index_offset(xaddr.exp2)
1378+
lvalhost = xalval.lval.lhost
1379+
return astree.mk_lval(lvalhost, astoffset)
1380+
1381+
elif xaddr.exp1.is_ast_lval_expr:
13761382
xlval = cast(AST.ASTLvalExpr, xaddr.exp1)
13771383
xlvaltype = xlval.ctype(astree.ctyper)
13781384
if xlvaltype is not None and xlvaltype.is_array:

0 commit comments

Comments
 (0)