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,