Plugins Kernel Specification Ivette (GUI)

Typestates

Overview

Typestates is a plug-in dedicated to specifying and verifying typestates properties. Introduced in 1, the notion of typestate allows specifying the operations that can be applied to an object of a given type depending on its current state. More precisely, it takes the form of an automaton whose edges are labeled with function names. Each object of the target type starts in an initial state. At each function call involving such an object o, we check that there’s an edge starting from the current state, and update the state of o according to the transition. Otherwise, the program does not respect the typestate specification. Moreover, at the end of its lifetime, o should be in a final state.

A canonical example for typestates is a FILE datatype, that starts in Closed state, can be opened in Writing mode, in which some write operation may be performed, leading to a Dirty mode, where you can either write or flush (going back to Writing). When in Writing, you can also close the FILE once you’re finished, going back to Closed, which is both the initial and the final state.

The plug-in introduces an ACSL extension to specify typestates over any C type, and instrument the code with ACSL annotations and ghost code in order for standard analyzers (e.g. WP, E-ACSL, or Eva) to verify that the code respects this specification. A formalization2 of the instrumentation on a small subset of C is being developed using Necro-coq.

Usage

Typestates is available as a separate open-source plug-in, on Gitlab (more information there). It is intended to be compatible with the latest state of Frama-C’s public repository.

Since Frama-C 33.0 Arsenic here also exists a companion release for each Frama-C version. It is also available through opam as the frama-c-typestates package.

Once installed, the plugin is activated by the -typestates option, which will parse the typestates specifications and instrument the code accordingly.

References

  1. Strom, R. E., & Yemini, S. (1986). Typestate: A Programming Language Concept for Enhancing Software Relability. IEEE Transactions on Software Engineering, 12(1). https://doi.org/10.1109/TSE.1986.6312929↩︎

  2. Patte, S., & Prevosto, V. (2025). Typestates specification and verification in Frama-C. 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), 146–156. https://doi.org/10.1109/FormaliSE66629.2025.00021↩︎