Skip to content

[SV-COMP'18 4/19] Constrain the malloc/alloca size to fit our object:offset encoding #1993

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

Closed
wants to merge 1 commit into from

Conversation

tautschnig
Copy link
Collaborator

See #311 for an extended discussion.

Do not merge: this needs to be adjusted to fit the command-line options or ongoing work to get rid of these object/offset limitations.

@tautschnig tautschnig requested a review from kroening as a code owner April 3, 2018 13:45
@tautschnig tautschnig self-assigned this Apr 5, 2018
@smowton
Copy link
Contributor

smowton commented Apr 9, 2018

Given the split is runtime-configurable, should these use an intrinsic __CPROVER_max_allocation_size() which goto-convert replaces with the actual value, rather than hard-coding something?

@NlightNFotis
Copy link
Contributor

Hi @tautschnig.

Do we still want this around? Is this something that can be merged after rebasing on develop (and fixing of the merge conflicts) or should we close the PR?

@martin-cs
Copy link
Collaborator

There is now __CPROVER_max_malloc_size which might do the job. Maybe this PR is obsolete?

@TGWDB
Copy link
Contributor

TGWDB commented Jul 9, 2021

Closing as this appears to be redundant/orphaned. If you believe this is erroneous please reopen.

@TGWDB TGWDB closed this Jul 9, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants