■

 js_symbolic_executionを入れるまでの過程を整理する

※この記事は解決していない、かつ情報として見て頂くためにまとめていないため非常に見づらいです。

また、現在解決していない問題はありますが、ご意見を頂けるような状態ではありません。

したがって読み飛ばして頂けると幸いです。

環境：UBUNTU 14

js-symbolic-executor：

js-symbolic-executor - A symbolic execution engine for JavaScript. - Google Project Hosting

参考サイト：

antコマンドを、通常のunixコマンドへの書き下し方法をご教授下… - 人力検索はてな

ant によりbuild.xmlを実行、さっそくエラー

maru@marU:~/js-symbolic-executor/js-symbolic-executor$ ant
Buildfile: /home/maru/js-symbolic-executor/js-symbolic-executor/build.xml

init:

closure-compiler:

compile:
    [javac] /home/maru/js-symbolic-executor/closure-compiler/build.xml:54: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
    [javac] /home/maru/js-symbolic-executor/closure-compiler/build.xml:60: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds

jar:

check-config.status:

configure-cvc3:
     [exec] checking for g++... g++
     [exec] checking whether the C++ compiler works... yes
     [exec] checking for C++ compiler default output file name... a.out
     [exec] checking for suffix of executables...
     [exec] checking whether we are cross compiling... no
     [exec] checking for suffix of object files... o
     [exec] checking whether we are using the GNU C++ compiler... yes
     [exec] checking whether g++ accepts -g... yes
     [exec] checking how to run the C++ preprocessor... g++ -E
     [exec] checking for ar... ar
     [exec] checking build system type... x86_64-unknown-linux-gnu
     [exec] checking host system type... x86_64-unknown-linux-gnu
     [exec] checking for install... /usr/bin/install
     [exec] checking for ldconfig... /sbin/ldconfig
     [exec] checking for time... /usr/bin/time
     [exec] checking for perl... /usr/bin/perl
     [exec] checking for bison... bison -y
     [exec] checking for flex... flex
     [exec] checking lex output file root... lex.yy
     [exec] checking lex library... none needed
     [exec] checking whether yytext is a pointer... no
     [exec] checking for compiler version (g++ --version)... 4.8.2
     [exec] checking for gmp... yes
     [exec] configure: error: Unable to locate Java directories
     [exec] Result: 1

cvc3:
     [exec] Makefile:1: Makefile.local: そのようなファイルやディレクトリはありません
     [exec] make: *** ターゲット `Makefile.local' を make するルールがありません.  中止.
     [exec] Result: 2

BUILD FAILED
/home/maru/js-symbolic-executor/js-symbolic-executor/build.xml:116: Warning: Could not find file /home/maru/js-symbolic-executor/cvc3/java/lib/libcvc3-3.0.0.jar to copy.

build.xmlターゲットのconfigure-cvc3とcvc3でエラー。

Result 1は失敗？Result2はなんだろう？

まずはconfigure-cvc3

<target name="configure-cvc3"
   depends="check-config.status"
   unless="config.status.present">
    <property name="arith" value="gmp"/>
    <exec dir="../cvc3" executable="./configure">
      <arg value="--enable-java"/>
      <arg value="--enable-dynamic"/>
      <arg value="--with-arith=${arith}"/>
    </exec>
  </target>

上記よりcvc3フォルダで、

$./configure --enable-java --enable-dynamic --with-arith=${gmp}

maru@marU:~/js-symbolic-executor/cvc3$ ./configure --enable-java --enable-dynamic --with-arith=${gmp}
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking how to run the C++ preprocessor... g++ -E
checking for ar... ar
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking for install... /usr/bin/install
checking for ldconfig... /sbin/ldconfig
checking for time... /usr/bin/time
checking for perl... /usr/bin/perl
checking for bison... bison -y
checking for flex... flex
checking lex output file root... lex.yy
checking lex library... none needed
checking whether yytext is a pointer... no
checking for compiler version (g++ --version)... 4.8.2
configure: error: "Unknown argument to with-arith"

次にcvc3ターゲット

ここからは教わったので大丈夫

    <target name="cvc3"
   depends="configure-cvc3,check-config.status"
   unless="config.status.present">
    <exec dir="../cvc3" executable="/usr/bin/make"/>
    <copy file="../cvc3/java/lib/${cvc3.jar}" todir="${lib.dir}" />
  </target>

$ (cd ../cvc3 ; /usr/bin/make)
$ cp ../cvc3/java/lib/libcvc3-3.0.0.jar ./lib

maru@marU:~/js-symbolic-executor/cvc3$ make
Makefile:1: Makefile.local: そのようなファイルやディレクトリはありません
make: *** ターゲット `Makefile.local' を make するルールがありません.  中止.
maru@marU:~/js-symbolic-executor/cvc3$

