Summary:
It modifies sizes and offsets of array values on pointer castings.
Currently, it supports only simple castings of pointer-to-integers.
Reviewed By: mbouaziz
Differential Revision: D12920589
fbshipit-source-id: a5ba831b8
Summary: It tries division on minmax value approximately, rather than just returning infinities. For example, `[0,2+min(6,s)] / 2` returns `[0,4]`.
Reviewed By: mbouaziz
Differential Revision: D10867091
fbshipit-source-id: d3f49987b
Summary: It uses big int, instead of 63bits int of OCaml, in the interval domain in order to get preciser numeric values in the future.
Reviewed By: jvillard
Differential Revision: D10123364
fbshipit-source-id: c217f4366
Summary:
It simplifies abstract memory instantiations of function calls. Now it instantiates callee memories by directly evaluating symbol paths, rather than constructing `subst_map`.
main changes are:
- no construction of `subst_map` and `trace_map`
- no symbol table in Inferbo's summary
- no `Symbol_not_found` exception (for when a required symbol was unavailable in `subst_map`)
Reviewed By: mbouaziz
Differential Revision: D9495597
fbshipit-source-id: 18cdcd6f7
Sungkeun Cho
Mehdi Bouaziz
Josh Berdine
Julian Sutherland