Frama-C Bug Tracking System
Unassigned ^ ] (0 - 0 / 0)
Resolved ^ ] (1 - 10 / 16)
0002330
1 attachment(s)
known, but inferrable, yet not inferred, property not given as precodition to provers
Plug-in > wp - 2019-10-17 17:30
0001484
1 attachment(s)
ill-typed alt-ergo proof obligation
Plug-in > wp - 2019-10-17 17:11
0002371
 1 attachment(s)
suggest to provide results of commandl-line "-wp-prop" evaluation in a file in the wp-out directory
Plug-in > wp - 2019-10-17 17:11
0002394
1 attachment(s)
conditional input annotations result in why3 type errors
Plug-in > wp - 2019-10-17 17:05
0002389
2 attachment(s)
Failure to detect qed libraries when running wp
Plug-in > wp - 2019-10-17 16:30
0002338
3 attachment(s)
\false provable from recursive logic definition
Plug-in > wp - 2019-10-17 15:30
0002464
Potassium does not install on the given Mac version from opam
Opam - 2019-10-17 14:50
0001806
Error in coq code generated by wp
Plug-in > wp - 2019-10-17 14:35
0002471
1 attachment(s)
frama-c/wp generates invalid why3
Plug-in > wp - 2019-10-17 14:29
0002469
wrong test path given in Compiling from source - Quick Start"
Documentation > website - 2019-09-20 13:59
Recently Modified ^ ] (1 - 10 / 1216)
0002100
1 attachment(s)
readability of coq(?) names
Plug-in > wp - 2019-10-17 18:03
0002285
2 attachment(s)
suggest boolean expressions for "-wp-prop" arguments
Plug-in > wp - 2019-10-17 18:03
0002329
2 attachment(s)
suggest unique term normalization for lemmas and goals
Plug-in > wp - 2019-10-17 18:02
0002332
2 attachment(s)
Information on C type of array is not present (in Coq)
Plug-in > wp - 2019-10-17 18:02
0002336
1 attachment(s)
suggest to supply previous "ensures" as hypotheses in proof obligation of next "ensures"
Plug-in > wp - 2019-10-17 18:02
0002180
Crash on loop with global assigns and per-behavior assigns
Plug-in > wp - 2019-10-17 18:01
0002340
3 attachment(s)
Coq translation of predicate name changes when additional files are processed by Frama-C
Plug-in > wp - 2019-10-17 18:01
0002353
5 attachment(s)
alt-ergo goals generated directly / via why3 differ in provability
Plug-in > wp - 2019-10-17 18:01
0002385
1 attachment(s)
Auto-generated assigns clause for a void* argument crashes wp
Plug-in > wp - 2019-10-17 18:00
0002401
2 attachment(s)
Newer releases of FramaC produce apparent WP plug-in bug
Plug-in > wp - 2019-10-17 18:00

newfeedbackacknowledgedconfirmedassignedresolvedclosed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker