PathCrawler automatically generates test inputs for your function written in ANSI C. The test set will guarantee coverage of all feasible execution paths under the conditions detailed below. Moreover, if you supply an oracle, PathCrawler will also provide the results according to the oracle when the tests are run on instrumented code on our server.
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.
To familiarize yourself with PathCrawler, try the tutorial, which uses these examples. You can then try testing some of the other examples from the Examples page. You should then be ready to try testing your own code, by clicking on Test your code at the top of the Examples page.
Follow 3 steps, explained in more detail below, to generate test-cases:
You must provide the ANSI C source files of the top-level function under test and of all other functions (including library functions) called by the function under test, so that it is possible for PathCrawler to recompile your code using gcc. See below for C constructions not yet treated by PathCrawler. No assembly code must be included in the files. Submit your C source code in a tar (but NOT tar.gz) or zip archive. The main file (including the definition of the function to be tested) may include other files using their relative paths. Absolute paths should not be used.
Indicate the function to be tested and the file containing the definition of this function, with its relative path in the archive.
The context includes
A default test context is automatically constructed by PathCrawler. In this default context
It is very important to check the default test context and modify it if necessary by clicking on Customize test parameters. If you do not do this then PathCrawler may spend a lot of time generating tests which are of no use to you because they do not correspond to realistic inputs for your function and reveal "false-positive" bugs which do not exist under realistic conditions. Here are a few examples:
The example functions in the tutorial and on the Examples page come with examples of test contexts that you can study by clicking on Customize test parameters. Once you have done that, try defining the test context for your code.
Start by restricting the domains of input parameters and enlarging those of variable dimensions, as necessary.
If the list of input parameters contains variables or data-structure elements which you are SURE are not really referenced by the tested function, then you can just remove them from the list. Also, by default all elements of the same array are given the same domain (by using a variable name starting with INDEX in the name of the element). If you want to give a specific domain to certain elements then add those elements as separate parameters.
Note that setting an interval for the dimension of an array which includes the value 0 signifies that the effective parameter may be a NULL pointer in some test-cases (remember that C treats all array inputs as pointers).
Suppose that one input parameter, pt, of the tested function is such a pointer and another input parameter, l, represents the number of elements to treat in the array pointed to by the first parameter. A test-case in which pt is set to 1 and l is set to 3 is likely to provoke a buffer overflow. To ensure that only test-cases which do not provoke a buffer overflow are generated, you must define a precondition to link the dimension of pt to the value of l.
There are three ways to define a precondition in PathCrawler. These mechanisms can be combined but it is easier to start by choosing just one.
PathCrawler can generate inputs to explore all behaviours of your function but it cannot know whether the results are what you expected. That is the role of the oracle. PathCrawler provides a default oracle program which just says that the verdict of each test-case (when run on instrumented code on our server) is unknown. You can change the default oracle in order to calculate another verdict, based on your knowledge of the expected outputs of the tested function. Look at the oracle for Bsearch to see an example (click on Customize test parameters). The default oracle always returns immediately after calling pathcrawler_verdict_unknown. Your oracle should return immediately after having called pathcrawler_verdict_success or pathcrawler_verdict_failure. Your oracle must have exactly the same name and signature as the default oracle. Its arguments are pathcrawler_retres__name of the tested function> for the value returned by the tested function, the input parameters of the tested function (representing their value after execution of the tested function), and the arguments whose name starts with Pre_ representing the values the input parameters had when the tested function was called.
Indeed, the output of the function under test may overwrite the input in some cases (for example, array sorting algorithms will usually overwrite the initial array) and PathCrawler runs the oracle function after the tested function, when the input may be already overwritten. Since the oracle has to examine both input and output data of the tested function, these additional parameters are added to the oracle function signature. The parameters with no prefix are exactly the variables which were provided while calling the function under test, so at the moment when the oracle function is called, they may contain the output values of the function under test. The parameters with the Pre_ prefix will contain (recursive) copies of the input data provided when the function was called. They are not in the scope of the tested function, so cannot be modified. Although this duplication of parameters is systematic, the difference is only important for pointers and arrays (or structures containing them). Note that the oracle can also use the same Pre_ naming convention to refer to the values before the tested function was called of any global variables that it may access.
You can also insert calls to the function pathcrawler_assert in the source-code of the tested function. This feature may be seen as another way to write an oracle. However, unlike the usual oracle described above, pathcrawler_assert may be used at any location in the program under test, and will force PathCrawler to generate test cases to cover both the case where its argument is true and the case where it is is false. pathcrawler_assert takes one argument which is an inequality between expressions over the variables in the scope of the tested function. This inequality is evaluated when the test-case is run and if its value is false then execution of the test-case is stopped and the violation of the assertion (and the line number of the assertion) is indicated in the test-case results.
This defines which items must be covered by the set of tests: set it to all to cover all feasible execution paths or, for a tested function containing loops with a variable number of iterations, it can be set to a positive integer, called k, to cover all k-paths i.e. all feasible execution paths with no more than k iterations of each loop with a variable number of iterations. Note that setting the k-path criterion does not guarantee that no tests with more than k iterations of each loop with a variable number of iterations will be generated. Indeed, PathCrawler may happen to generate such a test because PathCrawler searches for any test to cover a given path prefix, and does not choose the path suffix, so the suffix may contain the kth iteration of a loop. However, PathCrawler will not try to cover any path prefixes containing more than k iterations of a loop with a variable number of iterations.
Once you either click on Test with predefined parameters or confirm the modified test context by clicking Confirm parameters, then test-case generation will begin. Wait until it has finished to examine the results. These include
The following notation is used when displaying paths and partial paths: <filename>:+N (resp. -N) means that the (first) condition at line N of C source file <filename> is verified (resp. not verified) in the current path. So, merge.c:+10 means that the first condition at line 10 of file merge.c is verified and merge.c:-21 means that the condition at line 21 of file merge.c is not verified. Since line 10 of the source code of merge.c (see the examples on the Examples page) is while (i < l1 && j < l2) this line actually contains two sub-conditions. Here +10 actually means that the first condition i<l1 is verified and -10b means that the second condition j<l2 is not verified. In the same way +Nc or -Nc would represent the third condition of line N and so on. When a line contains more than one condition, the line number is suffixed with _1, _2, etc. so, for example, -34_2c refers to negation of the third sub-condition of the second if on line 34.
Within the covered path, the path prefix which PathCrawler was trying to cover when this path was generated is displayed in black type, whereas the rest of the path is displayed in grey type. This makes it easier to see the exploration of the tree of execution paths in the Paths explored page.
If the test-case runs to completion, then the verdict may be unknown if the default oracle is used or, if you supply an oracle, success or failure (with a message indicating the line number of the failure decision in the oracle source code). If the source code contains calls to pathcrawler_assert then the verdict may also be assertion violated (with a message indicating the line number of the relevant assertion). However, if the test case provokes some problem during execution then the verdict may be hung, crashed or interrupt. If PathCrawler detects what seems to be an attempt to read the value of an uninitialised variable during execution of the test-case, then the verdict will be uninit var (note that this can also arise because you mistakenly removed the variable from the list of effective input parameters in the test context). A test-case which covers a path containing a C language construction that PathCrawler was unable to treat is given the verdict untreated and if it covers a path which attempts to read the value of an uninitialised variable then it is given given the verdict uninit var. Cases whose treatment reveals some bug in PathCrawler are given verdict PC bug and they are saved by the server for analysis. If there is some problem during the execution of the oracle, then the verdict will be assert violated in oracle or bug oracle.
The status of path prefixes which are successfully covered by a test-case is covered. Note that the path effectively covered by the test-case which was found may well be longer than the prefix. Prefixes which are successfully proved to be infeasible have status infeasible. In this case, all paths which are extensions of such a prefix are also infeasible. Prefixes which are supposed infeasible because constraint solving timed out have status timeout. Prefixes which are not explored because they violate a call to pathcrawler_assume have status assume violated. A path prefix which has status subsumed was originally covered by a test-case which violated a pathcrawler_assume and so one extension of this path prefix was given the status assume violated. Only the alternative extensions, indicated by the explanatory message subsumed by, could therefore be explored.
The test set generated by PathCrawler is guaranteed to cover all feasible execution paths (or k-paths) providing that:
This is the online version of the PathCrawler test generation tool developed at CEA LIST. To obtain the unrestricted, executable version of PathCrawler, please contact PathCrawler@cea.fr. This usually necessitates the signature of a non-disclosure agreement but no payment in the case of use for research or evaluation.
PathCrawler's principal functionality, and the one demonstrated in this online version, is to automate structural unit testing by generating test inputs for full coverage of the C function under test. Full coverage can mean all feasible execution paths or k-path coverage which restricts the all-path criterion to paths with at most k consecutive loop iterations. These are available in this online version. PathCrawler can also be used to satisfy other coverage criteria (such as 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.
PathCrawler is also available as a plug-in of the Frama-C code analysis platform. As such, it can be used in combination with other Frama-C plug-ins. For example, the SANTE prototype combines PathCrawler with the Frama-C Value Analysis and Slicing plug-ins in order to confirm or invalidate possible run-time errors. Another combination currently being investigated at CEA LIST is the use of PathCrawler to test code annotations expressed in the language used by the E-ACSL plug-in.
PathCrawler is based on a method which was subsequently baptized concolic or Dynamic Symbolic Execution, i.e. it uses a combination of concrete test inputs and symbolic reasoning.
PathCrawler differs in two main ways from other tools based on this combination.
Like other tools, PathCrawler runs the program under test on each test-case in order to recover a trace of the execution path. However, in PathCrawler's case actual execution is chosen over symbolic execution merely for reasons of efficiency and to demonstrate that the test does indeed activate the intended execution path. Unlike tools designed mainly for bug-finding, PathCrawler does not use actual execution to recover the concrete results of calculations that it cannot treat. This is because these results can only provide an incomplete model of the program's semantics and PathCrawler aims for complete coverage of a certain class of programs rather than for incomplete coverage of any program.
Indeed, incomplete coverage often enables many bugs to be detected but PathCrawler was designed for use in more formal verification processes where coverage must be quantified and justified. If a branch or path is not covered by a test, then unreachableness of the branch or infeasibility of the path must be demonstrated. Moreover, using Pathcrawler in the other ways mentioned above also necessitates complete coverage.
The second main difference between Pathcrawler and other similar tools is that PathCrawler is based not on a SAT, linear or SMT solver but on the finite domain constraint solver COLIBRI, also developed at CEA LIST. PathCrawler and COLIBRI are both implemented in Constraint Logic Programming (CLP), which facilitates low-level control of constraint resolution and the development of specialized constraints, as well as providing an efficient backtracking mechanism.
COLIBRI can treat non-linear arithmetic and provides specialized constraints for modular integer arithmetic and floating-point arithmetic. Within PathCrawler, further specialized constraints have been developed to treat bit operations, casts, dynamic allocation, arrays with (any number of) variable dimensions and array accesses using variable index values.
The attempt to correctly treat all C instructions is ongoing but PathCrawler can already treat a large class of C programs.
For more information on how PathCrawler is implemented and has been used, as well as current research directions, please consult the following publications: