Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:06 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000966Frama-CKernelpublic2011-10-10 14:14
Assigned Tovirgile 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000966: bad default assigns generation
DescriptionIn the attached program "bug_copy.c", when calling

frama-c -jessie bug_copy.c

the kernel adds an "assigns \nothing" clause to the contract:

[jessie] Starting Jessie translation
[kernel] warning: No code for function copy, default assigns generated for default behavior

This added clause makes the contract invalid (i.e. jessie proves "assert(0)" after a call to function "copy"), since the behavior "from_init" actually assigns two cells of the "auto_state" array.

Additional InformationThe problem disappears when the "complete behaviors" clause is added.

svn id around 15100


frama-c -jessie bug_copy.c -jessie-gen-only -print

to see the "assigns \nothing" clause added by the kernel.
TagsNo tags attached.
Attached Files
  • c file icon bug_copy.c (756 bytes) 2011-09-19 10:52 -
    int auto_states[4] ; //   = { 1 , 0 , 0, 0 };
    enum states {
      Init = 0,
      Copy = 1,
      Final = 3
    // contract with missing "complete behaviors"
        behavior from_init:
          assumes auto_states[Init] == 1;
          ensures (auto_states[Copy] == 1) && (auto_states[Init] == 0);
          assigns auto_states[Init], auto_states[Copy];
        behavior from_other:
          assumes (auto_states[Init] == 0);
          assigns \nothing;
    void copy(int x);
    int main() {
      auto_states[Init] = 1;
      auto_states[Copy] = 0;
      auto_states[Set] = 0;
      auto_states[Final] = 0;
      //@ assert(0);
      //@ assert(auto_states[Init] == 0);
      //@ assert(auto_states[Copy] == 1);
      //@ assert(auto_states[Set] == 0);
      //@ assert(auto_states[Final] == 0);
    c file icon bug_copy.c (756 bytes) 2011-09-19 10:52 +




monate (reporter)

Jessie seems to do something fancy here: other plugins do not suffer from this.
The generated default assigns is
assigns auto_states[Init], auto_states[copy]
For example use "-val -print" or "-wp -print"

Anyway, whenever the "no code for function ... default assigns generated" appears, you should complete your specification. The auto-generation is only here to prevent from failing completly and to point out where you may need to proof check your specification.


virgile (developer)

The assigns \nothing indeed comes from Jessie itself. Kernel does the right thing here.
On the other hand, while I agree that auto-generation of assigns cannot be used reliably, it should at least be consistent with existing behavior-specific assigns when it generates a global assigns (i.e. take the union of location, as is the case for kernel, but apparently not for jessie).


virgile (developer)

My bad, this is indeed a kernel bug: the contribution of jessie is only that it adds a default behavior to each function, whose assigns is then dutifully filled by the default assigns generator. You can observe the same behavior if you add an ensures \true; at the beginning of the spec of copy, with -val -print.

-Issue History
Date Modified Username Field Change
2011-09-19 10:52 pherrmann New Issue
2011-09-19 10:52 pherrmann File Added: bug_copy.c
2011-09-19 11:50 pherrmann Description Updated
2011-09-20 07:44 signoles Status new => assigned
2011-09-20 07:44 signoles Assigned To => virgile
2011-09-20 22:03 monate Note Added: 0002301
2011-09-21 09:10 virgile Note Added: 0002302
2011-09-21 09:10 virgile Category Kernel => Plug-in > jessie
2011-09-21 10:40 virgile Note Added: 0002305
2011-09-21 10:40 virgile Category Plug-in > jessie => Kernel
2011-09-21 11:20 svn
2011-09-21 11:20 svn Status assigned => resolved
2011-09-21 11:20 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
+Issue History