Project

General

Profile

Actions
Copy link

Bug #10198

closed

Invalid serialization of post-decrement operation

Added by Evgeny Novikov about 4 years ago. Updated about 4 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Mikhail Mandrykin
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

Download all files
iuu_phoenix.c (4.09 MB) iuu_phoenix.c Evgeny Novikov, 04/02/2020 12:01 PM
toplevel.tar.xz (4.35 MB) toplevel.tar.xz Also attached an executable built under Debian 9 Mikhail Mandrykin, 04/02/2020 03:52 PM
Actions
Copy link

Also available in: Atom PDF