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

Fixes/calloc #145

Merged
merged 23 commits into from
Nov 25, 2020
Merged

Fixes/calloc #145

merged 23 commits into from
Nov 25, 2020

Conversation

ivanazuzic
Copy link
Contributor

This should fix #135:

  • The created Blobs keep track of their creator (so-called origin, which can be either Calloc or Malloc)
  • The idea is to know that the Blob created by calloc, which has a value Bot is actually supposed to be 0, because calloc zero-initializes the allocated place
  • The type argument was returned to the signature of the update_offset function from the value domain because it's necessary to know the type of the zero which is produced by calloc
  • Calloc used to take only one argument n * size and now those two are separated so calloc takes n and size
  • Tests for calloc have been added
  • Type was added as parameter to the eval _offset function of the value domain to make possible to read 0 when something was allocated by calloc and is not initialized yet
  • Functions bot_value, init_vaue and top_value have been moved from base analysis to valueDomain. There a top_value function already existed and now, not to keep two top_value functions, a combination is kept in the valueDomain only (it resembles more to the one from the base analysis, which was more specific about arrays). The functions is_mutex_type and is_immediate_type have been moved together because they were only used by the functions that now went to the value domain.
  • Partition arrays parameter has been added to the calloc tests.

src/analyses/base.ml Outdated Show resolved Hide resolved
src/cdomains/valueDomain.ml Outdated Show resolved Hide resolved
src/cdomains/valueDomain.ml Outdated Show resolved Hide resolved
src/cdomains/valueDomain.ml Outdated Show resolved Hide resolved
@ivanazuzic ivanazuzic added the sv-comp SV-COMP (analyses, results), witnesses label Nov 24, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Problematic handling of calloc
3 participants