Skip to content

Verification of unchecked functions with bounds-safe interface #732

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

Jump to bottom
Closed
secure-sw-dev-bot opened this issue Jan 16, 2022 · 0 comments
Closed

Verification of unchecked functions with bounds-safe interface #732

secure-sw-dev-bot opened this issue Jan 16, 2022 · 0 comments

Comments

@secure-sw-dev-bot
Copy link

This issue was copied from checkedc/checkedc-clang#736

In this PR, we want to verify unchecked function against their bounds-safe interface. The changes are:

  • Modify codegen to insert verification conditions at dynamic check points in the bit-code, to be picked up by Seahorn as a backend for verification.
  • Added bounds for unchecked pointers, so we can have dynamic checks on their dereference.
  • Added command line arguments for each of these two changes.
  • Tests for codegen (standalone tests) and full verification pipeline (requires Seahorn to be installed and in path).
  • Document: short description of seahorn and CheckedC+Seahorn pipeline

Note: The changes are not specific to Seahorn, any LLVM-based software verifier that uses the SV-COMP convention can be used as a backend.

See also #735
dtarditi pushed a commit that referenced this issue Jan 21, 2022
@john-h-kastner
More command line options clean up (#732)
94cd56c 
This is a follow up PR from #692 that moves all command line options into the
_3COptions structure, moves all of 3C's command line options into the same
category so that all options are shown by -help (fixes #393), and reformats some
of the code around creating command line options.

It also removes the the option -enable-itypeprop which was not referenced
anywhere in the code.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@secure-sw-dev-bot