draperlaboratory / cbat_tools

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

Create flag for turning off the chaos spec #371

Closed fortunac closed 2 years ago

fortunac commented 2 years ago

This PR creates the --no-chaos=<function list> flag. Normally, functions like malloc would use the verifier_nondet function spec. With this flag set, the specified functions will not use the verifier_nondet spec, but will be treated as all other functions. For each function, it will look at the list of default function specs, and apply the spec who's requirements are satisfied.