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.

Sign up for GitHub

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

Jump to bottom

Encode that malloc may return NULL in C (weaken postcondition) #1239

Open
wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

Encode that malloc may return NULL in C (weaken postcondition) #1239

wants to merge 1 commit into from

Conversation

wandernauta
Copy link
Contributor

The new field 'fallible' on the NewPointerArray AST node stores whether you are guaranteed to get a new pointer array (false) or merely probably get one (true).

Updates tests, fixes #1233.

@wandernauta
Encode that malloc may return NULL in C
c5c9cf6 
The new field 'fallible' on the NewPointerArray AST node stores whether you are guaranteed to get a new pointer array (false) or merely probably get one (true).

Updates tests, fixes utwente-fmt#1233.
sakehl
sakehl approved these changes Sep 23, 2024
View reviewed changes
Copy link
Contributor

@sakehl sakehl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems reasonable to me. When implementing malloc I indeed did not consider to have it possibly fail.

superaxander
superaxander approved these changes Sep 27, 2024
View reviewed changes
Copy link
Member

@superaxander superaxander left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good, I'll probably replace this with the version from my branches later though where I have a separate NonNullPointer type which I need for use in some axioms. (it becomes a Pointer type in Viper instead of an Option[Pointer])

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@superaxander superaxander superaxander approved these changes

@sakehl sakehl sakehl approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

VerCors optimistically assumes malloc always succeeds in C
3 participants
@wandernauta @superaxander @sakehl