That's fine as long as you make sure never to access value directly (it
should be protected but not public) and put a comment in BitVector.java
indicating that direct access to the value field is not guaranteed to be
safe.
On Mar 19, 2014 5:43 PM, "Andrei Stefanescu" <notifications@github.com>
wrote:

> In
> src/javasources/KTool/src/org/kframework/backend/java/builtins/BigIntegerBitVector.java:
>
> > +
> > +    private BigInteger signedMax() {
> > +        return BigInteger.ONE.shiftLeft(bitwidth - 1).subtract(BigInteger.ONE);
> > +    }
> > +
> > +    private BigInteger unsignedMin() {
> > +        return BigInteger.ZERO;
> > +    }
> > +
> > +    private BigInteger unsignedMax() {
> > +        return BigInteger.ONE.shiftLeft(bitwidth).subtract(BigInteger.ONE);
> > +    }
> > +
> > +    @Override
> > +    public BigInteger signedValue() {
> > +        return value
>
> Sorry, I answered without paying attention. The value coincides with the
> signed value and the unsigned value on the last bitwidth bits (essentially,
> if you add and it overflows, it does not normalize the value until it is
> needed). Should I just keep it normalized (I don't think it matters much
> though).
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/291/files#r10775504>
> .
>