Skip to content
Snippets Groups Projects
Commit 15d0d438 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

[Eva] Do not emit kernel warnings, emit Eva warnings instead

parent 5ec2bee1
No related branches found
No related tags found
No related merge requests found
...@@ -256,7 +256,7 @@ struct ...@@ -256,7 +256,7 @@ struct
let pick (m : t) = let pick (m : t) =
match Map.choose_opt m with match Map.choose_opt m with
| None -> Kernel.fatal "The disjunction should never be empty" | None -> assert false (* the disjunction should never be empty *)
| Some (k,s) -> k,s,Map.remove k m | Some (k,s) -> k,s,Map.remove k m
let pretty fmt (m : t) = let pretty fmt (m : t) =
......
...@@ -292,7 +292,7 @@ struct ...@@ -292,7 +292,7 @@ struct
match Int_val.min_int (to_int_val ~oracle b) with match Int_val.min_int (to_int_val ~oracle b) with
| Some l -> `Value l | Some l -> `Value l
| None -> | None ->
Kernel.warning ~current:true "cannot retrieve a lower bound for %a" Self.warning ~current:true "cannot retrieve a lower bound for %a"
pretty b; pretty b;
`Top `Top
...@@ -300,7 +300,7 @@ struct ...@@ -300,7 +300,7 @@ struct
match Int_val.max_int (to_int_val ~oracle b) with match Int_val.max_int (to_int_val ~oracle b) with
| Some u -> `Value u | Some u -> `Value u
| None -> | None ->
Kernel.warning ~current:true "cannot retrieve an upper bound for %a" Self.warning ~current:true "cannot retrieve an upper bound for %a"
pretty b; pretty b;
`Top `Top
...@@ -870,7 +870,7 @@ struct ...@@ -870,7 +870,7 @@ struct
| `Value m -> m | `Value m -> m
| `Bottom -> assert false | `Bottom -> assert false
| `Top -> | `Top ->
Kernel.warning ~current:true Self.warning ~current:true
"failed to introduce %a inside the array segmentation" "failed to introduce %a inside the array segmentation"
Bound.pretty b; Bound.pretty b;
m m
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment