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] First time with Frama-C

Hello,

just a few complements to David's excellent answer:

2017-02-03 8:21 GMT+01:00 David MENTRÉ <dmentre at linux-france.org>:
>
> Usually I give all the C source files on the command line, something like:
>
>   frama-c-gui <needed command line options> file1.c file2.c ...
>
> Most of the time, you'll need to use appropriate options to properly
> find and parse your header files.
>

While debugging parsing errors, I'd suggest to use the text-based interface:

frama-c [-cpp-extra-args="-DFOO -I/external/lib/path ..." ] file1.c file2.c ...

error message are much easier to read on the terminal. Once you're
confident that your files are accepted by Frama-C, you can easily
switch to frama-c-gui, as both accept the same set of options. In
addition, giving the appropriate set of pre-processing options might
be a little tricky. A possibility is to tweak your Makefile rules to
produce .i (pre-processed) files from .c, instead of .o. A priori, you
just need to add options -C (stop after pre-processing) and -E (keep
comments, in particular ACSL annotations) to the set of options used
to produce the .o in order to produce .i.

> the precise definition of your target platform regarding C types and
> endianess, i.e. big or little endian, size of int, short, long, etc. I
> would start with default definition for x86(_64?) platform and then
> tweak those parameters once you are comfortable with the use of the tool.
>

The default architecture (called machdep in Frama-C's terminology is
x86_32. Unless you know that some part of the code heavily depends on
the target architecture, it's indeed a good thing to start with the
default. If you really need to target another machdep, this recent
stackoverflow answer gives some direction on how to do it, but this is
an advanced topic:
https://stackoverflow.com/questions/41982091/syntax-error-in-frama-c-due-to-custom-machdep/41983384#41983384

>> 2. since there is an extern variable that is used in a bit of assembly
>> code, a single c source file complains of undefined reference.
>
> Frama-C plug-ins cannot analyze assembly code. You'll have to write some
> C code or ACSL contracts to be able to analyze those parts of your code.
>

If the code is written according to gcc's extended asm syntax, a
minimal contract (assigns clause) will be generated by default (since
Frama-C 13 Aluminium).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile