--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how jessie and why platform work to generate a .v output?





Hi all,
    I am trying to figure out the workflow from C source(plus embeddedACSL spec) to the .v file passed to proof assistant.
    I am using why2. Is the following workflow correct?
    C/ACSL -> (frama-c/jessie) 
                      -->filename.jc ->(jessie/why)
                                                  -->filename.why->(why)
                                                                            -->filename.v  

    I use simple program demo, max.c:
#define ZERO 0
int gFlag =0;
////////////////////////////////////////
/*@ requires x>0; 
  @ ensures \result >= x && \result >= y && \result>ZERO; 
  @ ensures \result == x || \result == y; 
@*/ 
int max (int x, int y) 
{ 
  int zz=1;
  if (x>y) 
    return x;
  /*@ assert zz>0; 
  @*/
  return y;
} 

int main(void){
  return max(0,1);
}
//////////////////////////////////////////
from 
>  frama-c -jessie -pp-annot max.c
I got max.why, which is over 300lines of code.
I then use why command to generate .v output for coq:
>  why --coq max.why
File "max.why", line 17, characters 29-35:
Unbound type 'tag_id'

   Did I miss something or some step?
   Thanks in advance.

xiaolei Cui


  

   

 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131102/2cdba736/attachment.html>