Re: Signed int overflow behavior in the security context

[Robert Dewar <dewar at adacore dot com>]

Brooks Moses wrote:

> I think you and Robert may be talking about different contexts.  I'm 
> pretty sure (though not positive) that Robert is talking about the case 
> after an undefined operation has occurred.  I'm not sure if you're 
> talking about that, or talking about normal program operation.
>
> In any case, for the "after an undefined operation" context, probably a 
> more useful way to think about it is this: After an undefined operation, 
> there are no guarantees about what code the program will be executing. 
> In particular, there is no guarantee that it will actually be executing 
> the code that you wrote.  And thus, any argument that assumes that it's 
> doing so -- for instance, an argument that it's accessing the same 
> location in memory twice, and thus should get the same result both times 
> -- is relying on incorrect axioms.

Yes, good summary ... that's exactly right
> This comes about because of a more fundamental and crucially important 
> observation: There is _never_ a guarantee about the particular code that 
> a program will be executing -- if there were, this would be assembly 
> language, and optimization would be illegal.  The C standard, if it is 
> anything like the Fortran standard, does not say anything at all about 
> what machine code will be executed.  The guarantee is that the code that 
> is being executed will have the _same result_ as the code that was 
> written, so long as the written code was legal.

Indeed the C standard is similar to the Fortran standard in this respect.
> It thus seems pretty easy to see why undefined results can cause 
> programs to act strangely.  The compiler is free, under the standard, to 
> write whatever code it wants so long as that code produces the "right" 
> answer to legal operations.  There's often no good reason to expect that 
> this code will still produce the "right" answer to illegal operations. 
> C is not assembly language.

Indeed?
> Does that logic work for you?

We will see :-)
> - Brooks