--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2016 ---
Hello Jens,  Indeed it is the "ACSL by example", and the option "-wp-out" works perfectly! Moreover, I didn't have any strong reason to use the Sodium release. So I have upgraded my frama-c version to Magnesium, and all the goals are now proved (which was not the case with Sodium). Thank you very much for your help.  Best regards, Paul Boniol ----- Mail original ----- De: "Jens Gerlach" <jens.gerlach at fokus.fraunhofer.de> Ã: frama-c-discuss at lists.gforge.inria.fr Envoyé: Vendredi 5 Août 2016 12:58:34 Objet: Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 98, Issue 1 Hello Paul, > > Hello everyone! > I'm completely new in frama-c and I encounter an issue. I try to verify a C code I found in the "FRAMA-C by examples" pdf (the find just out of curioisity, do you mean âACSL by Exampleâ? > algorithm). But when I apply the command line "frama-c -wp test.c test.h", I have this user error : >  > [wp] user error: Can not create output directory '/tmp/wpd596aa.dir/typedâ You could try the Frama-C option â-wp-outâ, e.g.,         "frama-c -wp -wp-out foo test.c test.hâ Does this help? >  > I don't know why it can not create this directory. It is possible to everybody to write in tmp (drwxrwxrwt). >  > Here is some information about my system: > -Frama-c version: Sodium-20150201 > -Linux 64 bits > -Ubuntu 16.04.1 LTS > -OCaml version : 4.02.3 >  By the way, is there a strong reason for you to use the Sodium release? I find the Aluminium better than Magnesium and similarly Magnesium better than Sodium. Regards Jens _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160805/52bfa3bb/attachment.html>