Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000673Frama-CPlug-in > slicingpublic2011-01-17 16:332014-02-12 16:55
Reportersignoles 
Assigned Topatrick 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000673: untypable ACSL in a sliced program containing \result
DescriptionIf a function contract contains \result, then the sliced function keeps it even if it now returns void.
Steps To Reproduce===== bug.c =====
void f(void) { return; }

/*@ ensures \result == 0; */
int main(void) { f(); return 0; }
==================

$ frama-c bug.c -slice-calls f -then-on "Slicing export" -print -ocode sliced_bug.c
$ more sliced_bug.c
/* Generated by Frama-C */
void f_slice_1(void)
{
  return;
}

/*@ ensures (\result ? 0);
      */
void main(void)
{
  f_slice_1();
  return;
}


$ frama-c sliced_bug.c
[kernel] preprocessing with "gcc -C -E -I. sliced_bug.c"
sliced_bug.c:7:[kernel] user error: \result meaningless in annotation.
[kernel] user error: skipping file "sliced_bug.c" that has errors.
[kernel] Frama-C aborted because of invalid user input.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001391)
Anne (reporter)
2011-01-17 16:59

Mmm... it seems that it comes from a bug in Pdg function [find_fun_postcond_nodes] in [annot.ml].

I must look deeper to find what it is...
(0001396)
Anne (reporter)
2011-01-18 09:52

The function used to know which zones (data) are needed to interpret a predicate is [!Db.Properties.Interp.To_zone.from_pred] with [!Db.Properties.Interp.To_zone.mk_ctx_func_contrat] request. The problem is that the \result is not really a 'zone'. I guess I need another function to test if \result is used in a postcondition because it would be to difficult to change [from_pred] signature since it is used for several different purposes.

What do you think, Patrick ?
(0001399)
Anne (reporter)
2011-01-18 16:43

@Patrick: I have added a comment to [find_fun_postcond_nodes] in [annot.ml] to give a hint of how to use the previous result.

- Issue History
Date Modified Username Field Change
2011-01-17 16:33 signoles New Issue
2011-01-17 16:33 signoles Status new => assigned
2011-01-17 16:33 signoles Assigned To => Anne
2011-01-17 16:35 signoles Summary unparsable ACSL in a sliced program containing \result => untypable ACSL in a sliced program containing \result
2011-01-17 16:59 Anne Note Added: 0001391
2011-01-17 16:59 Anne Status assigned => acknowledged
2011-01-18 09:52 Anne Note Added: 0001396
2011-01-18 09:52 Anne Status acknowledged => assigned
2011-01-18 09:52 Anne Assigned To Anne => patrick
2011-01-18 09:53 Anne Note View State: 1391: public
2011-01-18 16:43 Anne Note Added: 0001399
2011-01-19 16:52 svn Checkin
2011-01-19 16:52 svn Status assigned => resolved
2011-01-19 16:52 svn Resolution open => fixed
2011-02-09 14:36 signoles Status resolved => closed
2011-02-09 14:37 signoles Fixed in Version => Frama-C Carbon-20110201


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker