draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Parsing smtlib strings as pre and postconditions in comparative analyses #148

Closed fortunac closed 4 years ago

fortunac commented 4 years ago

In a comparative analysis, when including a custom pre or postcondition, it is possible for a user-declared variable to be overwritten when substituting variable names to include their mangled suffixes. This happens when a variable contains a Var.name appended with a _orig or _mod.

For example, if the user declares RDI_orig_1234, it will be overwritten to RDI0_1234.

We should extend the fix from #147 to https://github.com/draperlaboratory/cbat_tools/blob/75cc89f61d8ed1837df2c569e4bf09cc2d44745b/wp/lib/bap_wp/src/compare.ml#L61

fortunac commented 4 years ago

Handled in #149.