Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Detect Array out of bounds #257

Merged
merged 106 commits into from
Aug 24, 2021
Merged

Detect Array out of bounds #257

merged 106 commits into from
Aug 24, 2021

Conversation

Wherekonshade
Copy link
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