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] Small function on buffer doesn't verify

  • Subject: [Frama-c-discuss] Small function on buffer doesn't verify
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 31 May 2010 12:55:25 +0200
  • In-reply-to: <4BFFE4CE.4030904@inria.fr>
  • References: <1273591300.4338.8.camel@iti27> <4BFFE4CE.4030904@inria.fr>
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