--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Function-local static variables and preprocessor variables



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>