Critical software systems (e.g., weapon systems, medical devices, nuclear power plants, aircraft, cars, …) need strong safety and security guarantees, since a bug can have very bad consequences.

The C programming language, created in the 70s, is still widely used in critical systems because it is a mature low-level language, with a wide range of compilers for many CPU architectures, and a very large code base of battle-tested libraries. The C language gives developer much freedom, which is one of the reasons for its popularity, but makes it easy to write a bad program whose behavior is undefined by the C standard, leading to safety and security risks.

This calls for powerful verification techniques, such as formal methods, to assess C programs. Frama-C is an Open-Source platform dedicated to the analysis of C programs. Recently, a Frama-C plug-in has been developed for Typestates properties verification. These properties restrict possible operations on objects of a given datatype, depending on its current state. This plug-in instruments the original program with formal annotations, in order to then use standard Frama-C analyzers.

We propose in this paper a formalization for this instrumentation, in order to prove its correctness. In other words, if the original code is a valid program and respects its Typestates specification, then the instrumented code should be valid and produce identical results. Conversely, if the original code is invalid or non-compliant with its Typestates specification, its instrumented version should be invalid. To this end, we define a simple language with pointers and function calls, for which we define semantic rules and an instrumentation function in the Skel meta-language. Subsequently, we use the Necro Coq tool to build a mechanized formalization for the Coq proof assistant.