The specifications of statements are not translated
ID0000072: This issue was created automatically from Mantis Issue 72. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000072 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2010-02-12 |
| Reporter | bobot | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
No vc are produced with this function.
spec_statement.c :
void myfun(int p){ p = 1; /@ requires p==1; @ ensures \old(p)==p-1; @/ p = 2; }
spec_statement.jc:
unit myfun(integer p)
behavior default:
assumes true;
ensures (C_3 : true);
{
{ (C_1 : (p = 1));
(C_2 : (p = 2));
(return ())} }
Additional Information :
frama-c : 5186