--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 98, Issue 1



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>