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 (1 - 50 / 1220)  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
  0002485 1 Plug-in > wpminorassigned (correnson)2019-11-08-wp-out missing output for Why3 provers in Frama-C 20 beta
  0002484    Plug-in > wpminorassigned (correnson)2019-11-08alt-ergo support in Frama-C 20 beta
  0002483 1 Plug-in > wpminorassigned (correnson)2019-11-08Eprover in Frama-C 20 beta
  000248221 Plug-in > wpminorresolved (correnson)2019-10-22WP warning not clear
  000210061 Plug-in > wpminorclosed (correnson)2019-10-17readability of coq(?) names
  000228532 Plug-in > wpfeatureclosed (correnson)2019-10-17suggest boolean expressions for "-wp-prop" arguments
  000232922 Plug-in > wptweakclosed (correnson)2019-10-17suggest unique term normalization for lemmas and goals
  000233232 Plug-in > wpmajorclosed (correnson)2019-10-17Information on C type of array is not present (in Coq)
  000233621 Plug-in > wptweakclosed (correnson)2019-10-17suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
  00021802   Plug-in > wpcrashclosed (correnson)2019-10-17Crash on loop with global assigns and per-behavior assigns
  000234053 Plug-in > wpminorclosed (correnson)2019-10-17Coq translation of predicate name changes when additional files are processed by Frama-C
  000235325 Plug-in > wpminorclosed (correnson)2019-10-17alt-ergo goals generated directly / via why3 differ in provability
  000238511 Plug-in > wpcrashclosed (correnson)2019-10-17Auto-generated assigns clause for a void* argument crashes wp
  000240142 Plug-in > wpmajorclosed (correnson)2019-10-17Newer releases of FramaC produce apparent WP plug-in bug
  000239081 Plug-in > wpminorclosed (correnson)2019-10-17dubious discharge of postcondition
  000240961 Plug-in > wpcrashclosed (correnson)2019-10-17crash
  000240721 Plug-in > wpmajorclosed (correnson)2019-10-17contracts about memory mapped I/O through volatile memory locations
  00024141   Plug-in > wpmajorclosed (correnson)2019-10-17Mk_addr not defined in Memory.v (coqwp via why3ide)
  00024594   Plug-in > wpblockclosed (correnson)2019-10-17floating-point support is somwhat incomplete
  000245521 Plug-in > wpminorclosed (correnson)2019-10-17malloc breaks reasoning about assigns
  000233011 Plug-in > wpminorresolved (correnson)2019-10-17known, but inferrable, yet not inferred, property not given as precodition to provers
  00023371   Documentationtextclosed (correnson)2019-10-17explain wp's syntactic restrictions on "inductive" definitions
  000148411 Plug-in > wpminorresolved (correnson)2019-10-17ill-typed alt-ergo proof obligation
   000237121 Plug-in > wpfeatureresolved (correnson)2019-10-17suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
  000229021 Plug-in > wpminorclosed (correnson)2019-10-17incomplete loading of saved state when using WP?
  0002394 1 Plug-in > wpmajorresolved (correnson)2019-10-17conditional input annotations result in why3 type errors
  000240431 Plug-in > wpminoracknowledged (correnson)2019-10-17Shape of VC depends on selection of properties
  0002389172 Plug-in > wpcrashresolved (correnson)2019-10-17Failure to detect qed libraries when running wp
  000242751 Plug-in > wpminoracknowledged (correnson)2019-10-17Prove of \false
  0002420 1 Plug-in > wpcrashacknowledged (correnson)2019-10-17Wp crashes on a recursive function
  000233893 Plug-in > wpminorresolved (correnson)2019-10-17\false provable from recursive logic definition
  00024647   Opammajorresolved (correnson)2019-10-17Potassium does not install on the given Mac version from opam
  00018061   Plug-in > wpminorresolved (correnson)2019-10-17Error in coq code generated by wp
  000247131 Plug-in > wpmajorresolved (correnson)2019-10-17frama-c/wp generates invalid why3
  00024802   Plug-in > clangblockconfirmed (virgile)2019-10-06Syntax error in reorder_defs.ml after running make
  0002477    Kernel > ACSL implementationtextclosed (virgile)2019-09-23Freelance
  0002476    Kernel > ACSL implementationtweakclosed (virgile)2019-09-23FieldEngineer
  00024691   Documentation > websiteminorresolved (virgile)2019-09-20wrong test path given in Compiling from source - Quick Start"
  00024743   Documentation > websiteminorassigned (bobot)2019-09-18Can't view publications on the wiki
  0002378115 ptestsminorresolved (maroneze)2019-09-12Bytecode only compilation fails when linking to stdlib
  00024733   Kernel > Makefileminorclosed (bobot)2019-08-29Bytecode only build fail with error 127
  00024663   Opamblockresolved (maroneze)2019-08-22Can't build from source using opam
  000247211 Plug-in > E-ACSLcrashclosed (signoles)2019-08-22E-ACSL: segmentation fault on a simple strlen function
  000246741 Kernelcrashclosed (signoles)2019-08-22Crash at "hashtbl.ml", line 462
  0002468113 Opammajorresolved (maroneze)2019-08-21opam fails to install frama-c
  00024651   Plug-in > metricsmajorclosed (maroneze)2019-07-18Can we calculate or extract metrics from program dependency graph generated by frama-c
  00022361   Documentation > manualstextclosed (patrick)2019-07-17tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"
  00024381   Documentation > ACSLfeatureclosed (patrick)2019-07-17grammar and implementation disagree on predicate/logic declarations
  000220031 Documentation > ACSLtextresolved (patrick)2019-07-17explicitly mention operator precedences when referring to Fig.2.1 "Grammar of terms" in the acsl-implementation manual
  00021877   Documentation > ACSLtextclosed (patrick)2019-07-17Grammar omissions in 1.9
  [ 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