len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-15 09:17:44 -04:00
Code Issues Projects Releases Packages Wiki Activity
3073 commits 3 branches 99 tags 214 MiB
Commit graph

32 commits

Author SHA1 Message Date
Joseph Julicher
da9b9a800d [AUTO][RELEASE]: Bump file header version to "202012.00" 2020-12-15 11:50:37 -07:00
Joseph Julicher
2e2ba99a74 [AUTO][RELEASE]: Bump file header version to "202012.00" 2020-12-15 10:20:29 -07:00
Carl Lundin
b035e0321f
Re-add missing license files caused by PR #471 and fix patches (#477) 
* Re-add missing license files caused by PR #471.
* Fix proof patch.
 2020-12-14 17:35:36 -08:00
Carl Lundin
cf39a90d6d
Fix CBMC patches. (#471) 
* Fix CBMC patches.
 2020-12-12 21:00:03 -08:00
Ming Yue
9d937aa0ab
Remove duplicate WinBase.h and Windows.h. (#458) 2020-12-09 13:40:20 -08:00
Cobus van Eeden
c6f4284b76
Update kernel submodule pointer to version 47338393f (#456) 
* Update kernel submodule pointer to version 47338393f

* Fix patches.

Co-authored-by: Carl Lundin <lundinc@amazon.com>
 2020-12-08 15:44:14 -08:00
David Chalco
07f3cbafee [AUTO][RELEASE]: Bump file header version to "202011.00" 2020-11-10 14:45:34 -08:00
Nathan Chong
bc54c6bc10
Syntactic proof changes to track 10.4.1 changes (#322) 
All changes restricted to comments/formatting.
 2020-10-06 13:17:29 -07:00
Aniruddha Kanhere
8979b3817b
Remove CBMC proofs of TCP source code (#325) 
* Add CMock back for the integration tests.

* Removed the CBMC proofs for TCP

* Add the windows files to allow the CBMC proofs to run
 2020-10-06 13:03:52 -07:00
David Chalco
7bcc5b48b1
Move ./scripts --> FreeRTOS/Test/CMock/scripts (#298) 2020-09-24 17:17:34 -07:00
David Chalco
190c9e780d
Inititial stub for cmock tests (#297) 2020-09-24 17:06:28 -07:00
Cobus van Eeden
d5862dbe01
Sync back V10.4.1 (#282) 
* Move Kernel submodule pointer to 10.4.1
* Update version number to V10.4.1 (#281)
 2020-09-17 17:16:33 -07:00
David Chalco
89d475e9b1
Update Version number to 10.4.0 (#237) 2020-09-10 19:40:24 -07:00
Ravishankar Bhagavandas
584517d467
cbmc: Add patch to remove overflow assert (#232) 2020-09-01 09:26:25 -07:00
Nathan Chong
669084ee8f
List proofs and signoff (#194) 2020-08-27 11:59:12 -07:00
Cobus van Eeden
4a026fd703
Move forward Kernel submodule pointer (#218) 
* Move forward Kernel submodule pointer
* Fixing patches for CBMC proofs
* Update proofs to assume cTxLock != 127
* Update proofs to assume cRxLock != 127
 2020-08-26 23:50:09 -07:00
Cobus van Eeden
a691c6199e
Updating queue.c patches for CBMC proofs (#216) 2020-08-26 13:07:15 -07:00
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
 2020-08-03 16:45:10 -07:00
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!
 2020-08-01 16:38:23 -07:00
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
 2020-07-29 15:38:37 -07:00
Nathan Chong
8e36bee30e
Prove buffer lemmas (#124) 
* Prove buffer lemmas

* Update queue proofs to latest kernel source

All changes were syntactic due to uncrustify code-formatting

* Strengthen prvCopyDataToQueue proof

* Add extract script for diff comparison

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>
 2020-07-21 09:51:20 -07:00
Nathan Chong
529c481c39
Add VeriFast kernel queue proofs (#117) 2020-07-02 12:55:20 -07:00
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>
 2020-06-03 16:52:31 -07:00
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>
 2020-05-28 10:11:58 -07:00
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>
 2020-05-05 09:57:18 -07:00
markrtuttle
95ae7c6575
Change cbmc-viewer invocation in CBMC makefile (#63) 
* Exclude FreeRTOS/Demo from CBMC proof reports.

The script cbmc-viewer generates the CBMC proof reports.  The script
searches source files for symbol definitions and annotates source
files with coverage information.  This patch causes cbmc-viewer to
ignore the directory FreeRTOS/Demo containing 348M of data.  The
script now terminates in a few seconds.

* Make report default target for CBMC Makefile.

Modify the Makefile for CBMC proofs to generate the report by default
(and not just property checking) and modify property checking to
ignore failures (due to property assertions failing) and terminating
report generation.

Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
 2020-04-28 21:27:45 -07:00
Yuhui Zheng
d421ccc89f
Reword readme.md under ./Test. (#61) 2020-04-25 16:57:35 -07:00
Carl Lundin
3841286598
Removed a:FR reference. (#60) 2020-04-25 16:56:54 -07:00
AniruddhaKanhere
4db195c916
Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56) 
ParseDNSReply is to be added in the next PR.
 2020-04-21 15:40:08 -07:00
Yuhui Zheng
5b9777e11e A readme file to introduce what ./Test directory is about. 2020-03-31 14:21:53 -07:00
Yuhui Zheng
211bb4cbd9 Ignore whitespace when working with patches. 2020-03-31 14:21:53 -07:00
Yuhui Zheng
8156f64d1c Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is. 
The commit ID in aws/amazon-freertos is 0c8e0217f2a43bdeb364b58ae01c6c259e03ef1b.
 2020-03-31 14:21:53 -07:00