--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on September 2010 ---
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