The Verasco verified C static analyzer
Coq development
Putting all together
Interfaces
Libraries about abstract domains
- AdomLib: abstract domains,
concretization functions and how we combine them.
- ListAdom: a list of abstract values is
an abstract domain for a list of concrete values.
Abstract Iterator
State abstract domain
- MemCsharpminor: the abstract
domain and its proof.
- Cells: abstract memory cells.
- PExpr: C#minor expressions with resolved
loads.
- Nconvert: removing pointers from
expressions.
- TypesDomain: type information.
- MemChunkTree: map whose keys are
memory_chunk elements.
- OnMem: lemmas about the CompCert memory
model.
- NoError: when are expressions
blocking ?
Numeric domains
Generic libraries
- ArithLib: lemmas on arithmetics.
- FloatLib: lemmas on floats.
- AssocList: asociation lists.
- Sets: finite sets of positives.
- TreeAl: TREE definitions.
- ShareTree: extensions of the
TREE interface and its implementations, taking advantage of sharing.
- Util: various lemmas and tactics.
Debugging and tracing facilities