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
- Subject: [Frama-c-discuss] Separate proof-files for separate C-files
- From: michaelschausten at googlemail.com (Michael Schausten)
- Date: Sat, 11 Sep 2010 21:12:54 +0200
Hello, I have a couple of C-functions I'd like to prove with Coq. Having all of the functions in one single C-file gives me a huge coq-file, which takes quite some time to be verified with all the proofs filled in. 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() { /*...*/ } /*@ ensures ... *( file main.c: void main() { // ... func1(); // ... func2(); } Now I have 3 separate c-files, which I compile with frama-c -jessie -jessie-atp coq file1.c file2.c main.c However, this still results in 1 single coq-file, in which all 3 functions with there proofs are joined. What I'd like to have is 3 separate coq-files (file1_why.v, file2_why.v and main_why.v)? In main_why.v there would have to be some importing of the other 2 proof-files. Is this possible? Sincerely,
- Follow-Ups:
- [Frama-c-discuss] Separate proof-files for separate C-files
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Separate proof-files for separate C-files
- Prev by Date: [Frama-c-discuss] ACSL Course in Berlin on October 21/22 2010
- Next by Date: [Frama-c-discuss] Separate proof-files for separate C-files
- Previous by thread: [Frama-c-discuss] ACSL Course in Berlin on October 21/22 2010
- Next by thread: [Frama-c-discuss] Separate proof-files for separate C-files
- Index(es):