Frama-C Bug Tracking System - Frama-C
View Issue Details
0000725Frama-CKernelpublic2011-02-17 08:522014-02-12 16:59
pascal 
virgile 
normalminoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000725: passing (C && c) as argument to a function that expects int (csmith)
$ 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 }})
No tags attached.
c char_ampamp.c (126) 2011-02-17 14:46
https://bts.frama-c.com/file_download.php?file_id=175&type=bug
Issue History
2011-02-17 08:52pascalNew Issue
2011-02-17 08:52pascalStatusnew => assigned
2011-02-17 08:52pascalAssigned To => pascal
2011-02-17 08:52pascalFile Added: char_ampamp.c
2011-02-17 14:44pascalAssigned Topascal => virgile
2011-02-17 14:45pascalFile Deleted: char_ampamp.c
2011-02-17 14:46pascalFile Added: char_ampamp.c
2011-02-17 14:46pascalNote Added: 0001512
2011-02-17 18:42svnCheckin
2011-02-17 18:42svnStatusassigned => resolved
2011-02-17 18:42svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2011-10-21 14:38pascalStatusclosed => feedback
2011-10-21 14:38pascalResolutionfixed => reopened
2011-10-21 14:39pascalCategoryPlug-in > value analysis => Kernel
2011-10-21 14:39pascalStatusfeedback => closed
2011-10-21 14:39pascalResolutionreopened => fixed
2014-02-12 16:59Note Added: 0004832
2014-02-12 16:59Statusclosed => resolved

Notes
(0001512)
pascal   
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.