stephane / libmodbus

A Modbus library for Linux, Mac OS, FreeBSD and Windows
http://libmodbus.org
GNU Lesser General Public License v2.1
3.44k stars 1.74k forks source link

Bugs on libmodbus_src #753

Closed jongjcho94 closed 2 months ago

jongjcho94 commented 3 months ago

Hello, We recently ran the static analysis using MathWorks Polyspace on the libmodbus located in OpenPLC_v3/utils/libmodbus_src. We use both Polyspace Code Prover

Here are our results:

Polyspace Code Prover is a static analysis tool that rigorously proves the absence of run-time errors and undefined behaviors in C, C++, and Ada code without executing the program. It provides formal verification by analyzing source code to identify potential issues such as array bounds violations, division by zero, and invalid pointer accesses, ensuring code reliability and safety.

The code prover components are considered as follows:

Red: A link to the error message associated with the error which occurs at every execution. Orange: A link to an unproven message - an error may occur sometimes. Grey: A link to a check is shown as an unreachable code. The error message is in grey. Green: A link to a VOA (Value on Assignment) or an error condition that will never occur.

The reports are reported as follows: Number of Red Check 3 Number of Gray Check 61 Number of Orange Check 418 Number of Green Check 4057 Proven 90.8%

Currently, We were having this issues to use libmodbus in OpenPLC, We report this bug issues to OpenPLC as well.

I am attaching full reports on both code prover and bug finder on this report. modbus_CodeProver.pdf

Sincerely,

ladmanj commented 3 months ago

Hi

I can't see those bugs in my code copy.

For example:

static uint16_t crc16(uint8_t buffer, uint16_t buffer_length) { uint8_t crc_hi = 0xFF; / high CRC byte initialized / uint8_t crc_lo = 0xFF; / low CRC byte initialized / uint8_t i; / will index into CRC lookup */

 /* pass through message buffer */
 while (buffer_length--) {
     i = crc_hi ^ *buffer++; /* calculate the CRC  */
     crc_hi = crc_lo ^ table_crc_hi[i];
     crc_lo = table_crc_lo[i];
 }

 return (crc_hi << 8 | crc_lo);

}

I cant see any of the mentioned problems: 3736 Non-terminating loop crc16() The loop is infinite or contains a run-time error. No Unset Unreviewed

The buffer_length variable is decremented in every cycle and thus the while loop will end eventually.

6951 Overflow crc16() Warning: operation [conversion from int32 to unsigned int32] on scalar may overflow (result strictly lower than MIN UINT32) No Unset Unreviewed

There is no copy of unsigned32 to signed32 variable at all.

The analysis software is garbage or it is used improperly.

Regards

JL