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