Project

General

Profile

Feature #3387

[Z3] Raise an error when Z3 cannot be executed

Added by Simon Barner over 2 years ago. Updated about 2 months ago.

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
04/18/2018
Due date:
% Done:

0%

Estimated time:

Description

As discussed on #3385, the execution of Z3 has failed on MacOS because (the dependencies of) native libraries could not be resolved.

Since the problem can also occur on other platforms (e.g. because of an erroneous update of Z3, problem introduced into OS specific RCP application, change to OS such as introduction of System Integrity Protection as discussed in #3385, an error dialog should be displayed to the user in case Z3 cannot be executed. The current behavior is "fail-silent", apart from exceptions logged to the Eclipse <workspace/.metadata/.log file.

Testing
  • Temporarily remove native libraries from developer installation
    • First remove libz3.{dll,so,dylib}. It is required by libz3java.{dll,so,dylib} and should already raise an error
    • After reverting, remove libz3java.{dll,so,dylib}
    • On Windows, also test that the removal of the remaining DLLs (Visual Studio runtime etc.) is properly detected.
  • Testing in RCP product (e.g., from nightly build) is also recommended.

History

#1 Updated by Simon Barner over 2 years ago

  • Subject changed from [Z3] Raise an error when Z3 cannot be exected to [Z3] Raise an error when Z3 cannot be executed

#2 Updated by Marco Volpe over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to AF3 2.15 RC1 (Feature Freeze)

#3 Updated by Alexander Diewald over 1 year ago

  • Target version changed from AF3 2.15 RC1 (Feature Freeze) to AF3 2.15 RC1 (Feature Freeze)

#4 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.15 RC1 (Feature Freeze) to AF3 2.16 RC1 (Feature Freeze)

#5 Updated by Marco Volpe about 1 year ago

  • Target version changed from AF3 2.16 RC1 (Feature Freeze) to AF3 2.17 (Feature Freeze)

#6 Updated by Alexander Diewald 8 months ago

  • Target version changed from AF3 2.17 (Feature Freeze) to Backlog

#7 Updated by Marco Volpe about 2 months ago

  • Assignee changed from Marco Volpe to Johannes Eder

#8 Updated by Johannes Eder about 2 months ago

  • Status changed from New to Rejected
  • Assignee deleted (Johannes Eder)

Current implementation takes care that Z3 loads on all platforms.

Also available in: Atom PDF