ID0002160: **This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002160 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2015-09-15 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - | ### Description : When trying to analyse the this: #include <string.h> int main() { char a; memset(&a, 0, 1); } Using wp I get: [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: No definition for 'memchr' interpreted as reads nothing [wp] warning: No definition for 'strlen' interpreted as reads nothing [wp] warning: No definition for 'memset' interpreted as reads nothing [wp] warning: No definition for 'strchr' interpreted as reads nothing [wp] warning: No definition for 'strcmp' interpreted as reads nothing [wp] warning: No definition for 'strncmp' interpreted as reads nothing [wp] warning: No definition for 'wcscmp' interpreted as reads nothing [wp] warning: No definition for 'wcslen' interpreted as reads nothing [wp] warning: No definition for 'wcsncmp' interpreted as reads nothing [wp] warning: Missing RTE guards [kernel] Current source was: test.c:6 The full backtrace is: Raised at file "src/wp/MemVar.ml", line 474, characters 54-66 Called from file "src/wp/MemVar.ml", line 519, characters 16-38 Called from file "src/wp/MemVar.ml", line 543, characters 9-38 Called from file "list.ml", line 55, characters 20-23 Called from file "src/wp/Lang.ml", line 735, characters 25-40 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42 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 "list.ml", line 55, characters 20-23 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/cfgWP.ml", line 1087, characters 18-60 Called from file "src/wp/Warning.ml", line 155, characters 14-18 Called from file "src/wp/cfgWP.ml", line 1118, characters 23-207 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 448, characters 14-224 Called from file "src/wp/calculus.ml", line 595, characters 10-57 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 724, characters 40-59 Called from file "set.ml", line 304, characters 38-41 Called from file "map.ml", line 168, characters 20-25 Called from file "map.ml", line 168, characters 10-18 Called from file "map.ml", line 168, characters 10-18 Called from file "src/wp/calculus.ml", line 724, characters 4-64 Called from file "src/wp/calculus.ml", line 770, characters 19-51 Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/lib/bag.ml", line 96, characters 16-24 Called from file "src/wp/cfgWP.ml", line 1391, 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 15-40 Called from file "src/wp/register.ml", line 574, characters 17-24 Re-raised at file "src/wp/register.ml", line 578, characters 27-29 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 30-32 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 30-32 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 763, characters 2-9 Called from file "src/kernel/cmdline.ml", line 216, characters 4-8 Unexpected error (File "src/wp/MemVar.ml", line 474, characters 54-60: Assertion failed). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Sodium-20150201. 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