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] Source loop identification

  • Subject: [Frama-c-discuss] Source loop identification
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Wed, 12 Jun 2013 10:20:45 +0200
  • In-reply-to: <CAOT7Vm0=VJ4soZirFuHvLnQZ_+1TTCU2gG-11wJzuxyCht=jYQ@mail.gmail.com>
  • References: <CAOT7Vm0=VJ4soZirFuHvLnQZ_+1TTCU2gG-11wJzuxyCht=jYQ@mail.gmail.com>
Hello,

2013/6/11 Daniel Garcia <dhekir at gmail.com>:
> Some time ago someone told me about loop instrumentation using a source code
> analysis tool, and I think it was Frama-C he mentioned, but I don't remember
> it clearly. What I'd like to do is to identify, on the source code, which
> lines correspond to a loop body and which are outside the loop (only
> considering structured loops here). I've been looking for something like
> this on the Frama-C GUI and manual, but couldn't find it. Is there such a
> thing on Frama-C, or am I mistaken about this feature?

As far as I know, there's no such thing in Frama-C yet, but if I
understand correctly what you mean, this should not be too difficult
to achieve with a visitor (see Frama-C's developer manual for more
information about the visitor mechanism.

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile