Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002160Frama-CPlug-in > wppublic2015-09-14 23:502015-09-15 09:55
Reporterkroeckx 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002160: assertion failure using memset on a char
DescriptionWhen 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 [^]
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006037)
correnson (manager)
2015-09-15 09:55

Thank for the report.

However, you shall not use memset functions (and such) with WP since it generally involves heterogeneous pointer casts that are non-supported by its memory model.

Instead, you shall rewrite calls into dedicated functions. In your simple exemple :

//@ requires \valid(a); ensures *a == 0; assigns *a;
void memset_char (char *a);

- Issue History
Date Modified Username Field Change
2015-09-14 23:50 kroeckx New Issue
2015-09-14 23:50 kroeckx Status new => assigned
2015-09-14 23:50 kroeckx Assigned To => correnson
2015-09-15 09:55 correnson Note Added: 0006037
2015-09-15 09:55 correnson Status assigned => acknowledged


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker