Parsing "implicit attributes" in induction rul application

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-236

• Submitted on: 2003-10-17 by (at)angelaw

• Updated: 2011-02-15

• Assigned to: (at)most

Description

Not possible to parse the "implicit attributes" which
appear after object creation. Complaints that "<"
is not expected.

Steps to reproduce

(1) Proof attempt of program with some object creation 
    (I used an array).
(2) Apply heuristics.
(3) Pick induction rule (int_induction). Drag and drop the 
    pgm so it becomes most of the induction hypothesis.
    This now includes "implicit attributes" from (2).
(4) Apply and parsing fails! 

Additional Information

When reporting this bug:
1. I missed a category for "parsing".
2. This is a major problem for anybody attemting at 
   induction proofs for pgms t.contain objects. It might
   be possible to overcome temporarily for some cases by
   applying induction first and then heuristics.

Files

Notes

(at)rbubel at 2003-11-03

in version 0.812 the implicit attributes are parsed when they occur in terms
not in the program (latter one is work in progress)

(at)rbubel at 2004-01-21

version 0.871:
The implicit fields and methods are now part of the recoder model as far as only objects are affected (arrays is another thing). Parsing for them should work now.

(at)most at 2005-05-31

That should be fixed for long time now.

(at)bweiss at 2011-02-15

Closing as reporter is no longer available.

History

• (at)angelaw -- (NEW_BUG) 2003-10-17

• (at)rbubel -- (BUGNOTE_ADDED) 2003-11-03

• (at)rbubel -- (BUG_MONITOR) 2003-11-03

• (at)rbubel -- (NORMAL_TYPE) 2003-11-15

• (at)klebanov -- (NORMAL_TYPE) 2003-12-17

• (at)klebanov -- (NORMAL_TYPE) 2003-12-17

• (at)rbubel -- (BUGNOTE_ADDED) 2004-01-21

• (at)most -- (NORMAL_TYPE) 2005-05-31

• (at)most -- (NORMAL_TYPE) 2005-05-31

• (at)most -- (NORMAL_TYPE) 2005-05-31

• (at)most -- (BUGNOTE_ADDED) 2005-05-31

• (at)bweiss -- (BUGNOTE_ADDED) 2011-02-15

• (at)bweiss -- (NORMAL_TYPE) 2011-02-15

• (at)grahl -- (NORMAL_TYPE) 2014-01-03

• (at)grahl -- (NORMAL_TYPE) 2014-01-03

Attributes

• Category: Parser
• Status: CLOSED
• Severity: MAJOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: HIGH
• Reproducibility: ALWAYS
• Platform: Reiner's PC in Gbg
• Commit: None
• Build: key-0.788
• Tags []
• Labels: ~KeY Parser ~Bug ~HIGH

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:26:57.578Z
• updated_at: 2017-05-29T02:26:58.712Z
• closed_at: 2017-05-29T02:26:58.609Z (closed_by: )
• milestone:
• user_notes_count: 0