diff options
| author | Carl Lundin <53273776+lundinc2@users.noreply.github.com> | 2020-12-14 17:35:36 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-14 17:35:36 -0800 |
| commit | b035e0321f2cd4cf03e56711e8cd86910abe2bbf (patch) | |
| tree | 6dc35e8883a719a27183963a05908c60bf80ddf9 | |
| parent | bff2f04c5f872ed7fa3ec0dec7716fb78127c8fc (diff) | |
| download | freertos-git-b035e0321f2cd4cf03e56711e8cd86910abe2bbf.tar.gz | |
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.
| -rw-r--r-- | FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch | 6 | ||||
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch index cfd0ac916..566544706 100644 --- a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch +++ b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch @@ -1,5 +1,5 @@ diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c -index d2e27e55a..4dd164da6 100644 +index b01dfd11f..b219b599a 100644 --- a/FreeRTOS/Source/queue.c +++ b/FreeRTOS/Source/queue.c @@ -395,7 +395,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue, @@ -9,5 +9,5 @@ index d2e27e55a..4dd164da6 100644 - configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); + /* configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); */ - /* Allocate the queue and storage area. Justification for MISRA - * deviation as follows: pvPortMalloc() always ensures returned memory + /* Check for addition overflow. */ + configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) > xQueueSizeInBytes ); diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json index 70deca778..2788b60ec 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json @@ -17,6 +17,8 @@ # EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF # MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND # NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN # CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE # SOFTWARE. # |