search

tthtlc / crest

Automatically exported from code.google.com/p/crest
BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

error in installing crest-0.1.1 #17

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1.
2.
3.
Dear sir,
               I am trying to install crest-0.1.1 tool in my system but facing problem.. i have done following steps::
        1. downloaded crest tool
        2.  downloaded yices-1.0.36
        3. dowloaded ocaml-4.00.0
        4. configuring ocaml using commands ./configure
                                                                     make world
                                                                     make opt
                                                                     make instal
        5.Then using make cammand in crest source directory src folder ,,I   installed  crest
        6. in directory cil .... ./configure
         7. after this i typed cammand       make...
  and i m getting following error...........pls any one can resolve this problem....   

sangharatna@sangharatna-OptiPlex-980:~/Documents/crest-0.1.1/cil$ make
make cilly NATIVECAML= 
make[1]: Entering directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make[1]: Nothing to be done for `cilly'.
make[1]: Leaving directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make cilly NATIVECAML=1
make[1]: Entering directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make[1]: Nothing to be done for `cilly'.
make[1]: Leaving directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make cillib NATIVECAML=
make[1]: Entering directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make[1]: Nothing to be done for `cillib'.
make[1]: Leaving directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make cillib NATIVECAML=1
make[1]: Entering directory `/home/sangharatna/Documents/crest-0.1.1/cil'
ocamlopt -output-obj -o obj/x86_LINUX/libcil.a unix.cmxa str.cmxa 
obj/x86_LINUX/libperfcount.a obj/x86_LINUX/pretty.cmx obj/x86_LINUX/inthash.cmx 
obj/x86_LINUX/errormsg.cmx obj/x86_LINUX/alpha.cmx obj/x86_LINUX/trace.cmx 
obj/x86_LINUX/stats.cmx obj/x86_LINUX/util.cmx obj/x86_LINUX/clist.cmx 
obj/x86_LINUX/cilutil.cmx obj/x86_LINUX/escape.cmx obj/x86_LINUX/longarray.cmx 
obj/x86_LINUX/growArray.cmx obj/x86_LINUX/cabs.cmx obj/x86_LINUX/cabshelper.cmx 
obj/x86_LINUX/cabsvisit.cmx obj/x86_LINUX/whitetrack.cmx 
obj/x86_LINUX/cprint.cmx obj/x86_LINUX/lexerhack.cmx obj/x86_LINUX/machdep.cmx 
obj/x86_LINUX/cparser.cmx obj/x86_LINUX/clexer.cmx obj/x86_LINUX/cilversion.cmx 
obj/x86_LINUX/cil.cmx obj/x86_LINUX/cillower.cmx obj/x86_LINUX/formatparse.cmx 
obj/x86_LINUX/formatlex.cmx obj/x86_LINUX/formatcil.cmx 
obj/x86_LINUX/cabs2cil.cmx obj/x86_LINUX/patch.cmx obj/x86_LINUX/frontc.cmx 
obj/x86_LINUX/check.cmx obj/x86_LINUX/mergecil.cmx obj/x86_LINUX/dataflow.cmx 
obj/x86_LINUX/dominators.cmx obj/x86_LINUX/bitmap.cmx obj/x86_LINUX/ssa.cmx 
obj/x86_LINUX/ciltools.cmx obj/x86_LINUX/usedef.cmx obj/x86_LINUX/logcalls.cmx 
obj/x86_LINUX/logwrites.cmx obj/x86_LINUX/rmtmps.cmx 
obj/x86_LINUX/callgraph.cmx obj/x86_LINUX/epicenter.cmx 
obj/x86_LINUX/heapify.cmx obj/x86_LINUX/setp.cmx obj/x86_LINUX/uref.cmx 
obj/x86_LINUX/olf.cmx obj/x86_LINUX/ptranal.cmx obj/x86_LINUX/canonicalize.cmx 
obj/x86_LINUX/heap.cmx obj/x86_LINUX/oneret.cmx obj/x86_LINUX/partial.cmx 
obj/x86_LINUX/simplemem.cmx obj/x86_LINUX/simplify.cmx 
obj/x86_LINUX/dataslicing.cmx obj/x86_LINUX/sfi.cmx 
obj/x86_LINUX/expcompare.cmx obj/x86_LINUX/cfg.cmx obj/x86_LINUX/liveness.cmx 
obj/x86_LINUX/reachingdefs.cmx obj/x86_LINUX/deadcodeelim.cmx 
obj/x86_LINUX/availexps.cmx obj/x86_LINUX/availexpslv.cmx 
obj/x86_LINUX/predabst.cmx obj/x86_LINUX/testcil.cmx 
obj/x86_LINUX/crestInstrument.cmx obj/x86_LINUX/ciloptions.cmx 
obj/x86_LINUX/feature_config.cmx
The extension of the output file must be .o or .so
make[1]: *** [obj/x86_LINUX/libcil.a] Error 2
make[1]: Leaving directory `/home/sangharatna/Documents/crest-0.1.1/cil'
make: *** [setup] Error 2
sangharatna@sangharatna-OptiPlex-980:~/Documents/crest-0.1.1/cil$ 

What is the expected output? What do you see instead?
i want to resolved this problem..

What version of the product are you using? On what operating system?
crest-0.1.1 yices-1.0.29 ocaml-3.08.0 
ubantu linux  

Please provide any additional information below.

Original issue reported on code.google.com by sanghu1...@gmail.com on 3 Oct 2012 at 1:24

GoogleCodeExporter commented 9 years ago 
Hi,

have you solved the problem?
I would like to know how you solved it, 
thanks

Original comment by gaetanov...@gmail.com on 12 Mar 2013 at 1:20

GoogleCodeExporter commented 9 years ago 
Hi,
  have you solved this problem? I encountered the similar problem with you .
 I used crest-0.1.1(version 132) yices-1.0.38 ocaml-4.00.1
  ubuntu 12.04 linux  

   If you have some good solution to solve the peoblem, looking forward for your reply.

   thanks!

Original comment by liuch9...@163.com on 10 Apr 2013 at 2:33

GoogleCodeExporter commented 9 years ago 
Greetings!
          Sorry for delayed replying  gaetanov...@gmail.com and
zaohu...@yahoo.cn. Ya I have already resolved this problem one year ago.
Actually I forget how it resolved. But I have those steps. I am mentioning
please check that whether you have done those steps or not.

STEPS to install CREST TOOl:
1. Download a) crest-0.1.1 from code.google.com/p/crest/
            b) yices-1.0.29 from yices.csl.sri.com
            c) ocamal-3.08.0 from http://caml.inria.fr/ocaml/
2. Paste yices-1.0.29 and ocaml-3.08.0 folders inside crest-0.1.1 folder
3. Edit some .cc files
             a) symbolic_expression.cc
                        add:  #include<stdio.h>
                              #include<stdlib.h>
                              #include<string.h>
             b) run_crest.cc
                        add:  #include<stdio.h>
             c) To set path for yices in the makefile given in crest
directory.
4) Go to crest-0.1.1 folder:
             Home/sangharatna/Documents/crest-0.1.1$   (My systems path do
for yours)
5) Go to ocaml-3.08.0 folder
             Home/sangharatna/Documents/crest-0.1.1/ocaml-3.08.0 $

           and type following commands:
               a) ./configure
               b) make world
               c) make opt
               d) make install(if this will not work then {sudo apt-get
install ocaml.nox})
 6) Then go to crest source directory means src folder .. then type command
          Home/sangharatna/Documents/crest-0.1.1/src $ make
    then it will automatically install.
7) Go to cil folder
     cil $ ./configure
8) Type command cil $ make

I can't tell you the exactly solution for the problem arised, but after
following these steps, I hope you can work with crest.

If any other problem will arise so please let me know.

Original comment by sanghu1...@gmail.com on 10 Apr 2013 at 4:38

GoogleCodeExporter commented 9 years ago 
Greetings! 
          Sorry for delayed replying  gaetanov...@gmail.com and  zaohu...@yahoo.cn. Ya I have already resolved this problem one year ago. Actually I forget how it resolved. But I have those steps. I am mentioning please check that whether you have done those steps or not.

STEPS to install CREST TOOl:
1. Download a) crest-0.1.1 from code.google.com/p/crest/
            b) yices-1.0.29 from yices.csl.sri.com
            c) ocamal-3.08.0 from http://caml.inria.fr/ocaml/
2. Paste yices-1.0.29 and ocaml-3.08.0 folders inside crest-0.1.1 folder
3. Edit some .cc files
             a) symbolic_expression.cc
                        add:  #include<stdio.h>
                              #include<stdlib.h>
                              #include<string.h>
             b) run_crest.cc
                        add:  #include<stdio.h>
             c) To set path for yices in the makefile given in crest directory.
4) Go to crest-0.1.1 folder:
             Home/sangharatna/Documents/crest-0.1.1$   (My systems path do for yours)   
5) Go to ocaml-3.08.0 folder
             Home/sangharatna/Documents/crest-0.1.1/ocaml-3.08.0 $                     
           and type following commands:
               a) ./configure
               b) make world
               c) make opt
               d) make install(if this will not work then {sudo apt-get install ocaml.nox})   
 6) Then go to crest source directory means src folder .. then type command
          Home/sangharatna/Documents/crest-0.1.1/src $ make
    then it will automatically install.
7) Go to cil folder 
     cil $ ./configure
8) Type command cil $ make

I can't tell you the exactly solution for the problem arised, but after 
following these steps, I hope you can work with crest.

If any other problem will arise so please let me know.

Original comment by sanghu1...@gmail.com on 10 Apr 2013 at 4:39

GoogleCodeExporter commented 9 years ago 
Thank you for your reply ! very appreciate!

 I follow your steps , I can install CREST, I can  test the single-file  programs in the test/ directory successfully, such as uniform_test.c,concrete_return.c and so on.

But I still encounter some problems :
First :

when I  run "make" In cil/ directory, in the process of  compiling, I still saw 
the message :

gcc: selected multilib '64' not installed
make cilly NATIVECAML=
make[1]: Entering directory `/home/liuch/crest/cil'
make[1]: Nothing to be done for `cilly'.
make[1]: Leaving directory `/home/liuch/crest/cil'
make cilly NATIVECAML=1
make[1]: Entering directory `/home/liuch/crest/cil'

but  it doesn't report any errors in the end. I don't know why about this 
“Nothing to be done for `cilly'”， Can you have any ideas about it?

