Issues · pub / frama-c · GitLab

wp: the example from Getting Started guide doesn't work (all goals are Unknown)

#389 · created Dec 14, 2016 by mantis-gitlab-migration enhancement parsing
- 13
updated Apr 15, 2021
suggestion: translate axioms and implication premises in forward order to coq

#360 · created Mar 13, 2017 by Jochen Burghardt bug wp
- CLOSED
- 2
updated Apr 15, 2021
unable to use lemma separated_region

#620 · created Dec 28, 2014 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
Frama-C sleeps too much when discharging trivial goals

#369 · created Feb 13, 2017 by mantis-gitlab-migration enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
WP inserts unwanted new lines into Coq proofs

#385 · created Jan 02, 2017 by Jens Gerlach bug wp
- CLOSED
- 1
updated Apr 15, 2021
Why3 warning

#387 · created Dec 16, 2016 by Jens Gerlach bug wp
- CLOSED
- 2
updated Apr 15, 2021
more prover processes run than expected

#388 · created Dec 15, 2016 by Jens Gerlach bug wp
- CLOSED
- 4
updated Apr 15, 2021
error in Coq file generation

#405 · created Dec 03, 2016 by Alain Giorgetti bug wp
- CLOSED
- 1
updated Apr 15, 2021
Nested scopes may cause issues with the validity of created pointers

#409 · created Aug 17, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Validation fails when predicate is used with implicit type conversion.

#508 · created May 31, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Oddities in the modeling of floats and doubles

#509 · created May 16, 2016 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Apr 15, 2021
Crash with large array initialisation

#514 · created Mar 18, 2016 by mantis-gitlab-migration critical wp
- CLOSED
- 2
updated Apr 15, 2021
WP detect a non-natural loop on a do-while(0) loop

#518 · created Aug 19, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 4
updated Apr 15, 2021
zombie processes (again)

#526 · created Feb 01, 2016 by Jens Gerlach bug confirmed wp
- CLOSED
- 5
updated Apr 15, 2021
Unable to prove things that are provable, gets confused

#584 · created Oct 18, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
incomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."

#592 · created Sep 21, 2015 by Jochen Burghardt bug wp
- CLOSED
- 1
updated Apr 15, 2021
suggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligations

#593 · created Sep 21, 2015 by Jochen Burghardt enhancement wp
- CLOSED
- 1
updated Apr 15, 2021
assertion failure using memset on a char

#595 · created Sep 14, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
Slow in proof obligation generation

#598 · created Sep 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021
Able to assert a false statement

#803 · created Mar 03, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Apr 15, 2021

Prev
1
…
12
13
14
15
16
17
18
19
20
…
74
Next