The Design and Implementation of an Abstract Interpreter for OCaml Programs: A Pre...
summary
A static analyser called Salto analyser implements an abstract interpreter for OCaml that claims to precisely detect which exceptions can be raised and when code depends on under-specified semantics. It uses a novel abstract domain for inductively defined sets of trees (recursive-type/tree-automata style) and a dynamic fixpoint solver that inserts widening points automatically. Hash consing and memoization yield a 10x performance gain, example analyses take ~30s, and current scaling tests stop at about 200-line test programs; mutability, laziness and objects are not yet handled.
AI-written summary · about