Automatically exported from code.google.com/p/crest
License: BSD 3-Clause "New" or "Revised" License
About Me:
value for Apply1 should be the top level one?
UnOp (op, e1, _) ->
(instrumentExpr e1) @ [mkApply1 op e]
Original issue reported on code.google.com by [email protected] on 11 Apr 2012 at 2:00
What steps will reproduce the problem?
1. Declare a structure containing a bitfield, e.g. struct p{ unsigned error
: 1;}
2. Try to declare error as input e.g. CREST_int(p.error)
3. run crestc on the code
Original issue reported on code.google.com by [email protected] on 4 Aug 2009 at 9:08
It should be possible for CREST to use existing test inputs as a starting
point for generating new tests.
As a simple example, it would be nice to be able to initialize a single,
local search at a specific input. Something like:
run_crest PROGRAM 1000 -cfg -init_input=test.42
Original issue reported on code.google.com by [email protected] on 20 May 2008 at 7:41
I would like to ask a question.
when I do the testing with crest, I got out put like this:
"Iteration 1000 (38s, 0.0s): covered 83 branches [11 reach funs, 798 reach
branches].(83, 83)"
what does the "798 reach branches" mean??
Is it the same as "total branches read"?
Original issue reported on code.google.com by [email protected] on 7 Aug 2014 at 2:44
What steps will reproduce the problem?
1. "make" is successfully executed in src/ directory in crest-0.1.1
2. cd test
3. ../bin/crestc uniform_test.c, the following message is showed:
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/ly/Work/crest/crest-0.1.1/cil-1.3.7/obj/x86_LINUX/cilly.asm.exe --out
./uniform_test.cil.c --doCrestInstrument ./uniform_test.i
Read 0 branches.
Read 0 nodes.
Wrote 0 branch edges.
4. ../bin/run_crest ./uniform_test 10 -dfs, the following message is showed:
run_crest: run_crest/concolic_search.cc:70: crest::Search::Search(const
std::string&, int): Assertion `in' failed.
Aborted
What is the expected output? What do you see instead?
The expected output should be like what's illustrated in README file in
crest-0.1.1.
What version of the product are you using? On what operating system?
crest-0.1.1/ubuntu 10.01
I wonder the cause of such a problem, thanks!
Original issue reported on code.google.com by [email protected] on 12 Mar 2012 at 7:12
What steps will reproduce the problem?
1. Run ./configure in crest/benchmarks/grep-2.2
2. I modify permissions of src/Makefile :
chmod 777 Makefile
3. modify src/Makefile follow the steps in FAQ "Can CREST be used on
multi-file programs?"
45c45
< AUTOMAKE = automake
---
> AUTOMAKE = echo
63c63
< CC = gcc
---
> CC = cilly
116c116
< LDFLAGS =
---
> LDFLAGS = --merge --keepmerged
133c133
< CFLAGS = -g -O2
---
> CFLAGS = --merge -g -O2
3. run "make" in the src/ directory
I get the following error message:
cd .. && echo --gnu --include-deps src/Makefile
--gnu --include-deps src/Makefile
cilly -DHAVE_CONFIG_H -I. -I. -I.. -I../intl
-DLOCALEDIR=\"/usr/local/share/locale\" -D_LARGEFILE_SOURCE
-D_FILE_OFFSET_BITS=64 --merge -g -O2 -c grep.c
make: cilly: Command not found
make: *** [grep.o] Error 127
What version of the product are you using? On what operating system?
ubuntu 12.04
Please provide any additional information below.
If I don't modify the makefile ,run "make " in the grep/src/ directory.
I get the following error message:
configure.in:11: your implementation of AM_INIT_AUTOMAKE comes from an
configure.in:11: old Automake version. You should recreate aclocal.m4
configure.in:11: with aclocal and run automake again.
make: *** [Makefile.in] Error 63
Can anyone help me fix these error? Thanks. I have try my best to solve them ,
but still failed . Can anyone give any advices?
Original issue reported on code.google.com by [email protected] on 11 Apr 2013 at 3:10
What steps will reproduce the problem?
1. after succesful installation of yices, cil ,ocaml and crest, when i am
trying to execute i am facing the following error:
2. crestc simple.c
crestc: command not found
3. run_crest./function 10 -dfs
run_crest command not found
What is the expected output? What do you see instead?
The executable files crestc and run_crest have been created and are present in
the /bin folder but the programs are not executing.
What version of the product are you using? On what operating system?
crest -0.1.1 ubantu linux operating system
Please provide any additional information below.
Original issue reported on code.google.com by [email protected] on 5 May 2012 at 11:23
Can CREST allow add additional conditions to to restrict symbolic variables to
have valid ranges of values?
for example:
symbolic variable's data range is {1,2,3}, How can I define it in CREST?
Original issue reported on code.google.com by [email protected] on 19 Jul 2013 at 9:26
What steps will reproduce the problem?
1. "make" is successfully executed in src/ directory in crest-0.1.1
2. cd test
3. ../bin/crestc uniform_test.c, the following message is showed:
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/ly/Work/crest/crest-0.1.1/cil-1.3.7/obj/x86_LINUX/cilly.asm.exe --out
./uniform_test.cil.c --doCrestInstrument ./uniform_test.i
Read 0 branches.
Read 0 nodes.
Wrote 0 branch edges.
4. ../bin/run_crest ./uniform_test 10 -dfs, the following message is showed:
run_crest: run_crest/concolic_search.cc:70: crest::Search::Search(const
std::string&, int): Assertion `in' failed.
Aborted
What is the expected output? What do you see instead?
The expected output should be like what's illustrated in README file in
crest-0.1.1.
What version of the product are you using? On what operating system?
crest-0.1.1/ubuntu 10.01
I wonder the cause of such a problem, thanks!
Original issue reported on code.google.com by [email protected] on 12 Mar 2012 at 7:12
1. The same command runs at different times, why the number of covered
branches is different in the end?
for example:
-desktop:~/crest/benchmarks/replace$ ../../bin/run_crest ./replace 100 -dfs
Iteration 100 (2s): covered 62 branches [12 reach funs, 148 reach branches].
then run again:
-desktop:~/crest/benchmarks/replace$ ../../bin/run_crest ./replace 100 -dfs
Iteration 100 (2s): covered 63 branches [13 reach funs, 166 reach branches].
2.With the increase of iteration times, why the number of covered branches
did not increase ?
for example:
-desktop:~/crest/benchmarks/replace$ ../../bin/run_crest ./replace 100 -dfs
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 51 branches [12 reach funs, 160 reach branches].
Iteration 2 (0s): covered 62 branches [13 reach funs, 166 reach branches].
Iteration 3 (0s): covered 63 branches [13 reach funs, 166 reach branches].
........
Iteration 99 (2s): covered 63 branches [13 reach funs, 166 reach branches].
Iteration 100 (2s): covered 63 branches [13 reach funs, 166 reach branches].
From Iteration 3 to Iteration 100,the number of covered branches is unchanged.
Should CREST be able to grab all the paths, isn't it?
Could you please explain the reasons to me?
Thanks a lot !
Original issue reported on code.google.com by [email protected] on 19 Jul 2013 at 9:44
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 [email protected] on 3 Oct 2012 at 1:24
I am not sure whether or not this should go under "issues".
I am testing crest on some programs.
In the README file, it says that crest is invoked using [1]. If I run
"./run_crest" alone, it says that crest can be invoked using [2]. I would
like to know the available strategies e.g. how to control the depth of DFS
if I ever want to? According to report [3], this can be done, right?
[1]
./run_crest PROGRAM NUM_ITERATIONS -STRATEGY
[2]
./run_crest <program> <number of iterations> -<strategy> [strategy options]
[3]
Heuristics for Scalable Dynamic Test Generation, 2008, September.
Original issue reported on code.google.com by [email protected] on 25 Mar 2010 at 7:22
What steps will reproduce the problem?
1. make process
What is the expected output? What do you see instead?
What version of the product are you using? On what operating system?
crest 0.1.1
Please provide any additional information below.
Files 'run_crest/run_crest.cc' and 'base/symbolic_expression.cc' were missing
an '#include <stdio.h>' declaration. Must fix for the make process to build
successfully.
Original issue reported on code.google.com by [email protected] on 28 Dec 2010 at 11:17
Hi, there is an error for compilation
I tried to compile crest in ~/crest/src using 'make'
Then, yices_solver.cc error as follows
-> fatal error: yices_c.h: No such file or directory
What version of the product are you using? On what operating system?
-> ubuntu 14.04 version 0.1.1 for crest
Please provide any additional information below.
Original issue reported on code.google.com by [email protected] on 21 May 2014 at 2:40
1. I try to use crest (version 0.1.1) on my Ubuntu 9.10 (x86 cpu), gcc
version 4.3.4
2. It says on the webpage that CIL is required.
3. I run crest/cil/./configure
4. It complains about ocaml not being installed
5. I install ocaml via sudo apt-get install ocaml, this gets me version 3.11.1
6. I run configure again, it works.
7. I run make, I get the error:
....
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/amine/Downloads/crest-0.1.1/cil'
make: *** [setup] Error 2
Original issue reported on code.google.com by [email protected] on 21 Mar 2010 at 5:55
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 install
In make install i m getting this
if test -d /usr/local/bin; then : ; else mkdir -p /usr/local/bin; fi
if test -d /usr/local/lib/ocaml; then : ; else mkdir -p /usr/local/lib/ocaml; fi
mkdir: cannot create directory `/usr/local/lib/ocaml': Permission denied
make: *** [install] Error 1
i also tried that chmod -R 777 configure command but problem is not solved.
and pls me further steps also..
- Yours faithfully
Sangharatna Godboley
Original issue reported on code.google.com by [email protected] on 30 Sep 2012 at 1:23
Hi I am getting this error when I try to make in CIL directory:
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/bibhas/crest-0.1.1/cil'
make: *** [setup] Error 2
I am using Ubuntu 11.04..can someone please help me in fixing this error?
Original issue reported on code.google.com by [email protected] on 2 Feb 2012 at 4:28
On Mac OS X 10.7.4 and gcc <= 4.2.1, crestc will fail if you include stdlib.h
in your C-code. The issue with stdlib is that it causes cilly to fail due to
some Apple-defined versions of functions that take arguments of form:
void (^)(void),
which is not something that cilly can handle.
Since these are all specified within #ifdef __BLOCKS__ sections, the patch
simply undef that!
Shouldn't hurt on other platforms, so #undef globally.
Note, I also added a `set -e` at the top of the crestc script so that any error
in the script will cause the script to fail non-zero. Previously any error
code set by cilly would be swallowed because the script would happily run on
through process_cfg.
Patch is attached.
Original issue reported on code.google.com by [email protected] on 17 Jul 2012 at 9:01
Attachments:
Given the yices handles real variables out of the box, it is fairly trivial to
extend support. I have attached a preliminary patch, and test case for it.
(Apologies for some spacing edits in the patch file).
Original issue reported on code.google.com by [email protected] on 15 Aug 2012 at 6:39
Attachments:
What steps will reproduce the problem?
1. "make" is successfully executed in src/ directory in crest-0.1.1
2. cd test
3. ../bin/crestc uniform_test.c, the following message is showed:
gcc -D_GNUCC -E -I../bin/../include -DCIL=1 uniform_test.c -o ./uniform_test.i
/home/ly/Work/crest/crest-0.1.1/cil-1.3.7/obj/x86_LINUX/cilly.asm.exe --out
./uniform_test.cil.c --doCrestInstrument ./uniform_test.i
Read 0 branches.
Read 0 nodes.
Wrote 0 branch edges.
4. ../bin/run_crest ./uniform_test 10 -dfs, the following message is showed:
run_crest: run_crest/concolic_search.cc:70: crest::Search::Search(const
std::string&, int): Assertion `in' failed.
Aborted
What is the expected output? What do you see instead?
The expected output should be like what's illustrated in README file in
crest-0.1.1.
What version of the product are you using? On what operating system?
crest-0.1.1/ubuntu 10.01
I wonder the cause of such a problem, thanks!
Original issue reported on code.google.com by [email protected] on 12 Mar 2012 at 7:13
What steps will reproduce the problem?
1. cil make
1. crest make
What is the expected output? What do you see instead?
What version of the product are you using? On what operating system?
crest 0.1.1
Please provide any additional information below.
0. No error in ocaml, yices, nor cil ./configure
1. In the cil make:
The extension of the output file must be .o or .so
make[1]: *** [obj/x86_LINUX/libcil.a] Erreur 2
make[1]: quittant le répertoire « /usr/src/crest-0.1.1/cil »
make: *** [setup] Erreur 2
2. In crest make:
g++ -I. -I/usr/include -Wall -O2 -c -o base/symbolic_expression.o
base/symbolic_expression.cc
base/symbolic_expression.cc: In member function ‘void
crest::SymbolicExpr::AppendToString(std::string*) const’:
base/symbolic_expression.cc:59: error: ‘sprintf’ was not declared in this
scope
make: *** [base/symbolic_expression.o] Erreur 1
Original issue reported on code.google.com by [email protected] on 5 Mar 2011 at 11:00
Where can I find about how to specify inputs to CREST?
e.g., I know there is CREST_int(), and CREST_unsigned_char() from example
programs in the test directory.
I am looking for a comprehensive description of these features.
Original issue reported on code.google.com by [email protected] on 28 Mar 2010 at 2:00
What steps will reproduce the problem?
1. modify the /benchmarks/grep-2.2/makefile as the /grep-2.2/src/makefile.CREST
2. then run "make" in the grep-2.2/ directory
What is the expected output? What do you see instead?
I get the ffollowing information:
make:cilly: Command not found
What version of the product are you using? On what operating system?
crest-0.1.1(version 132)
ubuntu 12.04 gcc=4.6.3 g++=4.6.3
Please provide any additional information below.
I can use CREST to test the programs in test/ directory successfully.but I can't get the grep executable.
Original issue reported on code.google.com by [email protected] on 10 Apr 2013 at 7:20
Attachments:
React
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
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
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.
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.