Project

General

Profile

Bug #3497

FV does not work when array index is a variable

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

Status:
Feedback
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
08/28/2018
Due date:
% Done:

0%

Estimated time:

Description

If the model contains an expression of the form Output = Input[(Input0)]; then the file generated for the model checker is incorrect.

To reproduce:
1) Open the attached model
2) Try to run OCRA constraints

Expected: the status of checking the contract should be true
Actual: An error is logged in the console.

3497.af3_23 (7.77 KB) 3497.af3_23 Anonymous, 08/28/2018 03:21 PM

Related issues

Related to Bug #1756: NullPointerException by TL specification checkingClosed09/24/2013

History

#1 Updated by Anonymous about 2 years ago

  • Related to Bug #1756: NullPointerException by TL specification checking added

#2 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC2 (Tested, Bug-free) to Backlog

#3 Updated by Johannes Eder over 1 year ago

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

#4 Updated by Johannes Eder over 1 year ago

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

#5 Updated by Anonymous about 1 year ago

  • Status changed from New to Feedback
  • Assignee changed from Anonymous to Johannes Eder

Since nobody will maintain FV, I would reject

#6 Updated by Simon Barner about 1 year ago

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

#7 Updated by Simon Barner about 1 year ago

  • Assignee deleted (Johannes Eder)

Also available in: Atom PDF