From eb284abb4172c6162ac31b865dc2a7e9661fe413 Mon Sep 17 00:00:00 2001 From: kyessenov Date: Thu, 12 Aug 2010 23:24:31 +0000 Subject: Chalice: accept many input files at once; read from stdin if no input file specified --- Chalice/src/Ast.scala | 32 ++++++-- Chalice/src/Chalice.scala | 182 ++++++++++++++++++++++++------------------- Chalice/src/Parser.scala | 116 +++++++++++++-------------- Chalice/src/Translator.scala | 51 ++++++------ Chalice/test.bat | 2 +- 5 files changed, 209 insertions(+), 174 deletions(-) diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala index 53c2093d..4f63f57b 100644 --- a/Chalice/src/Ast.scala +++ b/Chalice/src/Ast.scala @@ -10,7 +10,9 @@ import scala.util.parsing.input.Positional trait ASTNode extends Positional -// classes and types +/** + * Classes and types + */ case class TopLevelDecl(id: String) extends ASTNode @@ -115,7 +117,9 @@ sealed case class TokenType(C: Type, m: String) extends Type("token", Nil) { // override def FullName: String = "token<" + C.FullName + "." + m + ">" } -// members +/** + * Members + */ sealed abstract class Member extends ASTNode { val Hidden: Boolean = false // hidden means not mentionable in source @@ -167,7 +171,9 @@ case class Precondition(e: Expression) extends Specification case class Postcondition(e: Expression) extends Specification case class LockChange(ee: List[Expression]) extends Specification -// statements +/** + * Statements + */ sealed abstract class Statement extends ASTNode case class Assert(e: Expression) extends Statement @@ -197,6 +203,9 @@ case class Call(declaresLocal: List[Boolean], lhs: List[VariableExpr], obj: Expr var locals = List[Variable]() var m: Method = null } +case class Spec(declaresLocal: List[Boolean], lhs: List[VariableExpr], pred: Expression) extends Statement { + var locals = List[Variable]() +} case class Install(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement case class Share(obj: Expression, lowerBounds: List[Expression], upperBounds: List[Expression]) extends Statement case class Unshare(obj: Expression) extends Statement @@ -228,7 +237,9 @@ case class Receive(declaresLocal: List[Boolean], ch: Expression, outs: List[Vari case class Fold(pred: Access) extends Statement case class Unfold(pred: Access) extends Statement -// expressions +/** + * Expressions + */ sealed abstract class RValue extends ASTNode { var typ: Class = null @@ -370,7 +381,10 @@ case class LockBelow(e0: Expression, e1: Expression) extends CompareExpr(e0,e1) override val OpName = "<<" } -// quantifiers +/** + * Expressions: quantifiers + */ + trait Quant object Forall extends Quant object Exists extends Quant @@ -384,7 +398,9 @@ sealed abstract class Quantification(q: Quant, is: List[String], e: Expression) case class SeqQuantification(q: Quant, is: List[String], seq: Expression, e: Expression) extends Quantification(q, is, e) case class TypeQuantification(q: Quant, is: List[String], t: Type, e: Expression) extends Quantification(q, is, e) -// sequences +/** + * Expressions: sequences + */ case class EmptySeq(t: Type) extends Literal case class ExplicitSeq(elems: List[Expression]) extends Expression @@ -428,7 +444,9 @@ case class CallState(token: Expression, obj: Expression, id: String, args: List[ def target() = token; } -// visitors / operations +/** + * AST operations + */ object AST { /** diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 0342964b..449db023 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -9,12 +9,12 @@ import java.io.InputStreamReader import java.io.File import java.io.FileWriter import scala.util.parsing.input.Position +import collection.mutable.ListBuffer object Chalice { def main(args: Array[String]): Unit = { var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe" - // parse command-line arguments - var inputName: String = null + val inputs = new ListBuffer[String]() var printProgram = false var vsMode = false; def ReportError(pos: Position, msg: String) = { @@ -55,109 +55,127 @@ object Chalice { "-autoFold" -> {() => autoFold = true}, "-autoMagic"-> {() => autoMagic = true} ) - val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") + + lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") + " [-boogie:path]" + " [-defaults:int]" + " []*" + - " "; + " "; for (a <- args) { if (options contains a) options(a)() else if (a == "-help") {Console.out.println(help); return} else if (a.startsWith("-boogie:")) boogiePath = a.substring(8) - else if (a.startsWith("-defaults:")) { try { defaults = Integer.parseInt(a.substring(10)); if(3<=defaults) { autoMagic = true; } } catch { case _ => CommandLineError("-defaults takes integer argument", help); } } + else if (a.startsWith("-defaults:")) { + try { + defaults = Integer.parseInt(a.substring(10)); + if (3<=defaults) { autoMagic = true; } + } catch { case _ => CommandLineError("-defaults takes integer argument", help); } + } else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe - else if (inputName != null) { CommandLineError("multiple input filenames: " + inputName + " and " + a, help); return } - else { inputName = a } + else inputs += a } - // check the command-line arguments - if (inputName == null && vsMode) { - inputName = "" - } else if (inputName == null) { CommandLineError("missing input filename", help); return } else { - val file = new File(inputName); - if(! file.exists()){ + // check that input files exist + var files = for (input <- inputs.toList) yield { + val file = new File(input); + if(! file.exists) { CommandLineError("input file " + file.getName() + " could not be found", help); return } + file; } - // parse program + + // parse programs val parser = new Parser(); - parser.parseFile(inputName) match { - case e: parser.NoSuccess => + val parseResults = if (files.isEmpty) { + List(parser.parseStdin) + } else for (file <- files) yield { + parser.parseFile(file) + } + + // report errors and merge declarations + assert(parseResults.size > 0) + var parseErrors = false; + val program:List[TopLevelDecl] = parseResults.map(result => result match { + case e:parser.NoSuccess => + parseErrors = true; if (vsMode) ReportError(e.next.pos, e.msg); else - Console.err.println("Error: " + e) + Console.err.println("Error: " + e); + Nil case parser.Success(prog, _) => if (printProgram) PrintProgram.P(prog) - if (doTypecheck) { - // typecheck program - Resolver.Resolve(prog) match { - case Resolver.Errors(msgs) => - 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 - val boogieFile = new File(boogiePath); - if(! boogieFile.exists() || ! boogieFile.isFile()) { - CommandLineError("Boogie.exe not found at " + boogiePath, help); return - } - // translate program to Boogie - val translator = new Translator(); - // set the translation options - TranslationOptions.checkLeaks = checkLeaks; - TranslationOptions.defaults = defaults; - TranslationOptions.autoFold = autoFold; - TranslationOptions.autoMagic = autoMagic; - TranslationOptions.skipDeadlockChecks = skipDeadlockChecks; - TranslationOptions.skipTermination = skipTermination; - 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 }; - val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl" - writeFile(bplFilename, bplText); - // run Boogie.exe on out.bpl - val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename); - // terminate boogie if interrupted - Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() { - def run { - val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe"); - kill.waitFor; - // just to be sure - boogie.destroy - } - })) - // the process blocks until we exhaust input and error streams - new Thread(new Runnable() { - def run { - val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream)); - var line = err.readLine; - while(line!=null) {Console.err.println(line); Console.err.flush} - } - }).start; - val input = new BufferedReader(new InputStreamReader(boogie.getInputStream)); - var line = input.readLine(); - var previous_line = null: String; - while(line!=null){ - Console.out.println(line); - Console.out.flush; - previous_line = line; - line = input.readLine(); - } - boogie.waitFor; - input.close; + prog + }).flatten; + if (parseErrors) return; - // generate code - if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack - val converter = new ChaliceToCSharp(); - println("Code generated in out.cs."); - writeFile("out.cs", converter.convertProgram(prog)); - } + // typecheck program + if (doTypecheck) { + Resolver.Resolve(program) match { + case Resolver.Errors(msgs) => + 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 + val boogieFile = new File(boogiePath); + if(! boogieFile.exists() || ! boogieFile.isFile()) { + CommandLineError("Boogie.exe not found at " + boogiePath, help); return + } + // translate program to Boogie + val translator = new Translator(); + // set the translation options + TranslationOptions.checkLeaks = checkLeaks; + TranslationOptions.defaults = defaults; + TranslationOptions.autoFold = autoFold; + TranslationOptions.autoMagic = autoMagic; + TranslationOptions.skipDeadlockChecks = skipDeadlockChecks; + TranslationOptions.skipTermination = skipTermination; + val bplProg = translator.translateProgram(program); + // write to out.bpl + Boogie.vsMode = vsMode; + val bplText = TranslatorPrelude.P + (bplProg map Boogie.Print).foldLeft(""){ (a, b) => a + b }; + val bplFilename = if (vsMode) "c:\\tmp\\out.bpl" else "out.bpl" + writeFile(bplFilename, bplText); + // run Boogie.exe on out.bpl + val boogie = Runtime.getRuntime.exec(boogiePath + " /errorTrace:0 " + boogieArgs + bplFilename); + // terminate boogie if interrupted + Runtime.getRuntime.addShutdownHook(new Thread(new Runnable() { + def run { + val kill = Runtime.getRuntime.exec("taskkill /T /F /IM Boogie.exe"); + kill.waitFor; + // just to be sure + boogie.destroy } + })) + // the process blocks until we exhaust input and error streams + new Thread(new Runnable() { + def run { + val err = new BufferedReader(new InputStreamReader(boogie.getErrorStream)); + var line = err.readLine; + while(line!=null) {Console.err.println(line); Console.err.flush} + } + }).start; + val input = new BufferedReader(new InputStreamReader(boogie.getInputStream)); + var line = input.readLine(); + var previous_line = null: String; + while(line!=null){ + Console.out.println(line); + Console.out.flush; + previous_line = line; + line = input.readLine(); + } + boogie.waitFor; + input.close; + + // generate code + if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack + val converter = new ChaliceToCSharp(); + println("Code generated in out.cs."); + writeFile("out.cs", converter.convertProgram(program)); } - } + } + } } } diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index 8999add9..b57a5ea4 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -10,17 +10,12 @@ import scala.collection.immutable.PagedSeq import scala.util.parsing.input.Position import scala.util.parsing.input.Positional import scala.util.parsing.input.NoPosition +import java.io.File class Parser extends StandardTokenParsers { - def parseFile(path: String): this.ParseResult[List[TopLevelDecl]] = { - val tokens = if (path == "") { - new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in)) - } else { - new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile path)); - } - phrase(programUnit)(tokens) - } + def parseStdin = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in))) + def parseFile(file: File) = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile file))) case class PositionedString(v: String) extends Positional @@ -44,8 +39,12 @@ class Parser extends StandardTokenParsers { ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::") def programUnit = (classDecl | channelDecl)* + def Semi = ";" ? + var currentLocalVariables = Set[String]() // used in the method context - // class and members + /** + * Top level declarations + */ def classDecl = positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ "{" ~ (memberDecl*) <~ "}" ^^ { @@ -54,31 +53,22 @@ class Parser extends StandardTokenParsers { ext match { case None => case Some(t) => cl.IsExternal = true } cl }) - def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | - predicateDecl | functionDecl) + def channelDecl = + "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ { + case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true)) + case id ~ ins ~ Some(e) => Channel(id, ins, e) + } + /** + * Member declarations + */ + + def memberDecl = positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl) def fieldDecl = ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, false) } | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id, t, true) } ) - def Ident = - positioned(ident ^^ PositionedString) - def idType = - idTypeOpt ^^ { - case (id, None) => (id, Type("int", Nil)) - case (id, Some(t)) => (id, t) } - def idTypeOpt = - ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) } - def typeDecl: Parser[Type] = - positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) } - | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) } - ) - def Semi = ";" ? - - var currentLocalVariables = Set[String]() - def invariantDecl = positioned("invariant" ~> expression <~ Semi ^^ MonitorInvariant) - def methodDecl = { currentLocalVariables = Set[String]() "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ @@ -88,51 +78,60 @@ class Parser extends StandardTokenParsers { case None => Method(id, ins, Nil, spec, body) case Some(outs) => Method(id, ins, outs, spec, body) }} } - def channelDecl = - "channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ { - case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true)) - case id ~ ins ~ Some(e) => Channel(id, ins, e) - } - def predicateDecl: Parser[Predicate] = + def predicateDecl: Parser[Predicate] = ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) } def functionDecl = - ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ { case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body) } + ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ { + case id ~ ins ~ out ~ specs ~ body => Function(id, ins, out, specs, body) + } + def conditionDecl = + "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ { + case id ~ optE => Condition(id, optE) } + def formalParameters(immutable: Boolean) = "(" ~> (formalList(immutable) ?) <~ ")" ^^ { case None => Nil case Some(ids) => ids } - def formalList(immutable: Boolean) = { - repsep(formal(immutable), ",") - } + def formalList(immutable: Boolean) = repsep(formal(immutable), ",") def formal(immutable: Boolean): Parser[Variable] = idType ^^ {case (id,t) => currentLocalVariables = currentLocalVariables + id; - if (immutable) - new ImmutableVariable(id,t) - else - new Variable(id,t) + if (immutable) new ImmutableVariable(id,t) + else new Variable(id,t) } + def Ident = positioned(ident ^^ PositionedString) + def idType = + idTypeOpt ^^ { + case (id, None) => (id, Type("int", Nil)) + case (id, Some(t)) => (id, t) } + def idTypeOpt = + ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) } + def typeDecl: Parser[Type] = + positioned(("int" | "bool" | ident | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) } + | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) } + ) + + /** + * Pre and post conditions + */ + def methodSpec = positioned( "requires" ~> expression <~ Semi ^^ Precondition | "ensures" ~> expression <~ Semi ^^ Postcondition | "lockchange" ~> expressionList <~ Semi ^^ LockChange ) - def blockStatement: Parser[List[Statement]] = { - "{" ~> blockStatementBody <~ "}" - } + + /** + * Statements + */ + + def blockStatement: Parser[List[Statement]] = "{" ~> blockStatementBody <~ "}" def blockStatementBody: Parser[List[Statement]] = { val prev = currentLocalVariables (statement*) ^^ { case x => currentLocalVariables = prev; x } } - - def conditionDecl = - "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ { - case id ~ optE => Condition(id, optE) } - - // statements - def statement: Parser[Statement] = positioned( "assert" ~> expression <~ Semi ^^ Assert | "assume" ~> expression <~ Semi ^^ Assume @@ -316,9 +315,11 @@ class Parser extends StandardTokenParsers { case l ~ None => (l,Nil) case l ~ Some(u) => (l,u) } ) - - // expressions + /** + * Expressions + */ + def expressionList = repsep(expression, ",") def expression = positioned(iteExpr) @@ -400,7 +401,6 @@ class Parser extends StandardTokenParsers { def exprBody = "{" ~> expression <~ "}" - // what is "FerSure"? def selectExprFerSure: Parser[MemberAccess] = positioned(atom ~ "." ~ ident ~ ("." ~> ident *) ^^ { case e ~ _ ~ field ~ moreFields => @@ -486,28 +486,22 @@ class Parser extends StandardTokenParsers { | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) } ) - // Scala type inference resists figuring out | (alternative) for these two - def quantifierSeq: Parser[Quantification] = (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierSeqBody(q, is)} - def quantifierSeqBody(q: Quant, is: List[String]) : Parser[Quantification] = (("in" ~> expression <~ "::") ~ (exprWithLocals(is))) ^^ { case seq ~ e => currentLocalVariables = currentLocalVariables -- is; SeqQuantification(q, is, seq, e); } - def quantifierType: Parser[Quantification] = (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierTypeBody(q, is)} - def quantifierTypeBody(q: Quant, is: List[String]) : Parser[Quantification] = ((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^ { case t ~ e => currentLocalVariables = currentLocalVariables -- is; TypeQuantification(q, is, t, e); } - def quant: Parser[Quant] = ( "forall" ^^^ Forall | "exists" ^^^ Exists) diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 45d875f0..d5ddfdcd 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -77,6 +77,8 @@ class Translator { translatePredicate(pred) case inv: MonitorInvariant => Nil // already dealt with before + case _: Condition => + throw new Exception("not yet implemented") } } @@ -159,40 +161,41 @@ class Translator { def definitionAxiom(f: Function): List[Decl] = { assert(f.definition.isDefined) val inArgs = (f.ins map {i => Boogie.VarExpr(i.UniqueName)}); - val frameFunctionName = "##" + f.FullName; - - /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n :: - wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body)) - */ val args = VarExpr("this") :: inArgs; - var formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar); + val formals = BVar(HeapName, theap) :: BVar(MaskName, tmask) :: BVar("this", tref) :: (f.ins map Variable2BVar); val applyF = FunctionApp(functionName(f), List(etran.Heap, etran.Mask) ::: args); - /** Limit application of the function by introducing a second limited function */ - val body = etran.Tr(if (f.isRecursive) { - val limited = Map() ++ (f.SCC zip (f.SCC map {f => - val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition); - result.Parent = f.Parent; - result; - })); - def limit: Expression => Option[Expression] = _ match { - case app @ FunctionApplication(obj, id, args) if (f.SCC contains app.f) => - val result = FunctionApplication(obj transform limit, id, args map (e => e transform limit)); - result.f = limited(app.f); - Some(result) - case _ => None + /** Limit application of the function by introducing a second (limited) function */ + val body = etran.Tr( + if (f.isRecursive && ! f.isUnlimited) { + val limited = Map() ++ (f.SCC zip (f.SCC map {f => + val result = Function(f.id + "#limited", f.ins, f.out, f.spec, f.definition); + result.Parent = f.Parent; + result; + })); + def limit: Expression => Option[Expression] = _ match { + case app @ FunctionApplication(obj, id, args) if (f.SCC contains app.f) => + val result = FunctionApplication(obj transform limit, id, args map (e => e transform limit)); + result.f = limited(app.f); + Some(result) + case _ => None + } + f.definition.get transform limit; + } else { + f.definition.get } - f.definition.get transform limit; - } else - f.definition.get); + ); + /* axiom (forall h: HeapType, m: MaskType, this: ref, x_1: t_1, ..., x_n: t_n :: + wf(h, m) && CurrentModule == module#C ==> #C.f(h, m, this, x_1, ..., x_n) == tr(body)) + */ Axiom(new Boogie.Forall( formals, new Trigger(applyF), (wf(VarExpr(HeapName), VarExpr(MaskName)) && (CurrentModule ==@ ModuleName(currentClass))) ==> (applyF ==@ body))) :: (if (f.isRecursive) - // define the limited function + // define the limited function (even for unlimited function since its SCC might have limited functions) Boogie.Function(functionName(f) + "#limited", formals, BVar("$myresult", f.out.typ)) :: Axiom(new Boogie.Forall( formals, new Trigger(applyF), @@ -1553,6 +1556,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case Frac(p) => (Tr(p), 0) : (Expr, Expr) case Epsilon => (0, 1) : (Expr, Expr) // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone case Epsilons(p) => (0, Tr(p)) : (Expr, Expr) + case Star => throw new Exception("not yet implemented") }; (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) ::: @@ -1731,6 +1735,7 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E case Frac(p) => (p, 0) : (Expr, Expr) case Epsilon => (0, 1) : (Expr, Expr) // TODO: check for infinity bounds -- or perhaps just wait till epsilons are gone case Epsilons(p) => (0, p) : (Expr, Expr) + case Star => throw new Exception("not yet implemented") }; (if (check) isDefined(s)(true) ::: isDefined(perm)(true) else Nil) ::: diff --git a/Chalice/test.bat b/Chalice/test.bat index 9bc0f5ea..b45207b6 100644 --- a/Chalice/test.bat +++ b/Chalice/test.bat @@ -1,7 +1,7 @@ @echo off echo start > Output -set CHALICE=call scala -cp bin Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe" +set CHALICE=call scala -cp bin chalice.Chalice -nologo -boogie:"C:\\Users\\t-kuayes\\Documents\\Boogie-2010-07-13\\Boogie.exe" REM to do: AssociationList -- cgit v1.2.3