Frama-C Bug Tracking System
Unassigned ^ ] (1 - 1 / 1)
0002301
1 attachment(s)
statement contract apparently confuses parser
Kernel - 2017-05-11 15:46
Resolved ^ ] (1 - 3 / 3)
0002253
File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
Kernel > libc - 2017-06-14 19:12
0001467
Parser does not handle mixed concatenations of wide and non-wide strings
Kernel - 2017-06-09 19:55
0002297
1 attachment(s)
syntax error before loop contract reported after loop contract
Kernel - 2017-05-31 19:19
Recently Modified ^ ] (1 - 10 / 1086)
0002314
1 attachment(s)
Incorrect overflow and cast assertions for bitfields
Plug-in > RTE - 2017-06-27 14:01
0002313
suggestions for improvement of Sect.3.6 and 3.7 of the wp manual
Documentation > manuals - 2017-06-23 10:44
0002137
2 attachment(s)
value analysis introduces weird pointer assert with variable length arrays
Plug-in > value analysis - 2017-06-15 15:56
0002312
1 attachment(s)
false postcondition shouldn't be verified in default memory-model setting
Plug-in > wp - 2017-06-15 15:14
0002311
1 attachment(s)
poor errors message texts for Hoare memory model checks
Plug-in > wp - 2017-06-15 12:58
0002253
File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
Kernel > libc - 2017-06-14 19:12
0002310
1 attachment(s)
Incorrect handling of \initialized when initialized struct is passed to a function by value
Plug-in > E-ACSL - 2017-06-14 07:55
0001467
Parser does not handle mixed concatenations of wide and non-wide strings
Kernel - 2017-06-09 19:55
0002309
1 attachment(s)
naming the default behavior influences proven obligations
Plug-in > wp - 2017-06-01 16:23
0002308
1 attachment(s)
suggest to check (loop) assigns clauses by data flow analysis
Plug-in > wp - 2017-06-01 13:25

newfeedbackacknowledgedconfirmedassignedresolvedclosed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker