From 67ca5794e4fcb8d754034d8a65685b3a6552ca92 Mon Sep 17 00:00:00 2001
From: l-kent <56100168+l-kent@users.noreply.github.com>
Date: Mon, 13 Apr 2020 17:09:23 +1000
Subject: [PATCH] updated mill, officially named tool
---
.gitignore | 3 +-
Makefile | 38 ++--
README.md | 12 +-
build.sc | 4 +-
buildandtest.sh | 2 +-
buildparser.sh | 5 +-
mill | 21 +-
{tool => wemelt}/lib/beaver-rt-0.9.11.jar | Bin
{tool => wemelt}/lib/com.microsoft.z3.jar | Bin
{tool => wemelt}/lib/libz3.dylib | Bin
{tool => wemelt}/lib/libz3.so | Bin
{tool => wemelt}/lib/libz3java.dylib | Bin
{tool => wemelt}/lib/libz3java.so | Bin
.../src/tool => wemelt/src/wemelt}/Exec.scala | 2 +-
.../src/wemelt}/Expression.scala | 2 +-
.../tool => wemelt/src/wemelt}/Parser.grammar | 2 +-
.../tool => wemelt/src/wemelt}/Parser.java | 2 +-
.../src/tool => wemelt/src/wemelt}/SMT.scala | 2 +-
.../tool => wemelt/src/wemelt}/Scanner.flex | 4 +-
.../tool => wemelt/src/wemelt}/Scanner.java | 199 ++++++++++++------
.../tool => wemelt/src/wemelt}/State.scala | 2 +-
.../src/wemelt}/Statement.scala | 2 +-
.../tool => wemelt/src/wemelt}/VarDef.scala | 2 +-
.../src/wemelt/WeMeLT.scala | 8 +-
.../tool => wemelt/src/wemelt}/package.scala | 2 +-
25 files changed, 191 insertions(+), 123 deletions(-)
rename {tool => wemelt}/lib/beaver-rt-0.9.11.jar (100%)
rename {tool => wemelt}/lib/com.microsoft.z3.jar (100%)
rename {tool => wemelt}/lib/libz3.dylib (100%)
rename {tool => wemelt}/lib/libz3.so (100%)
rename {tool => wemelt}/lib/libz3java.dylib (100%)
rename {tool => wemelt}/lib/libz3java.so (100%)
rename {tool/src/tool => wemelt/src/wemelt}/Exec.scala (99%)
rename {tool/src/tool => wemelt/src/wemelt}/Expression.scala (99%)
rename {tool/src/tool => wemelt/src/wemelt}/Parser.grammar (99%)
rename {tool/src/tool => wemelt/src/wemelt}/Parser.java (99%)
rename {tool/src/tool => wemelt/src/wemelt}/SMT.scala (99%)
rename {tool/src/tool => wemelt/src/wemelt}/Scanner.flex (98%)
rename {tool/src/tool => wemelt/src/wemelt}/Scanner.java (89%)
rename {tool/src/tool => wemelt/src/wemelt}/State.scala (99%)
rename {tool/src/tool => wemelt/src/wemelt}/Statement.scala (99%)
rename {tool/src/tool => wemelt/src/wemelt}/VarDef.scala (99%)
rename tool/src/tool/Tool.scala => wemelt/src/wemelt/WeMeLT.scala (95%)
rename {tool/src/tool => wemelt/src/wemelt}/package.scala (99%)
diff --git a/.gitignore b/.gitignore
index e5fb27a..c210260 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,5 +2,4 @@ out/
*.iml
.idea/
build/
-armlogictool.sh
-
+wemelt.sh
\ No newline at end of file
diff --git a/Makefile b/Makefile
index 2bf9909..2bac421 100644
--- a/Makefile
+++ b/Makefile
@@ -2,35 +2,35 @@
MILL = ./mill
-TOOL_JAVA = tool/src/tool/Parser.java \
- tool/src/tool/Scanner.java
+WEMELT_JAVA = wemelt/src/wemelt/Parser.java \
+ wemelt/src/wemelt/Scanner.java
-TOOL_JAR = out/tool/jar/dest/out.jar
-TOOL_LAUNCHER = ./out/tool/launcher/dest/run
-TOOL_SH = ./armlogictool.sh
+WEMELT_JAR = out/wemelt/jar/dest/out.jar
+WEMELT_LAUNCHER = ./out/wemelt/launcher/dest/run
+WEMELT_SH = ./wemelt.sh
-all: parser $(TOOL_JAR) $(TOOL_SH) macos_sip_fix
+all: parser $(WEMELT_JAR) $(WEMELT_SH) macos_sip_fix
-parser: $(TOOL_JAVA)
+parser: $(WEMELT_JAVA)
clean:
$(MILL) clean
- rm -f $(TOOL_JAVA)
- rm -f $(TOOL_SH)
+ rm -f $(WEMELT_JAVA)
+ rm -f $(WEMELT_SH)
check-dependencies:
$(MILL) mill.scalalib.Dependency/updates
-$(TOOL_LAUNCHER):
+$(WEMELT_LAUNCHER):
@echo $@
- $(MILL) tool.launcher
+ $(MILL) wemelt.launcher
-$(TOOL_JAR):
+$(WEMELT_JAR):
@echo $@
- $(MILL) tool.jar
+ $(MILL) wemelt.jar
-$(TOOL_SH): $(TOOL_LAUNCHER)
- @echo "[echo] $@"; echo "#!/usr/bin/env bash" > $@; echo "export LD_LIBRARY_PATH=$(PWD)/tool/lib" >> $@; echo "source $(TOOL_LAUNCHER)" >> $@
+$(WEMELT_SH): $(WEMELT_LAUNCHER)
+ @echo "[echo] $@"; echo "#!/usr/bin/env bash" > $@; echo "export LD_LIBRARY_PATH=$(PWD)/wemelt/lib" >> $@; echo "source $(WEMELT_LAUNCHER)" >> $@
@echo "[chmod] $@"; chmod +x $@
%.java: %.grammar
@@ -39,13 +39,13 @@ $(TOOL_SH): $(TOOL_LAUNCHER)
%.java: %.flex
jflex -nobak $^
-o: $(TOOL_OBJ)
- @echo $(TOOL_OBJ)
+o: $(WEMELT_OBJ)
+ @echo $(WEMELT_OBJ)
-macos_sip_fix: tool/lib/libz3java.dylib tool/lib/libz3.dylib
+macos_sip_fix: wemelt/lib/libz3java.dylib wemelt/lib/libz3.dylib
@if [ $$(uname -s) = "Darwin" ]; then \
make -s libz3java.dylib libz3.dylib; \
fi
-lib%.dylib: tool/lib/lib%.dylib
+lib%.dylib: wemelt/lib/lib%.dylib
ln -s $<
diff --git a/README.md b/README.md
index fb94f5b..461488a 100644
--- a/README.md
+++ b/README.md
@@ -9,17 +9,17 @@
## Building
-The tool should build by typing `make` in the top-level directory.
+WeMeLT should build by typing `make` in the top-level directory.
```
make
```
-This should produce a shell script `armlogictool.sh` for running it.
+This should produce a shell script `wemelt.sh` for running it.
## Running
-Run `armlogictool.sh`, supplying a list of files to analyse as command line
+Run `wemelt.sh`, supplying a list of files to analyse as command line
arguments.
`-v` can be used ato print the P, D, and Gamma values after each statement
@@ -27,9 +27,9 @@ arguments.
`-d` can be used to print additional debug information
```
-./armlogictool.sh file1 file2 ..
-./armlogictool.sh -v file1 file2 ..
-./armlogictool.sh -d file1 file2 ..
+./wemelt.sh file1 file2 ..
+./wemelt.sh -v file1 file2 ..
+./wemelt.sh -d file1 file2 ..
```
## Input file format
diff --git a/build.sc b/build.sc
index d659a2a..f1cd72e 100644
--- a/build.sc
+++ b/build.sc
@@ -1,9 +1,9 @@
import mill._
import mill.scalalib._
-object tool extends ScalaModule {
+object wemelt extends ScalaModule {
def scalaVersion = "2.12.8"
- def mainClass = Some("tool.Tool")
+ def mainClass = Some("wemelt.WeMeLT")
def unmanagedClasspath = T {
if (!ammonite.ops.exists(millSourcePath / "lib")) Agg()
else Agg.from(ammonite.ops.ls(millSourcePath / "lib").map(PathRef(_)))
diff --git a/buildandtest.sh b/buildandtest.sh
index 6d4848b..66a50a7 100644
--- a/buildandtest.sh
+++ b/buildandtest.sh
@@ -1,3 +1,3 @@
make clean
make
-./armlogictool.sh tests/* examples/*
+./wemelt.sh tests/* examples/*
diff --git a/buildparser.sh b/buildparser.sh
index 2018209..55e7d7c 100755
--- a/buildparser.sh
+++ b/buildparser.sh
@@ -1,3 +1,2 @@
-jflex -nobak tool/src/tool/Scanner.flex
-java -jar beaver.jar -t tool/src/tool/Parser.grammar
-
+jflex -nobak wemelt/src/wemelt/Scanner.flex
+java -jar beaver.jar -t wemelt/src/wemelt/Parser.grammar
diff --git a/mill b/mill
index d28d914..c16b90a 100755
--- a/mill
+++ b/mill
@@ -3,7 +3,7 @@
# This is a wrapper script, that automatically download mill from GitHub release pages
# You can give the required mill version with MILL_VERSION env variable
# If no version is given, it falls back to the value of DEFAULT_MILL_VERSION
-DEFAULT_MILL_VERSION=0.5.1
+DEFAULT_MILL_VERSION=0.6.1
set -e
@@ -17,13 +17,24 @@ if [ -z "$MILL_VERSION" ] ; then
fi
fi
-MILL_DOWNLOAD_PATH="$HOME/.mill/download"
-MILL_EXEC_PATH="${MILL_DOWNLOAD_PATH}/$MILL_VERSION"
+if [ "x${XDG_CACHE_HOME}" != "x" ] ; then
+ MILL_DOWNLOAD_PATH="${XDG_CACHE_HOME}/mill/download"
+else
+ MILL_DOWNLOAD_PATH="${HOME}/.cache/mill/download"
+fi
+MILL_EXEC_PATH="${MILL_DOWNLOAD_PATH}/${MILL_VERSION}"
+
+version_remainder="$MILL_VERSION"
+MILL_MAJOR_VERSION="${version_remainder%%.*}"; version_remainder="${version_remainder#*.}"
+MILL_MINOR_VERSION="${version_remainder%%.*}"; version_remainder="${version_remainder#*.}"
if [ ! -x "$MILL_EXEC_PATH" ] ; then
mkdir -p $MILL_DOWNLOAD_PATH
+ if [ "$MILL_MAJOR_VERSION" -gt 0 ] || [ "$MILL_MINOR_VERSION" -ge 5 ] ; then
+ ASSEMBLY="-assembly"
+ fi
DOWNLOAD_FILE=$MILL_EXEC_PATH-tmp-download
- MILL_DOWNLOAD_URL="https://github.com/lihaoyi/mill/releases/download/${MILL_VERSION%%-*}/$MILL_VERSION-assembly"
+ MILL_DOWNLOAD_URL="https://github.com/lihaoyi/mill/releases/download/${MILL_VERSION%%-*}/$MILL_VERSION${ASSEMBLY}"
curl --fail -L -o "$DOWNLOAD_FILE" "$MILL_DOWNLOAD_URL"
chmod +x "$DOWNLOAD_FILE"
mv "$DOWNLOAD_FILE" "$MILL_EXEC_PATH"
@@ -34,4 +45,4 @@ fi
unset MILL_DOWNLOAD_PATH
unset MILL_VERSION
-exec $MILL_EXEC_PATH -i "$@"
+exec $MILL_EXEC_PATH "$@"
\ No newline at end of file
diff --git a/tool/lib/beaver-rt-0.9.11.jar b/wemelt/lib/beaver-rt-0.9.11.jar
similarity index 100%
rename from tool/lib/beaver-rt-0.9.11.jar
rename to wemelt/lib/beaver-rt-0.9.11.jar
diff --git a/tool/lib/com.microsoft.z3.jar b/wemelt/lib/com.microsoft.z3.jar
similarity index 100%
rename from tool/lib/com.microsoft.z3.jar
rename to wemelt/lib/com.microsoft.z3.jar
diff --git a/tool/lib/libz3.dylib b/wemelt/lib/libz3.dylib
similarity index 100%
rename from tool/lib/libz3.dylib
rename to wemelt/lib/libz3.dylib
diff --git a/tool/lib/libz3.so b/wemelt/lib/libz3.so
similarity index 100%
rename from tool/lib/libz3.so
rename to wemelt/lib/libz3.so
diff --git a/tool/lib/libz3java.dylib b/wemelt/lib/libz3java.dylib
similarity index 100%
rename from tool/lib/libz3java.dylib
rename to wemelt/lib/libz3java.dylib
diff --git a/tool/lib/libz3java.so b/wemelt/lib/libz3java.so
similarity index 100%
rename from tool/lib/libz3java.so
rename to wemelt/lib/libz3java.so
diff --git a/tool/src/tool/Exec.scala b/wemelt/src/wemelt/Exec.scala
similarity index 99%
rename from tool/src/tool/Exec.scala
rename to wemelt/src/wemelt/Exec.scala
index d9b86f9..4278cdf 100644
--- a/tool/src/tool/Exec.scala
+++ b/wemelt/src/wemelt/Exec.scala
@@ -1,4 +1,4 @@
-package tool
+package wemelt
// remnant of handling break/continue/returns - might be useful in future
sealed trait Cont {
diff --git a/tool/src/tool/Expression.scala b/wemelt/src/wemelt/Expression.scala
similarity index 99%
rename from tool/src/tool/Expression.scala
rename to wemelt/src/wemelt/Expression.scala
index cc157bd..2eda87c 100644
--- a/tool/src/tool/Expression.scala
+++ b/wemelt/src/wemelt/Expression.scala
@@ -1,4 +1,4 @@
-package tool
+package wemelt
trait Expression extends beaver.Symbol {
diff --git a/tool/src/tool/Parser.grammar b/wemelt/src/wemelt/Parser.grammar
similarity index 99%
rename from tool/src/tool/Parser.grammar
rename to wemelt/src/wemelt/Parser.grammar
index face88d..5e38910 100644
--- a/tool/src/tool/Parser.grammar
+++ b/wemelt/src/wemelt/Parser.grammar
@@ -1,4 +1,4 @@
-%package "tool";
+%package "wemelt";
%class "Parser";
%terminals VAR;
diff --git a/tool/src/tool/Parser.java b/wemelt/src/wemelt/Parser.java
similarity index 99%
rename from tool/src/tool/Parser.java
rename to wemelt/src/wemelt/Parser.java
index db77efc..6056922 100644
--- a/tool/src/tool/Parser.java
+++ b/wemelt/src/wemelt/Parser.java
@@ -1,4 +1,4 @@
-package tool;
+package wemelt;
import beaver.*;
import java.util.ArrayList;
diff --git a/tool/src/tool/SMT.scala b/wemelt/src/wemelt/SMT.scala
similarity index 99%
rename from tool/src/tool/SMT.scala
rename to wemelt/src/wemelt/SMT.scala
index ddde5c5..99b28b4 100644
--- a/tool/src/tool/SMT.scala
+++ b/wemelt/src/wemelt/SMT.scala
@@ -1,4 +1,4 @@
-package tool
+package wemelt
import com.microsoft.z3
diff --git a/tool/src/tool/Scanner.flex b/wemelt/src/wemelt/Scanner.flex
similarity index 98%
rename from tool/src/tool/Scanner.flex
rename to wemelt/src/wemelt/Scanner.flex
index 3062d04..71bb90d 100644
--- a/tool/src/tool/Scanner.flex
+++ b/wemelt/src/wemelt/Scanner.flex
@@ -1,7 +1,7 @@
-package tool;
+package wemelt;
import beaver.Symbol;
-import tool.Parser.Terminals;
+import wemelt.Parser.Terminals;
%%
diff --git a/tool/src/tool/Scanner.java b/wemelt/src/wemelt/Scanner.java
similarity index 89%
rename from tool/src/tool/Scanner.java
rename to wemelt/src/wemelt/Scanner.java
index 1f07c7d..55241a8 100644
--- a/tool/src/tool/Scanner.java
+++ b/wemelt/src/wemelt/Scanner.java
@@ -1,15 +1,15 @@
-/* The following code was generated by JFlex 1.6.1 */
+/* The following code was generated by JFlex 1.7.0 */
-package tool;
+package wemelt;
import beaver.Symbol;
-import tool.Parser.Terminals;
+import wemelt.Parser.Terminals;
/**
* This class is a scanner generated by
- * JFlex 1.6.1
- * from the specification file tool/src/tool/Scanner.flex
+ * JFlex 1.7.0
+ * from the specification file wemelt/src/wemelt/Scanner.flex
*/
class Scanner extends beaver.Scanner {
@@ -289,11 +289,11 @@ the source of the yytext() string */
private int yycolumn;
/**
- * zzAtBOL == true <=> the scanner is currently at the beginning of a line
+ * zzAtBOL == true iff the scanner is currently at the beginning of a line
*/
private boolean zzAtBOL = true;
- /** zzAtEOF == true <=> the scanner is at the EOF */
+ /** zzAtEOF == true iff the scanner is at the EOF */
private boolean zzAtEOF;
/** denotes if the user-EOF-code has already been executed */
@@ -584,10 +584,10 @@ public Symbol nextToken() throws java.io.IOException, Scanner.Exception {
zzCh = Character.codePointAt(zzBufferL, zzCurrentPosL, zzMarkedPosL);
zzCharCount = Character.charCount(zzCh);
switch (zzCh) {
- case '\u000B':
- case '\u000C':
- case '\u0085':
- case '\u2028':
+ case '\u000B': // fall through
+ case '\u000C': // fall through
+ case '\u0085': // fall through
+ case '\u2028': // fall through
case '\u2029':
yyline++;
yycolumn = 0;
@@ -700,239 +700,298 @@ else if (zzAtEOF) {
switch (zzAction < 0 ? zzAction : ZZ_ACTION[zzAction]) {
case 1:
{ throw new Scanner.Exception("unexpected character '" + yytext() + "'");
- }
+ }
+ // fall through
case 60: break;
case 2:
{
- }
+ }
+ // fall through
case 61: break;
case 3:
{ return newToken(Terminals.DIV);
- }
+ }
+ // fall through
case 62: break;
case 4:
{ return newToken(Terminals.STAR);
- }
+ }
+ // fall through
case 63: break;
case 5:
{ return newToken(Terminals.LPAREN);
- }
+ }
+ // fall through
case 64: break;
case 6:
{ return newToken(Terminals.RPAREN);
- }
+ }
+ // fall through
case 65: break;
case 7:
{ return newToken(Terminals.LBRACK);
- }
+ }
+ // fall through
case 66: break;
case 8:
{ return newToken(Terminals.RBRACK);
- }
+ }
+ // fall through
case 67: break;
case 9:
{ return newToken(Terminals.LBRACE);
- }
+ }
+ // fall through
case 68: break;
case 10:
{ return newToken(Terminals.RBRACE);
- }
+ }
+ // fall through
case 69: break;
case 11:
{ return newToken(Terminals.BANG);
- }
+ }
+ // fall through
case 70: break;
case 12:
{ return newToken(Terminals.TILDE);
- }
+ }
+ // fall through
case 71: break;
case 13:
{ return newToken(Terminals.MOD);
- }
+ }
+ // fall through
case 72: break;
case 14:
{ return newToken(Terminals.PLUS);
- }
+ }
+ // fall through
case 73: break;
case 15:
{ return newToken(Terminals.MINUS);
- }
+ }
+ // fall through
case 74: break;
case 16:
{ return newToken(Terminals.LT);
- }
+ }
+ // fall through
case 75: break;
case 17:
{ return newToken(Terminals.GT);
- }
+ }
+ // fall through
case 76: break;
case 18:
{ return newToken(Terminals.ASG);
- }
+ }
+ // fall through
case 77: break;
case 19:
{ return newToken(Terminals.AMP);
- }
+ }
+ // fall through
case 78: break;
case 20:
{ return newToken(Terminals.CARET);
- }
+ }
+ // fall through
case 79: break;
case 21:
{ return newToken(Terminals.PIPE);
- }
+ }
+ // fall through
case 80: break;
case 22:
{ return newToken(Terminals.COLON);
- }
+ }
+ // fall through
case 81: break;
case 23:
{ return newToken(Terminals.COMMA);
- }
+ }
+ // fall through
case 82: break;
case 24:
{ return newToken(Terminals.SEMICOLON);
- }
+ }
+ // fall through
case 83: break;
case 25:
{ return resolve(yytext());
- }
+ }
+ // fall through
case 84: break;
case 26:
{ return newToken(Terminals.NUM, new Integer(yytext()));
- }
+ }
+ // fall through
case 85: break;
case 27:
{ return newToken(Terminals.NEQ);
- }
+ }
+ // fall through
case 86: break;
case 28:
{ return newToken(Terminals.MAPSTO);
- }
+ }
+ // fall through
case 87: break;
case 29:
{ return newToken(Terminals.SHL);
- }
+ }
+ // fall through
case 88: break;
case 30:
{ return newToken(Terminals.LE);
- }
+ }
+ // fall through
case 89: break;
case 31:
{ return newToken(Terminals.SHR);
- }
+ }
+ // fall through
case 90: break;
case 32:
{ return newToken(Terminals.GE);
- }
+ }
+ // fall through
case 91: break;
case 33:
{ return newToken(Terminals.EQ);
- }
+ }
+ // fall through
case 92: break;
case 34:
{ return newToken(Terminals.AND);
- }
+ }
+ // fall through
case 93: break;
case 35:
{ return newToken(Terminals.OR);
- }
+ }
+ // fall through
case 94: break;
case 36:
{ return newToken(Terminals.DO);
- }
+ }
+ // fall through
case 95: break;
case 37:
{ return newToken(Terminals.IF);
- }
+ }
+ // fall through
case 96: break;
case 38:
{ return newToken(Terminals.LPRED);
- }
+ }
+ // fall through
case 97: break;
case 39:
{ return newToken(Terminals.RW);
- }
+ }
+ // fall through
case 98: break;
case 40:
{ return newToken(Terminals.ASHR);
- }
+ }
+ // fall through
case 99: break;
case 41:
{ return newToken(Terminals.CAS);
- }
+ }
+ // fall through
case 100: break;
case 42:
{ return newToken(Terminals.LOW);
- }
+ }
+ // fall through
case 101: break;
case 43:
{ return newToken(Terminals.NOW);
- }
+ }
+ // fall through
case 102: break;
case 44:
{ return newToken(Terminals.ELSE);
- }
+ }
+ // fall through
case 103: break;
case 45:
{ return newToken(Terminals.VAR);
- }
+ }
+ // fall through
case 104: break;
case 46:
{ return newToken(Terminals.P_0);
- }
+ }
+ // fall through
case 105: break;
case 47:
{ return newToken(Terminals.NORW);
- }
+ }
+ // fall through
case 106: break;
case 48:
{ return newToken(Terminals.TRUE);
- }
+ }
+ // fall through
case 107: break;
case 49:
{ return newToken(Terminals.HIGH);
- }
+ }
+ // fall through
case 108: break;
case 50:
{ return newToken(Terminals.WHILE);
- }
+ }
+ // fall through
case 109: break;
case 51:
{ return newToken(Terminals.FENCE);
- }
+ }
+ // fall through
case 110: break;
case 52:
{ return newToken(Terminals.MODE);
- }
+ }
+ // fall through
case 111: break;
case 53:
{ return newToken(Terminals.FALSE);
- }
+ }
+ // fall through
case 112: break;
case 54:
{ return newToken(Terminals.CFENCE);
- }
+ }
+ // fall through
case 113: break;
case 55:
{ return newToken(Terminals.ARRAY);
- }
+ }
+ // fall through
case 114: break;
case 56:
{ return newToken(Terminals.GAMMA);
- }
+ }
+ // fall through
case 115: break;
case 57:
{ return newToken(Terminals.STABLE);
- }
+ }
+ // fall through
case 116: break;
case 58:
{ return newToken(Terminals.GAMMA_0);
- }
+ }
+ // fall through
case 117: break;
case 59:
{ return newToken(Terminals.INVARIANT);
- }
+ }
+ // fall through
case 118: break;
default:
zzScanError(ZZ_NO_MATCH);
diff --git a/tool/src/tool/State.scala b/wemelt/src/wemelt/State.scala
similarity index 99%
rename from tool/src/tool/State.scala
rename to wemelt/src/wemelt/State.scala
index 454d5e7..d5ec308 100644
--- a/tool/src/tool/State.scala
+++ b/wemelt/src/wemelt/State.scala
@@ -1,4 +1,4 @@
-package tool
+package wemelt
case class State(
gamma: Map[Id, Security],
diff --git a/tool/src/tool/Statement.scala b/wemelt/src/wemelt/Statement.scala
similarity index 99%
rename from tool/src/tool/Statement.scala
rename to wemelt/src/wemelt/Statement.scala
index 60bacaf..25c7d2b 100644
--- a/tool/src/tool/Statement.scala
+++ b/wemelt/src/wemelt/Statement.scala
@@ -1,4 +1,4 @@
-package tool
+package wemelt
object Block {
def empty = Block(Nil)
diff --git a/tool/src/tool/VarDef.scala b/wemelt/src/wemelt/VarDef.scala
similarity index 99%
rename from tool/src/tool/VarDef.scala
rename to wemelt/src/wemelt/VarDef.scala
index 7b43a32..a023b4d 100644
--- a/tool/src/tool/VarDef.scala
+++ b/wemelt/src/wemelt/VarDef.scala
@@ -1,4 +1,4 @@
-package tool
+package wemelt
// highest level parsed data structure
case class Global(variables: Set[Definition], P_0: Option[List[Expression]], gamma_0: Option[List[GammaMapping]], statements: List[Statement]) extends beaver.Symbol {
diff --git a/tool/src/tool/Tool.scala b/wemelt/src/wemelt/WeMeLT.scala
similarity index 95%
rename from tool/src/tool/Tool.scala
rename to wemelt/src/wemelt/WeMeLT.scala
index 2998140..b2f5890 100644
--- a/tool/src/tool/Tool.scala
+++ b/wemelt/src/wemelt/WeMeLT.scala
@@ -1,9 +1,9 @@
-package tool
+package wemelt
import java.io.FileReader
-import tool.error._
+import wemelt.error._
-object Tool {
+object WeMeLT {
def main(args: Array[String]): Unit = {
var toLog: Boolean = false // whether to print P/Gamma/D state information for each rule application
@@ -11,7 +11,7 @@ object Tool {
var noInfeasible: Boolean = false // whether to not check infeasible paths
if (args.isEmpty) {
- println("usage: ./armlogictool.sh file1 file2...")
+ println("usage: ./wemelt.sh file1 file2...")
} else {
for (file <- args) file match {
case "-v" =>
diff --git a/tool/src/tool/package.scala b/wemelt/src/wemelt/package.scala
similarity index 99%
rename from tool/src/tool/package.scala
rename to wemelt/src/wemelt/package.scala
index c88dafa..e077912 100644
--- a/tool/src/tool/package.scala
+++ b/wemelt/src/wemelt/package.scala
@@ -1,4 +1,4 @@
-package object tool {
+package object wemelt {
object error {
abstract class Error extends Exception {