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] Frama-C on a code subset?

  • Subject: [Frama-c-discuss] Frama-C on a code subset?
  • From: mrtuttle at amazon.com (Tuttle, Mark)
  • Date: Fri, 12 Jun 2020 11:43:53 +0000
Thanks, Loïc.

I am considering an approach similar to your proposal, but wondered if anyone had implemented it already, or if there is a better approach.

(What is the intended semantics of -wp-fct?  I run frama-c with “-wp -wp-ftc FOO” and frama-c checks properties of 222 functions.  I’m obviously not using it correctly.)

Thanks,
Mark

From: Frama-c-discuss <frama-c-discuss-bounces at lists.gforge.inria.fr> on behalf of CORRENSON Loic <loic.correnson at cea.fr>
Reply-To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Date: Friday, June 12, 2020 at 7:30 AM
To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Subject: RE: [Frama-c-discuss] Frama-C on a code subset?

Sorry, I missed the end of your e-mail. There is no such facility in WP.
You can use a plugin for that, using a CIL visitor to collect callees and/or make use of
the static calligraph API.
  L.

________________________________
De : Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Tuttle, Mark [mrtuttle at amazon.com]
Envoyé : vendredi 12 juin 2020 12:14
À : Frama-C public discussion
Objet : [Frama-c-discuss] Frama-C on a code subset?
What method do you use to restrict Frama-C to operate on a subset of the code?

I have a method FOO in an API defined in a large source file along with all the other methods in the API.  I write function contracts for FOO and all the function it depends on.

I run frama-c -wp on the file, and frama-c proves the function contracts, but it also appears to try proving the preconditions for FOO at all invocation sites for FOO in the file, which obviously fail because I haven’t written any contracts for those invocation sites.

I run fama-c -wp -rte on the file, and rte appears to insert assertions everywhere in the file and trying to prove them, which obviously fail.

What I’d like is a method for restricting frama-c to FOO and all the functions in the function call graph of FOO.  I’d like a path to automating this so I can consider using frama-c in continuous integration as the code changes.  I’m aware of -wp-fct and -wp-skip-fct but may not be using them correctly.

Thanks,
Mark
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200612/154978c7/attachment-0001.html>