Id,Project,Reporter,Assigned To,Priority,Severity,Reproducibility,Product Version,Projection,Category,Date Submitted,ETA,OS,OS Version,Platform,View Status,Updated,Summary,Status,Resolution,Fixed in Version,Duplicate ID
0000690,Frama-C,Julien Signoles,Boris Yakobowski,normal,feature,always,Frama-C Carbon-20101202-beta2,none,Plug-in > slicing,2011-01-26,none,,,,public,2012-05-16,Slicing does not preserve some ACSL constructs,assigned,open,,0000000
0001180,Frama-C,Mehdi Dogguy,Julien Signoles,normal,minor,always,Frama-C Nitrogen-20111001,none,Kernel,2012-05-16,none,,,,public,2012-05-16,Port to OCamlgraph 1.8.2,resolved,fixed,,0000000
0000419,Frama-C,Julien Signoles,Julien Signoles,low,text,have not tried,Frama-C Beryllium-20090902,none,Documentation,2010-02-23,none,,,,public,2012-05-16,Plug-in dev guide: tutorial for kernel integrated plug-in is out-of-date,resolved,fixed,,0000000
0000764,Frama-C,Julien Signoles,Julien Signoles,normal,feature,N/A,,none,Kernel,2011-03-25,none,,,,public,2012-05-16,Specifying several directories in environment variables FRAMAC_*,resolved,fixed,,0000000
0001179,Frama-C,Jochen,Loïc Correnson,normal,tweak,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2012-05-10,none,,,,public,2012-05-15,Suggest to supply values of global consts to provers,feedback,reopened,,0000000
0001089,Frama-C,Boris Hollas,Julien Signoles,normal,minor,N/A,Frama-C Nitrogen-20111001,none,Documentation,2012-02-09,none,,,,public,2012-05-10,Updated example in plugin-development-guide,resolved,fixed,,0000000
0001036,Frama-C,Florent Garnier,Julien Signoles,normal,feature,N/A,Frama-C Nitrogen-20111001,none,Documentation,2011-11-30,none,,,,public,2012-05-09,In section 5.11.5 of the Plugin developper manual : Reference to modules that neither appear in the API nor in Frama-c source.,resolved,fixed,,0000000
0001178,Frama-C,Anne Pacalet,Virgile Prevosto,normal,major,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-05-04,none,,,,public,2012-05-07,Several types for the same function,resolved,duplicate,"Frama-C SVN, precise the release id",0000728
0001085,Frama-C,Pascal Cuoq,Julien Signoles,normal,minor,always,,none,Documentation,2012-02-08,none,,,,public,2012-04-30,Cute boolean options too cute for their own good,resolved,fixed,,0000000
0001127,Frama-C,Anne Pacalet,Julien Signoles,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-03-21,none,,,,public,2012-04-26,Error in Type.pp_ml_name with Datatype.String.Set.ty,resolved,fixed,Frama-C Oxygen-2012xx01,0000000
0001165,Frama-C,Anne Pacalet,Virgile Prevosto,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-04-17,none,,,,public,2012-04-24,[libc] erreur: #endif sans #if,resolved,fixed,,0000000
0001136,Frama-C,Anne Pacalet,Virgile Prevosto,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-03-27,none,,,,public,2012-04-24,[Globals.Vars.get_astinfo] doesn't work,feedback,reopened,,0000000
0001110,Frama-C,Anne Pacalet,Boris Yakobowski,normal,crash,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-03-02,none,,,,public,2012-04-18,Using Filter without Value,resolved,fixed,,0000000
0001161,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,error in wp_behav.c,assigned,open,,0000000
0001159,Frama-C,Nicolas Muller,Claude Marché,normal,feature,have not tried,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,cast of pointer to structures,assigned,open,,0000000
0001162,Frama-C,Nicolas Muller,Virgile Prevosto,normal,minor,always,Frama-C Nitrogen-20111001,none,Kernel > ACSL implementation,2012-04-16,none,,,,public,2012-04-17,"for" clause is refused,resolved,fixed,Frama-C Nitrogen-20111001,0000000
0001154,Frama-C,Nicolas Muller,Claude Marché,normal,minor,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,erroneous left value (structure field),assigned,open,,0000000
0001156,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,struct type not supported in type invariant,assigned,open,,0000000
0001149,Frama-C,Nicolas Muller,Virgile Prevosto,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,function names are restricted due to exclusion of ACSL keywords,resolved,fixed,"Frama-C SVN, precise the release id",0000000
0001148,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,tsets union not accepted in predicates,feedback,reopened,,0000000
0001155,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,inductive clause seems not to pass jessie translation,assigned,open,,0000000
0001092,Frama-C,Jochen,Pascal Cuoq,normal,text,N/A,Frama-C Nitrogen-20111001,none,Documentation,2012-02-13,none,,,,public,2012-04-17,some typos etc. in the value-analysis manual,resolved,fixed,,0000000
0001157,Frama-C,Nicolas Muller,Claude Marché,normal,minor,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,erroneous logic syntax,assigned,open,,0000000
0001160,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,struct not supported as logic argument,assigned,open,,0000000
0001151,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,comparison of structures not implemented,assigned,open,,0000000
0001158,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,inlining of assembleur is not supported,assigned,open,,0000000
0001153,Frama-C,Nicolas Muller,Claude Marché,normal,feature,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-04-16,none,,,,public,2012-04-17,pointer casts not supported,assigned,open,,0000000
0001024,Frama-C,Pascal Cuoq,Boris Yakobowski,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2011-11-19,none,,,,public,2012-04-16,Emitted assertion wrongly reduces to bottom (apparently) (csmith),resolved,fixed,,0000000
0000687,Frama-C,Julien Signoles,Julien Signoles,normal,minor,always,,none,Kernel,2011-01-25,none,,,,public,2012-04-15,Losing some cmdline option settings when loading,assigned,open,,0000000
0001145,Frama-C,Anne Pacalet,Julien Signoles,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Kernel > Makefile,2012-04-12,none,,,,public,2012-04-12,PLUGIN_LINK_GUI_OFLAGS not used ?,resolved,fixed,,0000000
0000728,Frama-C,Virgile Prevosto,Virgile Prevosto,normal,minor,have not tried,Frama-C Carbon-20110201,none,Kernel,2011-02-17,none,,,,public,2012-04-12,Arguments are not checked when function call precedes function declaration,resolved,fixed,,0000000
0000759,Frama-C,David Delmas,Boris Yakobowski,normal,major,always,Frama-C Carbon-20110201,none,Plug-in > value analysis,2011-03-21,none,,,,public,2012-04-11,wrong treatment for const arrays in lib-entry mode,assigned,reopened,,0000000
0001144,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel,2012-04-07,none,,,,public,2012-04-09,"17944 using option -unspecified-access, no alarm for x + (x=0)",resolved,fixed,,0000000
0001142,Frama-C,Philippe Herrmann,Boris Yakobowski,normal,minor,always,,none,Plug-in > value analysis,2012-04-04,none,,,,public,2012-04-09,Bad AST generation ?,resolved,fixed,,0000000
0001026,Frama-C,Philippe Herrmann,Boris Yakobowski,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2011-11-25,none,,,,public,2012-04-08,value analysis memory consumption problem  when using -lib-entry option,assigned,open,,0000000
0001141,Frama-C,Anne Pacalet,Benjamin Monate,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-04-04,none,,,,public,2012-04-06,incorrect UINT8_MAX (and others),resolved,fixed,Frama-C Oxygen-2012xx01,0000000
0001140,Frama-C,Anne Pacalet,Benjamin Monate,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-04-04,none,,,,public,2012-04-06,Strange declaration mismatch,resolved,fixed,Frama-C Oxygen-2012xx01,0000000
0000915,Frama-C,David Delmas,Pascal Cuoq,normal,feature,always,Frama-C Carbon-20110201,none,Plug-in > value analysis,2011-08-05,none,,,,public,2012-04-05,interest for a built-in memset function,assigned,open,,0000000
0000831,Frama-C,Pierre-Loïc Garoche,Virgile Prevosto,normal,major,always,Frama-C Boron-20100401,none,Kernel,2011-05-20,none,,,,public,2012-04-05,Successive calls of Cil.emptyfunction  generate a Failure("trying to redefine an existing kernel function"),feedback,open,,0000000
0000594,Frama-C,Dillon Pariente,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel,2010-10-02,none,,,,public,2012-04-05,Kernel error with RTE generated annotations: invalid operands (bitwise),resolved,fixed,,0000000
0000384,Frama-C,Guillaume Melquiond,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel,2010-01-29,none,,,,public,2012-04-05,Labels in loops are not unrolled,resolved,fixed,,0000000
0001116,Frama-C,Jochen,Virgile Prevosto,normal,trivial,always,Frama-C Nitrogen-20111001,none,Kernel,2012-03-12,none,,,,public,2012-04-02,axiom outside axiomatic tacitly ignored in presence of struct,resolved,fixed,,0000000
0001139,Frama-C,Patrick Baudin,Patrick Baudin,normal,crash,have not tried,,none,Kernel,2012-04-02,none,,,,public,2012-04-02,unrolling labeled loops,resolved,fixed,,0000000
0001135,Frama-C,Patrick Baudin,Virgile Prevosto,normal,major,have not tried,"Frama-C SVN, precise the release id",none,Kernel,2012-03-27,none,,,,public,2012-04-02,unrolling loop statements with labels into there annotations are not handled correctly (in conjunction with -ulevel),resolved,fixed,,0000000
0001126,Frama-C,Philippe Herrmann,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel,2012-03-20,none,,,,public,2012-03-30,AST check failure : problem with generated block-local variables,resolved,fixed,,0000000
0001113,Frama-C,Pierre Karpman,Virgile Prevosto,normal,minor,sometimes,Frama-C Nitrogen-20111001,none,Kernel,2012-03-08,none,,,,public,2012-03-30,Preprocessing code may yield expanded code with undeclared variables,resolved,fixed,,0000000
0001128,Frama-C,Anne Pacalet,Julien Signoles,normal,feature,have not tried,Frama-C Nitrogen-20111001,none,Kernel > Makefile,2012-03-22,none,,,,public,2012-03-29,Install frama-c.top,acknowledged,open,,0000000
0000888,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel,2011-07-25,none,,,,public,2012-03-28,14292: warn for unspecified side-effect that are separated by a function call (csmith),assigned,open,,0000000
0001114,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel,2012-03-10,none,,,,public,2012-03-27,"17514, -unspecified-access and if (*p = (*p < 3)) (csmith)",resolved,fixed,,0000000
0001134,Frama-C,Joe Sapp,Virgile Prevosto,normal,minor,always,Frama-C Nitrogen-20111001,none,Kernel,2012-03-26,none,,,,public,2012-03-26,Crash when #include <complex.h>,assigned,open,,0000000
0001132,Frama-C,Anne Pacalet,Julien Signoles,normal,minor,have not tried,,none,Kernel,2012-03-23,none,,,,public,2012-03-26,-cpp-extra-args option should be a list,resolved,fixed,,0000000
0000929,Frama-C,inti testing,Virgile Prevosto,normal,feature,always,Frama-C Carbon-20110201,none,Kernel,2011-08-18,none,,,,public,2012-03-22,syntax error in value binary assignment,assigned,open,,0000000
0001122,Frama-C,Julien Signoles,Julien Signoles,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Graphical User Interface,2012-03-19,none,,,,public,2012-03-19,Opening consolidation graph crashes when 'dot' is missing,acknowledged,open,,0000000
0001117,Frama-C,Jochen,Philippe Herrmann,normal,tweak,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2012-03-12,none,,,,public,2012-03-14,"addr_eq versus = and <>  in generated axioms access_update, access_update_neq",resolved,open,,0000000
0001119,Frama-C,Jochen,Philippe Herrmann,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2012-03-13,none,,,,public,2012-03-14,couldn't verify series of struct member initializations,assigned,open,,0000000
0000107,Frama-C,Dillon Pariente,Boris Yakobowski,normal,major,always,"Frama-C SVN, precise the release id",none,Plug-in > slicing,2009-05-27,none,,,,public,2012-03-09,Slicer: slicing preserving some undesired function calls,resolved,fixed,,0000000
0001003,Frama-C,Jochen,Claude Marché,normal,tweak,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2011-10-27,none,,,,public,2012-03-06,conditional expression (?:) raises uncaught exception under why-2.30,feedback,reopened,,0000000
0001108,Frama-C,Loïc Correnson,Loïc Correnson,normal,minor,always,,none,Plug-in > wp,2012-02-29,none,,,,public,2012-03-01,Bitwise Operators,resolved,fixed,,0000000
0001098,Frama-C,Pierre-Loïc Garoche,Benjamin Monate,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Documentation,2012-02-17,none,,,,public,2012-02-28,Non working example in the documentation,confirmed,open,,0000000
0001102,Frama-C,Boris Hollas,Benjamin Monate,normal,tweak,N/A,Frama-C Nitrogen-20111001,none,Graphical User Interface,2012-02-21,none,,,,public,2012-02-28,Rename frama-c-gui.config,resolved,fixed,Frama-C Oxygen-2012xx01,0000000
0001104,Frama-C,Jochen,Loïc Correnson,normal,minor,always,Frama-C Nitrogen-20111001,none,Graphical User Interface,2012-02-24,none,,,,public,2012-02-24,value analysis warning disappears from 'Messages' window in gui after 'Reparse' button clicked,assigned,open,,0000000
0001023,Frama-C,Jochen,Virgile Prevosto,normal,text,N/A,Frama-C Nitrogen-20111001,none,Documentation,2011-11-18,none,,,,public,2012-02-23,\valid_range not mentioned in Acsl manual,resolved,fixed,,0000000
0000733,Frama-C,Boris Yakobowski,Boris Yakobowski,normal,major,always,Frama-C Carbon-20110201,none,Plug-in > inout,2011-02-20,none,,,,public,2012-02-23,Invalid results in presence of pseudo-recursive calls in inout and from,acknowledged,open,,0000000
0001103,Frama-C,Anne Pacalet,Virgile Prevosto,normal,feature,have not tried,,none,Kernel,2012-02-22,none,,,,public,2012-02-23,Default @requires property for the [main] function,assigned,open,,0000000
0001081,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,minor,always,Frama-C Nitrogen-20111001,none,Kernel,2012-02-05,none,,,,public,2012-02-22,foo ? (void)x : (signed char)y (csmithreduction),resolved,fixed,,0000000
0001070,Frama-C,Julien Signoles,Virgile Prevosto,normal,feature,N/A,,none,Kernel > configure,2012-01-23,none,,,,public,2012-02-22,Getting  frama-c version through --enable-external,resolved,fixed,,0000000
0001069,Frama-C,Julien Signoles,Virgile Prevosto,normal,minor,N/A,,none,Kernel > configure,2012-01-23,none,,,,public,2012-02-21,Handling error in external plug-in through --enable-external,resolved,fixed,,0000000
0001099,Frama-C,Boris Yakobowski,Virgile Prevosto,low,crash,always,Frama-C Nitrogen-20111001,none,Kernel,2012-02-18,none,,,,public,2012-02-21,Crash when parsing  an incorrect program with pointer to arrays,resolved,fixed,,0000000
0001100,Frama-C,Boris Yakobowski,Boris Yakobowski,low,minor,always,Frama-C Nitrogen-20111001,none,Kernel,2012-02-18,none,,,,public,2012-02-20,Loop unrolling sub-optimal in presence of some labels,resolved,fixed,,0000000
0001073,Frama-C,Anne Pacalet,Virgile Prevosto,normal,major,have not tried,Frama-C Nitrogen-20111001,none,Kernel,2012-01-27,none,,,,public,2012-02-17,Some functions lose their formals after File.create_project_from_visitor,resolved,fixed,,0000000
0001093,Frama-C,Fleckner und Simon Informationstechnik GmbH,Claude Marché,normal,crash,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2012-02-13,none,,,,public,2012-02-14,Passing multi-dimensional arrays via reference fails,assigned,open,,0000000
0000967,Frama-C,Mihaela Sighireanu,Virgile Prevosto,normal,minor,have not tried,Frama-C Carbon-20110201,none,Kernel > ACSL implementation,2011-09-19,none,,,,public,2012-02-09,unbound function \length in annotation,assigned,open,,0000000
0001088,Frama-C,Boris Hollas,Julien Signoles,normal,minor,N/A,Frama-C Nitrogen-20111001,none,Documentation,2012-02-09,none,,,,public,2012-02-09,Plugin-development-guide section 2.1.2,resolved,fixed,,0000000
0001014,Frama-C,Muriel Roger,Julien Signoles,normal,minor,always,Frama-C Nitrogen-20111001,none,Documentation,2011-11-10,none,,,,public,2012-02-09,gui and doc,resolved,fixed,,0000000
0001025,Frama-C,Florent Garnier,Boris Yakobowski,low,minor,always,Frama-C Carbon-20110201,none,Kernel,2011-11-21,none,,,,public,2012-02-08,Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast,resolved,fixed,,0000000
0001083,Frama-C,Sylvain Frédéric Nahas,Philippe Herrmann,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > RTE,2012-02-07,none,,,,public,2012-02-08,RTE does not check for downcast of unsigned integer,resolved,fixed,,0000000
0001082,Frama-C,Anne Pacalet,Julien Signoles,normal,trivial,have not tried,,none,Kernel > Makefile,2012-02-06,none,,,,public,2012-02-07,Bad links in  generated documentation modules.svg,resolved,fixed,,0000000
0001079,Frama-C,Boris Yakobowski,Boris Yakobowski,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > scope,2012-02-03,none,,,,public,2012-02-04,Imprecision of 'Defs' when querying precise location,resolved,fixed,,0000000
0000765,Frama-C,Anne Pacalet,Loïc Correnson,normal,minor,have not tried,,none,Plug-in > wp,2011-03-25,none,,,,public,2012-01-31,Post-state of statement spec,assigned,open,,0000000
0001076,Frama-C,Jochen,Pascal Cuoq,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2012-01-30,none,,,,public,2012-01-31,"volatile" ignored,assigned,open,,0000000
0001074,Frama-C,Boris Yakobowski,Pascal Cuoq,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2012-01-28,none,,,,public,2012-01-30,Imprecise result on almost deterministic program,resolved,fixed,,0000000
0000624,Frama-C,Qirun Zhang,Loïc Correnson,normal,crash,always,Frama-C Boron-20100401,none,Kernel,2010-11-10,none,,,,public,2012-01-30,Logging huge messages makes kernel crashing,acknowledged,open,,0000000
0000989,Frama-C,Anne Pacalet,Julien Signoles,normal,minor,have not tried,,none,Plug-in > syntactic callgraph,2011-10-19,none,,,,public,2012-01-27,Strange dot callgraphs,resolved,fixed,,0000000
0001071,Frama-C,Jochen,Pascal Cuoq,normal,tweak,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2012-01-26,none,,,,public,2012-01-27,relation chains exploited incompletely,resolved,fixed,,0000000
0001072,Frama-C,Julien Signoles,Boris Yakobowski,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2012-01-26,none,,,,public,2012-01-27,evaluation of && and || in term position,resolved,fixed,,0000000
0001067,Frama-C,Jochen,Pascal Cuoq,normal,trivial,N/A,Frama-C Nitrogen-20111001,none,Documentation,2012-01-19,none,,,,public,2012-01-26,suggest to mention option "-value-help" in value analysis manual,resolved,fixed,,0000000
0000252,Frama-C,Kerstin Hartig,Virgile Prevosto,normal,feature,always,Frama-C Beryllium-20090901,none,Plug-in > jessie,2009-09-21,none,,,,public,2012-01-21,type invariants,assigned,open,,0000000
0001066,Frama-C,Jochen,Pascal Cuoq,normal,trivial,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2012-01-19,none,,,,public,2012-01-19,suggest to use "NULL" rather than "&NULL" for null pointer,resolved,fixed,,0000000
0001062,Frama-C,karpulevich,Claude Marché,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2012-01-12,none,,,,public,2012-01-12,Jessie incorrectly handles initialization of static array with {} initialization,assigned,open,,0000000
0001061,Frama-C,karpulevich,Claude Marché,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2012-01-12,none,,,,public,2012-01-12,Jessie incorrectly handles initialization of array,assigned,open,,0000000
0001060,Frama-C,ASSAF,Loïc Correnson,normal,crash,always,"Frama-C SVN, precise the release id",none,Plug-in > wp,2012-01-11,none,,,,public,2012-01-11,WP 0.5 crashes with an Unbound label parameter 'Here',assigned,open,,0000000
0001059,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,major,always,Frama-C Nitrogen-20111001,none,Kernel,2012-01-07,none,,,,public,2012-01-08,Undefined behavior with embedded assignment goes undetected,assigned,open,,0000000
0001056,Frama-C,Dmitry,Virgile Prevosto,normal,crash,always,Frama-C Carbon-20110201,none,Kernel > ACSL implementation,2011-12-21,none,,,,public,2012-01-06,Frama-c fails when Starting Jessie Translation,resolved,fixed,,0000000
0001027,Frama-C,Julien Signoles,Virgile Prevosto,normal,crash,always,Frama-C Nitrogen-20111001,none,Kernel > ACSL implementation,2011-11-25,none,,,,public,2012-01-06,incompatible types for a correct spec,resolved,fixed,,0000000
0001058,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,have not tried,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2012-01-04,none,,,,public,2012-01-04,Jessie incorrectly handles labels,assigned,open,,0000000
0001050,Frama-C,ASSAF,Virgile Prevosto,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > aoraï,2011-12-14,none,,,,public,2012-01-04,Sequence number generated by aorai is incorrect,resolved,fixed,,0000000
0001051,Frama-C,Jochen,Loïc Correnson,normal,text,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2011-12-15,none,,,,public,2011-12-16,"suspicious axiomatization of included,zrange,zunion in .sx file",assigned,open,,0000000
0001047,Frama-C,Chernikova Tatiana,Claude Marché,normal,major,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-12-12,none,,,,public,2011-12-12,labels defined before loops and used after loops are not correctly translated in jessie,assigned,open,,0000000
0001046,Frama-C,Mikhail,Claude Marché,normal,minor,have not tried,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-12-11,none,,,,public,2011-12-11,Wrong sequence of lemmas,assigned,open,,0000000
0001044,Frama-C,Pascal Cuoq,Pascal Cuoq,normal,feature,always,,none,Plug-in > value analysis,2011-12-10,none,,,,public,2011-12-11,Smarter access to array of struct of array,assigned,open,,0000000
0001038,Frama-C,Jochen,Loïc Correnson,normal,text,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2011-12-05,none,,,,public,2011-12-05,lemma tacitly ignored in absense of C code,assigned,open,,0000000
0001028,Frama-C,Jochen,Loïc Correnson,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2011-11-28,none,,,,public,2011-12-01,unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool?,acknowledged,open,,0000000
0001037,Frama-C,Jochen,Loïc Correnson,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2011-12-01,none,,,,public,2011-12-01,undefined (or built-in?) predicate "global" in proof obligation,assigned,open,,0000000
0001033,Frama-C,jessie_user,Claude Marché,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2011-11-29,none,,,,public,2011-11-29,Feature request (Jessie): \fresh (and \separated),assigned,open,,0000000
0001032,Frama-C,jessie_user,Claude Marché,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2011-11-29,none,,,,public,2011-11-29,"assigns nothing is not possible to proof, if malloc is not in a same function",assigned,open,,0000000
0000997,Frama-C,Boris Yakobowski,Boris Yakobowski,normal,minor,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2011-10-23,none,,,,public,2011-11-21,Warnings in presence of Top floats,resolved,fixed,,0000000
0001021,Frama-C,Patrick Baudin,Boris Yakobowski,normal,minor,have not tried,Frama-C Nitrogen-20111001,none,Graphical User Interface,2011-11-18,none,,,,public,2011-11-18,request for pretty printing only one property by lines,resolved,fixed,,0000000
0001022,Frama-C,Jochen,Virgile Prevosto,normal,text,N/A,Frama-C Nitrogen-20111001,none,Documentation,2011-11-18,none,,,,public,2011-11-18,suggest to explain semantics of missing loop assigns clause in Acsl manual,assigned,open,,0000000
0001019,Frama-C,Jochen,Virgile Prevosto,normal,minor,always,Frama-C Nitrogen-20111001,none,Kernel > ACSL implementation,2011-11-16,none,,,,public,2011-11-16,"#defined variable unrecognized in assigns, except in parentheses",resolved,no change required,,0000000
0001008,Frama-C,Jochen,Claude Marché,normal,feature,N/A,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2011-11-03,none,,,,public,2011-11-16,suggest to supply lower-bound for constant_too_large_2147483647 to Simplify,assigned,open,,0000000
0001013,Frama-C,Boris Yakobowski,Boris Yakobowski,normal,crash,always,Frama-C Nitrogen-20111001,none,Kernel,2011-11-10,none,,,,public,2011-11-14,Crash when casting something to type void,resolved,fixed,,0000000
0001017,Frama-C,Jochen,Virgile Prevosto,normal,feature,always,Frama-C Nitrogen-20111001,none,Kernel > ACSL implementation,2011-11-10,none,,,,public,2011-11-14,suggest to warn about ensures clauses containing only \old variables,assigned,open,,0000000
0001007,Frama-C,Jochen,Virgile Prevosto,normal,major,always,Frama-C Nitrogen-20111001,none,Kernel > ACSL implementation,2011-11-03,none,,,,public,2011-11-10,wrong proof obligation generated for loop initialization [under why-2.30],assigned,open,,0000000
0001009,Frama-C,Virgile Prevosto,Virgile Prevosto,normal,minor,always,"Frama-C SVN, precise the release id",none,Kernel > ACSL implementation,2011-11-04,none,,,,public,2011-11-09,code annotation placed above a local declaration are not correctly handled,resolved,fixed,,0000000
0001006,Frama-C,Boris Yakobowski,Virgile Prevosto,low,minor,always,Frama-C Nitrogen-20111001,none,Kernel,2011-11-02,none,,,,public,2011-11-07,Kernel should desugar "complete behaviors",resolved,fixed,,0000000
0001002,Frama-C,Jochen,Claude Marché,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2011-10-27,none,,,,public,2011-11-07,weak feature request for \separated under why-2.30,assigned,open,,0000000
0001011,Frama-C,Jochen,Loïc Correnson,normal,feature,always,Frama-C Nitrogen-20111001,none,Plug-in > wp,2011-11-04,none,,,,public,2011-11-04,"suggest to provide FILE,LINE references for proof obligations in WP cmd-line output",assigned,open,,0000000
0001010,Frama-C,Jochen,Loïc Correnson,normal,feature,N/A,Frama-C Nitrogen-20111001,none,Documentation,2011-11-04,none,,,,public,2011-11-04,"warn on stderr about current restrictions, and list them in WP manual",assigned,open,,0000000
0000679,Frama-C,Patrick Baudin,Anne Pacalet,normal,crash,have not tried,,none,Plug-in > slicing,2011-01-19,none,,,,public,2011-11-04,"untypable ACSL in a sliced program containing \at(p,label) when the label was removed",resolved,fixed,,0000000
0000993,Frama-C,Boris Yakobowski,Boris Yakobowski,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > functional dependencies,2011-10-20,none,,,,public,2011-11-04,Incorrect dependencies in presence of declared functions,resolved,fixed,,0000000
0001005,Frama-C,Jochen,Virgile Prevosto,normal,crash,always,Frama-C Nitrogen-20111001,none,Kernel,2011-10-28,none,,,,public,2011-10-31,defining two axioms with same name causes kernel crash,resolved,fixed,,0000000
0001004,Frama-C,Boris Hollas,Claude Marché,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > jessie,2011-10-27,none,,,,public,2011-10-28,Jessie reports syntax error in .mlw file,resolved,fixed,,0000000
0000999,Frama-C,Boris Yakobowski,Virgile Prevosto,normal,minor,always,Frama-C Nitrogen-20111001,none,Kernel,2011-10-24,none,,,,public,2011-10-27,Missing or misleading warnings when merging two functions,resolved,fixed,,0000000
0001001,Frama-C,Boris Yakobowski,Pascal Cuoq,normal,major,always,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2011-10-27,none,,,,public,2011-10-27,Invalid handling of shift of pointer address,resolved,fixed,,0000000
0001000,Frama-C,Boris Yakobowski,Boris Yakobowski,normal,crash,unable to reproduce,Frama-C Nitrogen-20111001,none,Plug-in > value analysis,2011-10-25,none,,,,public,2011-10-26,Evaluation in the logic can cause crashes,resolved,fixed,,0000000
0000990,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,crash,always,Frama-C Nitrogen-20111001,none,Kernel,2011-10-19,none,,,,public,2011-10-20,Crash with multiple incompatible declarations,resolved,fixed,,0000000
0000992,Frama-C,Anne Pacalet,Loïc Correnson,high,major,have not tried,,none,Plug-in > wp,2011-10-20,none,,,,public,2011-10-20,Wrong WP computation when calling a function with behaviors (assigns problem ?),assigned,open,,0000000
0000672,Frama-C,Boris Yakobowski,Virgile Prevosto,normal,crash,always,Frama-C Carbon-20101202-beta2,none,Kernel,2011-01-17,none,,,,public,2011-10-20,Incorrect cil merging in presence of ACSL annotations,resolved,fixed,,0000000
0000991,Frama-C,Jochen,Julien Signoles,normal,text,N/A,Frama-C Nitrogen-20111001,none,Documentation,2011-10-20,none,,,,public,2011-10-20,outdated manual titles,acknowledged,open,,0000000
0000986,Frama-C,Anne Pacalet,Loïc Correnson,normal,minor,have not tried,,none,Plug-in > wp,2011-10-17,none,,,,public,2011-10-17,Wrong [\valid(p)] outside the pointed variable scope,resolved,fixed,,0000000
0000945,Frama-C,Pascal Cuoq,Pascal Cuoq,low,minor,have not tried,Frama-C Carbon-20110201,none,Plug-in > value analysis,2011-09-01,none,,,,public,2011-10-10,Should warn for overlapping lv=lv; assignments,confirmed,open,,0000000
0000980,Frama-C,Anne Pacalet,Virgile Prevosto,normal,feature,have not tried,,none,Kernel > ACSL implementation,2011-10-06,none,,,,public,2011-10-06,Functional expression in assigns properties,assigned,open,,0000000
0000936,Frama-C,Boris Yakobowski,Virgile Prevosto,normal,minor,always,Frama-C Carbon-20110201,none,Kernel,2011-08-24,none,,,,public,2011-09-14,Cil does not reject incorrect initializers,acknowledged,reopened,,0000000
0000912,Frama-C,Boris Yakobowski,Pascal Cuoq,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > functional dependencies,2011-08-05,none,,,,public,2011-09-07,Functional dependencies are incorrect in presence of value analysis builtins,assigned,open,,0000000
0000932,Frama-C,Julien Signoles,Julien Signoles,low,tweak,always,Frama-C Carbon-20110201,none,Kernel,2011-08-23,none,,,,public,2011-08-23,Journalisation of dynamic functions using abstract types does not work,confirmed,open,,0000000
0000923,Frama-C,jessie_user,Claude Marché,normal,major,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-08-12,none,,,,public,2011-08-12,"Jessie Plugin returns an error. Code with struct-statement, cannot be compiled.",assigned,open,,0000000
0000922,Frama-C,jessie_user,Claude Marché,normal,major,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-08-12,none,,,,public,2011-08-12,"Jessie Plugin returns an error. Code with struct-statement, cannot be compiled in a function by call by value.",assigned,open,,0000000
0000903,Frama-C,Patrick Baudin,Loïc Correnson,low,minor,have not tried,Frama-C Carbon-20110201,none,Plug-in > wp,2011-07-29,none,,,,public,2011-07-29,Support of \block_length,assigned,open,,0000000
0000895,Frama-C,Patrick Baudin,Loïc Correnson,normal,minor,always,"Frama-C SVN, precise the release id",none,Plug-in > wp,2011-07-28,none,,,,public,2011-07-28,Proof obligations of lemma properties,assigned,open,,0000000
0000745,Frama-C,Julien Signoles,Virgile Prevosto,low,minor,always,,none,Kernel > ACSL implementation,2011-03-04,none,,,,public,2011-07-26,Very big integer constants,assigned,open,,0000000
0000794,Frama-C,Patrick Baudin,Loïc Correnson,normal,feature,have not tried,"Frama-C SVN, precise the release id",none,Plug-in > wp,2011-04-14,none,,,,public,2011-07-04,initial value of strings,assigned,open,,0000000
0000875,Frama-C,Jochen,Pascal Cuoq,normal,feature,always,Frama-C Carbon-20110201,none,Plug-in > value analysis,2011-06-29,none,,,,public,2011-07-01,"suggest to issue a warning on (<)-comparisons between pointers, unless both are non-null",feedback,open,,0000000
0000873,Frama-C,David Delmas,Pascal Cuoq,normal,feature,always,Frama-C Carbon-20110201,none,Plug-in > value analysis,2011-06-28,none,,,,public,2011-06-28,Alignment of global charachter arrays,assigned,open,,0000000
0000856,Frama-C,Kerstin Hartig,Pascal Cuoq,normal,crash,always,Frama-C Carbon-20110201,none,Plug-in > value analysis,2011-06-07,none,,,,public,2011-06-14,non-constant size of 2-dim array leads to crash (some similarities to issue #852),feedback,open,,0000000
0000862,Frama-C,ckunz,Virgile Prevosto,normal,tweak,always,Frama-C Carbon-20110201,none,Kernel > ACSL implementation,2011-06-10,none,,,,public,2011-06-10,ACSL parser + pretty-printer,assigned,open,,0000000
0000852,Frama-C,Jochen,Virgile Prevosto,normal,minor,always,Frama-C Carbon-20110201,none,Kernel,2011-06-01,none,,,,public,2011-06-01,non-constant size of 2-dim array causes error in recursive procedure,assigned,open,,0000000
0000846,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-05-30,none,,,,public,2011-05-30,array access in "decreases"-clause causes "Unexpected internal region in logic",assigned,open,,0000000
0000816,Frama-C,Loïc Correnson,Loïc Correnson,normal,feature,N/A,,none,Plug-in > wp,2011-05-10,none,,,,public,2011-05-27,ACSL builtins,assigned,open,,0000000
0000840,Frama-C,Jochen,Virgile Prevosto,normal,text,always,Frama-C Carbon-20110201,none,Kernel,2011-05-27,none,,,,public,2011-05-27,syntax error message refers to (true error line + 5 lines),assigned,open,,0000000
0000834,Frama-C,Pierre Roux,Claude Marché,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-05-24,none,,,,public,2011-05-24,Computation of regions for axioms in axiomatics,assigned,open,,0000000
0000829,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-05-18,none,,,,public,2011-05-24,alias between int* and uint* handled incorrectly,assigned,open,,0000000
0000251,Frama-C,Pascal Cuoq,Pascal Cuoq,immediate,minor,always,Frama-C Beryllium-20090901,none,Plug-in > value analysis,2009-09-20,none,,,,public,2011-05-16,wrong origin displayed in the GUI,assigned,open,,0000000
0000772,Frama-C,Virgile Prevosto,Pascal Cuoq,low,tweak,always,"Frama-C SVN, precise the release id",none,Plug-in > value analysis,2011-03-30,none,,,,public,2011-05-14,Incorrect location of warnings emitted by value analysis,assigned,open,,0000000
0000813,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-05-09,none,,,,public,2011-05-09,struct dereferencing causes uncaught exception,assigned,open,,0000000
0000811,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Carbon-20110201,none,Plug-in > jessie,2011-05-02,none,,,,public,2011-05-06,double struct dereferencing causes unbound variable error,assigned,open,,0000000
0000750,Frama-C,Anne Pacalet,Virgile Prevosto,normal,feature,always,,none,Kernel > ACSL implementation,2011-03-08,none,,,,public,2011-03-11,Several [invariant] at a program point,acknowledged,open,,0000000
0000735,Frama-C,Virgile Prevosto,Virgile Prevosto,normal,minor,always,Frama-C Carbon-20110201,none,Kernel,2011-02-22,none,,,,public,2011-02-22,Pretty-printer and generated global annotations,assigned,open,,0000000
0000734,Frama-C,Julien Signoles,Loïc Correnson,normal,tweak,unable to reproduce,Frama-C Carbon-20110201,none,Kernel,2011-02-21,none,,,,public,2011-02-21,Command.command_generic may raise Sys_error,assigned,open,,0000000
0000722,Frama-C,Patrick Baudin,Virgile Prevosto,normal,minor,always,Frama-C Carbon-20110201,none,Kernel > ACSL implementation,2011-02-14,none,,,,public,2011-02-14,bitwise operator,assigned,open,,0000000
0000713,Frama-C,Boris Hollas,Virgile Prevosto,normal,feature,always,Frama-C Carbon-20101202-beta2,none,Kernel > ACSL implementation,2011-02-10,none,,,,public,2011-02-10,Any number of ";" should be allowed in specifications,assigned,open,,0000000
0000712,Frama-C,Boris Hollas,Claude Marché,normal,major,always,Frama-C Carbon-20101202-beta2,none,Plug-in > jessie,2011-02-10,none,,,,public,2011-02-10,Validity of valid pointer to struct member cannot be verified,assigned,open,,0000000
0000667,Frama-C,David MENTRE,Claude Marché,normal,crash,always,Frama-C Boron-20100401,none,Plug-in > jessie,2011-01-11,none,,,,public,2011-01-25,/usr/share/frama-c/libc/stdio.h:107:[jessie] failure: Unexpected exception.,assigned,open,,0000000
0000685,Frama-C,Virgile Prevosto,Virgile Prevosto,normal,feature,always,Frama-C Carbon-20101202-beta2,none,Kernel,2011-01-24,none,,,,public,2011-01-24,CIL's added return masks issues,assigned,open,,0000000
0000676,Frama-C,Pascal Cuoq,Virgile Prevosto,normal,minor,always,Frama-C Carbon-20101202-beta2,none,Kernel,2011-01-18,none,,,,public,2011-01-18,Strange AST produced with unspecified side-effects involve function calls in expressions,assigned,open,,0000000
0000670,Frama-C,lukaszc,Claude Marché,normal,minor,always,Frama-C Carbon-20101202-beta2,none,Plug-in > jessie,2011-01-12,none,,,,public,2011-01-12,In certain circumstances Jessie cannot analyse files that it generates,assigned,open,,0000000
0000658,Frama-C,evdenis,Claude Marché,normal,crash,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-12-29,none,,,,public,2010-12-29,loop assigns crash,assigned,open,,0000000
0000654,Frama-C,lost,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-12-25,none,,,,public,2010-12-25,Incorrect translation (Unbound variable),assigned,open,,0000000
0000653,Frama-C,lost,Claude Marché,normal,crash,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-12-25,none,,,,public,2010-12-25,jessie's Unexpected failure,assigned,open,,0000000
0000652,Frama-C,evdenis,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-12-24,none,,,,public,2010-12-24,pointer arithmetic,assigned,open,,0000000
0000651,Frama-C,evdenis,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-12-24,none,,,,public,2010-12-24,array id "shift",assigned,open,,0000000
0000643,Frama-C,Nikita,Virgile Prevosto,normal,minor,always,Frama-C Boron-20100401,none,Kernel > ACSL implementation,2010-12-17,none,,,,public,2010-12-18,Incorrect parsing of complex lemma,assigned,open,,0000000
0000636,Frama-C,helloworld,Claude Marché,normal,crash,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-12-09,none,,,,public,2010-12-16,Unexpected exception in block_length,feedback,unable to reproduce,,0000000
0000601,Frama-C,Jochen,Virgile Prevosto,normal,feature,always,Frama-C Boron-20100401,none,Kernel > ACSL implementation,2010-10-12,none,,,,public,2010-12-16,no multiple assert-clauses accepted in /*@...*/-style comment,assigned,open,,0000000
0000605,Frama-C,Boris Hollas,Virgile Prevosto,normal,minor,always,Frama-C Boron-20100401,none,Kernel > ACSL implementation,2010-10-13,none,,,,public,2010-12-16,Empty specification causes syntax error,assigned,open,,0000000
0000632,Frama-C,Jochen,Claude Marché,normal,feature,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-11-29,none,,,,public,2010-11-29,Suggest to rename user identifiers to avoid name clashes in ..._why.sx files,assigned,open,,0000000
0000617,Frama-C,Julien Narboux,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-10-26,none,,,,public,2010-11-17,assigns nothing ?,confirmed,open,,0000000
0000629,Frama-C,Nikita,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-11-16,none,,,,public,2010-11-17,Incorrect processing of "type var[]" constructions,assigned,open,,0000000
0000628,Frama-C,Jens G,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-11-13,none,,,,public,2010-11-13,Frama-C/Jessie does not recognize the length of array in struct,assigned,open,,0000000
0000615,Frama-C,Jochen,Claude Marché,normal,major,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-10-22,none,,,,public,2010-10-22,separately verified files show code-bug when linked together,assigned,open,,0000000
0000614,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-10-22,none,,,,public,2010-10-22,"\valid(&aaa)" unprovable for global variable aaa - missing antecedens in proof obligation?,assigned,open,,0000000
0000593,Frama-C,Maria,Virgile Prevosto,normal,minor,always,,none,Kernel,2010-09-30,none,,,,public,2010-10-01,Parse error when using a wide string literal to initialize uint16 array,confirmed,open,,0000000
0000590,Frama-C,Alexey Khoroshilov,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-09-22,none,,,,public,2010-09-22,Jessie plugin does not support logic label Post in ensures clause,assigned,open,,0000000
0000575,Frama-C,Patrick Baudin,Virgile Prevosto,normal,minor,have not tried,Frama-C Boron-20100401,none,Kernel > ACSL implementation,2010-08-25,none,,,,public,2010-08-25,set of set,assigned,open,,0000000
0000544,Frama-C,Tzu-hsiang Chien,Claude Marché,normal,feature,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-07-17,none,,,,public,2010-07-17,Enhancement on assigns annotation and the name of proof obligation,assigned,open,,0000000
0000102,Frama-C,Dillon Pariente,Claude Marché,normal,major,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2009-05-27,none,,,,public,2010-07-13,Jessie: struct field's validity,confirmed,open,,0000000
0000518,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-06-22,none,,,,public,2010-06-22,Loop assigns are not taken into account when proving a safety PO,assigned,open,,0000000
0000502,Frama-C,Pascal Cuoq,Claude Marché,low,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-06-09,none,,,,public,2010-06-13,Unbound label in Jessie-generated Why file when using logic function in assigns clause,assigned,open,,0000000
0000289,Frama-C,Sylvain Boulme,Virgile Prevosto,normal,major,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2009-10-19,none,,,,public,2010-06-09,unsoundness of Jessie with respect to expression evaluation of ANSI-C,acknowledged,open,,0000000
0000485,Frama-C,Boris Hollas,Claude Marché,normal,feature,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2010-05-18,none,,,,public,2010-05-18,Code containing consts should be verifiable,assigned,open,,0000000
0000480,Frama-C,tomahawkins,Claude Marché,normal,crash,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-05-12,none,,,,public,2010-05-12,volatile annotation breaks type checker,assigned,open,,0000000
0000444,Frama-C,Claude Marché,Virgile Prevosto,normal,minor,always,Frama-C Beryllium-20090902,none,Kernel > ACSL implementation,2010-04-08,none,,,,public,2010-05-11,predicate definitions should be of type prop,feedback,open,,0000000
0000249,Frama-C,Omar Chebaro,Julien Signoles,normal,minor,N/A,Frama-C Beryllium-20090601-beta1,none,Kernel,2009-09-17,none,,,,public,2010-04-26,dynamically link a library,confirmed,open,,0000000
0000456,Frama-C,Frédéric Gava,Claude Marché,normal,minor,always,Frama-C Boron-20100401,none,Plug-in > jessie,2010-04-23,none,,,,public,2010-04-23,Lack of parameter generation,assigned,open,,0000000
0000433,Frama-C,Jochen,Virgile Prevosto,normal,tweak,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2010-03-22,none,,,,public,2010-03-23,different translation of casted constants in program-code and in assertion,assigned,open,,0000000
0000424,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2010-03-08,none,,,,public,2010-03-22,Uncaught exception: Failure("Unexpected internal region in logic"),assigned,open,,0000000
0000416,Frama-C,Jochen,Claude Marché,normal,minor,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2010-02-22,none,,,,public,2010-02-22,local array decl with non-constant size causes Why error,assigned,open,,0000000
0000072,Frama-C,François Bobot,Claude Marché,normal,minor,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2009-04-30,none,,,,public,2010-02-12,The specifications of statements are not translated,assigned,open,,0000000
0000079,Frama-C,Boris Hollas,Virgile Prevosto,normal,feature,always,Frama-C Lithium-20081201,none,Kernel > ACSL implementation,2009-05-11,none,,,,public,2010-02-05,Better support of //@ style,assigned,open,,0000000
0000387,Frama-C,Sylvie Boldo,Virgile Prevosto,normal,feature,always,"Frama-C SVN, precise the release id",none,Kernel > ACSL implementation,2010-02-01,none,,,,public,2010-02-05,ghost integer ?,assigned,open,,0000000
0000336,Frama-C,Dillon Pariente,Claude Marché,normal,major,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2009-11-20,none,,,,public,2010-01-22,cast between homogenous struct and array,assigned,open,,0000000
0000379,Frama-C,Kerstin Hartig,Claude Marché,normal,crash,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2010-01-21,none,,,,public,2010-01-21,\separated,assigned,open,,0000000
0000373,Frama-C,Guillaume Melquiond,Claude Marché,normal,major,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2010-01-14,none,,,,public,2010-01-14,Global invariants are not verified,assigned,open,,0000000
0000348,Frama-C,Boris Hollas,Claude Marché,normal,major,always,Frama-C Beryllium-20090901,none,Plug-in > jessie,2009-12-03,none,,,,public,2009-12-03,Arithmetic safety of bitwise operators cannot be verified,assigned,open,,0000000
0000039,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-11-24,Frama-C/Jessie: memory set problem,confirmed,open,,0000000
0000335,Frama-C,Nicolas Rousset,Claude Marché,normal,minor,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2009-11-20,none,,,,public,2009-11-20,Unbound reference raised by Why,assigned,open,,0000000
0000328,Frama-C,Nicolas Rousset,Claude Marché,normal,major,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2009-11-12,none,,,,public,2009-11-13,assertion failed in Jessie with bitfields inside union,assigned,open,,0000000
0000291,Frama-C,Sylvain Boulme,Claude Marché,normal,minor,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2009-10-20,none,,,,public,2009-10-20,Unbound variable raised by why in presence of an unsafe cast,assigned,open,,0000000
0000040,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-10-15,Frama-C/Jessie: typing error,confirmed,open,,0000000
0000261,Frama-C,Jonathan-Christofer Demay,Virgile Prevosto,normal,minor,always,Frama-C Beryllium-20090901,none,Kernel,2009-10-01,none,,,,public,2009-10-01,Frama-C fails to parse a file,acknowledged,open,,0000000
0000256,Frama-C,j.crown,Claude Marché,normal,minor,always,Frama-C Beryllium-20090902,none,Plug-in > jessie,2009-09-25,none,,,,public,2009-09-25,array range in requires predicate,assigned,open,,0000000
0000025,Frama-C,Virgile Prevosto,Virgile Prevosto,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-09-21,type invariants,acknowledged,open,,0000000
0000239,Frama-C,Christoph,Loïc Correnson,normal,minor,always,Frama-C Beryllium-20090901,none,Plug-in > jessie,2009-09-11,none,,,,public,2009-09-14,internal error when analyzing max.h,assigned,open,,0000000
0000215,Frama-C,Nicolas Stouls,Claude Marché,normal,minor,always,"Frama-C SVN, precise the release id",none,Plug-in > jessie,2009-08-24,none,,,,public,2009-08-25,Mise en hypothèse de la précondition d'une opération appelée,assigned,open,,0000000
0000185,Frama-C,lukaszc,Claude Marché,normal,major,always,Frama-C Beryllium-20090601-beta1,none,Plug-in > jessie,2009-07-14,none,,,,public,2009-07-17,Frama-C cannot process properly arrays of structures,assigned,open,,0000000
0000178,Frama-C,Fabrice Derepas,Claude Marché,normal,minor,always,Frama-C Beryllium-20090601-beta1,none,Plug-in > jessie,2009-07-09,none,,,,public,2009-07-09,type error in generated why file,confirmed,open,,0000000
0000092,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-05-20,none,,,,public,2009-06-19,Why error with logic functions returning a pointer,assigned,reopened,,0000000
0000042,Frama-C,Virgile Prevosto,Claude Marché,normal,feature,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-06-17,Default invariant should be inferred for loops,assigned,open,,0000000
0000031,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-06-17,Why- error :-jessie-no-regions and assigns does not work,acknowledged,open,,0000000
0000032,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-04-10,Internal error with assign specification on bi-dimensional arrays,assigned,open,,0000000
0000038,Frama-C,Virgile Prevosto,Claude Marché,normal,minor,always,Frama-C Lithium-20081201,none,Plug-in > jessie,2009-04-07,none,,,,public,2009-04-10,Jessie crashes on simple program without annotations,assigned,open,,0000000