Second:

when I trying to run the multi-file program grep 2.2 in 
benchmark/directory,first  I modify the grep/Makefile the same as the 
/grep-2.2/src/makefile.CREST

 then I run make in grep/src directory, I get the following information:

cilly -DHAVE_CONFIG_H -I. -I. -I.. -I../intl 
-DLOCALEDIR=\"/usr/local/share/locale\" -I../../../../include 
-D_LARGEFILE_SOURCE -D_FILE_OFFSET_BITS=64 --merge -g -O2 -c grep.c
make: cilly: Command not found
make: *** [grep.o] Error 127

It shows that  cilly: Command not found. I guess it maybe has some relationship 
with above problem , because the cilly executable didn't been build 
successfully.

 I have try my best to solve it , But I don't know how to deal with it , can you have any ideas about it ?

Best!
I am looking forward for your reply.
Thanks again!

Original comment by liuch9...@163.com on 12 Apr 2013 at 1:54

GoogleCodeExporter commented 9 years ago 
Greetings!!
               Hi,
                    For your kind information let me tell you, CREST is a concolic tester. It results decision test suite by selecting the value for variables automatically. For that we need to edit variable declaration as .... CREST_int(variable); .. for each variable where ever you need to select. That .c file should be in bin folder. Now follow the commands to compile and execute:
