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