Actions
Bug #10198
closedInvalid serialization of post-decrement operation
Start date:
04/02/2020
Due date:
% Done:
0%
Estimated time:
Detected in build:
git
Platform:
Published in build:
Description
For the attached C source file and the given options:
toplevel.opt "-no-autoload-plugins" "-no-findlib" "-kernel-log" "e:problem desc.txt" "-machdep" "gcc_x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-no-annot" "-no-single-return" "-fold-temp-vars" "-shrink-initializers" "-keep-logical-operators" "-aggressive-merging" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i"
Frama-C (CIL) incorrectly serializes a post-decrement operation. This is the case for "dataout + DataCount ++" within iuu_uart_baud(). After all this results in possible buffer overflows since an array index is incremented before an array access that should be v.v.
Files
Updated by Evgeny Novikov about 4 years ago
I observe the only case where it hits, so, the issue is not so important.
Updated by Mikhail Mandrykin about 4 years ago
- File toplevel.tar.xz toplevel.tar.xz added
- Status changed from New to Resolved
It turned out to be caused by a missed case in the implementation of temporary variable folding. In this case temporary variables can't be folded and should be left as is, but in case of UnspecifiedSequence the detection of side effects between temp variable initialization and the main expression failed due to visiting additional effects fields in UnspecifiedSequence. Fixed in framac|9d27efaa.
Updated by Evgeny Novikov about 4 years ago
- Status changed from Resolved to Closed
The fix works well. Thank you for the binary distribution, but now I can do them myself at last.
Actions