同じエラー。。。

一端戻って

$./configure (引数を無しにしてみた)

maru@marU:~/js-symbolic-executor/cvc3$ ./configure
checking for g++... g++
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables...
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking how to run the C++ preprocessor... g++ -E
checking for ar... ar
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking for install... /usr/bin/install
checking for ldconfig... /sbin/ldconfig
checking for time... /usr/bin/time
checking for perl... /usr/bin/perl
checking for bison... bison -y
checking for flex... flex
checking lex output file root... lex.yy
checking lex library... none needed
checking whether yytext is a pointer... no
checking for compiler version (g++ --version)... 4.8.2
checking for gmp... yes
checking vector usability... yes
checking vector presence... yes
checking for vector... yes
checking list usability... yes
checking list presence... yes
checking for list... yes
checking deque usability... yes
checking deque presence... yes
checking for deque... yes
checking set usability... yes
checking set presence... yes
checking for set... yes
checking string usability... yes
checking string presence... yes
checking for string... yes
checking cstdlib usability... yes
checking cstdlib presence... yes
checking for cstdlib... yes
checking cstdio usability... yes
checking cstdio presence... yes
checking for cstdio... yes
checking functional usability... yes
checking functional presence... yes
checking for functional... yes
checking algorithm usability... yes
checking algorithm presence... yes
checking for algorithm... yes
checking for doxygen... no
checking for doxytag... no
checking for fig2dev... no
checking for dot... NO
checking for etags... no
checking for ebrowse... no
configure: creating ./config.status
config.status: creating Makefile.local
config.status: creating LICENSE
config.status: creating src/cvc3.pc
config.status: creating bin/unpack
config.status: creating bin/run_tests
config.status: creating bin/cvc2smt
config.status: creating doc/Doxyfile
config.status: creating doc/Makefile

CVC3 is configured successfully.
Platform: x86_64-linux-gnu
Version: 2010-09-02
Computer arithmetic: GMP

Run ./configure --help for additional configuration options.

Type 'make' to compile CVC3.

 成功♪引数の与え方がまずかったのかな？

引き続きmakeとファイルコピー

$ (cd ../cvc3 ; /usr/bin/make)
$ cp ../cvc3/java/lib/libcvc3-3.0.0.jar ./lib

※あまりに長いのでログは省きますがうまくいったようです。

../cvc3/java/lib/libcvc3-3.0.0.jar の./cvc3/java/以下がない。。

maru@marU:~/js-symbolic-executor/cvc3/lib$ ls
libcvc3.a  libcvc3.a.3.0.0  x86_64-linux-gnu

こちらにもコピーされていない。

 cvc3以下、makefileとconfigureファイルにはjarファイルの名前はなし。他で作られてる？

その後、とりあえずターゲットのcvc3がうまく行ったので、antを実行してみる。

buildxmlの呼び出し順とファイルが作られていそうな部分を探す

jar⇒conpile⇒{init,closure-compiler,cvc3}

cvc3⇒configure-cvc3,check-config.status

/js-symbolic-executor/build.xmlでは作られていない！

やっぱ直前のmake?うーん。。 

 そういえばgrep でテキスト検索したらどこかひっかかるんじゃ！

maru@marU:~/js-symbolic-executor$ grep -r libcvc3-3.0.0
.svn/pristine/52/52422e9e03f484c6514ffe9d20b295b7a84062a8.svn-base:  <property name="cvc3.jar" value="libcvc3-3.0.0.jar"/>
.svn/pristine/98/98579381c6ced0569a9f988a8e66e225c7be3737.svn-base:Class-Path: libcvc3-3.0.0.jar
js-symbolic-executor/build.xml:  <property name="cvc3.jar" value="libcvc3-3.0.0.jar"/>
cvc3/java/Test_manifest:Class-Path: libcvc3-3.0.0.jar

 ない・・または勘違いをしている？

