Skip to content

Add CBMC proof for DHCPProcess IPv4 #918

New issue

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

#

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

Already on GitHub? # to your account

Jump to bottom
Merged
merged 12 commits into from
Jun 22, 2023
Merged

Add CBMC proof for DHCPProcess IPv4 #918

merged 12 commits into from
Jun 22, 2023

Conversation

tony-josi-aws
Copy link
Member

Description

This PR adds CBMC proof to DHCPProcess()

Test Steps

cd test/cbmc/proof/
python3 prepare.py
cd <test_case>
make

Checklist:

  • I have tested my changes. No regression in existing tests.
  • I have modified and/or added unit-tests to cover the code changes in this Pull Request.

Related Issue

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@moninom1

This comment was marked as outdated.

# to view
@tony-josi-aws
Copy link
Member Author

Can you mention which function along with DHCPProcess is getting validated in this proof?

@moninom1, only DHCPProcess is validated. The changes to vDHCPProcessEndPoint is just refactoring changes.

@tony-josi-aws tony-josi-aws merged commit 5b0d45b into FreeRTOS:dev/IPv6_integration Jun 22, 2023
# for free to join this conversation on GitHub. Already have an account? # to comment
Reviewers

@shubnil shubnil shubnil approved these changes

@moninom1 moninom1 moninom1 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.
3 participants
@tony-josi-aws @moninom1 @shubnil