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 Frama-C Boron-20100401 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 (1 - 47 / 47)  Print Reports ]  CSV Export ]  Excel Export ]
    PID # Attachment count CategorySeverityStatusUpdatedSummary
  000043531 Plug-in > callgraphminorclosed (signoles)2018-11-30Too many edges in call graph
  00003143   Plug-in > Evaminorclosed (pascal)2014-02-12malloc.h can't be preprocessed: __func__ is not a macro
  00003101   Kernelminorclosed (signoles)2014-02-12Be careful when activating warnings.
  00003382   Plug-in > jessieminorclosed (cmarche)2014-02-12free() should permit 0 as valid argument
  000037411 Graphical User Interfaceminorclosed (signoles)2014-02-12"-cpp-command ..." parameter lost
  0000388    Plug-in > Evacrashclosed (monate)2014-02-12Incorrect 'assert false' in value analysis
  00004063   Plug-in > jessieminorclosed (cmarche)2014-02-12assert false (* TODO *)
  00003812   Plug-in > Evafeatureclosed (pascal)2014-02-12propagation of \result clauses
  00002572   Kernelminorclosed (pascal)2014-02-12get_varinfo not exported in src/ai/base.mli
  00002451   Kernelmajorclosed (virgile)2014-02-12Blocks are removed from the AST
  00001864   Plug-in > slicingcrashclosed (Anne)2014-02-12Stack overflow when slicing functions invoking themselves circularily
  00003052   Kernel > configureminorclosed (signoles)2014-02-12After ./confugure with --disable-all-staff options, make holds
  000032941 Kernel > ACSL implementationminorclosed (cmarche)2014-02-12Float promoted to double
  00003422   Kernel > ACSL implementationminorclosed (virgile)2014-02-12Assertion failed instead of typing error report
  00003661   Plug-in > jessieminorclosed (monate)2014-02-12Unicode minus sign (U+2212) not accepted by Jessie, yet used in documentation, causing mysterious failure
  00003462   Documentation > ACSLtextclosed (virgile)2014-02-12Example 2.31 of ACSL 1.4 (Beryllium implementation) incorrect
  00002721   Plug-in > jessiefeatureclosed (virgile)2014-02-12complete behaviors; disjoint behaviors;
  00002133   Kernelcrashclosed (virgile)2014-02-12crash in parser when double definition of variable in two different files, in some order
  00003984   Kernel > configureminorclosed (signoles)2014-02-12RTE compiled even with ./configure --disable-rte
  00003251   Plug-in > Evafeatureclosed (pascal)2014-02-12Precise widening when a loop condition involves a char or short
  000065041 Kernelminorclosed (virgile)2011-01-10loop assigns error
  000064811 Kernelminorclosed2010-12-23error with defined constants
  00003702   Plug-in > jessieminorclosed (cmarche)2010-04-19pragma JessieIntegerModel
  00003673   Plug-in > jessiemajorclosed (cmarche)2010-04-19bug with constants like 1E-6
  000036221 Plug-in > jessiemajorclosed (cmarche)2010-04-19wrong proof obligation generated with axiomatic def and array quantification
  000036121 Plug-in > jessieminorclosed (cmarche)2010-04-19"why" reports "unbound label"
  000045021 Plug-in > jessiecrashclosed (cmarche)2010-04-19Jessie translation fails with double assignment
  000044931 Plug-in > jessieminorclosed (cmarche)2010-04-19Jessie subprocess failed with enumerated type
  000044321 Plug-in > jessiemajorclosed (cmarche)2010-04-19assigns clause unchecked on arrays
  000042021 Plug-in > jessieminorclosed (cmarche)2010-04-19same formula translated differently as axiom/lemma
  00003992   Plug-in > jessiemajorclosed (cmarche)2010-04-19Statement contract and "hiding" of statement
  00003911   Plug-in > jessietweakclosed (cmarche)2010-04-19Why keywords as ACSL identifiers
  00003862   Plug-in > jessieminorclosed (cmarche)2010-04-19int32 and real can't be unified
  000043191 Kernelcrashclosed (signoles)2010-04-13Dgraph.DGraphModel.read_dot
  00004141   Plug-in > Evafeatureclosed (pascal)2010-04-13imprecision in widening/narrowing for char and short index
  00003933   Plug-in > slicingfeatureclosed (Anne)2010-04-13assigns clauses are missing from the sliced program
  00003922   Plug-in > Evacrashclosed (pascal)2010-04-13Failure("Function 'From.find_deps_no_transitivity' not registered yet")
  000038521 Kernelcrashclosed (virgile)2010-04-13File "src/kernel/", line 372, characters 13-19: Assertion failed
  000038211 Kernel > Makefileminorclosed (signoles)2010-04-13Should not call install-kernel-opt on bytecode architectures
  00003761   Plug-in > jessiemajorclosed (cmarche)2010-04-13unsigned long long constant becomes signed
  00003725   Plug-in > Evamajorclosed (virgile)2010-04-13Wrong postconditions are "valid according to value analysis"
  00003641   Plug-in > jessieminorclosed (virgile)2010-04-13complete/disjoint behaviors shouldn't accept undefined behaviors
  00003582   Kernel > ACSL implementationminorclosed (yakobowski)2010-04-13redeclaration as different kind of symbol
  00003322   Kernelminorclosed (virgile)2010-04-13goto generated by Frama-C and not supported by Jessie
  00003271   Kernel > ACSL implementationminorclosed (virgile)2010-04-13order of 'decreases' and 'behavior' clauses
  00003111   Kernelminorclosed (virgile)2010-04-13switch and case expressions must be integer
  00003093   Kernel > ACSL implementationcrashclosed (virgile)2010-04-13After ./confugure with --disable-all-staff options and make static, frama-c-Myplugin.byte crashes


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker