-
Notifications
You must be signed in to change notification settings - Fork 63
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
Generalize/strengthen build.sh
needs design
Technical design work is needed for issue to progress
tooling: build system
Issues involving SAW's build system
tooling: CI
Issues involving CI/CD scripts or processes
tooling: test infrastructure
Issues involving test infrastructure or test execution, or making SAW more testable
type: enhancement
Issues describing an improvement to an existing feature or capability
#2063
opened Jul 3, 2024 by
sauclovian-g
Support for invariants on ghost state
needs design
Technical design work is needed for issue to progress
type: feature request
Issues requesting a new feature or capability
#2053
opened Apr 24, 2024 by
sauclovian-g
Extensions to/limitations of the current ghost state API
needs design
Technical design work is needed for issue to progress
type: feature request
Issues requesting a new feature or capability
#2040
opened Mar 11, 2024 by
sauclovian-g
Support opaque pointers in Technical design work is needed for issue to progress
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
type: enhancement
Issues describing an improvement to an existing feature or capability
llvm_fresh_expanded_val
needs design
#1879
opened Jun 1, 2023 by
RyanGlScott
Support opaque pointers in Technical design work is needed for issue to progress
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
type: enhancement
Issues describing an improvement to an existing feature or capability
llvm_boilerplate
/function skeletons
needs design
#1877
opened May 31, 2023 by
RyanGlScott
Cleanup/refinement of goal tags
needs design
Technical design work is needed for issue to progress
type: enhancement
Issues describing an improvement to an existing feature or capability
usability
An issue that impedes efficient understanding and use
#1681
opened Jun 2, 2022 by
robdockins
Add tactic for case splitting on a boolean variable
needs design
Technical design work is needed for issue to progress
type: enhancement
Issues describing an improvement to an existing feature or capability
#1585
opened Feb 15, 2022 by
brianhuffman
Have Technical design work is needed for issue to progress
usability
An issue that impedes efficient understanding and use
print_goal
print out the provenance of each goal when sim-verbose
is high enough
needs design
#1372
opened Jul 8, 2021 by
RyanGlScott
Warning when overrides in Technical design work is needed for issue to progress
type: enhancement
Issues describing an improvement to an existing feature or capability
usability
An issue that impedes efficient understanding and use
llvm_verify
aren't used
needs design
#1362
opened Jun 29, 2021 by
RyanGlScott
Consider an interactive proof tactic
needs design
Technical design work is needed for issue to progress
type: enhancement
Issues describing an improvement to an existing feature or capability
Feature request: proof script profiling
needs design
Technical design work is needed for issue to progress
type: feature request
Issues requesting a new feature or capability
usability
An issue that impedes efficient understanding and use
Feature request: more ways to conditionalize a ProofScript
needs design
Technical design work is needed for issue to progress
type: feature request
Issues requesting a new feature or capability
Internal consistency of saw-core typechecking
needs design
Technical design work is needed for issue to progress
subsystem: saw-core
Issues related to the saw-core representation or the saw-core subsystem
tech debt
Issues that document or involve technical debt
type: enhancement
Issues describing an improvement to an existing feature or capability
get_opt
no longer works effectively
needs design
Add support for serializing / deserializing SAW core modules to/from disk
needs design
Technical design work is needed for issue to progress
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
Decide how to deal with JVM class initialization
needs design
Technical design work is needed for issue to progress
subsystem: crucible-jvm
Issues related to Java verification with crucible-jvm
type: bug
Issues reporting bugs or unexpected/unwanted behavior
unsoundness
Issues that can lead to unsoundness or false verification
saw-core-coq translateConstant needs some TLC
needs design
Technical design work is needed for issue to progress
subsystem: saw-core-coq
Issues related to converting saw-core to Gallina for use with the Coq/Rocq theorem prover
type: bug
Issues reporting bugs or unexpected/unwanted behavior
More evaluation for Technical design work is needed for issue to progress
subsystem: saw-core
Issues related to the saw-core representation or the saw-core subsystem
tech debt
Issues that document or involve technical debt
type: enhancement
Issues describing an improvement to an existing feature or capability
crucible_term
and friends
needs design
Goals in manual are used before being introduced
documentation debt
Documentation tasks previously deferred, postponed, etc.; technical debt in documentation
documentation
Issues involving documentation
needs design
Technical design work is needed for issue to progress
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Unify infrastructure for compositional verification
needs design
Technical design work is needed for issue to progress
subsystem: crucible-jvm
Issues related to Java verification with crucible-jvm
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
type: enhancement
Issues describing an improvement to an existing feature or capability
Set up a scheme for solver version constraints
needs design
Technical design work is needed for issue to progress
performance
Issues that involve or include performance problems
priority
High-priority issues
type: feature request
Issues requesting a new feature or capability
usability
An issue that impedes efficient understanding and use
Support calling the constructors in llvm.global_ctors
needs design
Technical design work is needed for issue to progress
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
type: feature request
Issues requesting a new feature or capability
unsoundness
Issues that can lead to unsoundness or false verification
breadth cutoff for goal printer
needs design
Technical design work is needed for issue to progress
type: enhancement
Issues describing an improvement to an existing feature or capability
usability
An issue that impedes efficient understanding and use
Operations on Technical design work is needed for issue to progress
type: enhancement
Issues describing an improvement to an existing feature or capability
Theorem
s for forward-reasoning
needs design
ProTip!
Find all open issues with in progress development work with linked:pr.