Open elizabethdinella opened 2 weeks ago
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:
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
infer debug
Hello, I would like some guidance in understanding the procedure summary output. I ran the following commands:
and selected the method for Add:
The output looks like:
A couple basic questions:
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