The Verasco verified C static analyzer

Coq development

Putting all together

• CsharpminorAnalysis: analyzer entry point.

Interfaces

• AbIdealEnv: abstract environments over ideal numbers.
• IdealExpr: expressions used in numeric domain over ideal numbers.
• AbIdealNonrel: abstract domains for ideal numbers.
• AbMachineEnv: abstract environments over machine numbers.
• AbMemSignatureCsharpminor: abstract memory states.
• IntSet: finite sets of machine integers.

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

• CsharpminorIter: its implementation.
• CsharpminorIterproof: its proof.
• CsharpminorLogic: hoare logic for C#minor.
• AlarmMon: the monad carrying the list of alarms.
• AnyDefs: axiomatization of any_double() and any_int64() primitives.

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

• IdealEnvToMachineEnv: handling machine arithmetics.
• IdealBoxDomain: from a non relational domain to an domain over environments.
• AbIdealEnvProduct: combining two abstract domains over idealized environments.
• ZIntervals: intervals of Z integers.
• FloatIntervals, FloatIntervalsBackward: intervals of floats.
• IdealIntervals, IdealIntervalsNonrel: intervals of floats or of Z integers.
• ZCongruences_defs, ZCongruences: abstract domain of congruences over Z integers.
• AbVarExpEq: symbolic domain of equalities between a variable and an expression.
• Hash: hash functions used by AbVarExpEq.
• CellEncoding: encoding cells into positive, because the polyhedric domain cannot be indexed by cells.
• LinearQuery, AbLinearize: linearization abstract domain.
• Octagons: octagon abstract domain.
• AbTyps: simple abstract domain for variable types.

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

• Debug: generic definitions.
• ToString: typeclass of printable types.
• PrintPos: converting integers to strings.
• DebugCminor: printing utilities for Cminor constructs.
• DebugCshm: printing utilities for C#minor constructs.
• DebugAbIdealNonrel: tracing wrapper for AbIdealNonrel.
• DebugAbMachineEnv: tracing wrapper for AbMachineEnv.
• DebugAbMemCsharpminor: tracing wrapper for AbMemSignatureCsharpminor.

CompCert Coq development