You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
"Stub" function calls are used to provide a simplified semantics for functions where: we don't have semantics for (i.e. they are from dynamically-linked libraries), the semantics are too complicated to reason about directly, or we want to represent as an observable event in the program trace.
Currently these are implemented as haskell functions that simply perform arbitrary modifications to the program state. This is a bit clumsy to manage, however, as it means that they need to be handled explicitly during verification, rather than implicitly during symbolic execution.
Ideally, these stubs should be implemented as crucible overrides, so their semantics are automatically included as part of any block, and so that they can be standardized between normal symbolic execution and symbolic execution during "Inline Callee"
The text was updated successfully, but these errors were encountered:
"Stub" function calls are used to provide a simplified semantics for functions where: we don't have semantics for (i.e. they are from dynamically-linked libraries), the semantics are too complicated to reason about directly, or we want to represent as an observable event in the program trace.
Currently these are implemented as haskell functions that simply perform arbitrary modifications to the program state. This is a bit clumsy to manage, however, as it means that they need to be handled explicitly during verification, rather than implicitly during symbolic execution.
Ideally, these stubs should be implemented as crucible overrides, so their semantics are automatically included as part of any block, and so that they can be standardized between normal symbolic execution and symbolic execution during "Inline Callee"
The text was updated successfully, but these errors were encountered: