summaryrefslogtreecommitdiff
path: root/src/jib
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib')
-rw-r--r--src/jib/anf.ml4
-rw-r--r--src/jib/jib_smt.ml2
2 files changed, 3 insertions, 3 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index bd4813ed..fdb4f941 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -556,8 +556,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
| E_lit lit -> mk_aexp (ae_lit lit (typ_of exp))
| E_block [] ->
- Util.warn (Reporting.loc_to_string l
- ^ "\n\nTranslating empty block (possibly assigning to an uninitialized variable at the end of a block?)");
+ Reporting.warn "" l
+ "Translating empty block (possibly assigning to an uninitialized variable at the end of a block?)";
mk_aexp (ae_lit (L_aux (L_unit, l)) (typ_of exp))
| E_block exps ->
let exps, last = split_block l exps in
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 0d6f42fe..74e56ef6 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -329,7 +329,7 @@ let add_pathcond_event ctx ev =
let overflow_check ctx smt =
if not !opt_ignore_overflow then (
- Util.warn "Adding overflow check in generated SMT";
+ Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l "";
add_event ctx Overflow smt
)