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?

Hi,
You can use -wp-fct <f>,... for that.
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/c5f2fe4d/attachment.html>