drivers should not be searched in the current directory
The driver files are currently search for in the current directory. This is a misleading feature. The semantics should be:
- if the driver is given by a name without extension, it should be searched in the Why3 library. This is already the case
- is the driver is given with an extension
.drv
, and possibly with a path, it should be searched in the filesystem with the given path, relatively to the configuration file it is written
The case 2 is already done since #743 (closed) was solved. There is no reason anymore to search in the current directory