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: rafael.bachmann.93 at gmail.com (Rafael Bachmann)
  • Date: Mon, 21 Jan 2019 17:20:04 +0100
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.
   2. 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?).

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 would appreciate any help, thanks in advance!

Rafael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190121/a2c75e22/attachment.html>