Choose any of the programs from the example menu to see an example of test generation. We provide predefined test parameters for each example. You can also elect to customize the test parameters first.
Select an example

Guidelines for code upload

  • Submit your C source code in a tar or zip archive.
  • Indicate the function under test and the main file under test with its relative path in the archive.
  • The main file may include other files using their relative paths.
  • Absolute paths should not be used.
Upload archive
Test function
File under test

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:

  1. upload the source code and identify the function to be tested;
  2. define the test context;
  3. automatically 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

  • The list of scalar variables and data structure elements which are effective input parameters of the tested function, including global variables and those pointed to by the formal parameters
  • If an array has one or more variable dimensions and it has elements which are effective input parameters, so that the number of effective input parameters depends on the variable dimensions of the array, then these dimensions are also considered as effective input parameters
  • The input domain for each of these parameters within which PathCrawler will select a value for each test-case
  • The preconditions: further restrictions on legitimate input parameter values, including relations between the values of different parameters
  • The oracle
  • The coverage criterion

A default test context is automatically constructed by PathCrawler. In this default context

  • All scalar variables and data structure elements which may be referenced by the tested function are counted as effective input parameters. These include the formal arguments of the function under test and any global variables.
  • The input domain is any value within the declared C type of the parameter. The default input domain of array dimensions is set to the declared domain, if there is one, and otherwise the interval 0..1. Note that this allows PathCrawler to construct test-cases including NULL pointers.
  • The precondition accepts as a legitimate test-case all combinations of values in the parameter domains.
  • The oracle always returns unknown

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:

  • do you want test-cases with NULL pointer inputs, i.e. in which the dimension of a pointer is set to 0 ?
  • do you want test-cases in which an array with a variable dimension is either a NULL pointer or has only one element (dimension = 0 or 1) ?
  • if a variable represents the speed of a vehicle in km/h, do you really want a test-case in which it is set to 500000 ?
  • do you really want test-cases which provoke integer overflows in the calculations ?

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.

List of input parameters and their domains

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).

Definition of the preconditions

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.

  • Write a C function which returns 1 if the test-case values satisfy the precondition and 0 if not. Include this precondition function in the file containing the definition of the tested function. In order for PathCrawler to recognise the precondition function, it must be called precond_name of the tested function and have the same signature as the tested function, except that its return type is int. See the MergePrecond example (click on Customize test parameters). Note that the precondition does not construct input values but just tests the validity of given combinations. Use the pathcrawler_dimension function to restrict dimension values. It is not currently possible to add a precondition definition to an ongoing PathCrawler session. If your source code did not include a precondition for the tested function and, when inspecting the default test context, you decide that you need a precondition and would like to write it in C, then stop your PathCrawler session, add the precondition function to your source code, start a new PathCrawler session, check that PathCrawler has found your precondition and check the box to indicate you want PathCrawler to use it.
  • Certain preconditions can be defined as formulae in a subset of 1st order logic. See the Merge example (click on Customize test parameters). Note that in this example, there are 2 types of precondition: simple preconditions and quantified preconditions. The latter apply to several elements of the same array; the element index is "universally quantified" and must be given a name which starts with INDEX. Array dimensions can be referred to in preconditions by using a term of the form dim(name of the array).
  • You can insert calls to the function pathcrawler_assume in the source-code of the tested function. pathcrawler_assume takes one argument which is an inequality between expressions over the variables in the scope of the tested function and which may also use pathcrawler_dimension.


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.

Coverage criterion

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 confirmation that test generation terminated normally or, if not, an indication of what went wrong in case you need to correct the test context and try again
  • the inputs, outputs, path covered and verdict of each test-case.

Display of paths and partial paths:

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.

Verdict of the test-case:

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.

You may also want to look at further information:

  • The C source file which can be used to run each test-case.
  • Path predicate: the conditions which the inputs must respect in order to activate the same path as the one covered by this test case.
  • Symbolic outputs: these are the output values expressed in terms of the input values. Along with the path predicate, they form a "specification" of the calculation implemented by this path.
  • Statistics (such as duration) of the test generation session and of each test case.
  • The order of exploration of all the paths and partial paths during test generation and, for each one, whether it was covered by a test-case, found to be infeasible or could not be treated for some reason.

Status of a path prefix:

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:

  • constraint resolution does not time out,
  • no run-time errors are found in the tested function,
  • test generation terminates normally within the limits on time and space which we are obliged to impose
  • and the tested function does not contain certain constructions which PathCrawler does not treat well yet, such as:
    • reading data from console or files (scanf, fscanf,...): simulate instructions such as scanf by defining a global array to store the file content and replacing the call to scanf by an array access
    • the floating-point type float (but double is treated),
    • explicit or implicit casts other than those between integer types (e.g. pointer casts, certain uses of unions),
    • assembly language code,
    • pointers to functions on input,
    • formal parameters which are functions,
    • recursive structures on input,
    • pointers of type void* on input,
    • functions with a variable number of arguments,
    • recursive functions,
    • volatile variables,
    • functions from a standard C library or any other function whose source code is not available may not be treated correctly,
    • some conversions of the type of integer constants: we can add the letter L (or l) at the end of the constant to ensure that the type long is used, and we can add U (or u) to specify the attribute unsigned. But we cannot write a positive constant greater than the capacity of unsigned long int type or a negative constant not representable in long int type because then the meaning is unclear and PathCrawler cannot guarantee good behaviour.

This is the online version of the PathCrawler test generation tool developed at CEA LIST. To obtain an unrestricted, executable version of PathCrawler, notably for evaluation or use in research, please contact .

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: