Project

General

Profile

Bug #3597

STL OCRA contract verification not working on Windows

Added by Anonymous almost 2 years ago. Updated about 1 year ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
Formal Verification
Target version:
Start date:
12/18/2018
Due date:
% Done:

0%

Estimated time:

Description

Try to verify OCRA contracts for STL in windows.

Expected: They should succeed with SUCCESS status

Actual: Status is ERROR

History

#1 Updated by Anonymous almost 2 years ago

The root of the problem is that I am using #define in my orca specification for functions and enums.
There are two possible options -
1) Talk to fbk ppl and ask them about this issue.
2) Find a workaround, i.e. replace the preprocessor with the actual value. This might be OK for functions without parameters, but if a function is taking a parameter then we will have to replace the function call with actual body instantiated with the actual parameter.

There is a 3rd option also - state that OCRA contracts are not fully supported on windows.

#2 Updated by Anonymous over 1 year ago

  • Assignee changed from Anonymous to Anonymous

I would like to go with the 3rd Option - declare that OCRA is not supported fully on windows.

#3 Updated by Anonymous over 1 year ago

I'm fine with it.
ERROR means that something went wrong and it is different from FAILURE right?

#4 Updated by Anonymous over 1 year ago

yes

#5 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.15 RC2 (Tested, Bug-free) to AF3 2.16 RC2 (Tested, Bug-free)

#6 Updated by Anonymous over 1 year ago

  • Assignee changed from Anonymous to Anonymous

Can this be closed?

#7 Updated by Simon Barner about 1 year ago

  • Category set to Formal Verification
  • Assignee deleted (Anonymous)
  • Target version changed from AF3 2.16 RC2 (Tested, Bug-free) to Backlog

Also available in: Atom PDF