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

  • Subject: [Frama-c-discuss] EVA: understanding behaviors for undefined functions
  • From: Andre.OLIVEIRAMARONEZE at cea.fr (Andre Maroneze)
  • Date: Tue, 10 Jan 2017 09:39:12 +0100
  • In-reply-to: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com>
  • References: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com>
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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170110/32ecab63/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3797 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170110/32ecab63/attachment.bin>