Comments (4)
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
Original comment by [email protected]
on 29 Mar 2010 at 7:47
- Changed state: Done
from crest.
So currently CREST cannot handle "structure" and/or "enum" data types?
Thanks,
Xiao
Original comment by [email protected]
on 29 Mar 2010 at 7:58
from crest.
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
Original comment by [email protected]
on 29 Mar 2010 at 8:12
from crest.
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
Original comment by [email protected]
on 29 Mar 2010 at 8:18
from crest.
Related Issues (20)
- run_crest is aborted by assertion HOT 4
- run_crest is aborted by assertion HOT 1
- unary operators intrumentation HOT 3
- crestc: command not found HOT 1
- Patched crestc for Mac OS X 10.7.4 and gcc <=4.2.1 HOT 1
- Support real valued variables HOT 1
- facing problem in installing crest-0.1.1 tool HOT 1
- error in installing crest-0.1.1 HOT 12
- make error in grep -2.2 "make: cilly command not found" HOT 1
- error in run CREST on the Grep-2.2 programs HOT 4
- can crest define the data range of symbolic variables?
- run_crest Some Detailed Questions HOT 1
- yices_c.cc can't be compiled HOT 2
- the meaning of "# reach branches"
- Options of Branch-Selection Strategies HOT 2
- crest make error HOT 5
- cil-crest make HOT 4
- Error in CIL make HOT 2
- run_crest is aborted by assertion HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from crest.