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 closed (And Above) any any any any
Show: View Status: Show Sticky Issues: Changed(hrs): Use Date Filters: Relationships:
50 any Yes 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 (1 - 50 / 279)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev 1 2 3 4 5 6 Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  0002412101 Plug-in > E-ACSLcrashconfirmed (signoles)2018-12-17E-ACSL crash with RTE generated assertion with booleans
  0002419    Plug-in > RTEminorconfirmed (signoles)2018-12-17Missing cast in code generated by RTE
  0002418    Documentation > manualstrivialnew2018-12-14Outdated -rte-all option in RTE manual
  000241741 Plug-in > E-ACSLmajorconfirmed (signoles)2018-12-12Invalid label with spaghetti code and E-ACSL full mmodel
  00024163   Plug-in > E-ACSLminoracknowledged (signoles)2018-12-11missing E-ACSL code, control flow graph, function pointer
  0002414    Plug-in > wpmajorassigned (correnson)2018-12-07Mk_addr not defined in Memory.v (coqwp via why3ide)
  000241321 Plug-in > E-ACSLmajorconfirmed (signoles)2018-12-06missing E-ACSL code when ignoring asm annotation
  0002389162 Plug-in > wpcrashassigned (correnson)2018-12-06Failure to detect qed libraries when running wp
  0001648    Kernelmajorassigned (maroneze)2018-11-30Wrong specification for standard library function memmove
  0001809    Kerneltweakassigned (maroneze)2018-11-30Frama-C should not have unimplemented headers
  0002378    ptestsminorassigned (bobot)2018-11-30Bytecode only compilation fails when linking to stdlib
  000240941 Plug-in > wpcrashconfirmed (correnson)2018-11-30crash
  000240711 Plug-in > wpmajorassigned (correnson)2018-10-31contracts about memory mapped I/O through volatile memory locations
  000240431 Plug-in > wpminorassigned (correnson)2018-10-09Shape of VC depends on selection of properties
  00024023   Plug-in > clangblockassigned (virgile)2018-10-03frama-clang fails to compile
  0002310 1 Plug-in > E-ACSLminorassigned (fmaurica)2018-10-02Incorrect handling of \initialized when initialized struct is passed to a function by value
  000240142 Plug-in > wpmajoracknowledged (correnson)2018-10-02Newer releases of FramaC produce apparent WP plug-in bug
  00023952   Plug-in > clangminorassigned (virgile)2018-09-07const fields in constructors
  000229021 Plug-in > wpminorassigned (correnson)2018-09-06incomplete loading of saved state when using WP?
  00023971   Kernel > ACSL implementationfeatureassigned (virgile)2018-08-27Model Variables in Frama C
  0002396    Plug-in > clangminorassigned (virgile)2018-08-24cast error with reference fields
  0002394 1 Plug-in > wpmajorassigned (correnson)2018-08-23conditional input annotations result in why3 type errors
  000239081 Plug-in > wpminorfeedback (correnson)2018-07-25dubious discharge of postcondition
  000238231 Kernelminorassigned (virgile)2018-07-10handling of escape sequences
  000238511 Plug-in > wpcrashassigned (correnson)2018-07-06Auto-generated assigns clause for a void* argument crashes wp
  0002376 1 Plug-in > jessiecrashassigned (cmarche)2018-05-29frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)).
  000237221 Kernel > configuremajorassigned (virgile)2018-03-28coq and ocaml conflict
   000237111 Plug-in > wpfeatureassigned (correnson)2018-03-26suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
  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
  0002194    Plug-in > E-ACSLminorassigned (fmaurica)2018-02-22Failure to record global variable with initialiser
  00023271   Plug-in > E-ACSLminorassigned (fmaurica)2018-02-22Failure to detect overflows into an allocated area within a struct
  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
  [ First Prev 1 2 3 4 5 6 Next Last ]


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker