search

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)
BSD 3-Clause "New" or "Revised" License
5 stars 3 forks source link

Variable references are not resolved in quantified expressions #11

Closed bafain closed 12 years ago

bafain commented 12 years ago

Parsing the Worthwhile annotation (for example by calling TestASTProvider::getRootASTNode) 

_axiom forall Integer a forall Integer b : a * b = b * a

results in the errors

Line 1: Couldn't resolve reference to VariableDeclaration 'a'.
Line 1: Couldn't resolve reference to VariableDeclaration 'b'.
Line 1: Couldn't resolve reference to VariableDeclaration 'b'.
Line 1: Couldn't resolve reference to VariableDeclaration 'a'.

(copied from the IllegalArgumentException, which was thrown by a getRootASTNode call, trace). Instead the variable references a and b should be considered declared by the quantified expression parameters Integer a and Integer b respectively.

jspam commented 12 years ago

Sollte ein Scoping-Problem sein, schaue ich mir sofort an.