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

[Frama-c-discuss] Partial verification



Hello !

Is it possible to run frama-c/ jessie only to one function of our program?

For example, if we have:

/**********************************/
/* program **************************/

/*@ requires a > 0,  b> 0 ;
    @  ensures  a < b ;
*/
int min (int a, int b){
....
}


/*@ requires
    @ ensures
*/

int max(int a, int b){
...
}

/****** end ************/

Is it possible to run the verification only for the function max, without generate anything for min?

Thank you in advance!
Maria
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111104/4c1c616b/attachment.htm>