UnitTestBot / UnitTestBot/usvm
[TS] Support `push` invocation in `InstanceCallExpr` resolution
Open
@CaelmBleidd is already working on this.
Since Jul 3, 2025.
- Dominant language
- Kotlin
- Stars
- 33
- Forks
- 27
- Avg merge
- 4d 3h
- Merged PRs (30d)
- 15
Description
Current implementation is
// TODO write tests
if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) {
return scope.calcOnState {
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
val lengthLValue = mkArrayLengthLValue(
resolvedInstance,
EtsArrayType(EtsUnknownType, dimensions = 1)
)
val length = memory.read(lengthLValue)
val newLength = mkBvAddExpr(length, 1.toBv())
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
// TODO check sorts compatibility
val newIndexLValue = mkArrayIndexLValue(
resolvedArg.sort,
resolvedInstance,
length,
EtsArrayType(EtsUnknownType, dimensions = 1)
)
memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr)
newLength
}
}
We need to check it and fix if required
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.