remove support for tuples in postcondition, since we don't support them

src/main/scala/daisy/Context.scala

@@ -30,8 +30,13 @@ case class Context(
   // indexed by FunDef.id
   inputRanges: Map[Identifier, Map[Identifier, Interval]] = Map(),
   inputErrors: Map[Identifier, Map[Identifier, Rational]] = Map(),
-  requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map(),
-  requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
+  // for now we only support a single result value, i.e. no tuples
+  // this map is indexed by fnc.id -> potentially partial interval bound of result
+  // and similar for the errors
+  resultRangeBounds: Map[Identifier, PartialInterval] = Map(),
+  resultErrorBounds: Map[Identifier, Rational] = Map()
+  //requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map(),
+  //requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
 ) {
 
   // on the first creation of a context, we also update the context variable

src/main/scala/daisy/analysis/SpecsProcessingPhase.scala

@@ -44,8 +44,10 @@ object SpecsProcessingPhase extends DaisyPhase {
 
     var allRanges: Map[Identifier, Map[Identifier, Interval]] = Map()
     var allErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
-    var requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map()
-    var requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
+    var resRanges: Map[Identifier, PartialInterval] = Map()
+    var resErrors: Map[Identifier, Rational] = Map()
+    //var requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map()
+    //var requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
 
     for (fnc <- prg.defs) {
 
@@ -81,10 +83,29 @@ object SpecsProcessingPhase extends DaisyPhase {
       fnc.postcondition match {
         case Some(post) =>
           val (ranges, errors) = extractPostCondition(post)
+          assert(ranges.size <= 1)
+          assert(errors.size <= 1)
+
+          // no range given in postcondition
+          if (ranges.size == 1) {
+            val tmp = ranges.values.head
+            resRanges += (fnc.id -> PartialInterval(tmp._1, tmp._2))
+          } else if (ranges.size > 1) {
+            reporter.error("Tuples are not supported.")
+          }
+
+          if (errors.size == 1) {
+            val tmp = errors.values.head
+            resErrors += (fnc.id -> tmp)
+          } else if (errors.size > 1) {
+            reporter.error("Tuples are not supported.")
+          }
+
+          //requiredOutputRanges += (fnc.id -> ranges.map( x =>
+          //  (x._1 -> PartialInterval(x._2._1, x._2._2) )))
+          //requiredOutputErrors += (fnc.id -> errors)
+
 
-          requiredOutputRanges += (fnc.id -> ranges.map( x =>
-            (x._1 -> PartialInterval(x._2._1, x._2._2) )))
-          requiredOutputErrors += (fnc.id -> errors)
 
         case _ =>
           //reporter.info("No post-condition found\n")
@@ -97,8 +118,11 @@ object SpecsProcessingPhase extends DaisyPhase {
     reporter.info("Finished specs preprocessing phase\n")
 
     reporter.debug(lang.RangePrinter(prg))
+    reporter.debug("range bounds: " + resRanges.mkString("\n"))
+    reporter.debug("error bounds: " + resErrors.mkString("\n"))
 
-    (ctx.copy(inputRanges = allRanges, inputErrors = allErrors, requiredOutputRanges = requiredOutputRanges, requiredOutputErrors = requiredOutputErrors), prg)
+    (ctx.copy(inputRanges = allRanges, inputErrors = allErrors,
+      resultRangeBounds = resRanges, resultErrorBounds = resErrors), prg)
   }