Document implementation-defined behavior following GCC #1415
Conversation
| @@ -17,3 +17,10 @@ _NB! This list is likely incomplete._ | |||
|
|
|||
| See [PR #1414](https://github.com/goblint/analyzer/pull/1414). | |||
|
|
|||
| 2. Implementation-defined behavior usually follows GCC. | |||
There was a problem hiding this comment.
For a well-documented list of assumptions, this is saying absolutely nothing and undermines the point of such documentation. It's like "Goblint assumes what GCC assumes, but sometimes also not."
The assumption should specifically be what is given as an example below for integer casts to smaller types doing modulo or whatnot.
|
|
||
| > > The result of, or the signal raised by, converting an integer to a signed integer type when the value cannot be represented in an object of that type (C90 6.2.1.2, C99 and C11 6.3.1.3). | ||
| > | ||
| > For conversion to a type of width N, the value is reduced modulo 2^N to be within range of the type; no signal is raised. |
There was a problem hiding this comment.
But this is only true with sem.int.signed_overflow being assume_wraparound, no?
There was a problem hiding this comment.
No, in general. The conversion unsigned to signed always behaves like this for us.
There was a problem hiding this comment.
Nothing here is saying that it's conversion from unsigned though. The quote just says "converting an integer".
This is exactly why we need to make the assumptions very explicit.
There was a problem hiding this comment.
Iirc unsigned types are integers and signed integers are called signed integers in the standard parlance.
There was a problem hiding this comment.
What standard parlance? The C standard very explicitly talks about "signed integers" and "unsigned integers". I couldn't find anywhere in the standard that defines "integer" to mean "natural number".
Standard mathematical terminology also has "integer" including negative numbers.
Having the extra word "unsigned" explicitly in our assumptions only makes things clearer and less ambiguous to everyone. One shouldn't need to be fluent in C standardese to understand our assumptions.
If the wording is not clear/precise enough for us the developers, then it definitely won't be to anyone else (users, students, etc).
As a follow-up of #1414 this documents one further instance where we make assumptions (implementation-defined behavior follows GCC).