Issues · pub / frama-c · GitLab

Annotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.

#401 · created Nov 24, 2016 by mantis-gitlab-migration bug rte
- CLOSED
- 3
updated Feb 22, 2021
Incorrect overflow and cast assertions for bitfields

#293 · created Jun 26, 2017 by Kostyantyn Vorobyov bug rte
- CLOSED
- 3
updated Feb 22, 2021
Missing cast in code generated by RTE

#181 · created Dec 17, 2018 by Julien Signoles bug confirmed rte
- CLOSED
- 1
updated Apr 20, 2021
Missing index_bound

#1857 · created May 24, 2013 by mantis-gitlab-migration bug rte
- CLOSED
- 2
updated Feb 22, 2021
Missing rte guard when assigning an unsigned int to an int

#1044 · created Apr 30, 2014 by Jens Gerlach bug rte
- CLOSED
- 6
updated Feb 22, 2021
RTE assertion for signed right shift is wrong

#235 · created Feb 03, 2018 by mantis-gitlab-migration bug rte
- CLOSED
- 2
updated Feb 22, 2021
RTE does not check for downcast of unsigned integer

#1997 · created Feb 07, 2012 by mantis-gitlab-migration bug rte
- CLOSED
- 5
updated Feb 22, 2021
RTE does not generate assertions for non initialized arguments

#2050 · created Jul 06, 2011 by Boris Yakobowski bug rte
- CLOSED
- 2
updated Feb 22, 2021
Unproven rte assertions for bit complement

#1045 · created May 01, 2014 by Jens Gerlach bug rte
- CLOSED
- 1
updated Feb 22, 2021
wrong generation of assigns \nothing at function call

#2156 · created Apr 18, 2011 by Patrick Baudin bug rte
- CLOSED
- 1
updated Feb 22, 2021