Skip to content

Latest commit

 

History

History
61 lines (42 loc) · 1.84 KB

README.md

File metadata and controls

61 lines (42 loc) · 1.84 KB

FV-Libc

This is an attempt at a formally-verified variant of klibc/baselibc.

It is directly derived from Baselibc, which is a fork of klibc with GPL code removed and tinyprintf.

Verification is being carried out using Frama-C/WP and ACSL. See https://frama-c.com/index.html for more information.

Targets

Just like Baselibc, this library targets small microcontrollers and deeply embedded systems. Therefore it is not an objective to support POSIX system calls.

Goals

  • Have all non I/O functions fully verified.
  • For functions that require I/O (and thus some board support or os support) have at least the specification for functions that should be provided.
  • Have something that is usable as a stand-alone C library (i.e., no need for newlib or any of that stuff.)
  • Keep the original C code as is: the way klibc is written makes it harder to verify, but that's the challenge.
  • Be independent of other C libraries' headers (using the compiler provided headers is OK). This includes Frama-C headers too.

Non goals

Things I will not do:

  • Support non C99 functions: this means no POSIX and no non-standard stuff.
  • Architecture or OS-specific code if not strictly needed: this means NO board support packages.

Usage / Building

Requirements

In addition to a compiler, you need Frama-C / Alt-Ergo. The easiest way to get it is via OPAM.

Building

Typing make or make all will verify all currently proven files and build the library, producing a static archive.

make library only compiles, while make proofs only runs Frama-C/WP without compiling.

TODO

  • Finish verifying all of string.h.
  • Weed out POSIX and BSD functions.
  • Add proper Makefiles to run th verification/compile, etc.
  • Figure out what's needed to cut dependencies on other C libraries in bare metal projects.
  • More stuff.