Issues · pub / frama-c · GitLab

Develop strategies to efficiently run WP with different ATP and Coq

#1145 · created Mar 14, 2014 by Jens Gerlach enhancement wp
- CLOSED
- 0
updated Sep 21, 2021
deficient axioms

#617 · created Jun 29, 2015 by David Cok bug wp
- CLOSED
- 1
updated Feb 22, 2021
CVC4 results are not displayed in the GUI

#682 · created Mar 12, 2014 by Jens Gerlach bug wp
- CLOSED
- 3
updated Feb 22, 2021
Creating a pointer to a local causes valid pointers above it to lose thier valid status

#425 · created Jun 21, 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
Crash with \is_infinite

#550 · created Feb 24, 2015 by mantis-gitlab-migration critical wp
- CLOSED
- 3
updated Feb 22, 2021
Crash when using wpo api get_result

#792 · created May 19, 2014 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
Crash on loop with global assigns and per-behavior assigns

#109 · created Oct 19, 2015 by Boris Yakobowski critical wp
- CLOSED
- 2
updated Feb 22, 2021
crash in presence of \result in assigns

#541 · created Jul 07, 2015 by David Cok critical wp
- CLOSED
- 2
updated Feb 22, 2021
crash

#116 · created Nov 13, 2018 by mantis-gitlab-migration critical wp
- CLOSED
- 6
updated Feb 22, 2021
couldn't verify series of struct member initializations

#1871 · created Mar 13, 2012 by Jochen Burghardt bug wp
- CLOSED
- 4
updated Feb 22, 2021
Coq translation of predicate name changes when additional files are processed by Frama-C

#111 · created Jan 04, 2018 by Jochen Burghardt bug wp
- CLOSED
- 5
updated Feb 22, 2021
coq fails to compile Cint because Zbits is not found

#501 · created Sep 02, 2015 by mantis-gitlab-migration bug wp
- CLOSED
- 3
updated Feb 22, 2021
coq 8.5: cannot find Memory.v

#384 · created Feb 11, 2016 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 2021
contracts about memory mapped I/O through volatile memory locations

#117 · created Oct 31, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021
Confusing bullets for unproven obligations under OSX

#1199 · created Jan 24, 2014 by Jens Gerlach bug wp
- CLOSED
- 7
updated Feb 22, 2021
conditional input annotations result in why3 type errors

#76 · created Aug 23, 2018 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
compatibility between \null in ACSL and NULL in C in wp

#777 · created Feb 17, 2014 by mantis-gitlab-migration bug wp
- CLOSED
- 1
updated Feb 22, 2021
Carbon beta coqide: need write rights to /usr/local/share/frama-c

#2227 · created Dec 15, 2010 by Holger Blasum bug wp
- CLOSED
- 2
updated Feb 22, 2021
cannot proof the rte assertion in the loop for

#2246 · created Feb 01, 2011 by mantis-gitlab-migration bug wp
- CLOSED
- 2
updated Feb 22, 2021

Prev
1
…
7
8
9
10
11
12
13
Next