Use of axioms in axiomatic specification is not supported
ID0001858: This issue was created automatically from Mantis Issue 1858. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001858 | Frama-Clang | Plug-in > clang | public | 2014-07-25 | 2014-08-08 |
| Reporter | lapawczykt | Assigned To | fvedrine | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | ubuntu 14.04 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C GIT, precise the release id |
Description :
As soon as an axiom is written inside an axiomatic specification frama-c complains: problem309.cpp:5:9: axiom foo_1should be declared inside an axiomatic. However this works in c.
Additional Information :
The problem309.c file can also be found in the acslplusplus repository.
Steps To Reproduce :
frama-c-gui.byte -wp -rte -pp-annot -no-unicode problem309.cpp