Re: [Jmlspecs-developers] JML build broken

[Patrice C. <ch...@cs...>]

Hi Yoonsik et. al.,

>It seems that jmlc, before this change, accidentally supported \bigint in a
>
A temporary support had been implemented in which \bigint was mapped to 
int ...

>certain context as used in the List.spec file, e.g., (\forall \bigint i; i >
>0L && i < 5L; true). In this case, the previous implementation translated
>the quantified type either long or int; the \bigint type happens to be
>translated into int as the implementation translates all non-long integral
>type into int.  The new fix doesn't do that anymore to cope with some
>type-cast errors, e.g., assigning 0L to the int variable i.
>
 From what I recall, my intent was to temporarily map \bigint to long, 
but that didn't work (e.g. some typing errors similar to what you 
mention) so mapping to int seemed a reasonable alternative while 
awaiting the bug fix.

>I made a quick, temporary fix to handle the use of \bigint in such cases as
>in the file List.spec so that we can at least build JML. But, we have to
>figure out how to support \bigint and \real in general. (Patrice, if you
>have something in mind, I'll look into its implementation in jmlc.)
>
Ok, great.  The proper solution is to use BigInteger for \bigint's.  
Fred and I looked into it (and gave it a try) but without success.  It 
turned out to be more difficult that we expected.  In fact, I'm not sure 
whether it can be done at all with the current design.  You are 
certainly in a better position to assess that.  We can discuss further 
if you would like.

Cheers,
Patrice

-- 
Patrice Chalin, Assistant Professor           Computer Science Department
http://www.cs.concordia.ca/~faculty/chalin    Concordia University