Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Files

- Relationships

-  Notes
(0000667)
patrick (developer)
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 (developer)
2010-02-04 16:39

Revision: 7633
(0000670)
signoles (manager)
2010-02-04 16:45

Will be definitively closed at the time of the next public release.

- Issue History
Date Modified Username Field Change
2010-02-04 14:04 pascal New Issue
2010-02-04 14:04 pascal Status new => assigned
2010-02-04 14:04 pascal Assigned To => Anne
2010-02-04 14:07 pascal Status assigned => acknowledged
2010-02-04 16:09 patrick Note Added: 0000667
2010-02-04 16:39 patrick Note Added: 0000668
2010-02-04 16:39 patrick Status acknowledged => closed
2010-02-04 16:39 patrick Resolution open => fixed
2010-02-04 16:39 patrick Fixed in Version => Frama-C svn, precise the release id
2010-02-04 16:45 signoles Status closed => resolved
2010-02-04 16:45 signoles Note Added: 0000670
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version Frama-C svn, precise the release id => Frama-C Boron


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker