Skip to content

Fix WISL cell creation bug#367

Merged
NatKarmios merged 3 commits into
masterfrom
wisl-cell-creation-bug
May 28, 2026
Merged

Fix WISL cell creation bug#367
NatKarmios merged 3 commits into
masterfrom
wisl-cell-creation-bug

Conversation

@NatKarmios

Copy link
Copy Markdown
Contributor

WISL is currently set to, when executing SetCell/SetBound/SetFreed, create the necessary heap entries if the relevant cell is missing. This makes sense when producing assertions, but causes false negatives when these actions are used directly in programs.

For example, this program succeeds, where one would expect it to fail as there is no cell at x:

{ (x == #x) }
function main(x) {
  [x] := 4;
  return null;
}
{ emp }

This change adds a alloc_if_missing argument to various functions, including WislSMemory.resolve_loc, WislSHeap.set_cell, etc. which specifies whether this behaviour should occur; it is off by default, but enabled inside WislSMemory.produce.

@NatKarmios NatKarmios merged commit 6095a9b into master May 28, 2026
12 checks passed
@NatKarmios NatKarmios deleted the wisl-cell-creation-bug branch May 28, 2026 12:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant