Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000725Frama-CKernelpublic2011-02-17 08:522014-02-12 16:59
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000725: passing (C && c) as argument to a function that expects int (csmith)
Description$ frama-c -val char_ampamp.c

char_ampamp.c:7:[value] reading left-value x.
        The contents is imprecise.
char_ampamp.c:7:[kernel] warning: accessing uninitialized left-value x: assert(Ook)
char_ampamp.c:7:[kernel] warning: accessing left-value x that contains escaping addresses; assert(Ook)
[value] Called Frama_C_show_each_x({{ ANYTHING }})
TagsNo tags attached.
Attached Filesc file icon char_ampamp.c [^] (126 bytes) 2011-02-17 14:46 [Show Content]

- Relationships

-  Notes
(0001512)
pascal (reporter)
2011-02-17 14:46

 Uncomment Format.printf "expr arg: %a %a@." in src/value/eval.ml.
For the attached program you will see :

expr arg: (int )c int
expr arg: c != (char)0 char

The second one is wrong.
(0004832)

2014-02-12 16:59

 Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-02-17 08:52 pascal New Issue
2011-02-17 08:52 pascal Status new => assigned
2011-02-17 08:52 pascal Assigned To => pascal
2011-02-17 08:52 pascal File Added: char_ampamp.c
2011-02-17 14:44 pascal Assigned To pascal => virgile
2011-02-17 14:45 pascal File Deleted: char_ampamp.c
2011-02-17 14:46 pascal File Added: char_ampamp.c
2011-02-17 14:46 pascal Note Added: 0001512
2011-02-17 18:42 svn Checkin
2011-02-17 18:42 svn Status assigned => resolved
2011-02-17 18:42 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2011-10-21 14:38 pascal Status closed => feedback
2011-10-21 14:38 pascal Resolution fixed => reopened
2011-10-21 14:39 pascal Category Plug-in > value analysis => Kernel
2011-10-21 14:39 pascal Status feedback => closed
2011-10-21 14:39 pascal Resolution reopened => fixed
2014-02-12 16:59 Note Added: 0004832
2014-02-12 16:59 Status closed => resolved

Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker