Commit Graph

9 Commits (a691c6199eebd1f8a8c434ac3e658337bfda6bf6)

Author SHA1 Message Date
Aniruddha Kanhere 86117b5173
CBMC proof for vProcessGeneratedUDPPacket (#203)
* Add Proof

* Update

* Update the proof

* Update the proof

* Clean-up

* Clean-up v2

* Update freertos_api.c

* update stub
5 years ago
Aniruddha Kanhere 3c573ad091
CBMC proof for ulARPRemoveCacheEntryByMac (#198)
* Add Proof

* update

* Delete ulARPRemoveCacheEntryByMAC_harness.c

* Changes after Mark's comments

* Update after @yanjos-dev's comment

* Remove confusing variable name

* Update ulARPRemoveCacheEntryByMac_harness.c
5 years ago
Aniruddha Kanhere 6eba275f89
CBMC: Add proof for vSocketBind (#202)
* Add proof

* Update

* Update MakefileCommon.json

* Undo changes

* Undo changes in MakefileCommon.json

* Update Makefile.json

* Update Makefile.json

* Update Makefile.json

* Change v1

* Change v2
5 years ago
Aniruddha Kanhere f32a0647c8
Remove CBMC patch which is not used anymore (#187)
* Delete 0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch

* Delete 0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch
5 years ago
Aniruddha Kanhere 08af68ef90
Remove dependency of CBMC on Patches (#181)
* Changes to DHCP

* CBMC DNS changes

* Changes for TCP_IP

* Changes to TCP_WIN

* Define away static to nothing

* Remove patches

* Changes after Mark's comments v1

* Update MakefileCommon.json

* Correction!
5 years ago
Aniruddha Kanhere f2611cc5e5
MISRA compliance changes in FreeRTOS_Sockets{.c/.h} (#161)
* MISRA changes Sockets

* add other changes

* Update FreeRTOSIPConfig.h

* Update FreeRTOSIPConfig.h

* Update FreeRTOSIPConfig.h

* Update FreeRTOSIPConfig.h

* correction

* Add 'U'

* Update FreeRTOS_Sockets.h

* Update FreeRTOS_Sockets.h

* Update FreeRTOS_Sockets.c

* Update FreeRTOS_Sockets.h

* Update after Gary's comments

* Correction reverted
5 years ago
Aniruddha Kanhere f11bcc8acc
Fix a Bug and corresponding CBMC patch (#84)
* Update remove-static-in-freertos-tcp-ip.patch

* Update FreeRTOS_TCP_IP.c

* Update remove-static-in-freertos-tcp-ip.patch

* Update remove-static-in-freertos-tcp-ip.patch

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
5 years ago
Aniruddha Kanhere cb7edd2323
Sync with a:FR (#75)
* AFR sync

* AFR sync: CBMC

* AFR sync: CBMC: remove .bak files

* AFR sync: CBMC: more cleanup

* Corrected CBMC proofs

* Corrected CBMC patches

* Corrected CBMC patches-1

* Corrected CBMC patches-2

* remove .bak files (3)

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
5 years ago
AniruddhaKanhere d95624c5d6
Move CBMC proofs to FreeRTOS+ directory (#64)
* move CBMC proofs to FreeRTOS+ directory

* Failing proofs corrected

* ParseDNSReply proof added back

* removed queue_init.h from -Plus/Test

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
5 years ago