--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on July 2012 ---
Hi, This problem seems related to the proof session system in Why3. Please fill a bug report into the Why3 BTS : https://gforge.inria.fr/tracker/?group_id=2990 and please attach both files pred.c, pred.jessie/pred.mlw and the pred.jessie/pred/why3session.xml A workaround might to remove the file pred.jessie/pred/why3session.xml, but this would lose all information about your previous proof attempts. May be you could just *rename* pred.jessie/pred/why3session.xml into something like pred.jessie/pred/saved.xml, while we try to figure out what is the problem. - Claude On 07/24/2012 08:10 PM, Boris Hollas wrote: > Hello, > > if I use "frama-c -jessie" on a random c-file, I get > > why3ml [...] pred.mlw > > field 'name' is missing > make: *** [why3ml] Error 1 > [jessie] user error: Jessie subprocess failed: make -f pred.makefile > why3ml > > Has there been a change of syntax in the new why releases? > > -Boris > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss