--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on June 2020 ---
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>