Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
pub
frama-c
Commits
77f80af0
Commit
77f80af0
authored
Nov 04, 2019
by
David Bühler
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
[Eva] Fixes the octagon domain with respect to the ival rewriting.
parent
840640e0
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
5 additions
and
4 deletions
+5
-4
src/plugins/value/domains/octagons.ml
src/plugins/value/domains/octagons.ml
+5
-4
No files found.
src/plugins/value/domains/octagons.ml
View file @
77f80af0
...
...
@@ -99,7 +99,7 @@ module Arith = struct
let
widen
=
let
hints
=
Integer
.
zero
,
(
Ival
.
Widen_Hints
.
default_widen_hints
,
(
Ival
.
Widen_Hints
.
empty
,
Fc_float
.
Widen_Hints
.
default_widen_hints
)
in
Ival
.
widen
hints
...
...
@@ -109,9 +109,10 @@ module Arith = struct
if
Ival
.(
equal
top
ival
)
then
Fval
.
top
else
project_float
ival
let
neg
=
function
|
Float
f
->
inject_float
(
Fval
.
neg
f
)
|
ival
->
neg_int
ival
let
neg
ival
=
if
Ival
.
is_int
ival
then
neg_int
ival
else
inject_float
(
Fval
.
neg
(
project_float
ival
))
let
int_or_float_operation
i_op
f_op
=
fun
typ
->
match
Cil
.
unrollType
typ
with
...
...
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