--- layout: fc_discuss_archives title: Message 121 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function on buffer doesn't verify



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