--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on December 2012 ---
Hello Daniel, Le jeu. 13 d?c. 2012 22:33:06 CET, daniel <dchapiesky2 at gmail.com> a ?crit : > Is there a way to use Frama on programs which contain pointers to > functions and the invocation of those functions using the (*myfunc)() > notation? > > > I see that equality comparison is available for function pointers in > the ACSL. > > > I have attempted to implement a preprocessor which converts the > following code into something Frama seems to want. As it is often the case with Frama-C, the answer mainly depends on what plug-ins you intend to use in the end. Value Analysis handles function pointers perfectly well (provided there isn't too much over-approximation over them), as should be the case for plug-ins derived from Value (Slicing, constant propagation, ...). For WP or Jessie, as you pointed out, there's the issue that you can't provide an ACSL contract for them (there has been some discussion on adding syntax for that, but it has not materialized yet). If you intend to use a plugin that do not support function pointers, I'd suggest that you take advantage of the information computed by Value Analysis in order to generate the possible cases, instead of an external pre-processor. In the easiest case, where each function pointer points to a unique function, you just have to call the semantic constant folding plug-in to get rid of them. Otherwise, after having replaced those constant pointers, you can use sequences of 'if (myFunc == &func_i) func_i();', as in your preprocessor, but using for the func_i the set of possible values computed by Value for myFunc at this program point. Best regards, -- E tutto per oggi, a la prossima volta. Virgile