| Re: [modeling-pmc] [CQ 11173] The Omega Project version 2.1 |
|
Assuming the project functions without this dependency, and given
no other objections/concerns being raised I'll approve it. +1
On 04.05.2016 11:59,
emo-ip-team@xxxxxxxxxxx wrote:
http://dev.eclipse.org/ipzilla/show_bug.cgi?id=11173 Arnault Lapitre <arnault.lapitre@xxxxxx> changed: What |Removed |Added ---------------------------------------------------------------------------- CC| |boutheina.bannour@xxxxxxxxx --- Comment #10 from Arnault Lapitre <arnault.lapitre@xxxxxx> 2016-05-04 05:59:51 --- In a nutshell, Omega is used only by one Formal Analysis Module (FAM) in efm-symbex which is optional: the symbolic execution kernel is completely independent, FAM modules are as plug-ins for the efm-symbex. In fact no other FAM modules is concerned. Users can activate (a) FAM module(s) upon need. Note that FAM modules can make use of existing tools such as constraint solvers Omega, CVC4, Z3, Yices… We have tried to our best to choose the solvers that are EPL compliant (e.g. we suppressed Yices and kept Z3 whose license changed recently). Now if using Omega in this module causes a license issues, we can remove the dependency to Omega and keep the module functioning with other solvers. Inline responses: 1. how this code is used by the project: The FAM module “behavior redundancy detection” may use solvers functions to compare two behaviors equivalence. Using Omega in this module is optional (as using any other solver). We can remove the dependency to Omega (the include omega.h in C++…). 2. what parts of the project depend on this: The formal analysis module “behavior redundancy detection” 3. what all doesn't function without it: The formal analysis module “behavior redundancy detection” is concerned, the other FAM modules and the symbolic execution kernel are not. |