-
Notifications
You must be signed in to change notification settings - Fork 11
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Phase 2x: Close out Phase 2 documentation, diagnostics, and regression coverage
documentationImprovements or additions to documentationImprovements or additions to documentationenhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1133 In jsiek/deduce;Phase 2w: Verify binary_search as the Phase 2 stress test
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1132 In jsiek/deduce;Phase 2v: Verify frame_preserves_sorted using observer read frames
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1131 In jsiek/deduce;Phase 2u: Verify early returns and linear_search
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1130 In jsiek/deduce;Phase 2t: Verify array loops with array_fill_zero and a missing-invariant regression
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1129 In jsiek/deduce;Phase 2s: Verify array_swap with old values and narrow frames
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1128 In jsiek/deduce;Phase 2r: Allocate mutable arrays from pure lists in verifier state
enhancementNew feature or requestNew feature or requestparsingRelated to the syntax / parser or deduceRelated to the syntax / parser or deducepriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1127 In jsiek/deduce;Phase 2q: Type array observers and preserve facts using read frames
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1126 In jsiek/deduce;Phase 2p: Resolve call labels and labeled postcondition facts
enhancementNew feature or requestNew feature or requesterror messageSome error messages are wrong or could be made betterSome error messages are wrong or could be made betterpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1125 In jsiek/deduce;Phase 2o: Verify procedure calls and instantiate contracts
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1124 In jsiek/deduce;Phase 2n: Check inline proofs and out-of-line imperative proof slots
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1123 In jsiek/deduce;Phase 2m: Verify loop decreases clauses and local_counter
enhancementNew feature or requestNew feature or requestpriority:mediumThis issue would be good to fix/implement when time permits.This issue would be good to fix/implement when time permits.testingrelated to `test-deduce.py` or github CIrelated to `test-deduce.py` or github CIStatus: Open.#1122 In jsiek/deduce;