PathCrawler plug-in

PathCrawler automatically finds test-case inputs.


PathCrawler-online Result Summary

What's it for ?

PathCrawler's principal functionality is to automate structural unit testing by generating test inputs which cover all the feasible execution paths of the C function under test.

It can also be used to satisfy other coverage criteria (like k-path coverage restricting the all-path criterion to paths with at most k consecutive loop iterations, branch coverage, MC-DC,...), to generate supplementary tests to improve coverage of an existing functional test suite or to generate just the tests necessary to cover the part of the code which has been impacted by a modification.

PathCrawler can be used to ensure, and demonstrate, code coverage when this is imposed by a standard. However, it can also be used even when code coverage is not imposed, as a convenient and rigorous way of debugging code fragments during development.

Apart from generating tests to ensure coverage, PathCrawler can be used to detect all run-time errors, anomalies such as uninitialized variables or integer overflows and unreachable code.

Another use is to cross-check one implementation against another (previous version or implementation for another platform) or to check conformity with a specification coded in C. PathCrawler will either find test-cases to demonstrate any differences between the results of the two codes or else demonstrate that no such differences exist.

The path tests generated by PathCrawler can also be used to measure the effective execution time of an uninterrupted task in a real-time application, and get an accurate estimate of the longest execution time.

Can I try it?

The PathCrawler-online web service makes a restricted version of PathCrawler freely available for evaluation and teaching. The user uploads the C source code to be tested and the server displays the test-cases generated by PathCrawler and a detailed justification of the coverage. The user can define the test context and browse the results using specialized interfaces in the form of web-pages. The server allows many test-case generation sessions to be run in parallel in a completely robust and secure way.

Automatic testing tools allow huge savings but they do not exonerate the user from thinking carefully about what they want testing to achieve. To successfully use PathCrawler, the user must provide not only the full source code (with C stubs for missing functions), but also must set the test parameters and program the oracle. This demands a different "mindset" from that used for manual unit testing and so PathCrawler-online proposes numerous code examples to help the user get started and a tutorial based on some of these examples.

Users who have tried PathCrawler-online and would like to use the PathCrawler plug-in are invited to contact PathCrawlera_d_ligaturecea.fr to obtain the executable code. This usually necessitates the signature of a non-disclosure agreement but no payment in the case of use for research or evaluation.

Usage

The plug-in is activated with the following command line:

frama-c -pc [options] -main <tested function> <file>.c

For further details, see the user manual.

Known restrictions

Note that PathCrawler is based on constraint resolution, which is NP-complete. This means that finding a test or demonstrating the infeasibility of the path to be covered, cannot always be guaranteed to terminate within a reasonable time. When this occurs, PathCrawler reports that the corresponding path is probably infeasible but that this cannot be demonstrated. This problem is usually only posed by functions under test which implement numerical algorithms in which the branch conditions involve the results of complex calculations.

A different problem is posed by functions which have too many feasible execution paths for all-path coverage to be practical, even when the effective calling context is taken into account. Indeed, the number of execution paths suffers from a combinatorial explosion in the presence of loops with input-dependent limits, cascades of conditional instructions, function calls, etc. For these functions, another coverage criterion may have to be used. Various specialised criteria are currently being developed.

Finally, there are certain constructions in C which PathCrawler cannot treat yet (Menu Documentation, Section "Limitations of PathCrawler").