| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001789 | Frama-C | Kernel > ACSL implementation | public | 2014-05-28 22:13 | 2015-03-17 22:17 | ||||
| Reporter | Ian | ||||||||
| Assigned To | correnson | ||||||||
| Priority | normal | Severity | crash | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Platform | OS | Ubuntu | OS Version | ||||||
| Product Version | Frama-C Neon-20140301 | ||||||||
| Target Version | Fixed in Version | Frama-C Sodium | |||||||
| Summary | 0001789: Crashes when using logic in assigns statement | ||||||||
| Description | WP crashes when using a statement defined with 'logic' | ||||||||
| Steps To Reproduce | Create the file logic_assigns.c : #include <stddef.h> int *var_ptr; /*@ logic int *the_var = var_ptr; */ /*@ //assigns var_ptr; // Works assigns the_var; // WP Crashes */ void function(){ var_ptr = NULL; } void main(){ function(); } With the above file, run: frama-c -cpp-command 'gcc -C -E -x c' -pp-annot -wp logic_assigns.c and the following output is received: [kernel] preprocessing with "gcc -C -E -x c -dD logic_assigns.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] failure: Non-assignable term (the_var{Pre}) [kernel] Current source was: logic_assigns.c:15 The full backtrace is: Raised at file "src/kernel/log.ml", line 524, characters 30-31 Called from file "src/kernel/log.ml", line 518, characters 9-16 Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicSemantics.ml", line 786, characters 21-75 Called from file "list.ml", line 57, characters 20-23 Called from file "src/wp/LogicSemantics.ml", line 808, characters 27-51 Called from file "src/wp/cfgWP.ml", line 412, characters 6-147 Called from file "src/wp/Warning.ml", line 155, characters 14-18 Called from file "src/wp/cfgWP.ml", line 468, characters 22-126 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/calculus.ml", line 334, characters 27-62 Called from file "src/wp/calculus.ml", line 341, characters 23-45 Called from file "src/wp/calculus.ml", line 613, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 586, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 579, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 574, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 699, characters 40-59 Called from file "set.ml", line 288, characters 38-41 Called from file "map.ml", line 169, characters 20-25 Called from file "map.ml", line 169, characters 10-18 Called from file "map.ml", line 169, characters 10-18 Called from file "src/wp/calculus.ml", line 699, characters 4-64 Called from file "src/wp/calculus.ml", line 745, characters 19-51 Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837 Called from file "src/wp/Model.ml", line 111, characters 17-20 Re-raised at file "src/wp/Model.ml", line 116, characters 25-28 Called from file "src/wp/Model.ml", line 117, characters 19-36 Called from file "src/wp/register.ml", line 435, characters 17-42 Called from file "src/wp/register.ml", line 574, characters 17-24 Re-raised at file "src/wp/register.ml", line 578, characters 29-31 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 32-34 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 32-34 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 735, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8 Plug-in wp aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Neon-20140301. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
virgile (developer) 2014-05-29 13:19 |
Arguably, the issue lies in the kernel, that should not allow in assigns clause a logic variable which by definition is immutable. On the contrary, assigns *the_var; would be a perfectly valid clause. (NB: the_var in fact depends on the program state's, but you still can't modify it as a logic variable, you can only assign var_ptr). |
|
correnson (manager) 2014-06-02 14:07 |
Transform to user-error |
|
correnson (manager) 2014-06-02 14:27 |
Fix committed to master branch. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2014-05-28 22:13 | Ian | New Issue | |
| 2014-05-28 22:13 | Ian | Status | new => assigned |
| 2014-05-28 22:13 | Ian | Assigned To | => correnson |
| 2014-05-28 22:13 | Ian | File Added: logic_assigns.c | |
| 2014-05-29 13:13 | virgile | Assigned To | correnson => virgile |
| 2014-05-29 13:19 | virgile | Note Added: 0005173 | |
| 2014-05-29 13:19 | virgile | Category | Plug-in > wp => Kernel > ACSL implementation |
| 2014-06-02 10:40 | correnson | Status | assigned => closed |
| 2014-06-02 10:40 | correnson | Assigned To | virgile => correnson |
| 2014-06-02 10:40 | correnson | Resolution | open => no change required |
| 2014-06-02 14:07 | correnson | Note Added: 0005178 | |
| 2014-06-02 14:07 | correnson | Status | closed => assigned |
| 2014-06-02 14:27 | correnson | Source_changeset_attached | => framac master bf674574 |
| 2014-06-02 14:27 | correnson | Note Added: 0005179 | |
| 2014-06-02 14:27 | correnson | Status | assigned => resolved |
| 2014-06-02 14:27 | correnson | Resolution | no change required => fixed |
| 2015-03-17 22:17 | signoles | Fixed in Version | => Frama-C Sodium |
| 2015-03-17 22:17 | signoles | Status | resolved => closed |
| Issue History |