* 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>
This change adds the OTA demos and required dependencies and helper components .
* Add demos , configs and project files
* Add subscription manager
* Add HTTP utils
* Submodules the OTA LTS 3.0 Library.
* Add OTA pal
* Minor update to the UART write function in the IAR/QEMU/MPS2 demo project. Now the function checks to ensure there is space in the Tx buffer before writing to the buffer - although this does not appear to be necessary in QEMU it is more correct.
* Update main.c
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
* Disregard coverage data without a function_name field set
* Fix calling make on subdirectories
* Undefine FORTIFY_SOURCE when running without ENABLE_SANITIZERS
* Add queue and semaphore unit tests
* Update FreeRTOS-Kernel submodule revision
* Add test for backlogged auto-reset timer
Must call vTimerDemoIncludeBacklogTests() to activate.
* Fix little style issues
- Update to new header
- Add parentheses (style)
- Remove trailing space accidentally introduced
* Don't verify full clearing of backlog
The timer task should be free to process the stop request without a
specific requirement to work through the backlog of callbacks for the
stopped timer. The timer task should be allowed to cancel the entire
backlog, part of it, or none of it. In other words, once the
application sends the stop request, it should not depend on receiving
any more callbacks, even backlogged ones.
The only requirement here is that the timer stop as requested.
Co-authored-by: Joseph Julicher <jjulicher@mac.com>
Co-authored-by: Cobus van Eeden <35851496+cobusve@users.noreply.github.com>
* Put XLEN into .o files.
Makes it easier to work on voth RV32 and RV64 binaries side-by-side.
* Let the debugger disable HTIF use.
* Makefile now links the binary at BASE_ADDRESS
I need this so I can easily generate the appropriate binaries for
riscv-tests/debug. Unfortunately there doesn't seem to be any good
mechanism to externally define values for lds files, so I'm running it
through the C preprocessor.
Co-authored-by: Joseph Julicher <jjulicher@mac.com>
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.
* Add RISC-V demo for the spike simulator.
* Figuring out what the header checker wants.
* Fix more headers.
* Ignore htif.c and htif.h for header checks.
These files are already stamped with BSD-3-Clause, which I'm not allowed
to remove. There are numerous other files with the same license in
FreeRTOS, so I assume this is fine.
* Use proxy syscalls for RV32.
Looks like spike won't be changed to make htif character writes work
propery for RV32.
This is now an even closer copy of the version in opensbi, which is
arguably strictly better.
* Support RV64 builds to use with spike.
OpenOCD does not currently support debugging 64-bit FreeRTOS, but now
that I have a target to test hopefully that will be remedied shortly.
* Tweak rv32 instructions.
This way you can have separate cross-tools installations that can
coexist side by side.
Co-authored-by: Joseph Julicher <jjulicher@mac.com>
* 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
an assertion is added to ensure a new task's priority is less than the
confirmed max. The CBMC proof for TaskCreate needs to include this assumption
in order to not assert and fail. Since this is now enforced in the code
we can add an assumption to the proof that a task must be created with a
priority smaller than the configured max.
* Added event_groups.c Unit Test.
* Formatted and more comments.
* Formatted
* Split some test cases and add comment and coverage tag.
* Update test cases.
* Remove xEventGroupDelete Invalid Input test case, since the implementation does not handle this.
When gcov outputs into it's intermediate json format, sometimes it marks blocks as unexecuted but also sets an execution count != 0. In this case, the "count" field is correct, but the "unexecuted_block" field is incorrect.
When outputting lcov formatted coverage data in filtercov.py, only output a branch coverage data lines (BRDA) with a "-" for the "taken" field when both count==0 and unexecuted_block==true in the input gcov json intermediate file.
