--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C on a code subset?



Hi,

On 6/12/20 1:14 PM, Tuttle, Mark wrote:
>
> 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.
>
We use this approach in Contiki-NG CI (https://github.com/evdenis/Contiki-NG/blob/develop/.travis.yml) For each "verified" function (https://github.com/evdenis/Contiki-NG/blob/develop/verif/contiki_status.conf) we "extricate" its source code with all dependencies and run frama-c on it to reprove the results. We also use the same tools to develop specs https://github.com/evdenis/spec-utils

Regards,

Denis