1) Compilation...

sangharatna@ratna:~/Documents/crest-0.1.1/bin$ sudo ./crestc triangle.c
gcc -D_GNUCC -E -I./../include -DCIL=1 triangle.c -o ./triangle.i
/home/sangharatna/Documents/crest-0.1.1/cil/obj/x86_LINUX/cilly.asm.exe --out 
./triangle.cil.c --doCrestInstrument ./triangle.i

triangle.c:62: Warning: Return statement with a value in function returning void
gcc -D_GNUCC -E -I./../include ./triangle.cil.c -o ./triangle.cil.i
gcc -D_GNUCC -c -I./../include -o ./triangle.o ./triangle.cil.i
triangle.c:11:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:12:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:13:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:14:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:15:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:16:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:17:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:18:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:19:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
triangle.c:20:1: warning: ‘__crest_skip__’ attribute directive ignored 
[-Wattributes]
./../include/crest.h:202:1: warning: ‘__crest_skip__’ attribute directive 
ignored [-Wattributes]
gcc -D_GNUCC -o triangle -I./../include ./triangle.o ./../lib/libcrest.a 
-L./../lib -lstdc++
Read 16 branches.
Read 25 nodes.
Wrote 21 branch edges.
sangharatna@ratna:~/Documents/crest-0.1.1/bin$

2) Execution..

sangharatna@ratna:~/Documents/crest-0.1.1/bin$ sudo ./run_crest ./triangle 10 
-dfs
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 4 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 3
Iteration 2 (0s): covered 6 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 2
Branch 3
Iteration 3 (0s): covered 7 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 2
Branch 3
Iteration 4 (0s): covered 11 branches [1 reach funs, 16 reach branches].
Branch 1
Iteration 5 (0s): covered 11 branches [1 reach funs, 16 reach branches].
Branch 1
Iteration 6 (0s): covered 12 branches [1 reach funs, 16 reach branches].
Branch 1
Iteration 7 (0s): covered 12 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 3
Iteration 8 (0s): covered 15 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 3
Iteration 9 (0s): covered 15 branches [1 reach funs, 16 reach branches].
Branch 2
Iteration 10 (0s): covered 15 branches [1 reach funs, 16 reach branches].
sangharatna@ratna:~/Documents/crest-0.1.1/bin$

If you are getting this results then CREST is working perfectly. After this go 
to bin folder you will have one input.txt and coverage.txt files those files 
contains the selected values and those are nothing but test suite.

Original comment by sanghu1...@gmail.com on 12 Apr 2013 at 5:42

