Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000393Frama-CPlug-in > slicingpublic2010-02-04 14:042010-04-13 15:33
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000393: assigns clauses are missing from the sliced program
DescriptionWhen the original program contains assigns clauses for functions with code,
the assigns are always omitted from the generated sliced program.

On the other hand pre- and post-conditions seem to be properly included.

In the attached example, the command produces a sliced program that contains:

/*@ requires \valid(p);
    behavior default:
      ensures (p->a > p->b);
        */
void g_slice_1(las *p )
{
...

The expected behavior is for g_slice_1 to contain in its contract the clause:
assigns p->a;
in addition to the requires and ensures.
Additional Informationframa-c -slicing-level 3 -slicing-keep-annotations -slice-assert main -slice-print -ocode slice.foo.c -main main -lib-entry -no-unicode -context-valid-pointers foo.c




# pragma JessieIntegerModel(exact)
typedef struct las { int a; int b; } las;

/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void f(las * p){ p->a = p->b + 1;}

/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void g(las * p) { f(p); }

/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void main(las * p) { g(p);
 //@ assert p->a>p->b;
}
TagsNo tags attached.
Relationships
Attached Files

Notes
(0000667)
patrick   
2010-02-04 16:09   
Done for assigns and variant clauses of function contracts:

Sending src/slicing/slicingTransform.ml
Sending tests/slicing/keep_annot.c
Sending tests/slicing/oracle/keep_annot.1.res.oracle
Sending tests/slicing/oracle/keep_annot.res.oracle
Transmitting file data ....
Committed revision 7634.
(0000668)
patrick   
2010-02-04 16:39   
Revision: 7633
(0000670)
signoles   
2010-02-04 16:45   
Will be definitively closed at the time of the next public release.

Issue History
Date ModifiedUsernameFieldChange
2010-02-04 14:04pascalNew Issue
2010-02-04 14:04pascalStatusnew => assigned
2010-02-04 14:04pascalAssigned To => Anne
2010-02-04 14:07pascalStatusassigned => acknowledged
2010-02-04 16:09patrickNote Added: 0000667
2010-02-04 16:39patrickNote Added: 0000668
2010-02-04 16:39patrickStatusacknowledged => closed
2010-02-04 16:39patrickResolutionopen => fixed
2010-02-04 16:39patrickFixed in Version => Frama-C svn, precise the release id
2010-02-04 16:45signolesStatusclosed => resolved
2010-02-04 16:45signolesNote Added: 0000670
2010-04-13 15:30signolesStatusresolved => new
2010-04-13 15:31signolesStatusnew => closed
2010-04-13 15:33signolesFixed in VersionFrama-C svn, precise the release id => Frama-C Boron