--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on January 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] EVA: understanding behaviors for undefined functions



Hi Andre,

Thank you very much for your suggestion. I was getting warnings about
preprocessor options before, but never got around to investigating them.
These are the warnings I used to get:

*[kernel] warning: your preprocessor is not known to handle option `
-nostdinc'. If pre-processing fails because of it, please add
-no-cpp-gnu-like option to Frama-C's command-line. If you do not want to
see this warning again, use explicitely -cpp-gnu-like option.*
*[kernel] warning: your preprocessor is not known to handle option `-dD'.
If pre-processing fails because of it, please add -no-cpp-gnu-like option
to Frama-C's command-line. If you do not want to see this warning again,
use explicitely -cpp-gnu-like option.*
*[kernel] warning: trying to preprocess annotation with an unknown
preprocessor.*

After using the `-cpp-extra-args` options, these have now gone.


Regards
Faraz.



On Tue, Jan 10, 2017 at 1:39 AM, Andre Maroneze <
Andre.OLIVEIRAMARONEZE at cea.fr> wrote:

> As a minor remark, I'd suggest replacing `-cpp-command` with
> `-cpp-extra-args`, e.g. in your example `-cpp-extra-args="-I
> ${CSMITH_HOME}/runtime -Dvolatile= "` might be sufficient.
>
> -cpp-command should only be necessary when using a preprocessor other than
> GCC or Clang. -cpp-extra-args is a more recent option, hence why it is not
> always mentioned in old tutorials and blog posts.
>
> On 10/01/2017 01:01, Faraz Hussain wrote:
>
> [note] I am using Silicon-20161101, on Ubuntu 16.04. The command executed
> is: *frama-c -metrics -metrics-libc  -cpp-command "gcc -C -Dvolatile= -E
> -I ${CSMITH_HOME}/runtime"  -machdep x86_64  wrong25.c*
>
>
> --
> André Maroneze
> Ingénieur-chercheur CEA/LIST
> Laboratoire Sûreté et Sécurité des Logiciels
>
>
> _______________________________________________
> 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/20170110/fa38ae37/attachment.html>