--- layout: fc_discuss_archives title: Message 121 from Frama-C-discuss on May 2010 ---
On Fri, 2010-05-28 at 17:44 +0200, Claude Marche wrote: > The problem is that the C typing is too loose so that even if the user > annotated a variable with const, it is not statically guaranted that the > value cannot change: you can take the address of the variable, cast it > to a non-const pointer, and then change its value. So, even if the C > norm says it is a mistake to modify a const memory location, the > compiler does not check it. This is nasty indeed. I see now that consts aren't what I believed them to be. This compiles without warnings on gcc: void foo(int* p) { (*p) = 0; } int main() { const int a = 1; foo((int *)&a); return 0; } > So what should be done is: > > 1) consider const as true constants, as expected > > 2) generate an additional VC to each assignment, to check whether the > assigned location is writable. > > 1) without 2) would be unsound. > > To support 2) I think we would need to introduce a distinction between > two variant of the \valid predicate, one being "valid for reading", the > other being "valid for both reading and writing". Another option is to keep const unsupported. Most C programmers use macros instead of consts anyway. In this case however, there should be a solution to support expressions such as (0..BUFF_SIZE). For example, a parser could introduce a withspace after .. before calling the preprocessor. Pascal Cuoq wrote that there's a problem with the gcc preprocessor that prevents (0..BUFF_SIZE) from being correctly parsed. On the other hand, keywords to specify IN, OUT, INOUT parameters as in Ada would be very useful. For pointers, this could be accomplished by predicates \valid_in, \valid_out, \valid_inout. This would improve readability of the specifications, serve as additional interface documentation, and prevent bugs resulting from uninitialized or overwritten values. \valid would then be equivalent to \valid_out or could be dropped. consts being passed by reference would then require a \valid_in predicate. -Boris