--- layout: fc_discuss_archives title: Message 2 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 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