Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>