diff options
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Boogie.scala | 4 | ||||
| -rw-r--r-- | Chalice/src/Chalice.scala | 21 | ||||
| -rw-r--r-- | Chalice/src/Translator.scala | 10 |
3 files changed, 20 insertions, 15 deletions
diff --git a/Chalice/src/Boogie.scala b/Chalice/src/Boogie.scala index 4fa21be0..afaff452 100644 --- a/Chalice/src/Boogie.scala +++ b/Chalice/src/Boogie.scala @@ -208,8 +208,8 @@ object Boogie { case Comment(msg) => indent + "// " + msg + nl
case assert@Assert(e) =>
val pos = if (Chalice.vsMode) {
- val r = assert.pos.line - 1;
- val c = assert.pos.column - 1;
+ val r = assert.pos.line;
+ val c = assert.pos.column;
r + "," + c + "," + r + "," + (c+5) + ":"
} else {
" " + assert.pos + ": "
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 43b3a330..0b2d43c5 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -9,6 +9,7 @@ import java.io.InputStreamReader import java.io.File
import java.io.FileWriter
import scala.util.parsing.input.Position
+import scala.util.parsing.input.NoPosition
import collection.mutable.ListBuffer
object Chalice {
@@ -36,16 +37,6 @@ object Chalice { var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"
val inputs = new ListBuffer[String]()
var printProgram = 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 boogieArgs = " ";
@@ -196,6 +187,14 @@ object Chalice { def CommandLineError(msg: String, help: String) = {
Console.err.println("Error: " + msg)
- Console.err.println(help);
}
+
+ def ReportError(pos: Position, msg: String) = {
+ if (vsMode) {
+ val (r,c) = (pos.line, pos.column)
+ Console.out.println(r + "," + c + "," + r + "," + (c+5) + ":" + msg);
+ } else {
+ Console.err.println(pos + ": " + msg)
+ }
+ }
}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 1ae56ca2..75d23e53 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -1015,8 +1015,8 @@ class Translator { isDefined(guard) ::: List(bassume(guard)) :::
translateStatement(body) :::
// check invariant
- Exhale(w.oldInvs map { inv => (inv, ErrorMessage(w.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained") :::
- tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(w.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained"), keepTag) :::
+ Exhale(w.oldInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained") :::
+ tag(Exhale(w.newInvs map { inv => (inv, ErrorMessage(inv.pos, "The loop invariant at " + inv.pos + " might not be preserved by the loop."))}, "loop invariant, maintained"), keepTag) :::
isLeaking(w.pos, "The loop might leak refereces.") :::
// check lockchange after loop iteration
Comment("check lockchange after loop iteration") ::
@@ -1622,6 +1622,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E **********************************************************************/
def Inhale(predicates: List[Expression], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+ if (predicates.size == 0) return Nil;
+
val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
Comment("inhale (" + occasion + ")") ::
BLocal(ihV) :: Boogie.Havoc(ih) ::
@@ -1633,6 +1635,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E }
def InhaleFrom(predicates: List[Expression], occasion: String, check: Boolean, useHeap: Boogie.Expr): List[Boogie.Stmt] = {
+ if (predicates.size == 0) return Nil;
+
val (ihV, ih) = Boogie.NewBVar("inhaleHeap", theap, true)
Comment("inhale (" + occasion + ")") ::
BLocal(ihV) :: Boogie.Assign(ih, useHeap) ::
@@ -1773,6 +1777,8 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E }
def Exhale(predicates: List[(Expression, ErrorMessage)], occasion: String, check: Boolean): List[Boogie.Stmt] = {
+ if (predicates.size == 0) return Nil;
+
val (emV, em) = NewBVar("exhaleMask", tmask, true)
Comment("begin exhale (" + occasion + ")") ::
BLocal(emV) :: (em := Mask) ::
|