Jar2bpl-generated bpl cause boogie to throw resolution errors

[davidyoung8906]

Jar2bpl-generated bpl cause boogie to throw resolution errors

[martinschaef]

Sorry about that. Here is a quick fix:
In each generated Boogie file, you will find the following two lines:

axiom (forall t : javaType :: $heap[$null,$type] <: t);

procedure $new(obj_type:javaType) returns ($obj:ref); requires $heap[$obj,$alloc] == false; ensures $obj != $null; ensures $heap[$obj,$type] == obj_type; ensures $heap[$obj,$alloc] == true;

which are generated as part of the prelude. Replace this by:

procedure $new(obj_type:javaType) returns ($obj:ref);

Then it should work. I'll try to change the code accordingly asap.

[crhf]

@martinschaef in this case, how do you make sure that $null is a subtype of everything?

[martinschaef]

Ha ... that conversation started 9 years ago; I had to think about that for a minute :D. In terms of casting-rules, shouldn't null be a subtype of everything? Because you cast null to everything but you can't cast anything to null.

That is you can write:

String foo = null;
Integer bar = null;

where the null constant is implicitly cast to whatever type you have on the left.
In the opposite direction, there is no Null type that you could cast to.

So if you think of the type lattice, you have java.lang.Object at the top and the null type at the bottom and everything else at the middle (with the exception of primitive types like int which you have to handle separately) ... does that sound right?

[crhf]

Ah, didn't expect such a quick response :) I totally agree that null is a subtype of everything. I mean, since you suggest removing axiom (forall t : javaType :: $heap[$null,$type] <: t); from the prelude, how do you enforce that null is a subtype of everything in the boogie program?

[martinschaef]

Oh ... that again, I would need to think about longer. I assume Boogie changed in the last 9 years, so I'm not sure how you would have to write that axiom. Depending on what type of properties you want to prove, you might not even need to state that subtype relation for null explicitly

[crhf]

It happens that I'm doing a proof about null pointer exception, so I think I need that axiom.., Did you have any way to specify that 9 years ago? Or other workaround that does not need the axiom?

[martinschaef]

That, I don't remember ... note that this issue is 9 years old, but the code is a lot older than that. So my recommendation would be to check the literature of the past 10 years, I'm sure there is a better way to model the heap by now.

[crhf]

I see, thanks for making jar2bpl and helping here :)

[crhf]

btw, would you mind taking a look at the other issue I just created ;)