--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Separate proof-files for separate C-files



  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,