Commit 88459e10 authored by Heiko Becker's avatar Heiko Becker
Browse files

rename testcases and fix some bugs, to finish merge request

parent 7e46da88
...@@ -31,9 +31,9 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions { ...@@ -31,9 +31,9 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
FlagOptionDef("noInitialErrors", "do not track initial errors specified by user"), FlagOptionDef("noInitialErrors", "do not track initial errors specified by user"),
FlagOptionDef("noRoundoff", "do not track roundoff errors"), FlagOptionDef("noRoundoff", "do not track roundoff errors"),
optionPrecision optionPrecision
) )
override implicit val debugSection = DebugSectionAnalysis implicit val debugSection = DebugSectionAnalysis
var reporter: Reporter = null var reporter: Reporter = null
......
...@@ -25,12 +25,12 @@ object CertificatePhase extends DaisyPhase { ...@@ -25,12 +25,12 @@ object CertificatePhase extends DaisyPhase {
def writeToFile (fileContent:String, prover:String, fname:String){ def writeToFile (fileContent:String, prover:String, fname:String){
import java.io.FileWriter import java.io.FileWriter
import java.io.BufferedWriter import java.io.BufferedWriter
val fileLocation = "./output/certificate_" + prg.id + fname val fileLocation =
val fstream =
if (prover == "coq") if (prover == "coq")
new FileWriter(fileLocation + ".v") "./coq/output/certificate_" + prg.id + "_" + fname + ".v"
else else
new FileWriter(fileLocation + ".hl") "./hol/output/certificate_" + prg.id + "_" + fname + ".hl"
val fstream = new FileWriter(fileLocation)
val out = new BufferedWriter(fstream) val out = new BufferedWriter(fstream)
out.write(fileContent) out.write(fileContent)
out.close out.close
......
...@@ -32,7 +32,7 @@ trait ErrorFunctions { ...@@ -32,7 +32,7 @@ trait ErrorFunctions {
var uniformPrecision: Precision = Float64 var uniformPrecision: Precision = Float64
var reporter: Reporter var reporter: Reporter
implicit val debugSection = DebugSectionAnalysis implicit val debugSection: DebugSection
/** /**
......
import daisy.lang._
import Real._
object Doppler {
def doppler(u: Real): Real = {
require(-100.0 <= u && u <= 100)
331.4 * u
}
}
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