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 (501 - 550 / 1186)  Print Reports ]  CSV Export ]  Excel Export ] [ First Prev  ... 6 7 8 9 10 11 12 13 14 15 16 ...  Next Last ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  0001439    Kerneltrivialclosed (Matthieu Lemerre)2014-03-13Few fixes in libc/sys/socket.h
  000147721 Plug-in > Evacrashclosed (yakobowski)2014-03-13Value analysis: bad type conversion plus unassigned fields in a struct leads to crash
  0001687    Plug-in > wpmajorassigned (correnson)2014-03-12Frama-C GUI discards candidate coq proof
  00006162   Kernelmajorclosed (monate)2014-02-12Comments parsing
  000071871 Plug-in > Evaminorclosed (pascal)2014-02-12possible unsoundness in r11866
  000071741 Plug-in > Evaminorclosed (pascal)2014-02-12possible unsoundness bug
  00007148   Kernel > ACSL implementationminorclosed (patrick)2014-02-12Lexing of ACSL characters
  000072531 Kernelminorclosed (virgile)2014-02-12passing (C && c) as argument to a function that expects int (csmith)
  00007232   Graphical User Interfacemajorclosed (signoles)2014-02-12r11920: Analyses -> Show callgraph requires a main function
  00007362   ptestsfeatureclosed (virgile)2014-02-12the input file should be the first argument to ptests
  000073261 Plug-in > Evamajorclosed (pascal)2014-02-12Incorrect states passed to value analysis callbacks in presence of slevel
  000072731 Kernelmajorclosed (virgile)2014-02-12Function specification not exposed through vspec visitor method
  00007202   Kernelcrashclosed (virgile)2014-02-12Incorrect handling of nearly-empty switch clauses with -simplify-cfg
  000072161 Plug-in > Evaminorclosed (pascal)2014-02-12Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
  000075221 Plug-in > Evacrashclosed (pascal)2014-02-12Unexpected error (Ival.Float_abstract.Bottom)
  000075981 Plug-in > Evamajorclosed (pascal)2014-02-12wrong treatment for const arrays in lib-entry mode
  000075410   Kernel > Makefileminorclosed (virgile)2014-02-12Dynamic plugin doc
  00007752   Kernelminorclosed (monate)2014-02-12Hex/octal signed constants can be represented in an unsigned extended integer type (csmith)
  00007742   Plug-in > slicingminorclosed (signoles)2014-02-12Slicing is sometimes not journalisable anymore
  00006893   Plug-in > Evamajorclosed (monate)2014-02-12Value may be incorrect in presence of several ensures
  000077031 Kernelminorclosed (virgile)2014-02-12r12430, some assertions are localized at Cabs2cil_start:0 (csmith)
  000078641 Plug-in > slicingminorclosed (Anne)2014-02-1212816: Missing label in sliced program (csmith)
  00007842   Plug-in > metricsminorclosed (monate)2014-02-12Generating metrics.html on demand
  0000781102 Plug-in > fromminorclosed (pascal)2014-02-12Sliced program computes value different from original (csmith)
  00007906   Kernel > ACSL implementationminorclosed (virgile)2014-02-12integrity problem of the AST on calls to functions with __attribute__ ((noreturn))
  00007294   Kernelfeatureclosed (signoles)2014-02-12Plugin.is_invisible is not see-through enough
  00007982   Plug-in > Evaminorclosed (pascal)2014-02-12Serial conversions in function result (csmith)
  00007852   Kernelminorclosed (pascal)2014-02-1212799, doubtful choice of promotion x86_64 mode (csmith)
  00007616   Kernel > ACSL implementationminorclosed (virgile)2014-02-12typing rule of \old(tab) or tab[index] construct
  000080761 Plug-in > slicingminorclosed (Anne)2014-02-12sliced program does not terminate (csmith)
  00008102   Kernelminorclosed (monate)2014-02-12pretty-printed program rejected by GCC. Affects -print, slicing, scf (csmith)
  000071931 Kernelminorclosed (monate)2014-02-12unsoundness due to packed structs
  00006913   Kernel > ACSL implementationmajorclosed (virgile)2014-02-12Comments parsing not always work
  000081741 Kernelminorclosed (monate)2014-02-12r13378, assertion failed with bit-fields
  000065571 Kernel > ACSL implementationminorclosed (virgile)2014-02-12using real function ( \max, \min, \abs ) instead of integer one in function contract
  00008234   Kernelminorclosed (monate)2014-02-12r13417 unsigned bit-fields of width 32 should be promoted to unsigned int (csmith)
  00008192   Plug-in > Evaminorclosed (pascal)2014-02-12wrong interpretation when a bit-field receives the result of a function (csmith)
  000080861 Plug-in > slicingminorclosed (Anne)2014-02-12r13089 sliced program computes differently from original (csmith)
  000082571 Plug-in > slicingminorclosed (Anne)2014-02-12r13465, crash in slicing (csmith)
  00008322   Kernelminorclosed (virgile)2014-02-12r13586 Spurious "assert \separated(...)" (csmith)
  000077121 Kernelminorclosed (virgile)2014-02-12r12436, unnecessary warning for side-effects (csmith)
  00008613   Kernelcrashclosed (yakobowski)2014-02-12Incorrect loop unrolling in presence of switch
  000085841 Plug-in > semantic constant foldingminorclosed (monate)2014-02-12emitted program computes differently from original (csmith)
  00008572   Kernelminorclosed (patrick)2014-02-12Ocaml 32 bits version 3.11.0
  000082761 Plug-in > slicingminorclosed (Anne)2014-02-12sliced program computes differently from original (csmith)
  00008593   Kernel > ACSL implementationtweakclosed (virgile)2014-02-12ACSL pretty-printer
  00008823   Kernelcrashclosed (yakobowski)2014-02-12Cil generates incorrect switch (with missing cases)
  00007512   Kernel > ACSL implementationminorclosed (virgile)2014-02-12Promotion from integer to boolean
  00008833   Plug-in > Evacrashclosed (yakobowski)2014-02-12Crash du builtin memcpy, par une exception non rattrapable
  00008902   Plug-in > Evamajorclosed (pascal)2014-02-12Results differ between value analysis and GCC on bitfields
  [ First Prev  ... 6 7 8 9 10 11 12 13 14 15 16 ...  Next Last ]


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker