Does it have test reports for each Kernel tag?

Is there a test result report available for the Kernel after the tag?

A number of checks, including unit tests, are run on every PR using GitHub Actions. Any failed check blocks the PR. The results of those can be accessed from GitHub UI. There is no other test report. What do you want to do with it?

I am attempting to run the tests in the project. I want the reports as a reference to ensure I am on the right track.
Thank you, for the help!

Which tests are you trying to run?

If you share your results, we can try to help.

“I am currently running CBMC proofs for the Task Create. The proof’s description mentions that it may take some time to run and that the output will be written to a file called cbmc.txt. The text VERIFICATION SUCCESSFUL is expected to appear at the end of this file. However, I cannot locate the cbmc.txt file. I assume that the generated cbmc.xml file is the result report. Can you please confirm if my understanding is correct?”

And into html/html/index.html


CBMC report

Coverage

Coverage: 0.99 (reached 140 of 141 reachable lines)

Coverage Function File
1.00 (6/6) [vListInitialise](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/list.c.html#49) [Source/list.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/list.c.html)
1.00 (2/2) [vListInitialiseItem](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/list.c.html#89) [Source/list.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/list.c.html)
1.00 (20/20) [prvAddNewTaskToReadyList](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html#2018) [Source/tasks.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html)
1.00 (17/17) [prvCreateTask](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html#1619) [Source/tasks.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html)
1.00 (11/11) [prvInitialiseTaskLists](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html#5997) [Source/tasks.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html)
1.00 (9/9) [xTaskCreate](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html#1717) [Source/tasks.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html)
1.00 (4/4) [pvPortMalloc](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/include/cbmc.h.html#112) [Test/CBMC/include/cbmc.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/include/cbmc.h.html)
1.00 (3/3) [vPortFree](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/include/cbmc.h.html#122) [Test/CBMC/include/cbmc.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/include/cbmc.h.html)
1.00 (19/19) [harness](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c.html#39) [Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c.html)
1.00 (8/8) [pcNondetSetString](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html#73) [Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html)
1.00 (3/3) [pxNondetSetTaskHandle](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html#62) [Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html)
1.00 (2/2) [vNondetSetCurrentTCB](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html#33) [Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html)
1.00 (3/3) [vPrepareTaskLists](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html#41) [Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html)
1.00 (3/3) [vSetGlobalVariables](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html#52) [Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Test/CBMC/proofs/Task/TaskCreate/tasks_test_access_functions.h.html)
0.97 (30/31) [prvInitialiseNewTask](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html#1792) [Source/tasks.c](file://///wsl.localhost/Ubuntu-20.04/home/tgrigorov/FreeRTOS/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/html/html/Source/tasks.c.html)

Warnings

Functions omitted from test (expected):

  • pxPortInitialiseStack
  • vPortEnterCritical
  • vPortExitCritical
  • vPortGenerateSimulatedInterrupt

Other warnings:

  • loop identifier prvInitialiseNewTask.1 provided with unwindset does not match any loop

Errors

None

Looks OK?

Yes, this report looks good as there is no error.

We will update the README as needed. Thank you for reporting it.

1 Like

For your information, PR#1196 has been created to update README.

Thank you.