Project

General

Profile

Support #3233

Inefficiency in checking contract against implementation

Added by Anonymous almost 3 years ago. Updated over 1 year ago.

Status:
New
Priority:
Low
Assignee:
-
Target version:
Start date:
12/14/2017
Due date:
% Done:

0%

Estimated time:

Description

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.

History

#1 Updated by Anonymous over 2 years ago

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

#2 Updated by Johannes Eder over 1 year ago

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

Also available in: Atom PDF