Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
AVA
FloVer
Commits
5220fc97
Commit
5220fc97
authored
Feb 27, 2017
by
Heiko Becker
Browse files
alpha renaming and comments in Context class
parent
5cf86e1f
Changes
4
Hide whitespace changes
Inline
Side-by-side
hol4/
e
xpressionsScript.sml
→
hol4/
E
xpressionsScript.sml
View file @
5220fc97
File moved
src/main/scala/daisy/Context.scala
View file @
5220fc97
...
...
@@ -38,8 +38,10 @@ case class Context(
specResultRangeBounds
:
Map
[
Identifier
,
PartialInterval
]
=
Map
(),
specResultErrorBounds
:
Map
[
Identifier
,
Rational
]
=
Map
(),
analysisAbsoluteErrors
:
Map
[
Identifier
,
Map
[
Expr
,
Rational
]]
=
Map
(),
analysisRanges
:
Map
[
Identifier
,
Map
[
Expr
,
Interval
]]
=
Map
(),
// the intermediate analysis results, since we rely on having them at hand when
// encoding the analysis result
intermediateAbsoluteErrors
:
Map
[
Identifier
,
Map
[
Expr
,
Rational
]]
=
Map
(),
intermediateRanges
:
Map
[
Identifier
,
Map
[
Expr
,
Interval
]]
=
Map
(),
// the analysed/computed roundoff errors for each function
resultAbsoluteErrors
:
Map
[
Identifier
,
Rational
]
=
Map
(),
...
...
src/main/scala/daisy/analysis/RangeErrorPhase.scala
View file @
5220fc97
...
...
@@ -171,8 +171,8 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
(
ctx
.
copy
(
resultAbsoluteErrors
=
res
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
_1
)),
resultRealRanges
=
res
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
_2
)),
analysis
AbsoluteErrors
=
roundoffErrorMap
,
analysis
Ranges
=
rangeResMap
),
prg
)
intermediate
AbsoluteErrors
=
roundoffErrorMap
,
intermediate
Ranges
=
rangeResMap
),
prg
)
}
...
...
src/main/scala/daisy/backend/CertificatePhase.scala
View file @
5220fc97
...
...
@@ -46,10 +46,10 @@ object CertificatePhase extends DaisyPhase {
val
thePrecondition
=
fnc
.
precondition
val
theBody
=
fnc
.
body
//must be set
assert
(
ctx
.
analysis
AbsoluteErrors
.
get
(
fnc
.
id
)
!=
None
)
val
errorMap
=
ctx
.
analysis
AbsoluteErrors
.
get
(
fnc
.
id
).
get
assert
(
ctx
.
analysis
Ranges
.
get
(
fnc
.
id
)
!=
None
)
val
rangeMap
=
ctx
.
analysis
Ranges
.
get
(
fnc
.
id
).
get
assert
(
ctx
.
intermediate
AbsoluteErrors
.
get
(
fnc
.
id
)
!=
None
)
val
errorMap
=
ctx
.
intermediate
AbsoluteErrors
.
get
(
fnc
.
id
).
get
assert
(
ctx
.
intermediate
Ranges
.
get
(
fnc
.
id
)
!=
None
)
val
rangeMap
=
ctx
.
intermediate
Ranges
.
get
(
fnc
.
id
).
get
prover
match
{
case
Some
(
prv
)
=>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment