Non-determinism with duplicate code definitions

softwarelanguageslab / maf

Static Analysis Framework for Modular Analyses

Other

13 stars 11 forks source link

Open jevdplas opened 3 years ago

jevdplas commented 3 years ago

Programs with duplicate definitions (such as test/DEBUG.scm in 10c34dcb6f347176df0d8e1dd8bee5c18d7dc223) seem to have the following issues:

The program may be unsound at times, e.g. the daily benchmarks fail sometimes.
The error is related to a duplicate definition, which is sometimes bound to bottom by the analysis, but not by the concrete interpreter.

However, even though duplicate definitions exist, this should not lead to unsoundness, and certainly not in a non-deterministic way.

bramvdbogaerde commented 2 years ago

I suppose this is solved now by our new undefiner and the additional restriction that a letrec should not contain duplicate bindings?