Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Following execution through function pointer

  • Subject: [Frama-c-discuss] Following execution through function pointer
  • From: virgile.prevosto at (Virgile Prevosto)
  • Date: Fri, 14 Dec 2012 08:48:00 +0100
  • In-reply-to: <1355455986.9200.11.camel@linuxFront>
  • References: <1355455986.9200.11.camel@linuxFront>

Hello Daniel,

Le jeu. 13 d?c. 2012 22:33:06 CET,
daniel <dchapiesky2 at> 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.