I’m trying to perform test on freeRTOS, in order to do that I have followed the readme.md files under FreeRTOS\FreeRTOS\Test (e.g. FreeRTOS\FreeRTOS\Test\CBMC\README.md).
And I have issues following the readme file.
e.g. running command cmake --build ~/build/freertos --target all-proofs results in:
ninja: error: unknown target ‘all-proofs’
And many more.
Is there a more detailed tutorial on how to run the tests on FreeRTOS?
Update:
I have run the command python prepare.py and when I run nmake inside the folder where Makefiles where generated I get this:
…\Makefile.common(128) : fatal error U1104: Unknown text function ‘dir’
Seems to be some issues with the generated Makefiles.
I apologize for the trouble you have had.
The instructions to use CMake are out of date. You can still follow the python based build instructions in the repository and they should work.
Also, since these proofs are compiled as 32-bit binaries, you might need to install 32-bit versions of libraries. If you are using linux/mac then this command should do the trick: sudo apt-get install gcc-multilib.
Thanks for the message, I am working on windows, by installing 32 bit version of libraries, you mean 32-bit version of the tools that I have installed, right?
For windows shouldn’t I use nmake instead of make?
Also below the result of running make cbmc and nmake cbmc:
Yes, on windows, you should use nmake and not make.
However, I highly recommend that you use something like WSL or a virtualbox to run these tests in Linux based environments. Windows based build has atrophied a bit and needs re-work - we are working on this.
