Support Floating Point Constraints for Path-Merged Regions

Java-Ranger is a path merging extension of Symbolic Pathfinder, that collapses multiple execution paths into a single region with a disjunctive constraint. Currently, it handles only integer constrains, which means, floating-point (FP) operations are either approximated unsoundly or cause solver errors. In this project, the aim is to add sound IEEE-754 floating-point support to Java ranger, enabling the correct summarization of regions containing FP arithmetic, comparisons, conversions, and library calls. The work heavily involves refactoring the underlying FP support in SPF (Modelling special values, rounding, comparisons, and conversions), then extending Java Ranger’s AST visitors, merging heuristics, and solver integration to handle the new FP constraints. The result will be an engine capable of analyzing FP-Java programs. Deliverables include: - New floating‑point expression nodes in the numeric package. - Updated bytecode handlers for all FP instructions. - Solver integration for Z3bitvector using the floating‑point theory. - Constant folding and simplification passes for FP expressions. - A test suite validating the correctness and coverage of FP handling. - Documentation of the new API and usage.