| CARVIEW |
Select Language
HTTP/2 200
date: Fri, 16 Jan 2026 17:49:46 GMT
content-type: text/html; charset=utf-8
cache-control: max-age=0, private, must-revalidate
content-security-policy: default-src 'none'; base-uri 'self'; child-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/; connect-src 'self' uploads.github.com www.githubstatus.com collector.github.com raw.githubusercontent.com api.github.com github-cloud.s3.amazonaws.com github-production-repository-file-5c1aeb.s3.amazonaws.com github-production-upload-manifest-file-7fdce7.s3.amazonaws.com github-production-user-asset-6210df.s3.amazonaws.com *.rel.tunnels.api.visualstudio.com wss://*.rel.tunnels.api.visualstudio.com github.githubassets.com objects-origin.githubusercontent.com copilot-proxy.githubusercontent.com proxy.individual.githubcopilot.com proxy.business.githubcopilot.com proxy.enterprise.githubcopilot.com *.actions.githubusercontent.com wss://*.actions.githubusercontent.com productionresultssa0.blob.core.windows.net/ productionresultssa1.blob.core.windows.net/ productionresultssa2.blob.core.windows.net/ productionresultssa3.blob.core.windows.net/ productionresultssa4.blob.core.windows.net/ productionresultssa5.blob.core.windows.net/ productionresultssa6.blob.core.windows.net/ productionresultssa7.blob.core.windows.net/ productionresultssa8.blob.core.windows.net/ productionresultssa9.blob.core.windows.net/ productionresultssa10.blob.core.windows.net/ productionresultssa11.blob.core.windows.net/ productionresultssa12.blob.core.windows.net/ productionresultssa13.blob.core.windows.net/ productionresultssa14.blob.core.windows.net/ productionresultssa15.blob.core.windows.net/ productionresultssa16.blob.core.windows.net/ productionresultssa17.blob.core.windows.net/ productionresultssa18.blob.core.windows.net/ productionresultssa19.blob.core.windows.net/ github-production-repository-image-32fea6.s3.amazonaws.com github-production-release-asset-2e65be.s3.amazonaws.com insights.github.com wss://alive.github.com wss://alive-staging.github.com api.githubcopilot.com api.individual.githubcopilot.com api.business.githubcopilot.com api.enterprise.githubcopilot.com; font-src github.githubassets.com; form-action 'self' github.com gist.github.com copilot-workspace.githubnext.com objects-origin.githubusercontent.com; frame-ancestors 'none'; frame-src viewscreen.githubusercontent.com notebooks.githubusercontent.com; img-src 'self' data: blob: github.githubassets.com media.githubusercontent.com camo.githubusercontent.com identicons.github.com avatars.githubusercontent.com private-avatars.githubusercontent.com github-cloud.s3.amazonaws.com objects.githubusercontent.com release-assets.githubusercontent.com secured-user-images.githubusercontent.com/ user-images.githubusercontent.com/ private-user-images.githubusercontent.com opengraph.githubassets.com marketplace-screenshots.githubusercontent.com/ copilotprodattachments.blob.core.windows.net/github-production-copilot-attachments/ github-production-user-asset-6210df.s3.amazonaws.com customer-stories-feed.github.com spotlights-feed.github.com objects-origin.githubusercontent.com *.githubusercontent.com; manifest-src 'self'; media-src github.com user-images.githubusercontent.com/ secured-user-images.githubusercontent.com/ private-user-images.githubusercontent.com github-production-user-asset-6210df.s3.amazonaws.com gist.github.com github.githubassets.com; script-src github.githubassets.com; style-src 'unsafe-inline' github.githubassets.com; upgrade-insecure-requests; worker-src github.githubassets.com github.com/assets-cdn/worker/ github.com/assets/ gist.github.com/assets-cdn/worker/
link: ; rel=preload; as=fetch; crossorigin=use-credentials
referrer-policy: no-referrer-when-downgrade
server-timing: issue_layout-fragment;desc="issue_layout fragment";dur=273.817447,issue_conversation_content-fragment;desc="issue_conversation_content fragment";dur=507.550244,nginx;desc="NGINX";dur=0.496037,glb;desc="GLB";dur=102.794031
strict-transport-security: max-age=31536000; includeSubdomains; preload
vary: X-PJAX, X-PJAX-Container, Turbo-Visit, Turbo-Frame, X-Requested-With, X-Issues-React-Relay-Cache, Accept,Accept-Encoding, Accept, X-Requested-With
x-content-type-options: nosniff
x-frame-options: deny
x-voltron-version: 69ef6d1
x-xss-protection: 0
server: github.com
content-encoding: gzip
accept-ranges: bytes
set-cookie: _gh_sess=lG1qrSzyDMjQdsgaOY55CjHxux9Itou3RIRxHBDxS8xYx6Lk712i6niD68lFDWiqa6hUSn0RiY0Qlg2jB%2BkVR%2F1wXWnzWhK7Y3378mYyIFIWJxXpvtxP%2Fq68RfwUYKR%2BPXhjw0oHWqVG2xJCQwjwbpPAnm2BIP2Xq6vKtY8oSNBJCwjft9cgG1PDQS%2B5FmeTdb1qLoGJpCG3BjzJ6lr4TVDivwdDIxDYYNucp9t8aaMNyO7ZtajAmSd0gPtxo97C55ulE1xGgJ1c4QTfdbQ1yA%3D%3D--ydJGRq8E1PxxmLhM--VU6r%2BEGeU6WcMFPWiRTt2w%3D%3D; Path=/; HttpOnly; Secure; SameSite=Lax
set-cookie: _octo=GH1.1.1582140985.1768585785; Path=/; Domain=github.com; Expires=Sat, 16 Jan 2027 17:49:45 GMT; Secure; SameSite=Lax
set-cookie: logged_in=no; Path=/; Domain=github.com; Expires=Sat, 16 Jan 2027 17:49:45 GMT; HttpOnly; Secure; SameSite=Lax
x-github-request-id: BA90:36C6B6:8B91BC:9B2A13:696A7A39
Remove deprecated `kani::check` · Issue #3561 · model-checking/kani · GitHub
No one assignedNo typeNo projectsNo milestoneNone yetNo branches or pull requests
Skip to content
Navigation Menu
{{ message }}
generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 134
Closed
Labels
[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.
Description
Proposed change: Deprecate the recently added kani::check function that generates non-fatal properties. I believe this was accidentally added as a new stable function as part of the uninitialized memory checks work.
Motivation: I don't think we have a clear use-case for this API today, and this will likely cause more confusion around which API to use, assertion vs cover vs check.
I'm OK keeping this internal to Kani for cases where we implement checks using demonic non-determinism to ensure some conditions are never violated.
- Deprecate API (Kani 0.56)
- Make it private (Kani 0.57)
Note: I have changed my mind since I created #695. I think cover is a much better fit for the cases I originally had in mind.
Metadata
Metadata
Assignees
Labels
[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.
Type
Projects
Milestone
Relationships
Development
Issue actions
You can’t perform that action at this time.