Update and expand examples

[Johanmyst]

See this pull request #1460

[jumormt]

Thanks for your contribution @Johanmyst . I am wondering whether this patch supports linking the debug version of SVF so developer can debug SVF code. Currently this function is implemented like this, which link the debug-version SVF if SVF-example is built in debug mode and release-version otherwise.

[jumormt]

Another issue is that it requires a Z3Config.cmake to be able to link with z3. However, if a user is using a z3 pre-built binary the cmake configuration will crash like this:

Here is the structure of z3 pre-built binary:

[jumormt]

I also tried building current SVF-example with your patch but get the error:

Although I've already set the Z3_DIR in both the environment and command line.

[Johanmyst]

Thanks for your contribution @Johanmyst . I am wondering whether this patch supports linking the debug version of SVF so developer can debug SVF code. Currently this function is implemented like this, which link the debug-version SVF if SVF-example is built in debug mode and release-version otherwise.

As far as I am aware (I tested both builds) this should happen automatically. Whichever version you build, once you run cmake --install <build_dir>, it will install whatever tree was built into the specified installation prefix. The SVFConfig.cmake will be placed under <prefix>/lib/cmake/SVF/SVFConfig.cmake. As long as (if you install in a non-standard location) that directory is searched by cmake (the default prefix /usr/local is picked up automatically, but otherwise you might need to add the <prefix>/lib directory to $CMAKE_PREFIX_PATH (see this link) for it to be picked up.

Note that you could also install both build types (in separate locations) and specify whichever you want by prioritising it through the HINTS system in find_package(). If you were to install the Release-build into prefix A, and the Debug-build into prefix B, you could prioritise either build type like this: find_package(SVF CONFIG REQUIRED HINTS ${PREFIX_A}). The HINTS paths are searched before others, so this would ensure the desired version is found first.

If you encounter issues with this, please let me know as in my tests this seemed to work perfectly fine!

[Johanmyst]

Another issue is that it requires a Z3Config.cmake to be able to link with z3. However, if a user is using a z3 pre-built binary the cmake configuration will crash like this: Here is the structure of z3 pre-built binary:

Ah, this is because the pre-built Z3 libraries don't seem to come with the cmake package files. I thought I addressed this in this commit (#1460).

In that commit I made the Z3 CMake package non-mandatory; if it was not found I simply applied the "old way" of searching for the Z3 files manually. I used find_dependency() in the SVFConfig.cmake.in file, which according to its documentation should mirror the original find_package() call's signature (i.e. if the original find_package(Z3) was called without REQUIRED, this call shouldn't use REQUIRED either. In that case it should just revert back to how Z3 was found previously.

Was the SVF build you were using when you saw this error including this last commit (#1460)? If so, I could just replace the find_dependency() call with an explicit find_package() call without the REQUIRED marker.