2021-01-17 22:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001844Frama-CPlug-in > wppublic2014-07-17 22:41
Assigned Tocorrenson 
PlatformOSLinux Ubuntu 14.04 LTSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001844: assigns crash on incorrect locations
DescriptionOn the file "crash_assigns.c",
an invalid assign clause makes wp crash with the message:
Current source was: crash_assigns.c:5
The full backtrace is:
Raised at file "hashtbl.ml", line 353, characters 18-27
Called from file "hashtbl.ml", line 361, characters 22-38

Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Steps To Reproducerun frama-c-gui crash_assigns.c

and try to prove assigns clause using wp.
Additional InformationReplacing the invalid assigns clause with a valid one like
  assigns t[0..9];
makes the pb disappear...
TagsNo tags attached.
Attached Files
  • c file icon crash_assigns.c (77 bytes) 2014-07-17 22:41 -
    /*@ requires \valid(t+(0..9));
      @ assigns t+(0..9);
    void foo(int *t) {
    c file icon crash_assigns.c (77 bytes) 2014-07-17 22:41 +


There are no notes attached to this issue.

-Issue History
Date Modified Username Field Change
2014-07-17 22:41 boulme New Issue
2014-07-17 22:41 boulme Status new => assigned
2014-07-17 22:41 boulme Assigned To => correnson
2014-07-17 22:41 boulme File Added: crash_assigns.c
+Issue History