checkedc-clang
This is the primary development repository for 3C, a tool for automatically converting legacy C code to the Checked C extension of C, which aims to enforce spatial memory safety. This repository is a fork of Checked C's. (by correctcomputation)
verifast
Research prototype tool for modular formal verification of C and Java programs (by verifast)
| checkedc-clang | verifast | |
|---|---|---|
| 1 | 2 | |
| 14 | 342 | |
| - | 3.2% | |
| 0.0 | 9.2 | |
| almost 2 years ago | 1 day ago | |
| C++ | Rust | |
| - | GNU General Public License v3.0 or later |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
checkedc-clang
Posts with mentions or reviews of checkedc-clang.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-02-02.
-
Refactoring the FreeBSD Kernel with Checked C [pdf]
At Correct Computation (https://correctcomputation.com/, we are hiring), we are developing a tool called 3C to provide automation assistance for the conversion of C code into Checked C. A completely automated approach is impractical (i.e., without making lots of changes to the target program's code and adding lots of overhead), but we have found a "best effort" approach works well.
See here for more info (which transitively links to a tutorial of 3C's use): https://github.com/correctcomputation/checkedc-clang/blob/ma...
verifast
Posts with mentions or reviews of verifast.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2021-02-02.
- VeriFast
-
Refactoring the FreeBSD Kernel with Checked C [pdf]
Checked c is interesting, but I think a more fruitful avenue would be verifast[0]. Verifast is completely compatible with existing c codebases (so you can keep using your existing c compiler), and is able to verify more interesting behaviour than checked c. [1] finds that it would have prevented 5 of 50 recent CVEs in FreeBSD, whose causes include unlocked memory accesses, fd leaks, and bad use of reference counts.
0. https://github.com/verifast/verifast
1. https://metasepi.org/en/posts/2020-10-14-avoid-freebsd-secur...
What are some alternatives?
When comparing checkedc-clang and verifast you can also consider the following projects:
ctl - My variant of the C Template Library
checkedc - Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.