2015-02-09

javascript unix上でデバッグ方法メモ

sudo apt-get install libv8-dev
cp /usr/share/doc/libv8-dev/examples/shell.cc.gz .
gunzip shell.cc.gz
g++ shell.cc -lv8

2014-12-24

後に取り組むかもしれないメモ（落書き）

JPFを使ってみた

時間があれば原因を調べる、可能性のありそうなものから
・バージョンの問題（eclipse側で追ってみる
・ファイルが欠損していなかったか

1. windows側 - tortoisehgより落としたもの

1_1cmdより

C:\Users\mar\sharefolder\jpf-symbc>ant
Buildfile: C:\Users\mar\sharefolder\jpf-symbc\build.xml

-init:

-compile-annotations:

-compile-main:
    [javac] Compiling 266 source files to C:\Users\mar\sharefolder\jpf-symbc\build\main
    [javac] 警告: [options] ブートストラップ・クラスパスが-source 1.6と一緒に設定されていません

    [javac] 警告: [options] ソース値1.6は廃止されていて、今後のリリースで削除される予定です
    [javac] 警告: [options] 廃止されたオプションについての警告を表示しないようにするには、-Xlin
t:オプションを使用します。

1_2 unix側(JDK1.8_40とJDK-7-oracle)

Buildfile: /mnt/sharefolder/jpf-symbc/build.xml

-init:

-compile-annotations:

