Input Specification about crest HOT 4 CLOSED

The complete list of CREST_int, CREST_unsigned_char, etc., can be found in 
header file 
//src/libcrest/crest.h.  (This file can be viewed online at 
http://code.google.com/p/crest/source/browse/trunk/src/libcrest/crest.h .)

Currently, there are six such functions for getting symbolic inputs, one for 
each of char, unsigned char, 
short, unsigned short, int, and unsigned int.  Each is used by passing an 
lvalue of the appropriate type to 
indicate that the lvalue is a symbolic input for CREST.

Please let me know if this is the information you were looking for or if you 
have any further questions.

 -- Jacob

So currently CREST cannot handle "structure" and/or "enum" data types?

Thanks,
Xiao

CREST has no way to mark an entire struct as symbolic.  For structures with 
only numeric fields, one can 
write something like:

    struct point {
        int x, y;
    };

    void CREST_point(struct point* p) {
       CREST_int(p->x);
       CREST_int(p->y);
    }


For structs with pointer members, however, there is no effective way to have 
CREST handle the structure symbolically.  For example, consider a binary tree:

    struct node {
        struct node* left;
        struct node* right;
        int data;
    }

Unlike in some previous symbolic execution tools (e.g., CUTE), CREST cannot 
treat the entire tree as 
symbolic and solve for a whole tree structure needed to cover some path or 
branch.

 -- Jacob

CREST does not have any special handling for enums.  enums can sometimes be 
treated as integers -- e.g.:

    enum example {
        A, B, C, D, E, F;
    } letter;

    int main(void) {
        letter x;
        CREST_int(x);
        if (x < A || x > F)
            exit(0);
        ...
    }

This approach is less effective when the enumerated values are not contiguous.

 -- Jacob