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

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 98, Issue 1
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Fri, 5 Aug 2016 10:58:34 +0000
  • In-reply-to: <mailman.13.1470391207.728.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.13.1470391207.728.frama-c-discuss@lists.gforge.inria.fr>
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