--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2019 ---
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>