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] Separate proof-files for separate C-files

Hello,

On Sat, Sep 11, 2010 at 10:12 PM, Michael Schausten
<michaelschausten at googlemail.com> wrote:

> I then tried to put the functions into separate c-files, including them in a
> main file, e.g.:
>
> /*@ ensures ... */
> file1.c:
> void func1() { /*...*/ }
>
> /*@ ensures ...*/
> file2.c:
> void func2() { /*...*/ }

I have no experience with the Coq back-end, but after a few hours of
thought (you might say I'm a slow thinker), I think that's irrelevant.
Jessie offers a modular verification methodology, and that should be
true regardless of the back-end.

So, what happens if you...

1/ provide headers file1.h, ... with only the contract of the function
func1(), ... (the contract is the part of the ACSL annotations that
tells the rest of the program how to use it. requires, ensures,
assigns, this sort of things),

2/ include these headers in main.c, and use only the contracts of
func1(), ... to verify main(),

3/ use the separate commands:

frama-c -jessie -jessie-atp coq file1.c
frama-c -jessie -jessie-atp coq file2.c
frama-c -jessie -jessie-atp coq main.c

for the verification?

I believe this is the intended usage for modular verification,
regardless of the back-end.

Pascal