search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
822 stars 259 forks source link

Incorrect evaluation of logical conditions in VSD intervals #6323

Open martin-cs opened 3 years ago

martin-cs commented 3 years ago

These tests uncover a couple of issues in evaluation:

https://github.com/diffblue/cbmc/pull/6300#pullrequestreview-741844376

jimgrundy commented 3 years ago

Are there possible soundness issues here? If so, we'd be interested in it.

TGWDB commented 3 years ago

@jimgrundy This is a soundness issue with the abstract interpretation done for variable sensitivity (an experimental feature) in the goto-analyzer program. These are not included/used in the cbmc executable itself (and so cbmc does not have a soundness problem here). Thus, this should only be a soundness concern if you're using goto-analyzer and the variable sensitivity (experimental) features. Does that address your concern?

jimgrundy commented 3 years ago

@TGWDB ok, thanks for the analysis, removing "soundness" label.