Interpreting procedure summaries

[elizabethdinella]

Hello, I would like some guidance in understanding the procedure summary output.
I ran the following commands:

infer capture -- javac NetBigInteger/NetBigInteger.java
infer analyze  
infer debug --procedures --procedures-summary

and selected the method for Add:

public NetBigInteger Add(NetBigInteger value) {
        if (m_sign == 0)
            return value;
        if (m_sign != value.m_sign) {
            if (value.m_sign == 0)
                return this;
            if (value.m_sign < 0)
                return Subtract(value.Negate());
            return value.Subtract(Negate());
        }
        return AddToMagnitude(value.m_magnitude);
    }

The output looks like:

NetBigInteger.NetBigInteger* NetBigInteger NetBigInteger.Add(NetBigInteger)(NetBigInteger.NetBigInteger* this, NetBigInteger.NetBigInteger* value)
ERRORS:
WARNINGS:
FAILURE:NONE SYMOPS:0
Pulse: pre/posts:20 main pre/post(s)
      ....
#19:
     Current post:
       this<<->-, .m_sign->->>
       * return=value
       ∧ this:NetBigInteger.NetBigInteger, SourceFile [None]
     &return: { Initialized, WrittenTo (7, ) }

     Inferred pre: value=- * this< <->-, .m_sign->->> ∧ {this.m_sign-> = 0}
     &this: { MustBeInitialized(, t=0), MustBeValid(, None, t=0) }
     &value: { MustBeInitialized(, t=0), MustBeValid(, None, t=0) }
     this: { MustBeInitialized(, t=0), MustBeValid(, None, t=0) }
     this.m_sign: { MustBeInitialized(, t=2), MustBeValid(, None, t=2) }
     this.m_sign->: { UsedAsBranchCond(NetBigInteger NetBigInteger.Add(NetBigInteger), line 282, ) }

           

A couple basic questions:

1. Why are there 20 pre/post pairs?
2. What is the meaning of this notation value=- * this<<->-, .m_sign->->> ?

I've attached the input file as well as the output of infer debug in a tar file
add.tar.gz