-
Notifications
You must be signed in to change notification settings - Fork 31
Issues: rems-project/cerberus
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
CN: Delete unused annotation
cn
technical debt
Something for internal cleanup
#919
opened Mar 7, 2025 by
dc-mak
CN: Fix source location in Issue with presentation or user experience
resourceInference.ml
cn
ui/ux
#914
opened Mar 6, 2025 by
dc-mak
CN: Potential bug in loop/focus related resource reasoning
bug
Something isn't working
cn
resource reasoning
Related to reasources in specs
#913
opened Mar 6, 2025 by
dc-mak
Record not found in map
bug
Something isn't working
CN-exec
Related to CN executable spec generation, called using `cn instrument`
#912
opened Mar 6, 2025 by
yav
[CN-Test-Gen] Automatically compile and verify bug counterexample code.
CN spec testing
cn
enhancement
New feature or request
#911
opened Mar 5, 2025 by
ZippeyKeys12
CN: Implement translation validation of resource inference steps in Rocq
#909
opened Mar 5, 2025 by
vzaliva
CN: Replace resultWithData with appropriate Result.t
cn
technical debt
Something for internal cleanup
#903
opened Mar 4, 2025 by
dc-mak
CN: Simplify arguments to provable(withUnknown)
cn
solver
Related to the SMT solver backend
technical debt
Something for internal cleanup
#902
opened Mar 4, 2025 by
dc-mak
Handle quantified predicates and basetype variables in check_pred
cn
enhancement
New feature or request
#901
opened Mar 4, 2025 by
cassiatorczon
Update Issue with presentation or user experience
check_pred
display based on feedback
cn
ui/ux
#900
opened Mar 4, 2025 by
cassiatorczon
Change Something for internal cleanup
label
to its own datatype in report.ml
cn
technical debt
#899
opened Mar 4, 2025 by
cassiatorczon
[CN-exec] Create CN subcommand for instrumenting and running Fulminate
#894
opened Feb 28, 2025 by
rbanerjee20
[CN-exec] Make precondition and postcondition assertions fail with different exit codes
CN-exec
Related to CN executable spec generation, called using `cn instrument`
#893
opened Feb 28, 2025 by
rbanerjee20
[CN-Test-Gen] Flag to toggle using builtin New feature or request
malloc
versus cn_fl_malloc
CN spec testing
cn
enhancement
#891
opened Feb 26, 2025 by
ZippeyKeys12
[CN-Test-Gen] Update pointer bookkeeping to use new allocator
CN spec testing
cn
technical debt
Something for internal cleanup
#890
opened Feb 26, 2025 by
ZippeyKeys12
[CN] misleading error message concerning undefined struct arguments
cn
ui/ux
Issue with presentation or user experience
#888
opened Feb 25, 2025 by
peterohanley
[CN] Call Related to the SMT solver backend
technical debt
Something for internal cleanup
reset_solver
from make
cn
solver
#886
opened Feb 25, 2025 by
dc-mak
Add a Windows CI runner for Cerberus / CN
CI
Related to CI infrastructure
#883
opened Feb 20, 2025 by
septract
[CN-Seq-Test] running seq_test --with-static-check causes duplicate symbol errors
bug
Something isn't working
cn
ui/ux
Issue with presentation or user experience
#879
opened Feb 18, 2025 by
echoumcp1
[CN-Seq-Test] Move seq_test into own directory
cn
technical debt
Something for internal cleanup
#875
opened Feb 15, 2025 by
echoumcp1
[CN] Crash when logging SMT output with Something isn't working
cn
solver
Related to the SMT solver backend
--solver-logging
bug
#874
opened Feb 15, 2025 by
septract
[CN] segfault with large global array
bug
Something isn't working
cn
#872
opened Feb 14, 2025 by
peterohanley
Previous Next
ProTip!
Adding no:label will show everything without a label.