Frama-C Bug Tracking System

Reporter: Monitored By: Assigned To: Category: Severity: Resolution: Profile:
any any any any any any any
Status: Hide Status: Product Version: Fixed in Version: Target Version: Priority:
any none any any any any
Show: View Status: Show Sticky Issues: Changed(hrs): Use Date Filters: Relationships:
50 any No 6 No any
Platform: OS: OS Version: Tags:
any any any
Note By: any Sort by: Updated Descending  
Match Type: All Conditions  
- Search  Advanced Filters ]

Viewing Issues (101 - 150 / 1211)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 7 8 9 10 11 ...  Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  0002370    Kernel > ACSL implementationfeatureassigned (virgile)2018-03-08Expose ACSL annotations through host language pragmas
  00023698   Plug-in > E-ACSLminoracknowledged (signoles)2018-02-23e-acsl-gcc failes on macOS
  000236711 Plug-in > clangminorassigned (virgile)2018-02-12C-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}'
  0002366 1 Plug-in > clangminorassigned (virgile)2018-02-12loop assigns clause ginored under strange circumstances
  0002365 1 Plug-in > clangminorassigned (virgile)2018-02-12user-defined type not accepted after builtin type in quantifier chain
   0002364 1 Plug-in > clangfeatureassigned (virgile)2018-02-12Frama-clang reports overloading ambiguity where Frama-C doesn't
  0002363 1 Plug-in > clangminorassigned (virgile)2018-02-12variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless
  0002362 1 Plug-in > clangminorassigned (virgile)2018-02-12"let" in predicate body unrecognized
  0002361 1 Plug-in > clangcrashassigned (virgile)2018-02-12"assigns" in statement contract causes abort or crash
  0002360 1 Plug-in > clangcrashassigned (virgile)2018-02-12"Here" as predicate label in statement contract causes Segmentation fault
  0002359 1 Plug-in > clangfeatureassigned (virgile)2018-02-12Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't
  000235621 Plug-in > clangfeatureconfirmed (virgile)2018-02-09insufficient contracts for generated constructors and assignment operator(s)
  000235721 Plug-in > clangminorassigned (virgile)2018-02-08can't handle lemma with 3 labels
  0002358 1 Plug-in > clangfeatureassigned (virgile)2018-02-08predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang
  000235022 Plug-in > clangminoracknowledged (virgile)2018-02-08kernel warns about invalid implicit conversion
  000235511 Plug-in > clangminorassigned (virgile)2018-02-05Alt-Ergo reports about " bool and int cannot be unified"
  000148411 Plug-in > wpminorassigned (correnson)2018-02-05ill-typed alt-ergo proof obligation
  000234043 Plug-in > wpminoracknowledged (correnson)2018-02-02Coq translation of predicate name changes when additional files are processed by Frama-C
  000235315 Plug-in > wpminorassigned (correnson)2018-02-01alt-ergo goals generated directly / via why3 differ in provability
  0002352 1 Plug-in > clangcrashassigned (virgile)2018-01-31Frama-Clang crashes on error in contract
  000235111 Plug-in > clangminorassigned (virgile)2018-01-31no diagnostics on wrong keyword
  000234912 Plug-in > clangfeatureconfirmed (virgile)2018-01-31warning from kernel about exceptions
  00023431   Documentationminorclosed (signoles)2018-01-31BTS does not allow do select "Frama-C 16 Sulfur" as "Product Version"
  000234812 Plug-in > clangminorassigned (virgile)2018-01-30unknown variable in contract is not treated as an error
  000234713 Plug-in > clangcrashassigned (virgile)2018-01-23direct initialisation of bool by nullptr
  0002346 2 Plug-in > clangminorassigned (virgile)2018-01-19C++11 delegating constructor not supported
  0002345 1 Plug-in > clangminorassigned (virgile)2018-01-19range based for loop from C++11 not supported
  000234221 Plug-in > clangminorconfirmed (virgile)2018-01-18std::bad_alloc not supported
  00014312   Graphical User Interfacefeatureconfirmed (maroneze)2018-01-12How to use the "Callers ..." context menu item
  000234121 Plug-in > frommajorclosed (yakobowski)2018-01-11Incorrect dependency assignment using arraay inside for loop
  000231432 Plug-in > RTEmajorclosed (signoles)2017-12-29Incorrect overflow and cast assertions for bitfields
  00023353   Kernelminorclosed (maroneze)2017-12-29opam upgrade/update failed to update frama-c
  00023371   Documentationtextassigned (correnson)2017-12-29explain wp's syntactic restrictions on "inductive" definitions
  00009454   Plug-in > Evaminorassigned (maroneze)2017-12-17Should warn for overlapping lv=lv; assignments
  000225411 Plug-in > Evaminorassigned (maroneze)2017-12-17Option "-lib-entry" results misses possible values of function pointers
  00022594   Plug-in > Evatextclosed (yakobowski)2017-12-17suggest to provide and document a unique warning string to grep for in value-analysis output files
  000225641 Plug-in > Evaminorassigned (maroneze)2017-12-17"pointer comparison" warning emitted for "p==NULL"
  00021801   Plug-in > wpcrashassigned (correnson)2017-12-17Crash on loop with global assigns and per-behavior assigns
  00021668   Plug-in > Evaminorassigned (buhler)2017-12-17Substraction results in unknown values
  000230621 Kernelminorassigned (maroneze)2017-12-17Support for flexible array members
  000233611 Plug-in > wptweakassigned (correnson)2017-12-08suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
  000230211 Plug-in > slicingmajorclosed (Nikolai_Kosmatov)2017-12-06the return statement of a called function was wrongly removed
  000232242 Kernelcrashclosed (virgile)2017-12-06repeated predicate definitions in separate file cause crash
  000215152 Kernel > ACSL implementationcrashclosed (virgile)2017-12-06predicate overloading causes crash when multiple files are given to wp
  000230412 Plug-in > E-ACSLmajorclosed (signoles)2017-12-06E-ACSL: compilation fail: generated functions doesn't have static inline attributes
  000230312 Plug-in > E-ACSLmajorclosed (signoles)2017-12-06E-ACSL generates functions definitions without argument-names
  000229721 Kernelminorclosed (maroneze)2017-12-06syntax error before loop contract reported after loop contract
  000233111 Kernel > Makefileminorclosed (bobot)2017-12-06opam installation of frama-c-base fails
  00022705   Graphical User Interfacemajorclosed (maroneze)2017-12-06Command "Show callgraph" fails.
  00023285   Plug-in > E-ACSLcrashclosed (kvorobyov)2017-12-06compilation fails on i386 with gcc-7
  [ First Prev 1 2 3 4 5 6 7 8 9 10 11 ...  Next Last ]

newfeedbackacknowledgedconfirmedassignedresolvedclosed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker