Ambiguous path error using why3
ID0002454: This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 |
| Reporter | jwaksbaum | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | i386 | OS | Darwin | OS Version | 18.6.0 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path: both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
Steps To Reproduce :
Why3 errors on the generated goals produce by w3 on certain inputs with the following message:
Ambiguous path: both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information