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

Remove redundant TCP includes in FreeRTOS CBMC proofs #1254

Merged
merged 2 commits into from
Aug 23, 2024
Merged

Remove redundant TCP includes in FreeRTOS CBMC proofs #1254

merged 2 commits into from
Aug 23, 2024

Conversation

moninom1
Copy link
Member

@moninom1 moninom1 commented Aug 23, 2024 •
edited
Loading

Description

  • Remove includes from FreeRTOS cbmc proofs which are not needed.
  • Remove redundant aws_freertos_tcp_verification_access_tcp_define.h file.
  • Remove redundant aws_freertos_ip_verification_access_ip_define.h file.

Test Steps

CBMC proofs

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 moninom1 requested a review from a team as a code owner August 23, 2024 05:49
@moninom1 moninom1 changed the title Remove unnecessary TCP includes in FreeRTSO cbmc proofs Remove unnecessary TCP includes in FreeRTOS cbmc proofs Aug 23, 2024
@kar-rahul-aws
Copy link
Member

In addition to this we can also remove this file aws_freertos_ip_verification_access_ip_define.h, since this API publicProcessIPPacket is not getting used in the tests?

@moninom1 moninom1 changed the title Remove unnecessary TCP includes in FreeRTOS cbmc proofs Remove redundant TCP includes in FreeRTOS CBMC proofs Aug 23, 2024
@kar-rahul-aws
Copy link
Member

This folder https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS/Test/CBMC/windows can also be removed .

@tony-josi-aws
Copy link
Member

tony-josi-aws commented Aug 23, 2024 •
edited
Loading

This folder https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS/Test/CBMC/windows can also be removed .

I believe these files are required by the kernel MSVC port. And it is not available on the system we use to run CBMC. Hence, those dummy files were created. I had to create similar ones for +TCP in this PR: FreeRTOS/FreeRTOS-Plus-TCP#1113

@moninom1 moninom1 merged commit c304913 into FreeRTOS:main Aug 23, 2024
50 checks passed
@moninom1 moninom1 deleted the tcp_update branch August 23, 2024 06:48
moninom1 added a commit that referenced this pull request Aug 23, 2024
@moninom1
Remove redundant TCP includes in FreeRTOS CBMC proofs (#1254)
66e1e57 
* Remove unnecessary TCP includes

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

@tony-josi-aws tony-josi-aws tony-josi-aws approved these changes

@aggarg aggarg aggarg 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.
4 participants
@moninom1 @kar-rahul-aws @tony-josi-aws @aggarg