generate verification conditions for array access

src/main/scala/leon/Analysis.scala

@@ -68,6 +68,7 @@ class Analysis(val program : Program, val reporter: Reporter = Settings.reporter
         allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
         allVCs ++= tactic.generatePostconditions(funDef)
         allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+        allVCs ++= tactic.generateArrayAccessChecks(funDef)
       }
       allVCs = allVCs.sortWith((vc1, vc2) => {
         val id1 = vc1.funDef.id.name

src/main/scala/leon/ArrayTransformation.scala

@@ -35,7 +35,7 @@ object ArrayTransformation extends Pass {
       IfExpr(
         And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
         ArraySelect(TupleSelect(ar, 1), ir).setType(sel.getType),
-        Error("Array out of bound access").setType(sel.getType)
+        Error("Index out of bound").setType(sel.getType)
       ).setType(sel.getType)
     }
     case ArrayUpdate(a, i, v) => {
@@ -49,7 +49,7 @@ object ArrayTransformation extends Pass {
       IfExpr(
         And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
         Block(Seq(Assignment(id, Tuple(Seq(ArrayUpdated(array, i, v).setType(array.getType), length)).setType(TupleType(Seq(array.getType, Int32Type))))), IntLiteral(0)),
-        Error("Array out of bound access").setType(Int32Type)
+        Error("Index out of bound").setType(Int32Type)
       ).setType(Int32Type)
     }
 

src/main/scala/leon/DefaultTactic.scala

@@ -194,6 +194,35 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
       toRet
     }
 
+    def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition] = {
+      val toRet = if (function.hasBody) {
+        val cleanBody = matchToIfThenElse(function.body.get)
+
+        val allPathConds = collectWithPathCondition((t => t match {
+          case Error("Index out of bound") => true
+          case _ => false
+        }), cleanBody)
+
+        def withPrecIfDefined(conds: Seq[Expr]) : Expr = if (function.hasPrecondition) {
+          Not(And(mapGetWithChecks(matchToIfThenElse(function.precondition.get)), And(conds)))
+        } else {
+          Not(And(conds))
+        }
+
+        allPathConds.map(pc =>
+          new VerificationCondition(
+            withPrecIfDefined(pc._1),
+            if(function.fromLoop) function.parent.get else function,
+            VCKind.ArrayAccess,
+            this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+        ).toSeq
+      } else {
+        Seq.empty
+      }
+
+      toRet
+    }
+
     def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition] = {
       generateMapAccessChecks(function)
     }

src/main/scala/leon/Extensions.scala

@@ -46,6 +46,7 @@ object Extensions {
     def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
     def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
     def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
+    def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
   }
 
   // The rest of the code is for dynamically loading extensions

src/main/scala/leon/VerificationCondition.scala

@@ -49,6 +49,7 @@ object VCKind extends Enumeration {
   val Postcondition = Value("postcond.")
   val ExhaustiveMatch = Value("match.")
   val MapAccess = Value("map acc.")
+  val ArrayAccess = Value("arr. acc.")
   val InvariantInit = Value("inv init.")
   val InvariantInd = Value("inv ind.")
   val InvariantPost = Value("inv post.")