Feature #6570
closed
Iterate over dictionaries deterministically in EMG
Added by Ilja Zakharov over 8 years ago.
Updated about 8 years ago.
Category:
Environment models
Description
All loops over dictionaries should be rewritten to guarantee deterministical generation of an environment model code, since default Python "for" loops do that differently from time to time.
- Category set to Environment models
BTW this nondeterminism leads to we can't use our simple error trace comparison algorithms since function names vary from time to time.
- Priority changed from High to Normal
#6814 suggests the much more universal approach than deterministic names of functions from environment models.
- Priority changed from Normal to High
nondetermism in generated EMG models leads to nondeterministics of results produced by verification tools, thus this bug is still important to fix
- Priority changed from High to Urgent
For at least 3 modules from the validation set CPAchecker can consume several times more resources and even fails with time outs instead of finding target bugs likely due to non-determinism in generated environment models. Without deterministic behaviour even at that level we can not perform reliable experiments.
- Status changed from New to Resolved
- Priority changed from Urgent to High
The problem is solved and corresponding code merged to master.
Aspect files generated by EMG and corresponding cil files should be equivalent now. If you encounter any problems with non-determinism caused by EMG it is preferable to open a new issue with details about your task provided.
- Status changed from Resolved to Closed
Also available in: Atom
PDF