Frama-C API - Asm_contracts
Code transformation for inferring contracts from information given in GNU's extended assembly syntax. Registered as a transformation occurring after annotations table are filled.
val category : File.code_transformation_categorythe corresponding code transformation category.
val emitter : Emitter.temitter for the generated annotations.