search

pietrobraione / jbse

A symbolic Java virtual machine for program analysis, verification and test generation
http://pietrobraione.github.io/jbse/
GNU General Public License v3.0
102 stars 29 forks source link

Path Conditions details #16

Closed danglotb closed 6 years ago

danglotb commented 6 years ago

Hi,

I am running JBSE against some project.

I have a quite strange path condition at the end of the execution:

NARROW-I(WIDEN-D({V3}) * 1.1) >= 0

Could you please explain what does it mean?

pietrobraione commented 6 years ago

WIDEN and NARROW are the operators for numeric type conversions. WIDEN-D({V3}) is the conversion to double of the value {V3}; since the conversion is a WIDEN ("widening", i.e., conversion to a bigger type) it means that {V3} is a smaller type than double (e.g., int or float) and that the conversion is exact. Then the resulting number is multiplied by 1.1, and the result of the multiplication (that has still type double) is converted ("narrowed") to int. This conversion is from a bigger to a smaller type, thus it is not exact in general, it may lose precision.

danglotb commented 6 years ago

Okay, thank you very much!