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
The fffuu Haskell tool fails with the error message "undefined" if some precondition of the Isabelle-generated code does not hold. For example, Isabelle assumes that an ipassmt does not have wildcard interface names in it. For safety reasons, the Isabelle-generated code checks preconditions at runtime. If it fails, it just aborts with "undefined". There are many different cases how this undefined can be triggered. It is almost impossible to debug which "undefined" triggered. Feature request: human-readable error messages for each undefined!
The text was updated successfully, but these errors were encountered:
TODOs:
Asses where safe versions of Isabelle-generated functions can be exported without cluttering the code with error handling.
If Isabelle-generated functions are called wrongly, then this is a coding error and an exception is fine. If functions are given an unsupported input at runtime and we need to explain to the user what the error was, we probably want safe functions. What does Isabelle Monad syntax provide?
Functions that should only be exported in their safe version:
The fffuu Haskell tool fails with the error message "undefined" if some precondition of the Isabelle-generated code does not hold. For example, Isabelle assumes that an ipassmt does not have wildcard interface names in it. For safety reasons, the Isabelle-generated code checks preconditions at runtime. If it fails, it just aborts with "undefined". There are many different cases how this undefined can be triggered. It is almost impossible to debug which "undefined" triggered. Feature request: human-readable error messages for each undefined!
The text was updated successfully, but these errors were encountered: