--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2011 ---
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>