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 / 1180)  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
  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
  00022533   Kernel > libcminorclosed (maroneze)2017-12-06File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
  00014673   Kernelfeatureclosed (valentin.perrelle)2017-12-06Parser does not handle mixed concatenations of wide and non-wide strings
  00022763   Graphical User Interfacetweakacknowledged (maroneze)2017-11-27Duplicates are created on the tab "Messages"
  000233232 Plug-in > wpmajoracknowledged (correnson)2017-11-22Information on C type of array is not present (in Coq)
  0002330 1 Plug-in > wpminorassigned (correnson)2017-10-26known, but inferrable, yet not inferred, property not given as precodition to provers
  000232912 Plug-in > wptweakassigned (correnson)2017-10-12suggest unique term normalization for lemmas and goals
  000228512 Plug-in > wpfeatureassigned (correnson)2017-10-09suggest boolean expressions for "-wp-prop" arguments
  000210051 Plug-in > wpminoracknowledged (correnson)2017-10-09readability of coq(?) names
  000232521 Graphical User Interfaceminorclosed (maroneze)2017-09-01Make it build on bytecode architectures
  000232322 Documentationminorclosed (virgile)2017-09-01Spelling errors
  000232631 Plug-in > Evaminorclosed (yakobowski)2017-09-01Value.cmo needs LoopAnalysis.cmo
  000232461 Kernelminorclosed (yakobowski)2017-08-14Port to OCaml 4.05
  00017632   Kernel > configureminorclosed (virgile)2017-08-12Configure step fails on bytecode architectures
  000230121 Plug-in > wpcrashassigned (correnson)2017-07-21statement contract apparently confuses parser
  0002317    Documentation > manualstextassigned (correnson)2017-07-19Statement contracts and WP
  000230021 Documentation > ACSLtextclosed (patrick)2017-07-18suggest to clarify semantics of statement contract in ACSL implementation manual
  0002316 1 Plug-in > pathcrawlerminorassigned (nicky)2017-07-07Instrumentation Failure Error in Online Pathcrawler
  000231531 Plug-in > Evablockclosed (yakobowski)2017-07-03unsoundness after external function call
  000220021 Documentation > ACSLtextacknowledged (patrick)2017-06-28explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
  00023131   Documentation > manualstextassigned (correnson)2017-06-23suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
  000213782 Plug-in > Evaminorclosed (yakobowski)2017-06-15value analysis introduces weird pointer assert with variable length arrays
  000231211 Plug-in > wptweakassigned (correnson)2017-06-15false postcondition shouldn't be verified in default memory-model setting
  0002311 1 Plug-in > wptextassigned (correnson)2017-06-15poor errors message texts for Hoare memory model checks
  0002309 1 Plug-in > wpminorassigned (correnson)2017-06-01naming the default behavior influences proven obligations
  0002308 1 Plug-in > wpfeatureassigned (correnson)2017-06-01suggest to check (loop) assigns clauses by data flow analysis
  0001740 1 Plug-in > E-ACSLmajorclosed (signoles)2017-05-31Incorrectness when early exiting a block
  000073351 Plug-in > inoutminorclosed (yakobowski)2017-05-31Invalid results in presence of pseudo-recursive calls in inout and from
  00022793   Plug-in > Evatweakclosed (yakobowski)2017-05-31EVA analysis does not start with click on "Execution" button.
  000227771 Plug-in > Evamajorclosed (yakobowski)2017-05-31Operability depends on the order of options changes
   0002269    Plug-in > obfuscatortextclosed (signoles)2017-05-31There is a typo in description of plug-in: "objuscator" instead of "obfuscator".
  0002252 1 Plug-in > E-ACSLminorclosed (signoles)2017-05-31GMP typing issue
  00022353   Kernelcrashclosed (virgile)2017-05-31Functions that claim to return a struct but don't cause a crash
  0002284 1 Plug-in > E-ACSLcrashclosed (signoles)2017-05-31E-ACSL type system crash
  00022832   Plug-in > wpminorclosed (correnson)2017-05-31type of float parameter changed unexpectedly to double
  000230752 Kernelminorassigned (virgile)2017-05-31preprocessor fail: unterminated comment
  000213521 Kernel > libcfeatureclosed (maroneze)2017-05-23sigsetjmp and siglongjmp in setjmp.h
  [ First Prev 1 2 3 4 5 6 7 8 9 10 11 ...  Next Last ]


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker