Skip to content

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
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
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 llvm_fresh_expanded_val needs design 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
#1879 opened Jun 1, 2023 by RyanGlScott
Support opaque pointers in llvm_boilerplate/function skeletons needs design 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
#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 print_goal print out the provenance of each goal when sim-verbose is high enough needs design Technical design work is needed for issue to progress usability An issue that impedes efficient understanding and use
#1372 opened Jul 8, 2021 by RyanGlScott
Warning when overrides in llvm_verify aren't used 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
#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
#1200 opened Apr 19, 2021 by atomb Someday
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
#1196 opened Apr 19, 2021 by msaaltink Someday
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
#1195 opened Apr 19, 2021 by msaaltink Someday
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
#1264 opened Mar 18, 2021 by robdockins Someday
get_opt no longer works effectively needs design Technical design work is needed for issue to progress needs test Issues for which we should add a regression test regression Something that used to work, but now doesn't type: feature request Issues requesting a new feature or capability
#1068 opened Feb 10, 2021 by ghost Someday
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
#1257 opened Jan 19, 2021 by eddywestbrook Someday
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
#916 opened Nov 18, 2020 by brianhuffman 2025T1
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
#1251 opened Nov 17, 2020 by robdockins Someday
More evaluation for crucible_term and friends 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
#855 opened Oct 5, 2020 by robdockins Someday
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
#748 opened Jun 16, 2020 by bboston7 2024T3
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
#553 opened Oct 1, 2019 by atomb 2025T1
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
#390 opened Mar 28, 2019 by langston-barrett 2025T1
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
#357 opened Jan 22, 2019 by langston-barrett 2025T1
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
#318 opened Oct 31, 2018 by msaaltink Someday
Operations on Theorems for forward-reasoning needs design Technical design work is needed for issue to progress type: enhancement Issues describing an improvement to an existing feature or capability
#91 opened Jan 13, 2016 by brianhuffman Someday
ProTip! Find all open issues with in progress development work with linked:pr.