Why3 warning
ID0002263: This issue was created automatically from Mantis Issue 2263. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002263 | Frama-C | Plug-in > wp | public | 2016-12-16 | 2016-12-16 |
| Reporter | jens | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
When running WP I observe the following warning
[Config] reading extra configuration file /Users/jens/.opam/4.04.0/share/frama-c/wp/why3/why3.conf File "/Users/jens/.opam/4.04.0/share/why3/drivers/smt-libv2.drv", line 34, characters 7-14: Library file not found: int
The problem occurs both under Linux and macOS.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information