|
Viewing Issues (1 - 50 / 283)
[ Print Reports ] [ CSV Export ] [ Excel Export ]
[ First Prev 1 2 3 4 5 6 Next Last ]
|
| | | P | ID | # |  |
Category | Severity | Status | Updated | Summary |
|
| | |  | 0002409 | 3 | 1 |
Plug-in > wp | crash | resolved (correnson) | 2018-11-14 | crash |
| | | | 0002408 | | |
Plug-in > wp | minor | assigned (correnson) | 2018-11-03 | Some issues related to Frama-C 18.0 (beta) "Argon" |
| | | | 0002407 | 1 | 1 |
Plug-in > wp | major | assigned (correnson) | 2018-10-31 | contracts about memory mapped I/O through volatile memory locations |
| | | | 0002379 | 3 | 1 |
Kernel > libc | minor | resolved (maroneze) | 2018-10-29 | FE_* API is available on OpenBSD |
| | | | 0002399 | 4 | |
Opam | major | resolved (maroneze) | 2018-10-29 | Failed to install framaC on macosx using opam |
| | | | 0002384 | 3 | 2 |
Kernel | minor | resolved (valentin.perrelle) | 2018-10-18 | user error: scalar value (of type int) initialized by compound initializer |
| | | | 0002354 | 2 | |
Plug-in > RTE | minor | resolved (signoles) | 2018-10-15 | RTE assertion for signed right shift is wrong |
| | | | 0002404 | 3 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2018-10-09 | Shape of VC depends on selection of properties |
| | | | 0002386 | 4 | 2 |
Plug-in > E-ACSL | minor | resolved (fmaurica) | 2018-10-05 | E-ACSL: internal error: raised at file "src/libraries/project/project.ml", line 402 |
| | | | 0001762 | 1 | |
Plug-in > E-ACSL | minor | resolved (fmaurica) | 2018-10-04 | Generate out-of-scope variable when using quantified variable in a \old |
| | | | 0002402 | 3 | |
Plug-in > clang | block | assigned (virgile) | 2018-10-03 | frama-clang fails to compile |
| | | | 0002305 | 1 | 2 |
Plug-in > E-ACSL | minor | resolved (fmaurica) | 2018-10-02 | E-ACSL: proper bitfileds handling |
| | | | 0002310 | | 1 |
Plug-in > E-ACSL | minor | assigned (fmaurica) | 2018-10-02 | Incorrect handling of \initialized when initialized struct is passed to a function by value |
| | | | 0002401 | 4 | 2 |
Plug-in > wp | major | acknowledged (correnson) | 2018-10-02 | Newer releases of FramaC produce apparent WP plug-in bug |
| | | | 0002395 | 2 | |
Plug-in > clang | minor | assigned (virgile) | 2018-09-07 | const fields in constructors |
| | | | 0002290 | 2 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2018-09-06 | incomplete loading of saved state when using WP? |
| | | | 0002398 | 1 | |
Documentation > manuals | minor | resolved (signoles) | 2018-09-06 | Name of RTE plugin in documentation |
| | | | 0002397 | 1 | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2018-08-27 | Model Variables in Frama C |
| | | | 0002396 | | |
Plug-in > clang | minor | assigned (virgile) | 2018-08-24 | cast error with reference fields |
| | | | 0002394 | | 1 |
Plug-in > wp | major | assigned (correnson) | 2018-08-23 | conditional input annotations result in why3 type errors |
| | | | 0002389 | 12 | 2 |
Plug-in > wp | crash | assigned (correnson) | 2018-08-17 | Failure to detect qed libraries when running wp |
| | | | 0002390 | 8 | 1 |
Plug-in > wp | minor | feedback (correnson) | 2018-07-25 | dubious discharge of postcondition |
| | | | 0002382 | 3 | 1 |
Kernel | minor | assigned (virgile) | 2018-07-10 | handling of escape sequences |
| | | | 0002385 | 1 | 1 |
Plug-in > wp | crash | assigned (correnson) | 2018-07-06 | Auto-generated assigns clause for a void* argument crashes wp |
| | | | 0002380 | 1 | |
Plug-in > wp | minor | assigned (correnson) | 2018-06-25 | `strlen` used from code makes it no longer possible to prove `assigns \nothing`. |
| | | | 0002378 | | |
ptests | minor | assigned (virgile) | 2018-06-18 | Bytecode only compilation fails when linking to stdlib |
| | | | 0002376 | | 1 |
Plug-in > jessie | crash | assigned (cmarche) | 2018-05-29 | frama-c/jessie crashes with Unexpected error (Cil.SizeOfError("Undefined sizeof on a function.", _)). |
| | | | 0002372 | 2 | 1 |
Kernel > configure | major | assigned (virgile) | 2018-03-28 | coq and ocaml conflict |
| | | | 0002371 | 1 | 1 |
Plug-in > wp | feature | assigned (correnson) | 2018-03-26 | suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory |
| | | | 0002370 | | |
Kernel > ACSL implementation | feature | assigned (virgile) | 2018-03-08 | Expose ACSL annotations through host language pragmas |
| | | | 0002369 | 8 | |
Plug-in > E-ACSL | minor | acknowledged (signoles) | 2018-02-23 | e-acsl-gcc failes on macOS |
| | | | 0002194 | | |
Plug-in > E-ACSL | minor | assigned (fmaurica) | 2018-02-22 | Failure to record global variable with initialiser |
| | | | 0002327 | 1 | |
Plug-in > E-ACSL | minor | assigned (fmaurica) | 2018-02-22 | Failure to detect overflows into an allocated area within a struct |
| | | | 0002367 | 1 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | C-function returning a struct causes warning on missing Ctor code/spec when inside 'extern "C" {...}' |
| | | | 0002366 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | loop assigns clause ginored under strange circumstances |
| | | | 0002365 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | user-defined type not accepted after builtin type in quantifier chain |
| | | | 0002364 | | 1 |
Plug-in > clang | feature | assigned (virgile) | 2018-02-12 | Frama-clang reports overloading ambiguity where Frama-C doesn't |
| | | | 0002363 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | variable declared in "for" init-part unrecognized in loop body assigns clause; 100% verification degree reported nevertheless |
| | | | 0002362 | | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-12 | "let" in predicate body unrecognized |
| | | | 0002361 | | 1 |
Plug-in > clang | crash | assigned (virgile) | 2018-02-12 | "assigns" in statement contract causes abort or crash |
| | | | 0002360 | | 1 |
Plug-in > clang | crash | assigned (virgile) | 2018-02-12 | "Here" as predicate label in statement contract causes Segmentation fault |
| | | | 0002359 | | 1 |
Plug-in > clang | feature | assigned (virgile) | 2018-02-12 | Frama-clang complains when reserved keywords are used as property labels, while Frama-C doesn't |
| | | | 0002356 | 2 | 1 |
Plug-in > clang | feature | confirmed (virgile) | 2018-02-09 | insufficient contracts for generated constructors and assignment operator(s) |
| | | | 0002357 | 2 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-08 | can't handle lemma with 3 labels |
| | | | 0002358 | | 1 |
Plug-in > clang | feature | assigned (virgile) | 2018-02-08 | predicate argument type "struct S" accepted by Frama-C, but not by Frama-clang |
| | | | 0002350 | 2 | 2 |
Plug-in > clang | minor | acknowledged (virgile) | 2018-02-08 | kernel warns about invalid implicit conversion |
| | | | 0002355 | 1 | 1 |
Plug-in > clang | minor | assigned (virgile) | 2018-02-05 | Alt-Ergo reports about " bool and int cannot be unified" |
| | | | 0001484 | 1 | 1 |
Plug-in > wp | minor | assigned (correnson) | 2018-02-05 | ill-typed alt-ergo proof obligation |
| | | | 0002340 | 4 | 3 |
Plug-in > wp | minor | acknowledged (correnson) | 2018-02-02 | Coq translation of predicate name changes when additional files are processed by Frama-C |
| | | | 0002353 | 1 | 5 |
Plug-in > wp | minor | assigned (correnson) | 2018-02-01 | alt-ergo goals generated directly / via why3 differ in provability |
|
[ First Prev 1 2 3 4 5 6 Next Last ]
|
