Inefficiency in checking contract against implementation
At present OCRA gives an error (segmentation fault) if we try to pass the contract for implementation with -C option. So, at present for implementation all the contracts in the specification file are verified.
This results in inefficiency as demonstrated by the following example:
Consider a component with 5 contracts. This results in 5 “constraints”.
Now due to above mentioned problem the total number of verified
contracts is 25 (5 * 5). This results in inefficient implementation.
Now, either this should be resolved by fbk or we should adapt our
implementation.
(from redmine: issue id 3233, created on 2017-12-14)