Skip to content

Issues: model-checking/kani

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.

Sign up for GitHub

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

402 Open 723 Closed
402 Open 723 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Some concrete playback regressions fail with latest CBMC [C] Bug This is a bug. Something isn't working.
#2123 opened Jan 13, 2023 by zhassan-aws
Kani crashes when an intrinsic call using ZST is invalid [C] Bug This is a bug. Something isn't working.
#2121 opened Jan 13, 2023 by celinval
We need tests to verify that Kani works correctly when making cross ABI calls [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2120 opened Jan 13, 2023 by danielsn
Print all the stubs that were exercised in a harness [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2119 opened Jan 13, 2023 by celinval Function/method stubbing - enabling proofs for unprovable harnesses
Multiple --harness arguments. [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2118 opened Jan 13, 2023 by YoshikiTakashima
1
Update rust toolchain version for Kani 0.22 Z-Sync Upstream Fetch changes from rustc repository. Old Rebase
#2115 opened Jan 12, 2023 by celinval
@adpaco-aws
Update rust toolchain version for Kani 0.21 Z-Sync Upstream Fetch changes from rustc repository. Old Rebase
#2114 opened Jan 12, 2023 by celinval
@tedinski
Update rust toolchain version for Kani 0.20 Z-Sync Upstream Fetch changes from rustc repository. Old Rebase
#2113 opened Jan 12, 2023 by celinval
@karkhaz
Kani builds don't enable features the same as ordinary cargo builds [C] Bug This is a bug. Something isn't working.
#2112 opened Jan 12, 2023 by tedinski
Tracking issue: common unsupported features [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
#2107 opened Jan 12, 2023 by tedinski
Kani is unable to build some crates due to package naming [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2104 opened Jan 11, 2023 by tedinski
1
kani-compiler panic on unimplemented scalar [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
#2099 opened Jan 10, 2023 by tedinski
Compilation doesn't test for symtab2gb on PATH [C] Bug This is a bug. Something isn't working.
#2098 opened Jan 10, 2023 by feliperodri
Implement stub-sets [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2096 opened Jan 9, 2023 by celinval Function/method stubbing - enabling proofs for unprovable harnesses
Implement automatic stubbing for unreachable function [C] Feature / Enhancement A new feature request or enhancement to an existing feature.
#2084 opened Jan 5, 2023 by celinval
4 tasks
Function/method stubbing - enabling proofs for unprovable harnesses
@feliperodri
KR3: publish the GOTO back-to-back checking tool on the github model-checking org [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2083 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
KR2: publish the GOTO reference evaluator on the github model-checking org [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2082 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
KR1: publish the GOTO syntax and semantics reference document on the github model-checking or [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2081 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
Scope work to produce goto instead of irep
#2080 opened Jan 5, 2023 by celinval Create a reference evaluator and back-to-back testing tool for the GOTO language
@celinval
Develop GOTO trace loader/deserialiser [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2079 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
Develop back-to-back testing tool using the evaluator [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2078 opened Jan 5, 2023 by remi-delmas-3000
Develop reference trace evaluator for GOTO models [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2077 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
Develop type-checking and invariant checking for GOTO models [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2076 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
Develop GOTO model AST for the evaluator [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2075 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
Develop GOTO binary loader and deserialiser [C] Internal Tracks some internal work. I.e.: Users should not be affected.
#2074 opened Jan 5, 2023 by remi-delmas-3000 Create a reference evaluator and back-to-back testing tool for the GOTO language
@remi-delmas-3000
ProTip! Mix and match filters to narrow down what you’re looking for.