search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Function symbols with clashing names are not detected #3403

Closed mattulbrich closed 6 months ago

mattulbrich commented 6 months ago

Description

Since it occurred in practice: If function symbols are (accidently) redefined using a different signature, the system does not report an error or warning, but the new definition is silently ignored. It does not matter if the conflict is within a user-extension or wrt the background builtin symbols.

Reproducible

always

Steps to reproduce

Load a KeY-file with the following content. It should report a clashes (f vs. f, and null vs. built-in null), but does not. The null definition taken by KeY is the old one btw. 

\functions {
  int f(int);
  boolean f(Object);

  int null(int);
}

\problem {
  null = null
}
mattulbrich commented 6 months ago

It seems that this has been indeed fixed since I last updated my branches. Then let me underline that this is an important fix that kept us confused us for quite some time. ... Thanks, @wadoon