diff options
| author | Carl Lundin <53273776+lundinc2@users.noreply.github.com> | 2021-04-07 12:26:03 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-07 12:26:03 -0700 |
| commit | d0d633a5243e7fb07693e16ee6449abecf645997 (patch) | |
| tree | 175b64fd06af1081d8112042604c6bc6d393c376 | |
| parent | 8dafa9fe4a87062ca26ca184a90b2b06d8d1dbe6 (diff) | |
| download | freertos-git-d0d633a5243e7fb07693e16ee6449abecf645997.tar.gz | |
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.
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json index 2788b60ec..d2d1ab1f3 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/Configurations.json @@ -30,6 +30,15 @@ "ENTRY": "TaskResumeAll", "DEF": [ + { "default": + [ + "FREERTOS_MODULE_TEST", + "PENDED_TICKS=1", + "'mtCOVERAGE_TEST_MARKER()=__CPROVER_assert(1, \"Coverage marker\")'", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0" + ] + }, { "useTickHook1": [ "FREERTOS_MODULE_TEST", |