Skip to content

Commit 788b6c9

Browse files
committed
Add assumption about malloc blob initialization
1 parent ff6f52c commit 788b6c9

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

docs/user-guide/assumptions.md

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,5 +34,20 @@ _NB! This list is likely incomplete._
3434

3535
See [PR #1511](https://github.com/goblint/analyzer/pull/1511).
3636

37+
3. Memory allocated with `malloc` is initialized before reading.
38+
39+
[C11's N1570][n1570] at J.2 states that
40+
41+
> The behavior is undefined in the following circumstances:
42+
>
43+
> - [...]
44+
> - The value of the object allocated by the `malloc` function is used (7.22.3.4).
45+
46+
after a long list of undefined behaviors.
47+
48+
Goblint does not report reading from uninitialized memory allocated by `malloc`.
49+
50+
This affects the `base` analysis.
51+
3752

3853
[n1570]: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf

0 commit comments

Comments
 (0)