Mentions légales du service

Skip to content

Clone location for let defn

Benedikt Becker requested to merge clone-location-for-let-defn into master

Currently, when a let definition is cloned, the identifier retains the location of the original definition in the cloned module. In particular, when a module is cloned several times, the resulting definitions have the same name and location. However, a counterexample maps source locations and variable names (i.e., strings) to model values. Model values may be lost (or ill-typed) for variables that were cloned several times (with different type substitutions).

With this MR, the location of the clone is used in Pmodule.clone_export as the location of the cloned let definitions, to improve counterexamples in presence of multiple clones.

Edited by Benedikt Becker

Merge request reports