-
Notifications
You must be signed in to change notification settings - Fork 62
Issues: GaloisInc/saw-script
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Invalid logic in s2n tls proof
tech debt
Issues that document or involve technical debt
test assets
Issues involving test programs or other test assets
tooling: CI
Issues involving CI/CD scripts or processes
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Make the warnings introduced by #2162 into errors
easy
Issues that are expected to be easy to resolve and might therefore be good for new contributors
tech debt
Issues that document or involve technical debt
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: enhancement
Issues describing an improvement to an existing feature or capability
CI is breaking on archaic downloads
tech debt
Issues that document or involve technical debt
test assets
Issues involving test programs or other test assets
tooling: CI
Issues involving CI/CD scripts or processes
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Cannot embed Cryptol newtypes in let {{ }}
missing cryptol features
Issues about features in Cryptol that don't work in SAW
needs test
Issues for which we should add a regression test
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Builtin vs. hardcoded types
needs test
Issues for which we should add a regression test
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Oddities of top-level binds
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
usability
An issue that impedes efficient understanding and use
write_goal
only writes the last proof goal to a file, unlike other goal-writing proof scripts
subsystem: saw-core
Deprecate llvm_struct()
better-when-documented
Issues whose root causes include missing or wrong documentation
documentation
Issues involving documentation
easy
Issues that are expected to be easy to resolve and might therefore be good for new contributors
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
usability
An issue that impedes efficient understanding and use
saw-script interpreter typechecks one line at a time
needs design
Technical design work is needed for issue to progress
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
SAW User Manual Issues and Recommendations
documentation
Issues involving documentation
type: enhancement
Issues describing an improvement to an existing feature or capability
usability
An issue that impedes efficient understanding and use
Support implications as rewrite rules
subsystem: saw-core
Issues related to the saw-core representation or the saw-core subsystem
type: feature request
Issues requesting a new feature or capability
usability
An issue that impedes efficient understanding and use
#2155
opened Dec 5, 2024 by
mrogers67
MIR Technical design work is needed for issue to progress
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
type: bug
Issues reporting bugs or unexpected/unwanted behavior
bool
arrays are cumbersome to use in SAW
needs design
Reading a static mutable reference crashes with empty mux tree
needs test
Issues for which we should add a regression test
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: bug
Issues reporting bugs or unexpected/unwanted behavior
usability
An issue that impedes efficient understanding and use
Unhelpful empty counterexample
easy
Issues that are expected to be easy to resolve and might therefore be good for new contributors
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: bug
Issues reporting bugs or unexpected/unwanted behavior
usability
An issue that impedes efficient understanding and use
SAW should respond to SIGINFO
topics: error-messages
Issues involving the messages SAW produces on error
type: feature request
Issues requesting a new feature or capability
saw-core position reporting doesn't print correctly
needs test
Issues for which we should add a regression test
topics: error-messages
Issues involving the messages SAW produces on error
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Systematize error-issuing and other printing functions
tech debt
Issues that document or involve technical debt
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: enhancement
Issues describing an improvement to an existing feature or capability
Position tracking by global variable isn't robust
tech debt
Issues that document or involve technical debt
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Signatures not shown on Downloads Page but mentioned
documentation
Issues involving documentation
type: bug
Issues reporting bugs or unexpected/unwanted behavior
usability
An issue that impedes efficient understanding and use
Execution of impossible paths during verification
performance
Issues that involve or include performance problems
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Typechecker gap in mir_assert
needs test
Issues for which we should add a regression test
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: bug
Issues reporting bugs or unexpected/unwanted behavior
usability
An issue that impedes efficient understanding and use
Printing of Cryptol newtypes in counterexamples throws away too much information
subsystem: cryptol-saw-core
Issues related to Cryptol -> saw-core translation with cryptol-saw-core
tech debt
Issues that document or involve technical debt
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
usability
An issue that impedes efficient understanding and use
Better synchronize SAW with the High-priority issues
subproject
Issues involving one of the various subprojects SAW depends on
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
type: bug
Issues reporting bugs or unexpected/unwanted behavior
mir-json
version it depends on
priority
The repository README should mention the docker images
documentation debt
Documentation tasks previously deferred, postponed, etc.; technical debt in documentation
documentation
Issues involving documentation
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Bogus stack trace with MIR verification and wrong return type
needs test
Issues for which we should add a regression test
topics: error-handling
Issues involving the way SAW responds to an error condition
topics: error-messages
Issues involving the messages SAW produces on error
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Previous Next
ProTip!
Find all open issues with in progress development work with linked:pr.