-compile-main:
    [javac] Compiling 266 source files to /mnt/sharefolder/jpf-symbc/build/main
    [javac] 警告: [options] ブートストラップ・クラスパスが-source 1.6と一緒に設定されていません
    [javac] /mnt/sharefolder/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:3: エラー: シンボルを見つけられません
    [javac] import gov.nasa.jpf.ListenerAdapter;
    [javac]                    ^
    [javac]   シンボル:   クラス ListenerAdapter
    [javac]   場所: パッケージ gov.nasa.jpf
    [javac] /mnt/sharefolder/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:4: エラー: パッケージgov.nasa.jpf.searchは存在しません
    [javac] import gov.nasa.jpf.search.Search;
    [javac]                           ^
    [javac] /mnt/sharefolder/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:7: エラー: シンボルを見つけられません
    [javac] public class GreenListener extends ListenerAdapter {
    [javac]                                    ^
    [javac]   シンボル: クラス ListenerAdapter
    [javac] /mnt/sharefolder/jpf-symbc/src/main/gov/nasa/jpf/symbc/GreenListener.java:12: エラー: シンボルを見つけられません
    [javac] 	public void searchFinished(Search s) {
    [javac] 	                           ^
    [javac]   シンボル:   クラス Search
    [javac]   場所: クラス GreenListener

2. windows - eclipseより落としたもの

2_1.eclipseでは通らない

 [javac] コンパイラで例外が発生しました(1.9.0-ea)。Bug Paradeに同じバグが登録されていないことをご確認の上、Java Developer Connection(http://java.sun.com/webapps/bugreport)でバグの登録をお願いいたします。レポートには、そのプログラムと下記の診断内容を含めてください。ご協力ありがとうございます。
    [javac] java.lang.NoSuchMethodError: java.nio.ByteBuffer.position(I)Ljava/nio/ByteBuffer;
    [javac] 	at com.sun.tools.javac.util.BaseFileManager.makeByteBuffer(BaseFileManager.java:336)
    [javac] 	at com.sun.tools.javac.file.RegularFileObject.getCharContent(RegularFileObject.java:118)
    [javac] 	at com.sun.tools.javac.file.RegularFileObject.getCharContent(RegularFileObject.java:56)

2_2.Dropbox経由では通った(JDK_7_oracle)
ただし1_2のシンボルを見つけられない（つまりファイルが存在しない点については同じ状況であった）

2014-11-22

今日の取り組み

js-symbolic-execution導入続き

機能に引き続き再びチャレンジ！今日はよく寝たし、うまく行くはず...!

maru@marU:/mnt/sharefolder/js-symbolic-executor/js-symbolic-executor$ ant
Buildfile: /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml

init:

closure-compiler:

compile:
    [javac] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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 /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build/classes
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicExpression.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:23: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:24: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Op;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:25: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.QueryResult;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:26: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Type;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:27: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.ValidityChecker;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicExpression.java:36: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context);
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: インタフェース SymbolicExpression
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:45: エラー: シンボルを見つけられません
    [javac]   private final ValidityChecker context;
    [javac]                 ^
    [javac]   シンボル:   クラス ValidityChecker
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:51: エラー: シンボルを見つけられません
    [javac]   private final Type intType;
    [javac]                 ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:52: エラー: シンボルを見つけられません
    [javac]   private final Type stringType;
    [javac]                 ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:53: エラー: シンボルを見つけられません
    [javac]   private final Type jsType;
    [javac]                 ^
    [javac]   シンボル:   クラス Type
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:120: エラー: シンボルを見つけられません
    [javac]   public Expr lookupVar(String name) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:125: エラー: シンボルを見つけられません
    [javac]   public Op lookupOp(String opString) {
    [javac]          ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:170: エラー: シンボルを見つけられません
    [javac]   private Expr toBoolean(SymbolicExpression constraint) {
    [javac]           ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:205: エラー: シンボルを見つけられません
    [javac]   private HashMap<Expr, Expr> getConcreteModel() {
    [javac]                   ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:205: エラー: シンボルを見つけられません
    [javac]   private HashMap<Expr, Expr> getConcreteModel() {
    [javac]                         ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:210: エラー: シンボルを見つけられません
    [javac]   public Expr jsNum(int n) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:215: エラー: シンボルを見つけられません
    [javac]   public Expr ratExpr(int n){
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/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] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:233: エラー: シンボルを見つけられません
    [javac]   public Expr stringConstant(String string) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/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] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:345: エラー: シンボルを見つけられません
    [javac]   private int constIntExprToInt(Expr value) {
    [javac]                                 ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/ApiBasedInputGenerator.java:21: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsBool.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsBool.java:41: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsBool
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsDouble.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsDouble.java:41: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsDouble
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsNull.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsNull.java:36: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsNull
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsString.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsString.java:42: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsString
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsUndefined.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsUndefined.java:36: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス JsUndefined
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicOperation.java:21: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicOperation.java:53: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス SymbolicOperation
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:19: エラー: パッケージcvc3は存在しません
    [javac] import cvc3.Expr;
    [javac]            ^
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:47: エラー: シンボルを見つけられません
    [javac]   public Expr toCvc3(Cvc3Context context) {
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス SymbolicValue
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:57: エラー: シンボルを見つけられません
    [javac]     context = ValidityChecker.create();
    [javac]               ^
    [javac]   シンボル:   変数 ValidityChecker
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:88: エラー: シンボルを見つけられません
    [javac]     Expr symVar = varExpr("sym" + i, jsType);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:89: エラー: シンボルを見つけられません
    [javac]     Expr symInt = varExpr("symInt" + i, intType);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:90: エラー: シンボルを見つけられません
    [javac]     Expr symStr = varExpr("symStr" + i, stringType);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:153: エラー: シンボルを見つけられません
    [javac]     Op op = lookupOp(opString);
    [javac]     ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/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] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:184: エラー: シンボルを見つけられません
    [javac]     QueryResult queryResult = context.query(toBoolean(constraint));
    [javac]     ^
    [javac]   シンボル:   クラス QueryResult
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:185: エラー: シンボルを見つけられません
    [javac]     if (queryResult == QueryResult.VALID) {
    [javac]                        ^
    [javac]   シンボル:   変数 QueryResult
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:188: エラー: シンボルを見つけられません
    [javac]     } else if (queryResult == QueryResult.INVALID) {
    [javac]                               ^
    [javac]   シンボル:   変数 QueryResult
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:189: エラー: シンボルを見つけられません
    [javac]       HashMap<Expr, Expr> model = getConcreteModel();
    [javac]               ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:189: エラー: シンボルを見つけられません
    [javac]       HashMap<Expr, Expr> model = getConcreteModel();
    [javac]                     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:234: エラー: シンボルを見つけられません
    [javac]     Expr stringVar = stringConstants.get(string);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:264: エラー: シンボルを見つけられません
    [javac]     Expr value = model.get(variable);
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:280: エラー: シンボルを見つけられません
    [javac]       Op operator = value.getOp();
    [javac]       ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:298: エラー: シンボルを見つけられません
    [javac]     List<Expr> varsAlreadySeen = Lists.newArrayList();
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:320: エラー: シンボルを見つけられません
    [javac]     List<Expr> varsAlreadySeen = Lists.newArrayList();
    [javac]          ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:322: エラー: シンボルを見つけられません
    [javac]     Op charCons = lookupOp("char_cons");
    [javac]     ^
    [javac]   シンボル:   クラス Op
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:323: エラー: シンボルを見つけられません
    [javac]     Expr charNil = lookupOp("char_nil").getExpr();
    [javac]     ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス Cvc3Context
    [javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/ApiBasedInputGenerator.java:52: エラー: シンボルを見つけられません
    [javac]     Set<Expr> assumptions = Sets.newHashSet();
    [javac]         ^
    [javac]   シンボル:   クラス Expr
    [javac]   場所: クラス ApiBasedInputGenerator
    [javac] /mnt/sharefolder/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
/mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml:69: Compile failed; see the compiler error output for details.

Total time: 27 seconds

build.xml実行部分のターゲット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>

configure-cvc3、check-config.statusは完了している。
ので一度cvc3ターゲットを再現してみる
（antで実行できなかったものを、コマンドで実行する理由ってなんだろう？）

makeで凄い膨大な量のコメントが出る。
antで出ないのは、そういった仕様なんでしょうか。
いっぱい出ちゃうと、ant自体がどこまで進んだかわかりませんもんね。

makeの終わりの方のログ(続きより*2に全てのログ)

Unpacking parser
Unpacking translator
Unpacking vcl
Unpacking c_interface
cat UNPACKED | xargs g++ -shared -m64 -fPIC  \
    -Wl,-soname,libcvc3.so.3 -o '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0' `` -lgmp 
/sbin/ldconfig -nv /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu
/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu:
	<span style="color: #cc0000">libcvc3.so.3 -> libcvc3.so.3.0.0/sbin/ldconfig.real: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3 から libcvc3.so.3.0.0 へリンクできません</span>
 (スキップされました)
ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0
<span style="color: #cc0000">ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです</span>
<span style="color: #cc0000">make[2]: *** [/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0] エラー 1
</span>
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make[1]: *** [build] エラー 2
make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make: *** [build] エラー 2

と、とりあえずmakefile読んでみる！(*makefile初心者)
（ところでこのようなエラーを見るのってどのくらい常識なんでしょうか・・。やはり問題が発生しない限り見ないもの？）

makefileには情報はなく、そこから色々なファイルを実行していてそれらを読む必要がありそう。
（先ほどのCVC3ターゲットのエラーの真の原因はここ？手当たり次第やるより、もう少し広く見た方がいいかも、まだcvc3ターゲットのどのコマンドが失敗だったか理解していない）

とりあえずlibのリンクがどこかに対してできていない。libcvc3.so.3.0.0ファイルは存在している
make[2]:***はよくわからないけどmakeじゃ検索できないし、エラーでも出てこないから標準出力かな？ググるも出てこない

直感だとlibcvc3.so.3リンクを張れていない事によるエラーをひきずっている気がする。
どこのシンボリックリンクを張れなかったのかはまだわからない。
(find再帰のお勉強)

maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ find -name libcvc3.so.3*
./lib/x86_64-linux-gnu/libcvc3.so.3.0.0

ファイルは見当たらず、エラーもまだわからない
grepで実行ファイルを洗い出しエラーの特定しかないかな（-）
今更だが、海外のソフトで日本語のエラーがでるはずがない事に気づく
日本語以外のログで検索せねば。

/usr/local/lib、javahome以下に無し

maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ grep -r libcvc3.so.3
バイナリファイル lib/x86_64-linux-gnu/libcvc3.so.3.0.0 に一致しました
maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ ^C
maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ grep -r libcvc3.so.
INSTALL:variable) and both <code>libcvc3.so</code> and
java/README:libcvc3.so (by default, /usr/local/lib) and the Java library into
java/README:CLASSPATH environment variable) and both libcvc3.so and libcvc3jni.so
java/README:Note that libcvc3.so and libcvc3jni.so may be installed into different
java/README:3. libcvc3.so, as it is used by libcvc3jni.so
java/README:Make sure that the version of libcvc3.so found at runtime has the same

cvc/java/READMEのヘルプ
http://js-symbolic-executor.googlecode.com/svn/trunk/cvc3/java/README
いずれにおいてもlibcvc3.soの説明ならあるが、libcvc3.so.3の説明は特になし

makeのログでlibcvc3を検索、ヒントになりそうな所はなし。

そういえば、make正確にはその他ファイルはどのようなログをはいているのだろうか。実行ログだったら参考になるが、そのようには所々コマンドのようでコマンドではないようなログもある

libcvc3.so.3は一般のファイルなのかなということでググってみる
ひっかかるのは大抵自分の質問（苦笑
ただ、似た種類だとrpmで落とせるのかな？

libcvc3.so.2なら落とせそうだけどなあ
rpm -ivh libcvc3.so.3　とはいかないしなあ
そもそもlivcvc3ってなんやねん！パッケージでやっている事をググっても出てこない。マイナーなファイルなのかな

rpmインストールして、パッケージ検索してみようかなんて遊んでたら
maru@marU:/$ sudo apt-get install libcvc3-
libcvc3-5 libcvc3-5-java libcvc3-5-jni libcvc3-dev
予測変換でちょっと関係ないのが出てきた
libcvc3って普通に落とせてインストールする関係のファイル？

少し戻って、makeの後は、コピーファイル。そのファイルが存在しないのでやっぱこのmakeの問題を解決しなければならないらしい（遅

うーん。rpmコマンド入れてみたけど、まだインストールしていないパッケージを探す方法はググってもない？直感だとありそうだけどなあ

次の手段は何だろう。そろそろ思いつかない
１．livcvc3.so.5と少し違うものをいれてみる
２．もともとjavaにもあるということで、他のJDKを入れてみる
３．make distcleanというおまじないをcvc以下で唱えてみる

とりあえず手頃なので前回失敗した理由のよくわからない、３番を試すだけ試す
なんかさっきよりも進んでるっぽい・・。もやもやする。
$ ../cvc3 make distclean
$ ../js-symbolic-executor ant (*1　続きより)

経緯
少し前に../js-symbolic-execution antを実行してcvc3ターゲットが実行できていない
cvc3ターゲットの初手の../cvc3 makeを実行する
../cvc3 make distcleanする
../js-symbolic-execution ant
ただのまやかしな気がします。
そもそも　初手のcvc3ターゲットをantで実行した際にmakeは実行されていたのでしょうか？いなかった気がする

ant終わったけど通っていませんでした。
出たエラーは同様のものでしたね。

２．のJDKについてwindows上のJdk 1.9.0,1.8_25,1.8.0_20にはありませんでしたね。

とりあえず今日は夜更かししすぎちゃったので、ここまで。
質問するにも質問が難しすぎる
libcvc3.so.3はどこから手に入りますか。と聞いても入手方法知ってる人いなさそう・・

続きはdistclean後のant(*1)とmake(*2)の全ログ

2014-11-21

「はてな記法」のれんしゅう

あとでターミナル画面とシェルを探して更新してみよう

「>|ruby|」と「||<」を行の最初に持ってくる。（シンタックスがオンになってない方は半角スペース空いている

 class Foo
   def bar'baz' # return baz
   end
 end

>|ruby|
class Foo
def bar'baz' # return baz
end
end
| | <

参考：
<a href="http://d.hatena.ne.jp/hatenadiary/20061215/1166155734">入力したプログラムコードを色付けするスーパーpre記法シンタックス・ハイライトの実装について - はてなダイアリー日記</a>
入力したプログラムコードを色付けするスーパーpre記法シンタックス・ハイライトの実装について - はてなダイアリー日記

ソースコードを色付けして記述する（シンタックス・ハイライト） - はてなダイアリーのヘルプ

2014-11-21

error: Unable to locate Java directoriesの対処法

質問解決

<a href="http://q.hatena.ne.jp/1416546990" data-mce-href="http://q.hatena.ne.jp/1416546990"> error: Unable to locate Java directoriesの対処法こちらで詳しく質問させて頂いています。…</a>
error: Unable to locate Java directoriesの対処法こちらで詳… - 人力検索はてな

error: Unable to locate Java directoriesの対処法

$ ./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
checking for gmp... yes
configure: error: Unable to locate Java directories
$ echo $PATH
/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/usr/local/java/jdk1.8.0_40/bin

==エラーの箇所（configure）==

if ! ( test -n "${JAVA_INCLUDE_PATH}" -a -d "${JAVA_INCLUDE_PATH}" ) ; then
if test -d ${JAVA_HOME}/include ; then
JAVA_INCLUDE_PATH=${JAVA_HOME}/include
elif test -d ${JAVA_HOME}/Headers; then
JAVA_INCLUDE_PATH=-I${JAVA_HOME}/Headers
else
as_fn_error "Unable to locate Java directories" "$LINENO" 5
fi

"${JAVA_INCLUDE_PATH}が何を指しているのかわかれば問題がきちんとわかりそうなので追ってみました。

# Check whether --with-java-includes was given.
if test "${with_java_includes+set}" = set; then :
withval=$with_java_includes; JAVA_INCLUDE_PATH="${withval}"
fi

問題はここかなと思うのですが、shellに関して詳しくないためうまく構文が把握できません。

質問①：
>if test "${with_java_includes+set}" = set; then :
これはtest構文かと思うのですが、 = は　"eq"を意味し、"${with_java_includes+set}" と set　が同値であるかの真偽判定をしているのでしょうか？

質問②：
setとは何を指すものなのでしょうか？
configure中にはsetは無数にあり、
shellではセットはオプションであり、今回のsetとは関係ないように感じ、どう解釈すべきか迷っています。

質問③：

このエラーの原因について
JAVA_HOMEが設定されているので、きちんとJDKが導入されていないという事になるのでしょうか？
普通はconfigureを追う事なく、JDKの確認を皆様ならされますか？

任意質問④：

># Check whether --with-java-includes was given.

は./configure 実行時にオプションとして--with-java-includesが存在するかどうかチェックしているといった解説なのでしょうか。

最後に./configureファイルの中身を添付させて頂きます

Dropbox - configure

2014-11-20

■

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

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

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

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

環境：UBUNTU 14

js-symbolic-executor：

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

参考サイト：

&amp;amp;amp;amp;amp;amp;amp;lt;a href="http://q.hatena.ne.jp/1416132420" data-mce-href="http://q.hatena.ne.jp/1416132420"&amp;amp;amp;amp;amp;amp;amp;gt;antコマンドを、通常のunixコマンドへの書き下し方法をご教授下さい。…&amp;amp;amp;amp;amp;amp;amp;lt;/a&amp;amp;amp;amp;amp;amp;amp;gt;
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

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

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

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