Skip to content

Fix initialization of solver in symbolic execution

Tomáš Dacík requested to merge xdacik00/broom:smt_queries into master

The solver for symbolic execution is initialized as a constant expression and its initialization therefore ignores command line parameters as it is evaluated before parameters are parsed. This is fixed by adding an unit argument to the initialization function.

This PR also:

  • makes bit width of memory addresses configurable from the command line
  • change filename extension of generated queries for external solver to correct string ".smt2" which helps e.g. with syntax highlighting in editors

Merge request reports