jburnim / crest Goto Github PK

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

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.

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

I was trying to run ../bin/crestc uniform_test.c and it shows this error

Cannot find GNUCC version

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?

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?

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.

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

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.

Brief description: Fatal error message is displayed while installing CREST

Steps to reproduce:

1. Download and install Yices 2.2.2
2. Change YICES_DIR in src/Makefile to point to Yices location
3. Build CIL by running "configure" and "make" in the cil/ directory
4. Try to build CREST by running "make" in the src/ directory

Expected results:

• CREST should be properly build after step #4.

Actual result:

• A fatal error message is displayed stating that yices_c.h cannot be found (fatal error: yices_c.h: No such file or directory)
• This is the complete error message:

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:

• Ubuntu 14.04 (64-bit)
• Crest 0.1.2
• Yices 2.2.2

Additional information:

• It seems that this issue has been already reported at google code page for the CREST project (Issue 22) since May, 2014.

How can I solve it?

/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

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!