--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on June 2011 ---
Hello, Le 31/05/2011 17:13, haihao shen a ?crit : > I have another question on kernel_function (kf) and normal function (f). > I searched some utility functions in module kernel_function and found > that for kernel function, the module provides several functions to > handle detailed specification per function preconditions and > postconditions. I would like to know whether there is similar function > to handle normal function (f). Not directly. Kernel function groups in a single type function declarations and function definitions, as well as it provides an easy access to its specification. That is not the case of what you call "normal" function. But it is still possible to get the kernel function corresponding to a "normal" function and conversely, for instance via their shared varinfo. Also, I would like to know whether there > are other utility function to handle predicate or logic. The Plug-in Development Guide (http://frama-c.com/download/frama-c-plugin-development-guide.pdf), even if partially out-of-date, explains how Frama-C sources are organized. For instance, have a look at Section 5.1. The full API documentation is also available in html format here: http://frama-c.com/download/frama-c-Carbon-20110201_api.tar.gz. > ==utility function in module kernel_function == > let postcondition <javascript:void(0)> kf <javascript:void(0)> = > Logic_const <javascript:void(0)>.pands <javascript:void(0)> > (List <javascript:void(0)>.map <javascript:void(0)> Ast_info > <javascript:void(0)>.behavior_postcondition <javascript:void(0)> > (get_spec <javascript:void(0)> kf <javascript:void(0)>).spec_behavior > <javascript:void(0)>) Usually, when looking for a function, it is easier to look at the module interface than at the module implementation, even if you can improve your OCaml skill this last way (only if the implementation is clear enough: that is arguably and unfortunately not always the case in Frama-C). Hope this helps, Julien