Queries related to explicit-edge analysis about cbat_tools HOT 4 OPEN

Full disclosure: this plugin was written by one of our students who has since moved on. I'm going to try to crawl through the code and documentation, but it might take a bit.

from cbat_tools.

Thank you for taking your time on this. No problem.

from cbat_tools.

I'll chime in with answers to the first 3.

1. The numbers displayed there are the TIDs.

   cbat_tools/value_set/plugin/value_set.ml

   Line 45 in aa89797

   "%a@ @[Precondition:@ %a@]@ @[Postcondition:@ %a@]@."

2. Here the VSA is intentionally stopping, because (as the message says) it's trying to do a left bit shift, and one of the value-sets has a maximum element that's bigger than the width of the other value-set. We didn't implement handling of such cases, so the analysis simply stops and reports this. To get past this, try running the plugin with the --value-set-keep-trying flag. That will tell the plugin to simply use top as the result of the bitshift operation, rather than stopping.

3. Good question. This can be a bit hard to spot in the README for the explicit-edge plugin, but it notes that --explicit-edge-sub is different from --value-set-sub. So you need to include both flags in your command if you want the value-set to only run on main, and then you also want the explicit-edge to run on main. Like this: bap ./switch -p explicit-edge --value-set-sub main --explicit-edge-sub main

from cbat_tools.

Thank you @jtpaasch for your inputs. I will work with these changes and update if I have any queries.

from cbat_tools.