Basic application illustrating use of SymEx-VP with RIOT.
To build and use them follow the [instructions in the RIOT repository][riot-setup]. If all prerequisites are installed, application can simply be compiled using:
$ make -C <application>
Afterwards, a compiled application can be executed with SymEx-VP.
Assuming that SymEx-VP is in $PATH, simply run the following command
to execute one of the provided applications:
$ make -C <application> simulate
By default, applications are executed with a five minute time budget and SymEx-VP stops executing upon encountering the first error.
As described in the SymEx-VP repo, there are basically three aspects regarding the employment of VP-based concolic software testing. The following listing briefly explains how these aspects are implemented in the RIOT context.
- Symbolic Inputs: The RIOT applications provided in this
repository generate symbolic inputs explicitly via the
SymbolicCTRLperipheral. Functions for interacting with this peripheral are available in./include/symex.h. - Termination Points: Termination points are also declared
explicitly by invoking
vp_symbolic_ctrl(SYMEX_EXIT)from./include/symex.hafter performed tests are completed. - Path Analyzers: For clarity, no specific path analyzer is
employed in this repository. However, we discuss such path analyzer
in other work [1] [2]
[3]. The example applications provided here are
presently only able to detect invocations of RIOT's panic handler
(e.g. on failing assertions) as errors through the provided
panic.cfile.