Commit 173ba3fd authored by Heiko Becker's avatar Heiko Becker

Fix bug in Certificate Phase

parent aa571dab
......@@ -81,9 +81,6 @@ object SpecsProcessingPhase extends DaisyPhase with PrecisionsParser {
case None =>
}
// ctx.reporter.info("precision map:")
// ctx.reporter.info(precisionMap)
var allRanges: Map[Identifier, Map[Identifier, Interval]] = Map()
var allErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
var resRanges: Map[Identifier, PartialInterval] = Map()
......
......@@ -73,7 +73,7 @@ object CertificatePhase extends DaisyPhase {
reporter.info(s"Generating certificate for ${fnc.id}")
val precisionMap: Map[Identifier, Precision] = if (mixedPrecision) {
ctx.specResultPrecisions
ctx.specInputPrecisions.get(fnc.id).get
} else {
allVariablesOf(fnc.body.get).map(id => (id -> constPrecision)).toMap
}
......@@ -81,7 +81,9 @@ object CertificatePhase extends DaisyPhase {
//first retrieve the values
//these should be defined, otherwise the generation will fail
val thePrecondition = fnc.precondition.get
reporter.info(s"${fnc.body.get}")
val theBody = (changeType (fnc.body.get, precisionMap))._1
reporter.info(s"$theBody")
val errorMap = ctx.intermediateAbsErrors.get(fnc.id).get
val rangeMap = ctx.intermediateRanges.get(fnc.id).get
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment