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] Function-local static variables and preprocessor variables

  • Subject: [Frama-c-discuss] Function-local static variables and preprocessor variables
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Mon, 21 Jan 2019 18:58:45 +0100
  • In-reply-to: <CAHnaJbvwMbZWLiJ=gdm4Bmi-xELx4MY6qUMGigXRyv29KdAYJg@mail.gmail.com>
  • References: <CAHnaJbvwMbZWLiJ=gdm4Bmi-xELx4MY6qUMGigXRyv29KdAYJg@mail.gmail.com>
Hello,

First of all, thanks for your very valuable feedback on Frama-C.

Le lun. 21 janv. 2019 à 17:20, Rafael Bachmann <rafael.bachmann.93 at gmail.com>
a écrit :

> Hello,
> I had mostly good experiences applying Frama-C(WP). But I found 2 issues
> which (in my opinion) may encourage/enforce commonly discouraged
> programming style:
>
>    1. When declaring array size, static const is not const enough.
>    Instead, literals or preprocessor defines must be used. This is how gcc
>    also handles the situation (
>    https://stackoverflow.com/questions/13645936/variably-modified-array-at-file-scope-in-c
>    ).
>    However, clang/LLVM however accept the following snippet:
>    static const size_t BUFFER_SIZE = 10;
>    int arr[BUFFER_SIZE];
>    I gather that this has to do with VLAs? Understandably hard to support
>    (especially as it is not mandatory as per C standard), but I personally
>    would like to at least have the option to use static const's instead of
>    preprocessor literals.
>
>
This has indeed mainly to do with the fact that C11 does not recognize a
const (be it static or not) variable as an integer constant expression even
though 6.6§10 leaves open the possibility to have other kinds of constant
expression, than the one mandated by the paragraphs before. Note that, on
the other hand, an enumeration constant is an integer constant expression,
so that

enum { BUFFER_SIZE=10U };
int arr[BUFFER_SIZE];

is a perfectly valid C11 program, and is accepted by Frama-C.


>
>    1. Function-local static variables are supported, but they are not
>    bound in the function contract. Effectively, I cannot use them for the
>    function specification:
>    #include <limits.h>
>    #include <stdint.h>
>    /*@ requires *counter* < UINT64_MAX;
>        ensures \result > \old(*counter*);
>    */
>    uint64_t millis() {
>        // works fine if counter is global, not local
>    *    static* uint64_t *counter* = 0;
>        return counter++;
>    }
>    I see that CIL transforms the local statics to
>    $functionname_variablename, but renaming my logic variable accordingly did
>    not work either.
>    This forces me to raise the scope of function-local statics to global
>    statics, unless I am overlooking something here. Regardless, I think this
>    case should be documented (or is it?).
>
>
This is indeed an issue (I'm afraid it is not really documented except on
the archives of this mailing list). ACSL currently does not have any
construction to deal with that It might be possible to open up the
possibility of type-checking contracts in an environment where the static
variables of the function are known, but this not technically that easy and
it would not solve all issues with static variables. In particular, this
change will not help when you're writing a function contract in a .h for a
function whose implementation
is using a static variable that only exists in the .c. For that, as
explained in this stackoverflow question:
https://stackoverflow.com/questions/50386182/frama-c-function-calls-and-static-variables,
you might be able to have some results by using a (global) ghost variable
to store the address of
your static variable, and use it in the contracts, but I fear that it can
quickly become awkard.



> Apart from these (I may be wrong, usually am), I had difficulties finding
> good documentation regarding floating point numbers.
> This habilitation: https://hal.inria.fr/tel-01089643/document contains
> many very good examples, none of which I can reproduce (the author uses Coq
> sometimes, but in other cases gappa suffices). On my machine, the
> verification simply fails. Might something be wrong with my Frama-C
> installation?
>
>
I don't think there's anything wrong with your installation. The
habilitation is 4 years old, and mentions that the given examples have been
developed over several years. Sadly, it's quite probable that they are
simply not compatible anymore with the newest Frama-C versions

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190121/d780b618/attachment.html>