GoogleCodeExporter commented 9 years ago 
Greetings!!
               Hi,
                    For your kind information let me tell you, CREST is a
concolic tester. It results decision test suite by selecting the value for
variables automatically. For that we need to edit variable declaration as
.... CREST_int(variable); .. for each variable where ever you need to
select. That .c file should be in bin folder. Now follow the commands to
compile and execute:
1) Compilation...

sangharatna@ratna:~/Documents/crest-0.1.1/bin$ sudo ./crestc triangle.c
gcc -D_GNUCC -E -I./../include -DCIL=1 triangle.c -o ./triangle.i
/home/sangharatna/Documents/crest-0.1.1/cil/obj/x86_LINUX/cilly.asm.exe
--out ./triangle.cil.c --doCrestInstrument ./triangle.i

triangle.c:62: Warning: Return statement with a value in function returning
void
gcc -D_GNUCC -E -I./../include ./triangle.cil.c -o ./triangle.cil.i
gcc -D_GNUCC -c -I./../include -o ./triangle.o ./triangle.cil.i
triangle.c:11:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:12:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:13:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:14:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:15:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:16:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:17:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:18:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:19:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
triangle.c:20:1: warning: ‘__crest_skip__’ attribute directive ignored
[-Wattributes]
./../include/crest.h:202:1: warning: ‘__crest_skip__’ attribute directive
ignored [-Wattributes]
gcc -D_GNUCC -o triangle -I./../include ./triangle.o ./../lib/libcrest.a
-L./../lib -lstdc++
Read 16 branches.
Read 25 nodes.
Wrote 21 branch edges.
sangharatna@ratna:~/Documents/crest-0.1.1/bin$

2) Execution..

sangharatna@ratna:~/Documents/crest-0.1.1/bin$ sudo ./run_crest ./triangle
10 -dfs
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 4 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 3
Iteration 2 (0s): covered 6 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 2
Branch 3
Iteration 3 (0s): covered 7 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 2
Branch 3
Iteration 4 (0s): covered 11 branches [1 reach funs, 16 reach branches].
Branch 1
Iteration 5 (0s): covered 11 branches [1 reach funs, 16 reach branches].
Branch 1
Iteration 6 (0s): covered 12 branches [1 reach funs, 16 reach branches].
Branch 1
Iteration 7 (0s): covered 12 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 3
Iteration 8 (0s): covered 15 branches [1 reach funs, 16 reach branches].
Branch 1
Branch 3
Iteration 9 (0s): covered 15 branches [1 reach funs, 16 reach branches].
Branch 2
Iteration 10 (0s): covered 15 branches [1 reach funs, 16 reach branches].
sangharatna@ratna:~/Documents/crest-0.1.1/bin$

If you are getting this results then CREST is working perfectly. After this
go to bin folder you will have one input.txt and coverage.txt files those
files contains the selected values and those are nothing but test suite.

Original comment by sanghu1...@gmail.com on 12 Apr 2013 at 5:43

GoogleCodeExporter commented 9 years ago 
Thanks everyone for reporting this issue and possible fixes!  I believe this 
issue has been resolved in CREST 0.1.2, available at 
https://github.com/jburnim/crest/releases/tag/v0.1.2 .

Original comment by jbur...@gmail.com on 7 Feb 2014 at 5:29

GoogleCodeExporter commented 9 years ago 
Can anyone please tell me if I use any version of Yices with v0.1.2 of CREST? 
If no, which version should I use exactly? 

Thanks,
Markus

Original comment by markus.m...@gmail.com on 10 Dec 2014 at 8:30

GoogleCodeExporter commented 9 years ago 
Hi Markus!!
You may use yices-1.0.29.

I have already mentioned all the steps to install crest-0.1.1 in previous 
comments.

Thanks 

Sangharatna godboley

Original comment by sanghu1...@gmail.com on 10 Dec 2014 at 9:46

GoogleCodeExporter commented 9 years ago 
Hi Sangharatna godboley,

I followed your instructions for installing crest 0.1.2 on a Ubuntu 14.04 
however, when I try to run crestc from the test directory I get the following 
error:

$ ../bin/crestc uniform_test.c 
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/user/crest-eae2f42/cil/bin/cilly.native --out ./uniform_test.cil.c 
--doCrestInstrument ./uniform_test.i
The command
/home/user/crest-eae2f42/cil/bin/cilly.native --out ./uniform_test.cil.c 
--doCrestInstrument ./uniform_test.i
received signal %d
127

Can anyone please help me with this issue?

Original comment by markus.m...@gmail.com on 10 Dec 2014 at 11:28

GoogleCodeExporter commented 9 years ago 
Markus!!!
         Please mention ./ before the command.

         $ ../bin/./crestc uniform_test.c

Original comment by sanghu1...@gmail.com on 10 Dec 2014 at 11:35