maru@marU:~/js-symbolic-executor$ grep -r libcvc3-
js-symbolic-executor/build.xml:  <property name="cvc3.jar" value="libcvc3-3.0.0.jar"/>
cvc3/INSTALL:<code>libcvc3-X.Y.Z.jar</code> (where "X.Y.Z" is the CVC3 version) to
cvc3/INSTALL:    javac -cp lib/libcvc3-X.Y.Z.jar Client.java
cvc3/INSTALL:  java -Djava.library.path=/path/to/cvc3/libs -cp lib/libcvc3-X.Y.Z.jar Client
cvc3/java/Makefile:LIB_CVC3  = libcvc3-$(LIB_VERSION).jar
cvc3/java/README:- libcvc3-X.Y.Z.jar (where "X.Y.Z" is the version of CVC3):
cvc3/java/README:To access the library, you must add the file libcvc3-X.Y.Z.jar (where
cvc3/java/README:1. libcvc3-X.Y.Z.jar, as CVC3 uses the Java wrapper classes
cvc3/java/README:   libcvc3-X.Y.Z.jar
cvc3/java/Test_manifest:Class-Path: libcvc3-3.0.0.jar

 ここかな？INSTALLとmakefileとreadmeを嫁だとおお

面倒だからターゲットcvc3を実行してみよう

ant cvc3　普通に通ったけどjarファイルは生成されない

とりあえず一回antを通してみよう、

それからjarファイルの行方を探してみよう。。。

maru@marU:~/js-symbolic-executor/js-symbolic-executor$ ant
Buildfile: /home/maru/js-symbolic-executor/js-symbolic-executor/build.xml

init:

closure-compiler:

compile:
    [javac] /home/maru/js-symbolic-executor/closure-compiler/build.xml:54: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
    [javac] /home/maru/js-symbolic-executor/closure-compiler/build.xml:60: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds

jar:

check-config.status:

configure-cvc3:

cvc3:

compile:
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/build.xml:69: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
    [javac] Compiling 26 source files to /home/maru/js-symbolic-executor/js-symbolic-executor/build/classes
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicExpression.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:23: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:24: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Op;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:25: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.QueryResult;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:26: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Type;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:27: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.ValidityChecker;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicExpression.java:36: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context);
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: インタフェース SymbolicExpression
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:45: エラー: シンボルを見つけられません
    [javac]   private final ValidityChecker context;
    [javac]                 ^
    [javac]   シンボル:   クラス ValidityChecker
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:51: エラー: シンボルを見つけられません
    [javac]   private final Type intType;
    [javac]                 ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:52: エラー: シンボルを見つけられません
    [javac]   private final Type stringType;
    [javac]                 ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:53: エラー: シンボルを見つけられません
    [javac]   private final Type jsType;
    [javac]                 ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:104: エラー: シンボルを見つけられません
    [javac]   public Expr construct(String constructor, Expr... args) {
    [javac]                                             ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:104: エラー: シンボルを見つけられません
    [javac]   public Expr construct(String constructor, Expr... args) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:120: エラー: シンボルを見つけられません
    [javac]   public Expr lookupVar(String name) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:125: エラー: シンボルを見つけられません
    [javac]   public Op lookupOp(String opString) {
    [javac]          ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:132: エラー: シンボルを見つけられません
    [javac]   public Expr varExpr(String name, Type type) {
    [javac]                                    ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:132: エラー: シンボルを見つけられません
    [javac]   public Expr varExpr(String name, Type type) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:141: エラー: シンボルを見つけられません
    [javac]   public Expr funExpr(String opString, Expr... exprs) {
    [javac]                                        ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:141: エラー: シンボルを見つけられません
    [javac]   public Expr funExpr(String opString, Expr... exprs) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:152: エラー: シンボルを見つけられません
    [javac]   public Expr funExpr(String opString, SymbolicExpression[] args) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:170: エラー: シンボルを見つけられません
    [javac]   private Expr toBoolean(SymbolicExpression constraint) {
    [javac]           ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:205: エラー: シンボルを見つけられません
    [javac]   private HashMap<Expr, Expr> getConcreteModel() {
    [javac]                   ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:205: エラー: シンボルを見つけられません
    [javac]   private HashMap<Expr, Expr> getConcreteModel() {
    [javac]                         ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:210: エラー: シンボルを見つけられません
    [javac]   public Expr jsNum(int n) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:215: エラー: シンボルを見つけられません
    [javac]   public Expr ratExpr(int n){
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:230: エラー: シンボルを見つけられません
    [javac]   private final HashMap<String, Expr> stringConstants = Maps.newHashMap();
    [javac]                                 ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:233: エラー: シンボルを見つけられません
    [javac]   public Expr stringConstant(String string) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:263: エラー: シンボルを見つけられません
    [javac]   private JsValue exprToJsValue(Expr variable, Map<Expr, Expr> model) {
    [javac]                                 ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:263: エラー: シンボルを見つけられません
    [javac]   private JsValue exprToJsValue(Expr variable, Map<Expr, Expr> model) {
    [javac]                                                    ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:263: エラー: シンボルを見つけられません
    [javac]   private JsValue exprToJsValue(Expr variable, Map<Expr, Expr> model) {
    [javac]                                                          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:295: エラー: シンボルを見つけられません
    [javac]   private int exprToJsNum(Expr expr, Map<Expr, Expr> model) {
    [javac]                           ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:295: エラー: シンボルを見つけられません
    [javac]   private int exprToJsNum(Expr expr, Map<Expr, Expr> model) {
    [javac]                                          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:295: エラー: シンボルを見つけられません
    [javac]   private int exprToJsNum(Expr expr, Map<Expr, Expr> model) {
    [javac]                                                ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:317: エラー: シンボルを見つけられません
    [javac]   private String exprToJsString(Expr expr, Map<Expr, Expr> model) {
    [javac]                                 ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:317: エラー: シンボルを見つけられません
    [javac]   private String exprToJsString(Expr expr, Map<Expr, Expr> model) {
    [javac]                                                ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:317: エラー: シンボルを見つけられません
    [javac]   private String exprToJsString(Expr expr, Map<Expr, Expr> model) {
    [javac]                                                      ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:345: エラー: シンボルを見つけられません
    [javac]   private int constIntExprToInt(Expr value) {
    [javac]                                 ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/ApiBasedInputGenerator.java:21: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsBool.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsBool.java:41: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsBool
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsDouble.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsDouble.java:41: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsDouble
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsNull.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsNull.java:36: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsNull
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsString.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsString.java:42: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsString
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsUndefined.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsUndefined.java:36: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsUndefined
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicOperation.java:21: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicOperation.java:53: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス SymbolicOperation
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:47: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス SymbolicValue
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:57: エラー: シンボルを見つけられません
    [javac]     context = ValidityChecker.create();
    [javac]               ^
    [javac]   シンボル:   変数 ValidityChecker
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:88: エラー: シンボルを見つけられません
    [javac]     Expr symVar = varExpr("sym" + i, jsType);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:89: エラー: シンボルを見つけられません
    [javac]     Expr symInt = varExpr("symInt" + i, intType);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:90: エラー: シンボルを見つけられません
    [javac]     Expr symStr = varExpr("symStr" + i, stringType);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:153: エラー: シンボルを見つけられません
    [javac]     Op op = lookupOp(opString);
    [javac]     ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:154: エラー: シンボルを見つけられません
    [javac]     List<Expr> argList = Lists.newArrayListWithCapacity(args.length);
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:184: エラー: シンボルを見つけられません
    [javac]     QueryResult queryResult = context.query(toBoolean(constraint));
    [javac]     ^
    [javac]   シンボル:   クラス QueryResult
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:185: エラー: シンボルを見つけられません
    [javac]     if (queryResult == QueryResult.VALID) {
    [javac]                        ^
    [javac]   シンボル:   変数 QueryResult
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:188: エラー: シンボルを見つけられません
    [javac]     } else if (queryResult == QueryResult.INVALID) {
    [javac]                               ^
    [javac]   シンボル:   変数 QueryResult
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:189: エラー: シンボルを見つけられません
    [javac]       HashMap<Expr, Expr> model = getConcreteModel();
    [javac]               ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:189: エラー: シンボルを見つけられません
    [javac]       HashMap<Expr, Expr> model = getConcreteModel();
    [javac]                     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:234: エラー: シンボルを見つけられません
    [javac]     Expr stringVar = stringConstants.get(string);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:264: エラー: シンボルを見つけられません
    [javac]     Expr value = model.get(variable);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:280: エラー: シンボルを見つけられません
    [javac]       Op operator = value.getOp();
    [javac]       ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:298: エラー: シンボルを見つけられません
    [javac]     List<Expr> varsAlreadySeen = Lists.newArrayList();
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:320: エラー: シンボルを見つけられません
    [javac]     List<Expr> varsAlreadySeen = Lists.newArrayList();
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:322: エラー: シンボルを見つけられません
    [javac]     Op charCons = lookupOp("char_cons");
    [javac]     ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:323: エラー: シンボルを見つけられません
    [javac]     Expr charNil = lookupOp("char_nil").getExpr();
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/ApiBasedInputGenerator.java:52: エラー: シンボルを見つけられません
    [javac]     Set<Expr> assumptions = Sets.newHashSet();
    [javac]         ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス ApiBasedInputGenerator
    [javac] /home/maru/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:48: エラー: シンボルを見つけられません
    [javac]     Expr expr = context.lookupVar(name);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス SymbolicValue
    [javac] エラー72個

BUILD FAILED
/home/maru/js-symbolic-executor/js-symbolic-executor/build.xml:69: Compile failed; see the compiler error output for details.

 ここからはなんかよくわからないけど./cvc3以下を

make distclean

antで通してたな。大丈夫だろうか。。

maru@marU:~/js-symbolic-executor/cvc3$ make distclean
cd /home/maru/js-symbolic-executor/cvc3/src; make distclean
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src' に入ります
make build TARGET=distclean
make[2]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src' に入ります
cd util && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/util' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/util' から出ます
cd context && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/context' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/context' から出ます
cd expr && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/expr' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/expr' から出ます
cd theorem && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theorem' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theorem' から出ます
cd sat && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/sat' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/sat' から出ます
cd theory_core && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_core' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_core' から出ます
cd theory_arith && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_arith' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_arith' から出ます
cd theory_array && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_array' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_array' から出ます
cd theory_bitvector && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_bitvector' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_bitvector' から出ます
cd theory_datatype && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_datatype' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_datatype' から出ます
cd theory_quant && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_quant' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_quant' から出ます
cd theory_records && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_records' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_records' から出ます
cd theory_simulate && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_simulate' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_simulate' から出ます
cd theory_uf && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_uf' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/theory_uf' から出ます
cd search && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/search' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/search' から出ます
cd parser && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/parser' に入ります
rm -f parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parsePL_defs.h parsePL.output parseLisp_defs.h parseLisp.output parsesmtlib_defs.h parsesmtlib.output parsesmtlib2_defs.h parsesmtlib2.output
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/parser' から出ます
cd translator && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/translator' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/translator' から出ます
cd vcl && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/vcl' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/vcl' から出ます
cd c_interface && make distclean
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/c_interface' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/c_interface' から出ます
cd cvc3 && make distclean VERSION=2010-09-02
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/cvc3' に入ります
rm -f
make[3]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src/cvc3' から出ます
make[2]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src' から出ます
rm -rf cvc3.pc
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/src' から出ます
cd /home/maru/js-symbolic-executor/cvc3/doc; make distclean
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/doc' に入ります
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/doc' から出ます
cd /home/maru/js-symbolic-executor/cvc3/test; make distclean
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/test' に入ります
Making dependencies for main.cpp george.cpp
g++ -M -m64 -O2 -Wall -I. -I/home/maru/js-symbolic-executor/cvc3/src/include -O0  main.cpp george.cpp >> /home/maru/js-symbolic-executor/cvc3/test/obj/x86_64-linux-gnu/Makefile.tmp
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/test' から出ます
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/test' に入ります
rm -f
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/test' から出ます
cd /home/maru/js-symbolic-executor/cvc3/java; make distclean
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/java' に入ります
if [ ! -d obj ]; then mkdir -p obj; fi
rm -f src/cvc3/EmbeddedManager.cpp src/cvc3/Expr.cpp src/cvc3/ExprMut.cpp src/cvc3/ExprManager.cpp src/cvc3/Type.cpp src/cvc3/TypeMut.cpp src/cvc3/Op.cpp src/cvc3/OpMut.cpp src/cvc3/Rational.cpp src/cvc3/RationalMut.cpp src/cvc3/Theorem.cpp src/cvc3/TheoremMut.cpp src/cvc3/Proof.cpp src/cvc3/ProofMut.cpp src/cvc3/Context.cpp src/cvc3/ContextMut.cpp src/cvc3/Flag.cpp src/cvc3/Flags.cpp src/cvc3/FlagsMut.cpp src/cvc3/Statistics.cpp src/cvc3/StatisticsMut.cpp src/cvc3/ValidityChecker.cpp
rm -fr obj/cvc3/*
rm -fr /home/maru/js-symbolic-executor/cvc3/java/lib/*
rm -f include/cvc3/EmbeddedManager.h include/cvc3/Expr.h include/cvc3/ExprMut.h include/cvc3/ExprManager.h include/cvc3/Type.h include/cvc3/TypeMut.h include/cvc3/Op.h include/cvc3/OpMut.h include/cvc3/Rational.h include/cvc3/RationalMut.h include/cvc3/Theorem.h include/cvc3/TheoremMut.h include/cvc3/Proof.h include/cvc3/ProofMut.h include/cvc3/Context.h include/cvc3/ContextMut.h include/cvc3/Flag.h include/cvc3/Flags.h include/cvc3/FlagsMut.h include/cvc3/Statistics.h include/cvc3/StatisticsMut.h include/cvc3/ValidityChecker.h include/cvc3/EmbeddedManager.h.gch include/cvc3/Expr.h.gch include/cvc3/ExprMut.h.gch include/cvc3/ExprManager.h.gch include/cvc3/Type.h.gch include/cvc3/TypeMut.h.gch include/cvc3/Op.h.gch include/cvc3/OpMut.h.gch include/cvc3/Rational.h.gch include/cvc3/RationalMut.h.gch include/cvc3/Theorem.h.gch include/cvc3/TheoremMut.h.gch include/cvc3/Proof.h.gch include/cvc3/ProofMut.h.gch include/cvc3/Context.h.gch include/cvc3/ContextMut.h.gch include/cvc3/Flag.h.gch include/cvc3/Flags.h.gch include/cvc3/FlagsMut.h.gch include/cvc3/Statistics.h.gch include/cvc3/StatisticsMut.h.gch include/cvc3/ValidityChecker.h.gch include/cvc3/JniUtils.h.gch
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/java' から出ます
rm -rf /home/maru/js-symbolic-executor/cvc3/test/bin /home/maru/js-symbolic-executor/cvc3/test/obj
cd /home/maru/js-symbolic-executor/cvc3/testc; make distclean
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/testc' に入ります
Making dependencies for
gcc -M -g -I../src/include main.c >> /home/maru/js-symbolic-executor/cvc3/testc/obj/x86_64-linux-gnu/Makefile.tmp
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/testc' から出ます
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/testc' に入ります
rm -f /home/maru/js-symbolic-executor/cvc3/testc/obj/x86_64-linux-gnu/main.o
make[1]: ディレクトリ `/home/maru/js-symbolic-executor/cvc3/testc' から出ます
rm -rf /home/maru/js-symbolic-executor/cvc3/testc/bin /home/maru/js-symbolic-executor/cvc3/testc/obj
mv: `/home/maru/js-symbolic-executor/cvc3/bin/CVS' を stat できません: そのようなファイルやディレクトリはありません
make: [distclean] エラー 1 (無視されました)
mv: `/home/maru/js-symbolic-executor/cvc3/bin/.cvsignore' を stat できません: そのようなファイルやディレクトリはありません
make: [distclean] エラー 1 (無視されました)
rm -rf /home/maru/js-symbolic-executor/cvc3/bin
rm -f TAGS BROWSE FILES LICENSE Makefile.local
rm -rf /home/maru/js-symbolic-executor/cvc3/autom4te.cache
rm -f config.log config.status
rm -f regressions.log
rm -rf /home/maru/js-symbolic-executor/cvc3/lib /home/maru/js-symbolic-executor/cvc3/obj

で、なんかよくわからんけど通った！となるはずが通らない！うーむ。

一日中張り付いてこれは死にたくなる（笑

とりあえず明日かなあ。。