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