diff options
| -rw-r--r-- | Chalice/src/Boogie.scala | 14 | ||||
| -rw-r--r-- | Chalice/src/Chalice.scala | 30 | ||||
| -rw-r--r-- | Chalice/src/Resolver.scala | 13 |
3 files changed, 40 insertions, 17 deletions
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala index 492e0669..b60ce521 100644 --- a/Chalice/src/Boogie.scala +++ b/Chalice/src/Boogie.scala @@ -133,7 +133,9 @@ object Boogie { (v,e)
}
- // def out(s: String) = Console.out.print(s)
+ var vsMode = false; // global variable settable from outside the class (non-ideal design)
+
+ // def out(s: String) = Console.out.print(s)
var indentLevel = 1
def indent: String = {
def doIndent(i: int): String = {
@@ -194,7 +196,15 @@ object Boogie { }
def PrintStmt(s: Stmt): String = s match {
case Comment(msg) => indent + "// " + msg + nl
- case assert@Assert(e) => indent + "assert " + "{:msg \" " + assert.pos + ": " + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl
+ case assert@Assert(e) =>
+ val pos = if (vsMode) {
+ val r = assert.pos.line - 1;
+ val c = assert.pos.column - 1;
+ r + "," + c + "," + r + "," + (c+5) + ":"
+ } else {
+ " " + assert.pos + ": "
+ }
+ indent + "assert " + "{:msg \"" + pos + assert.message + "\"}" + " " + PrintExpr(e) + ";" + nl
case Assume(e) => indent + "assume " + PrintExpr(e) + ";" + nl
case If(guard, thn, els) =>
indent + "if (" +
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 1bba1a99..1a6e3e48 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -7,6 +7,7 @@ import java.io.BufferedReader import java.io.InputStreamReader
import java.io.File
import java.io.FileWriter
+import scala.util.parsing.input.Position
object Chalice {
def main(args: Array[String]): unit = {
@@ -14,6 +15,16 @@ object Chalice { // parse command-line arguments
var inputName: String = null
var printProgram = false
+ var vsMode = false;
+ def ReportError(pos: Position, msg: String) = {
+ if (vsMode) {
+ val r = pos.line - 1;
+ val c = pos.column - 1;
+ Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);
+ } else {
+ Console.err.println(pos + ": " + msg)
+ }
+ }
var doTypecheck = true
var doTranslate = true
var checkLeaks = false
@@ -32,6 +43,7 @@ object Chalice { if (a == "-print") printProgram = true
else if (a == "-noTranslate") doTranslate = false
else if (a == "-noTypecheck") doTypecheck = false
+ else if (a == "-vs") vsMode = true
else if (a == "-checkLeaks") checkLeaks = true
else if (a == "-noDeadlockChecks") skipDeadlockChecks = true
else if (a.startsWith("-boogie:")) boogiePath = a.substring(8)
@@ -54,18 +66,19 @@ object Chalice { // parse program
val parser = new Parser();
parser.parseFile(inputName) match {
- case e: parser.NoSuccess => Console.err.println("Error: " + e)
+ case e: parser.NoSuccess =>
+ if (vsMode)
+ ReportError(e.next.pos, e.msg);
+ else
+ Console.err.println("Error: " + e)
case parser.Success(prog, _) =>
if (printProgram) PrintProgram.P(prog)
if (doTypecheck) {
// typecheck program
Resolver.Resolve(prog) match {
- case Resolver.Error(pos, msg) =>
- Console.err.println("The program did not typecheck.\n");
- Console.err.println(msg)
case Resolver.Errors(msgs) =>
- Console.err.println("The program did not typecheck.");
- msgs foreach { msg => Console.err.println(msg) }
+ if (!vsMode) Console.err.println("The program did not typecheck.");
+ msgs foreach { msg => ReportError(msg._1, msg._2) }
case Resolver.Success() =>
if (doTranslate) {
// checking if Boogie.exe exists
@@ -73,7 +86,7 @@ object Chalice { if(! boogieFile.exists() || ! boogieFile.isFile()) {
CommandLineError("Boogie.exe not found at " + boogiePath); return
}
- // translate program to BoogiePL
+ // translate program to Boogie
val translator = new Translator();
// set the translation options
TranslationOptions.checkLeaks = checkLeaks;
@@ -83,6 +96,7 @@ object Chalice { TranslationOptions.skipDeadlockChecks = skipDeadlockChecks;
val bplProg = translator.translateProgram(prog);
// write to out.bpl
+ Boogie.vsMode = vsMode;
val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b };
writeFile("out.bpl", bplText);
// run Boogie.exe on out.bpl
@@ -115,6 +129,6 @@ object Chalice { def CommandLineError(msg: String) = {
Console.err.println("Error: " + msg)
- Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")
+ Console.err.println("syntax: chalice [-print] [-noTypecheck] [-noTranslate] [-vs] [-boogie:path] [-defaults] [-autoFold] [-checkLeaks] [-noDeadlockChecks] inputFile")
}
}
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala index 00daaa92..9e8e5b4a 100644 --- a/Chalice/src/Resolver.scala +++ b/Chalice/src/Resolver.scala @@ -9,8 +9,7 @@ import scala.util.parsing.input.Positional object Resolver {
sealed abstract class ResolverOutcome
case class Success extends ResolverOutcome
- case class Error(pos: Position, s: String) extends ResolverOutcome
- case class Errors(ss: List[String]) extends ResolverOutcome
+ case class Errors(ss: List[(Position,String)]) extends ResolverOutcome
var seqClasses = Map[String, SeqClass]();
@@ -19,9 +18,9 @@ object Resolver { val CurrentClass = currentClass
var currentMember = null: Member;
def CurrentMember = currentMember: Member;
- var errors: List[String] = Nil
+ var errors: List[(Position,String)] = Nil
def Error(pos: Position, msg: String) {
- errors = errors + (pos + ": " + msg)
+ errors = errors + (pos, msg)
}
def AddVariable(v: Variable): ProgramContext = {
new LProgramContext(v, this);
@@ -48,7 +47,7 @@ object Resolver { var decls = Map[String,TopLevelDecl]()
for (decl <- BoolClass :: IntClass :: RootClass :: NullClass :: MuClass :: prog) {
if (decls contains decl.id) {
- return Error(decl.pos, "duplicate class/channel name: " + decl.id)
+ return Errors(List((decl.pos, "duplicate class/channel name: " + decl.id)))
} else {
decl match {
case cl: Class =>
@@ -57,7 +56,7 @@ object Resolver { case m: NamedMember =>
m.Parent = cl
if (cl.mm contains m.Id) {
- return Error(m.pos, "duplicate member name " + m.Id + " in class " + cl.id)
+ return Errors(List((m.pos, "duplicate member name " + m.Id + " in class " + cl.id)))
} else {
cl.mm = cl.mm + (m.Id -> m)
}
@@ -67,7 +66,7 @@ object Resolver { decls = decls + (decl.id -> decl)
}
}
- var errors = List[String]()
+ var errors = List[(Position,String)]()
// resolve types of members
val contextNoCurrentClass = new ProgramContext(decls, null)
|