View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000673 | Frama-C | Plug-in > slicing | public | 2011-01-17 16:33 | 2014-02-12 16:55 | ||||
Reporter | signoles | ||||||||
Assigned To | patrick | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Carbon-20101202-beta2 | ||||||||
Target Version | Fixed in Version | Frama-C Carbon-20110201 | |||||||
Summary | 0000673: untypable ACSL in a sliced program containing \result | ||||||||
Description | If 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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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... |
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 ? |
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. |
![]() |
|||
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 | ||
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 |
2013-12-19 01:12 | patrick | Source_changeset_attached | => framac master 79f0b302 |
2014-02-12 16:55 | patrick | Source_changeset_attached | => framac stable/neon 79f0b302 |