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] Unknows Pragma



I downloaded the last frama-c source and added the patch, make and 
installed.

But using the option example is giving me some errors I can not solve 
(quite new to linux bash and pipes :) )

MyCommand:
frama-c -cpp-command "gcc -C -E -I. < %1 | grep -v pragma\ LINK_INFO > 
%2" -val HC12DIN.c

The output:
[kernel] preprocessing with "gcc -C -E -I. < %1 | grep -v pragma\ 
LINK_INFO > %2  HC12DIN.c"
gcc: no input files
[kernel] user error: failed to run: gcc -C -E -I. < 'HC12DIN.c'   | grep 
-v pragma\ LINK_INFO > '/tmp/HC12DIN.c8c11de.i'
                      you may set the CPP environment variable to select 
the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "HC12DIN.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.

seems like gcc is complaining, but I don't know how to solve this.

best regards, Patrik

On 28.5.2010 15:36, Pascal Cuoq wrote:
>> How do I get frama-c to understand these pragmas?
>>
>> #pragma LINK_INFO DERIVATIVE   "MC9S12C32"
>> #pragma LINK_INFO OSCFREQUENCY "16000000"
>>      
> That's easy, if by "understand" you mean "ignore":
> grep them out at pre-processing (after pre-processing,
> in case these pragmas are found inside include files).
>
> Use the option:
>
> -cpp-command "gcc -C -E -I. -<  %1  | grep -v pragma\ LINK_INFO>  %2"
>
> in addition to what you were already doing.
>
> You may find that the option -cpp-command does not
> handle the tokens %1 and %2 as documented.
> That's an unfortunate bug. But since you are already setting
> yourself up for compiling Frama-C from sources with
> your exotic target architecture, it won't be too much additional
> trouble to apply the following patch :
>
> --- src/kernel/file.ml	(revision 8516)
> +++ src/kernel/file.ml	(working copy)
> @@ -498,7 +498,7 @@
>   	  in
>   	  (* Format.eprintf "-cpp-command cmd2=|%s|@\n" cmd2; *)
>             let cmd3 =
> -	    String.sub cmdl (percent2 + 2) (String.length cmdl - percent2 + 2)
> +	    String.sub cmdl (percent2 + 2) (String.length cmdl - (percent2 + 2))
>             in
>   	  (* Format.eprintf "-cpp-command cmd3=|%s|@\n" cmd3; *)
>             Format.sprintf "%s%s %s %s%s%s" cmd1
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>