Skip to content

Detect Array out of bounds#257

Merged
sim642 merged 106 commits intogoblint:masterfrom
vandah:array_oob
Aug 24, 2021
Merged

Detect Array out of bounds#257
sim642 merged 106 commits intogoblint:masterfrom
vandah:array_oob

Conversation

@Wherekonshade
Copy link
Copy Markdown
Contributor

This PR fixes #198
We introduced detection for out of bounds accesses in arrays. This works for both statically and dynamically sized arrays. With interval analysis enabled we can also properly detect out of bounds accesses inside for loops or other constructs taken into account by the interval analysis.
We added regression tests for the following cases:

  • basic
  • pointer
  • multidimensional
  • dynamically sized
  • pointer to arrays of different sizes
  • arrays within structures

The warnings fall into the behavior category and in the new warning system, they can be disabled with --disable dbg.warn.behavior along with other Behavior warnings.
The warnings are also tagged as May/Must according to the certainty with which we know that the situation occurs.
The warning can also specify if the access happened PastEnd, BeforeStart or Unknown

Wherekonshade and others added 24 commits July 1, 2021 11:25
also renames Warning -> WarningWithCertainty and WarnType -> Warning
also remove the array type because arrayoob is under UB
also uses concatenation instead of redundant sprintf
and replace unused parameters with `_`
also adds optional location to warn_each
this eliminates the need to specify the regexes separately in
update_suite.rb
later it would probably be nice if the categories were parsed and
checked there

also changes formatting of the warning tags
also adds optional msg argument and removes string params from unknown
and debug
@sim642 sim642 merged commit a7ef19f into goblint:master Aug 24, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

practical-course Practical Course at TUM student-job

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Detect Array out of bounds

7 participants