chinglee-iot
7adb08eff5
Update single core CMBC and unit test ( #1045 )
...
This PR fixes CBMC and unit test for single core FreeRTOS in the FreeRTOS-Kernel PR - https://github.com/FreeRTOS/FreeRTOS-Kernel/pull/716 .
- xYieldPendings and xIdleTaskHandles are now an array. Update in FreeRTOS unit test.
- Update CBMC patches.
2023-07-24 15:42:20 +05:30
kar-rahul-aws
6682dbbc5b
Update submodule pointer for Kernel V10.6.0 ( #1037 )
...
* Update submodule pointer for Kernel V10.6.0
* Update commit hash
* Fix failed CBMC proofs
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Update manifest.yml
* Update hash commit to match submodule
---------
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com>
2023-07-18 09:28:02 +05:30
Gaurav-Aggarwal-AWS
3c09383fab
Fix CBMC proof failures ( #946 )
...
* Fix CBMC proof failures
These were introduced in PR #620 .
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Update manifest
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
---------
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
2023-03-06 15:15:38 +05:30
Kareem Khazem
408c3841ea
Add CBMC proof-running GitHub Action ( #924 )
...
This commit adds a GitHub Action that runs the CBMC proofs upon every
push and pull request. This is intended to replace the current CBMC CI.
2023-03-03 14:35:42 -08:00
Kareem Khazem
c7b3124565
Use CBMC XML output to enable VSCode debugger ( #912 )
...
Prior to this commit, CBMC would emit logging information in plain text
format, which does not contain information required for the CBMC VSCode
debugger. This commit makes CBMC use XML instead of plain text.
Co-authored-by: Mark Tuttle <tuttle@acm.org>
2023-01-13 13:03:06 -08:00
jasonpcarroll
6f7f9fd9ed
[AUTO][RELEASE]: Bump file header version to "202212.00"
2022-12-10 01:17:30 +00:00
jasonpcarroll
b9f2248c5b
[AUTO][RELEASE]: Bump file header version to "202211.00"
2022-12-01 00:34:31 +00:00
Soren Ptak
8424589ed1
FreeRTOS Windows Simulator Build Changes and LTS 2.0 Update ( #872 )
...
* Update mbedtls to version v3.2.1
* Adjust include paths for github workflow
* Update FreeRTOS+TCP to v3.1.0
* Add initial VS project files for Kernel, +TCP, and mbedtls
* winpcap: Consolidate to a single copy of WinPcap
* Downgrade library projects to VS 2019. Add heap_4 to kernel.
* Remove *.vcxproj.user files and add to gitignore
* Disable unwanted kernel config options
* Update FreeRTOS+TCP and Kernel include paths
* Update FreeRTOS+TCP Windows Minimal sln
* Remove .suo and .vcxproj.user files
* Update mbedtls transport implementations for mbedtls v3.2.1
* Fix typo in mbedtls_freertos_port.c
* Update vcxproj files for +TCP, Kernel, Mbedtls
* Fix typo in name WindowSimulator -> WindowsSimulator
* Add wpcap lib to FreeRTOS+TCP.vcxproj
* Update FreeRTOS+TCP Minimal Demo for Windows Simulator
* Mask MSVC string function warnings
Aad _CRT_SECURE_NO_WARNINGS preprocessor definition.
* Move projects to their own directories to make VisualStudio happy
* mbedtls_freertos_port.c: Fix formatting?
* Add coreHTTP, Logging libs. Adjust dependencies
* Disable FreeRTOS Kernel malloc failed hook
* Update coreHTTP Plaintext demo
* Rename / relocate transport interface implementations
* Remove old VS project files
* Remove extra core_http_config.h files
* Remove extra FreeRTOSConfig.h files
* Remove extra FreeRTOSIPConfig.h files
* Remove old mbedtls_config.h files
* Remove old FreeRTOSConfig and core_http_config files
* Update HTTP Mutual Auth Demo build files
* Fix transport_plaintext.h include name
* Update HTTP_Plaintext demo build files
* Update CoreHTTP_S3_Download VS project files
* Update HTTP_S3_Upload demo build files
* Update CoreHTTP_S3_Download_Multithreaded demo build files
* Add GithubActions builds for FreeRTOS+ CoreHTTP Demos
* Update S3DownloadHTTPExample.c to be compatible with mbedtls 3.x
* Update GithubActions FreeRTOS+ config file
* Combine core_pkcs11_config.h files into a single one
* Add corePKCS11 VS project file
* Update corePKCS11 WinSim demo project and build files
* Update corePKCS11 library to version 3.5.0
* Modifiying demos to build using static libraries
* Adding a header file
* Two more demos
* Update corePKCS11 demo code and auto-format
* Downgrade corePKCS11 library build file to v142 / VS 2019
* Speed up CI builds with selective submodule initialization
* Separate corePKCS11 demo into it's own job.
* Remove WIN32.vcxproj and WIN32.vcxproj.filters files
* Remove old configuration header files
Partially reverts 73829ced6061e4584e521185178a61b4a437c5e0
* Revert unwanted coreHTTP demo changes
* Changing include paths for demos
* Adding an include
* MQTT WoflSSL Demo update
* wolfSSL Demo changes
* Config changes for MQTT Demos
* Initial Device Defender demo update.
* Initial Device Shadow demo update.
* Update mbedtls_transport_pkcs11 for Mbedtls 3.x
* Update corePKCS11 MQTT Mutual Auth demo
* Add a default definition of SdkLog
* Update CorePKCS11 + MQTT Mutual Auth demo sln name
* Build all configs of coreHTTP demos
* Update coreSNTP Demo build files.
* Update coreSNTP Demo sln name
* Update FreeRTOS+TCP Posix demo
* Update FreeRTOS+TCP Qemu ARM MPS2 AN385 Demo
* Update FreeRTOS+TCP Demo Github Actions builds
* Update Fleet Provisioning WinSim Demo build files
* Remove mbedtls_pk_info_t references from mbedtls_pk_pkcs11.h
* Restore / update the FreeRTOS+TCP Minimal WinSim demo
* Initial Jobs demo update.
* Fix jobs demo build.
* Initial OTA over HTTP demo update.
* Initial OTA over MQTT demo update.
* Ota_Over_Mqtt_Demo build fix.
* OTA over MQTT demo fix.
* Update HTTP demo solution file name for CI.
* Update Github actions workflow to old HTTP demo names.
* Update coreSTNP demo to old solution name.
* Fix defender demo / fix mbedtls config to use threading alt.
* Add MBEDTLS_CONFIG_FILE definition to each config
* Fix config file name.
* MQTT Mutual auth fixes.
* Fix job demo.
* Device shadow demo fixes.
* Fix coreSNTP demo not setting alt threading functions for mbedtls.
* Enable Static allocation, Add default hooks for FreeRTOS Kernel and +TCP
* Add xPlatformIsNetworkUp platform function to FreeRTOS+TCP hooks
* Enable runtime statistics in the Windows Simualator Kernel config
* Revert "Fix coreSNTP demo not setting alt threading functions for mbedtls."
This reverts commit 9069707519561ca8136d58c0f18fb176c9050a1d.
* Revert mbedtls threading related config changes
* Add xPlatformIsNetworkUp function prototype
* Remove boileplate FreeRTOS kernel and +tcp hooks
* Refactor device defender demo for clarity
* Add wait loop calling xPlatformIsNetworkUp
* Add missing vPlatformInitLogging function
* Add vPlatformInitLogging and vLoggingPrintf defitions to logging headers
* Updating the FreeRTOS_Plus_CLI_with_Trace_Windows_Simulator
* Updating the FreeRTOS_Plus_Reliance_Edge_and_CLI_Windows_Simulator demo
* Updates to the FreeRTOS_Plus_WolfSSL_Windows_Simulator demo
* Fixing wrong include path
* Upating FreeRTOS_Plus_WolfSSL_FIPS_Ready_Windows_Simulator demo
* Update coreMQTT WinSim demos to print start and end condition.
* Modifiying repos updated as part of the CLI demo GitHub workflow
* Removing duplicate functions from the FreeRTOS_Plus_TCP_Minimal_Windows_Simulator demo
* Updated FreeRTOS_Plus_TCP_UDP_Mode_CLI_Windows_Simulator demo
* Updating corePKCS11_MQTT_Mutual_Auth_Windows_Simulator Demo to call the static function that creates task
* Fix log message using unitialized string in MQTT Multitask demo.
* Fixing a broken extern function
* Fixing a typo extern function name
* Added a reference to coreHTTP
* Fixing a pre-processor issue in the OTA_Over_Http_Demo
* Updating the MQTT_Mutual_Auth_Demo_with_BG96 demo
* Updating the MQTT_Mutual_Auth_Demo_with_HL7802 demo
* Changes to the MQTT_Mutual_Auth_Demo_with_SARA_R4 demo
* Fix demos for CI.
* Adding the source path to the CBMC proofs for FreeRTOS+TCP
* Spell check fixes, adding words to lexicons
* Fixing a typo
* Add arg to skip prompt in setup script.
* Update paths of script to be relative to the file.
* Changing manifest.yml file to point to corePKCS11 3.5.0
* Added CI markers to cellular demos.
* Fix cellular demo flow.
* Fix celullar demos.
* Initial TCP sockets wrapper rework - will break things.
* First cellular demo fix for new sockets wrapper.
* Minor fix to cellular sockets wrapper.
* Fix mbedtls bio using FreeRTOS Plus TCP call.
* Clean up BG96 demo project files.
* Update HL7802 demo.
* Fix SARA R4 demo for new sockets wrapper.
* Fix Device Defender, Device Shadow, and Fleet PRovisioning.
* Fix Jobs demo.
* Fix OTA over HTTP demo.
* Fix OTA over MQTT demo.
* Fix HTTP mutual auth demo.
* Fix OTA over MQTT demo endianness.
* Fix OTA over HTTP demo endianness.
* Fix HTTP Plaintext demo.
* Fix HTTP S3 download demo.
* Fix plaintext transport
* Fix OTA demos.
* Fix OTA demos.
* Fix OTA HTTP demo.
* Fix HTTP S3 Download multithreaded demo.
* Fix HTTP S3 Upload demo
* Fix corePKCS11 Mutual Auth demo.
* Updating MQTT_Mutual_Auth
* Update pkcs11 setup script.
* Updating the MQTT_Basic_TLS Demo
* Organize PKCS11 demos project.
* Updating MQTT_Keep_Alive demo
* Clean up SNTP demo.
* Updated MQTT_Multitask demo
* Updated MQTT_Plain_Text
* Updating the MQTT_Serializer Demo
* Updating corePKCS11_MQTT_Mutual_Auth_Windows_Simulator
* Updating coreSNTP_Windows_Simulator
* Clean up demo projects.
* Add markers to PKCS11 mutual auth demo.
* Fix Fleet Provisioning demo script.
* Fix SNTP demo solution.
* Fix coreSNTP project files.
* Fix Fleet Provisiong script.
* Fix fleet provisioning script.
* Fix demo config template.
* Fleet provisioning demo markers.
* Updating MQTT_Mutual_Auth_wolfSSL demo and the transport_wolfSSL file
* Fixing FreeRTOS_Plus_TCP_Echo_POSIX
* Fixing CLI and Trace Demos
* Fixing TCP_ECHO_POSIX demo
* Adding a word to the lexicon
* Remove unneeded files.
* Update github workflows to use Ubuntu 20.04.
* Change OTA demo target names to RTOSDemo for OTAE2E tests.
* Fixing Headers
* Updating headers
* Two more headers
* Adding words to the lexicon
* Whitepsace
* Ignore mbedtls config file for header check.
* Removing FreeRTOS Header from the mbedtls_config_v3.2.1.h file
* Fix bug in lPKCS11PkMbedtlsCloseSessionAndFree. Add doxygen api docs.
* Update lexicon.txt
* Fix spelling
* Apply suggestions from code review
Co-authored-by: jasonpcarroll <23126711+jasonpcarroll@users.noreply.github.com>
* Add return code comment for p11_ecdsa_ctx_init
* Rename WindowsSimulator folder to VisualStudio_StaticProjects.
* Remove references to coroutines
* Fix mbedtls_pk_pkcs11.c
* Update to LTS 2.0 submodule pointers (#880 )
* Update submodule pointers to LTS 2.0
* Initial coreMQTT 2.1.1 update.
* Update AWS demos for coreMQTT 2.1.1
* Fix deprecated macro for coreMQTT demos.
* Fix keep alive demo.
* Fix plaintext demo.
* Fix MQTT wolfSSL demo.
* Fix MQTT PKCS11 demo.
* Remove duplicate functions.
* Fix Mutual auth demos for Cellular.
* Fix OTA demos.
* Fix header of plaintext demo config.
* Set writev to NULL for OTA demos.
* Fix mbedlts config for OTA demos.
* Fix spelling.
Co-authored-by: Jason Carroll <czjaso@amazon.com>
* Removing blank line
* Fix jobs demo race condition.
* Fix race condition from WinPCap network interface.
* Update lexicon.
Co-authored-by: Paul Bartell <pbartell@amazon.com>
Co-authored-by: Jason Carroll <czjaso@amazon.com>
Co-authored-by: Paul Bartell <paul.bartell@gmail.com>
Co-authored-by: jasonpcarroll <23126711+jasonpcarroll@users.noreply.github.com>
2022-11-29 14:21:09 -08:00
akshayutture
856d0e8363
Created a generic portmacro.h file in the CBMC include folder ( #847 )
...
* Created a generic portmacro.h file in the CBMC include folder instead of using the default MSVC-MingW one. This allows each proof to define the portmacro constants it needs and cover all code in the Task Scheduler
* Removed the license text from the portmacro file
* Fix CI checks
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Fix spell check
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: Gaurav-Aggarwal-AWS <33462878+aggarg@users.noreply.github.com>
2022-09-26 14:43:54 -07:00
Angelo Nakos
8e881fe73c
Remove litani submodule and update README to include a section on CBMC ( #829 )
...
* Remove Litani submodule
* Update README to include section on CBMC
* Update litani references in Python run script
2022-07-25 13:52:10 -07:00
johnrhen
43defa566c
Apply release changes to main branch ( #759 )
...
* Update History.txt and README.md for December release (#744 )
* Update History.txt and README.md for release
* Bump mbedtls submodule to v2.28.0 (#745 )
* Patch project files for mbedtls (#751 )
* Apply group 1 patches
* Apply patches for group 2
* Update project files for mbedTLS new version
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Fix warnings in projects
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
* Fix warnings in HTTP_S3_Download demo
Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com>
* Update changelog and history for corePKCS11 update (#752 )
* Update submodule pointer and manifest.yml for corePKCS11 (#754 )
* Update readme and history.txt to show that Sigv4 is a newly added library (#756 )
* Revert update to v143 of VS toolset (#757 )
* [AUTO][RELEASE]: Bump file header version to "202112.00"
* Update file headers to satisfy core checks
Co-authored-by: Muneeb Ahmed <54290492+muneebahmed10@users.noreply.github.com>
Co-authored-by: Gaurav Aggarwal <aggarg@amazon.com>
Co-authored-by: johnrhen <johnrhen@users.noreply.github.com>
2021-12-23 10:16:27 -08:00
Mark Tuttle
21f2799392
Always prepare source tree for cbmc proofs ( #743 )
...
Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
2021-12-17 10:59:10 -08:00
aggarg
ecd1a8f9f1
[AUTO][RELEASE]: Bump file header version to "202111.00"
2021-11-13 02:37:14 +00:00
Mark Tuttle
0390b0fc9b
Add CBMC viewer configuration files ( #683 )
...
* Revert cbmc-viewer flags
* Add cbmc-viewer configuration files
* Repair CBMC patch to prvCopyDataToQueue
Authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
2021-09-13 21:23:35 -04:00
tianmc1
176f1cae02
[AUTO][RELEASE]: Bump file header version to "202107.00"
2021-07-24 00:32:35 +00:00
alfred gedeon
ae92d8c6ee
Add uncrustify github workflow ( #659 )
...
* Add uncrustify github workflow
* Fix exclusion pattern
* fix find expression
* exclude uncrustify files
* Uncrustify common demo and test files
* exlude white space checking files
* Fix EOL whitespace checker
* Remove whitespaces from EOL
* Fix space at EOL
* Fix find spaces at EOL
Co-authored-by: Archit Aggarwal <architag@amazon.com>
2021-07-22 14:23:48 -07:00
Dan Good
b6624fa44d
Remove or rework assumptions in queue proofs ( #603 )
...
This commit is paired with another to queue.c in the kernel. To
accomodate changes in newer versions of CBMC, the
--pointer-overflow-check is removed.
2021-06-04 15:42:14 -04:00
Aniruddha Kanhere
1bc759d413
Aws only files spell check ( #593 )
...
* Added spell check
* All words
* Add a missing word
* Fix header checks
* Fix header checks v1
* Fix header check v2
* Updated freertos link in header
* Fixed afr link in the header
* Fix last of header checks
* Update the spell check script to check amazon licensed files only
* Fixed paths and added comments
* Try with modified repo
* Add inplace substitute option to sed
* Use official repo as the spell checker source
* Add vendor file to the ignored list
Co-authored-by: root <root@ip-172-31-5-28.us-west-2.compute.internal>
2021-05-13 16:07:56 -07:00
Carl Lundin
d0d633a524
Reintroduce quarantined CBMC test ( #516 )
...
This CBMC test would go over the memory limit of most hosts, causing the
kernel to kill the process. With larger memory capabilities, this can be
re-enabled.
2021-04-07 12:26:03 -07:00
Carl Lundin
aaece95529
Update Tasks.c CBMC Proofs to Latest Code ( #547 )
...
* Fix Tasks.c patch, line numbers were out of sync and patching was
broken.
* Add assumption to TaskCreate proof that a task's priority is less than
the configured max.
With the introduction of
9efe10b805
2021-04-02 14:17:26 -07:00
Carl Lundin
f6dff3fea3
Add Litani to run CBMC proofs ( #501 )
...
Update to out of source makefile build and add run-cbmc-proofs.py
CBMC proofs can now be run with Litani with the command
"./run-cbmc-proofs.py"
Based on commits:
* 1646301 - Ignore CBMC proof failures, fail the build later (4 months ago) <Kareem Khazem>
* 7e8c91a - Fix Makefile prerequisite symbol for CBMC proofs (4 months ago) <Kareem Khazem>
* bee04be - Enable CBMC proofs to run in CI (4 months ago) <Kareem Khazem>
Found in https://github.com/FreeRTOS/FreeRTOS-Plus-TCP
2021-02-12 10:21:07 -08: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
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
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
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
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
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
