search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
628 stars 42 forks source link

Refactor `AssumptionStack` #1169

Closed langston-barrett closed 7 months ago

langston-barrett commented 7 months ago

Towards #1168.

langston-barrett commented 7 months ago

It seems that pushing/popping operations are exposed via IsSymBackend. Ideally, we would only expose operations that automatically enforce the desired matching push/pop condition (basically, just an operation like inFreshFrame). However, I'm not really familiar with the code that uses this API (Lang.Crucible.Backend.Online), and it's not clear to me how feasible it would be to refactor it to fit this pattern. However, I think the current PR is already an improvement, in that it makes it possible to avoid panicing functions in the public API.