40 lines
1.8 KiB
Diff
40 lines
1.8 KiB
Diff
--- jc/jc_annot_inference.ml.orig 2011-10-24 09:21:06.000000000 -0600
|
|
+++ jc/jc_annot_inference.ml 2011-11-23 13:47:40.438177237 -0700
|
|
@@ -148,7 +148,7 @@
|
|
Some(tptr,offt)
|
|
end
|
|
| JCTvar _ | JCTderef _ | JCTapp _ | JCTold _ | JCTat _ | JCTif _
|
|
- | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
|
|
+ | JCTlet _ | JCTrange _ | JCTmatch _ | JCTaddress _ | JCTbase_block _
|
|
| JCTconst _ | JCTbinary _ | JCTunary _ | JCToffset _ | JCTinstanceof _
|
|
| JCTreal_cast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTcast _ ->
|
|
None
|
|
@@ -491,7 +491,7 @@
|
|
in
|
|
Format.fprintf Format.str_formatter "%a" Jc_output.assertion a;
|
|
let formula = Format.flush_str_formatter () in
|
|
- let lab = Output.reg_pos "G" ?id ?kind ?name ~formula loc in
|
|
+ let lab = Output.old_reg_pos "G" ?id ?kind ?name ~formula (Loc.extract loc) in
|
|
new assertion_with ~mark:lab a
|
|
|
|
|
|
@@ -608,8 +608,8 @@
|
|
Atp.Fn(atp_of_unop uop, [atp_of_term t1])
|
|
| JCTvar _ | JCTderef _ | JCTapp _ | JCToffset _ ->
|
|
Atp.Var (Vwp.variable_for_term t)
|
|
- | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _
|
|
- | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _
|
|
+ | JCTshift _ | JCTold _ | JCTat _ | JCTmatch _ | JCTinstanceof _ | JCTlet _
|
|
+ | JCTcast _ | JCTrange_cast _ | JCTbitwise_cast _ | JCTreal_cast _
|
|
| JCTaddress _ | JCTif _ | JCTrange _ | JCTunary _ | JCTbase_block _ ->
|
|
err ()
|
|
|
|
@@ -1198,7 +1198,7 @@
|
|
| JCTunary _ | JCTshift _ | JCTinstanceof _ | JCTmatch _
|
|
| JCTold _ | JCTat _ | JCTcast _ | JCTbitwise_cast _
|
|
| JCTrange_cast _ | JCTreal_cast _ | JCTaddress _ | JCTbase_block _
|
|
- | JCTrange _ | JCTif _ ->
|
|
+ | JCTlet _ | JCTrange _ | JCTif _ ->
|
|
err ()
|
|
with Failure "linearize" ->
|
|
(TermMap.add t (Int 1) TermMap.empty, Int 0)
|