Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Comparison property builder combinator #91

Closed
fortunac opened this issue Oct 31, 2019 · 1 comment
Closed

Comparison property builder combinator #91

fortunac opened this issue Oct 31, 2019 · 1 comment
Labels
enhancement New feature or request WP Involves the Weakest Precondition computation

Comments

@fortunac
Copy link

Currently for our comparison analysis, different postconditions are built separately in with compare_subs_eq and compare_subs_fun in https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/compare.ml.

We should add combinator in order to build postconditions that compare multiple properties (ex: compares both the register values and the function calls), giving the user the ability to pick multiple.

We should also move all the variable computation from

let compare_projs (proj : project) (file1: string) (file2 : string)
into the compare module.

@fortunac fortunac added enhancement New feature or request WP Involves the Weakest Precondition computation labels Oct 31, 2019
@fortunac
Copy link
Author

Closed in #158.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request WP Involves the Weakest Precondition computation
Projects
None yet
Development

No branches or pull requests

1 participant