jburnim / crest Goto Github PK
View Code? Open in Web Editor NEWCREST is a concolic test generation tool for C.
Home Page: http://jburnim.github.io/crest/
License: BSD 2-Clause "Simplified" License
CREST is a concolic test generation tool for C.
Home Page: http://jburnim.github.io/crest/
License: BSD 2-Clause "Simplified" License
Hi,
So I'm trying to run the test program just to make sure crest is functioning and keep getting the error:
uniform_test.c:12:19: error: crest.h: No such file or directory
Where is crest.h supposed to be located?
and also will this program work with bam, fasta, sam, or fastq files at all?
Thanks in advance,
Ram Ayyala
/home/yzb/Downloads/crest-master/benchmarks/grep-2.2/src/grep.c:112: undefined reference to __CrestChar' /home/yzb/Downloads/crest-master/benchmarks/grep-2.2/src/grep.c:112: undefined reference to
__CrestChar'
grep_comb.o: In function main': /home/yzb/Downloads/crest-master/benchmarks/grep-2.2/src/grep.c:957: undefined reference to
__CrestChar'
collect2: error: ld returned 1 exit status
make: *** [grep] Error 1
Could anyone tell me how to fix this problem?I can get the grep_comb.c,but failed to make the executable grep.
@jburnim
I was trying to run ../bin/crestc uniform_test.c
and it shows this error
Cannot find GNUCC version
Hello, I have been modified yicies_solver for my term project.
I found that kMinValue[0](Minimum value of U_CHAR) does not give me correct value(0)
for(size_t i = 0 ; i < 1 ; ++i)
{
fprintf(stdout, "\tkMinValue[%u, %s]: %lld\n", i, type_names[i], kMinValue[i]);
fprintf(stdout, "\tkMaxValue[%u, %s]: %lld\n", i, type_names[i], kMaxValue[i]);
}
from above codes,
I saw the result live below
I know that kMaxValue is initialized at basic_types.cc as numeric_limits::min()
but I wonder why I got the wrong result.
kMinValue[0, U_CHAR]: 154468404
kMaxValue[0, U_CHAR]: 255
Thanks.
Compiling
struct a {
char const b;
} g_1782;
struct a c() {
for (;;)
return g_1782;
}
int main() { }
With crestc
gives me
test7.c: In function ‘c’:
test7.c:6:15: error: assignment of read-only variable ‘__retres1’
return g_1782;
Is this some sort of instrumentation bug?
Given this program:
unsigned int a, b;
int main() {
__CrestUInt(&a);
if( a < 1 || a > 1) {
exit(0);
}
(-1 > a ) || b;
printf("g_4: %d\n", a);
}
I would expect crest to explore 3 branches, printing "g_4: 1" once, however I get:
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 2 branches [1 reach funs, 8 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 3 (0s): covered 5 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 4 (0s): covered 5 branches [1 reach funs, 8 reach branches].
Prediction failed!
/usr/include/stdio.h:27:10: fatal error: bits/libc-header-start.h: No such file or directory
#include <bits/libc-header-start.h>
^~~~~~~~~~~~~~~~~~~~~~~~~~
on Ubuntu 18 64 bits
I had to install 32 bit compatibility library.
Hi, I just tried to run crest with uniform.c example, it successfully read branches and write branches, but it just stopped without iteration, and also no error message showed. The output message is shown below:
yh570:~/crest/test$ ../bin/crestc uniform_test.c
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/yh570/crest/cil/bin/cilly.native --out ./uniform_test.cil.c --doCrestInstrument ./uniform_test.i
gcc -D_GNUCC -E -I../bin/../include ./uniform_test.cil.c -o ./uniform_test.cil.i
gcc -D_GNUCC -c -I../bin/../include -o ./uniform_test.o ./uniform_test.cil.i
uniform_test.c:16:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
16 | int a, b, c, d;
| ^ ~~~~
uniform_test.c:17:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
17 | CREST_int(a);
| ^ ~~~~
uniform_test.c:18:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
18 | CREST_int(b);
| ^ ~~~~
uniform_test.c:19:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
19 | CREST_int(c);
| ^ ~~~~
uniform_test.c:20:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
20 | CREST_int(d);
| ^ ~~~~
uniform_test.c:21:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
21 |
| ^
uniform_test.c:22:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
22 | if (a == 5) {
| ^ ~~~~
uniform_test.c:23:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
23 | if (b == 19) {
| ^ ~~
uniform_test.c:24:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
24 | if (c == 7) {
| ^
uniform_test.c:25:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
25 | if (d == 4) {
| ^
../bin/../include/crest.h:202:1: warning: ‘crest_skip’ attribute directive ignored [-Wattributes]
202 | EXTERN void __CrestInt(int* x) __SKIP;
| ^~~~~~
gcc -D_GNUCC -o uniform_test -I../bin/../include ./uniform_test.o -L../bin/../lib -lcrest -lstdc++
Read 8 branches.
Read 13 nodes.
Wrote 6 branch edges.
yh570:~/crest/test$
Would you please help me solve this issue? Thank you.
Brief description: Fatal error message is displayed while installing CREST
Steps to reproduce:
Expected results:
Actual result:
g++ -I. -I/home/user/Downloads/yices-2.2.2/include -Wall -O2 -c -o base/yices_solver.o base/yices_solver.cc
base/yices_solver.cc:17:21: fatal error: yices_c.h: No such file or directory
#include <yices_c.h>
^
compilation terminated.
make: *** [base/yices_solver.o] Error 1
Environment information:
Additional information:
If I compile and run
#include <crest.h>
unsigned int a;
int main() {
__CrestUInt(&a);
printf("a: %d\n",a);
if( a < 4294967295) {
exit(0);
}
}
with something like crestc example.c && run_crest ./example 1000 -dfs
I get
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
a: 1058183384
Iteration 1 (0s): covered 1 branches [1 reach funs, 2 reach branches].
a: 0
Iteration 2 (0s): covered 1 branches [1 reach funs, 2 reach branches].
Prediction failed!
So what I assume is happening is that in iteration 1 a path that skips the if is meant to be taken, but a gets set to 0 for some reason, so the path with the if is taken again which causes the prediction failed. This behaviour can be observed for quite a while, for example it happens if the constant is 2294967295
and disappears by the time it is 1294967295
.
Is this a real bug or some known limitation?
I think I found another issue with crest when dealing with bit fields.
Given a program like:
struct {
unsigned a : 16;
} b = {1};
int d;
int main() {
if (b.a < -1) {
d = 9;
}
printf("d: %d\n",d);
}
Crest outputs d: 9
, while the correct output should clearly be d: 0
. Interestingly if the width of a is changed to 32, the bug disappears. Any other width but 32, shows the error.
Hi,
I am trying to run an example from the repo but I'm getting stuck during the first compilation step:
../bin/crestc uniform_test.c
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/ruraj/src/opensource/crest/cil/bin/cilly.native --out ./uniform_test.cil.c --doCrestInstrument ./uniform_test.i
I've left it running for hours with no results. Any ideas?
Hello,
I'am starting using CREST but as subject, I have a problem of "narrowing conversion" as follow
vagrant@vagrant:~/vagrant_data/tools/jburnim-crest-f5ff7fc/src$ make
g++ -I. -I../../yices-1.0.40/include -Wall -O2 -c -o base/basic_types.o base/basic_types.cc
base/basic_types.cc:96:1: error: narrowing conversion of '18446744073709551615u' from 'long unsigned int' to 'crest::value_t {aka long long int}' inside { } [-Wnarrowing]
};
^
base/basic_types.cc:96:1: error: narrowing conversion of '18446744073709551615ull' from 'long long unsigned int' to 'crest::value_t {aka long long int}' inside { } [-Wnarrowing]
: recipe for target 'base/basic_types.o' failed
make: *** [base/basic_types.o] Error 1
How is it? Does anyone have same problem?
I'm using Lubuntu 16.10, running on VM.
Thank you for your help.
uwevil
I've encountered another prediction failed issue, it looks very different from the other one to me. Running:
unsigned short a = 0;
unsigned char b = 1;
void main() {
__CrestUShort(&a);
__CrestUChar(&b);
int ak = --b;
a && 0;
ak >= 2 || 0;
}
with the latest crest(3e5ecec) gives me:
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 2 branches [1 reach funs, 4 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 4 reach branches].
Iteration 3 (0s): covered 3 branches [1 reach funs, 4 reach branches].
Prediction failed!
Iteration 4 (0s): covered 3 branches [1 reach funs, 4 reach branches].
Prediction failed!
Any insight into this bug would be greatly appreciated.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.