[<prev] [next>] [thread-next>] [day] [month] [year] [list]
Message-ID:
<LV5PR07MB117784DEE29CA16570210E5C3A96CA@LV5PR07MB11778.namprd07.prod.outlook.com>
Date: Mon, 16 Feb 2026 15:00:03 +0000
From: "Mahmoud Ahmad Alawneh [C]" <mahmoud@...ence.com>
To: "musl@...ts.openwall.com" <musl@...ts.openwall.com>
CC: Ayman Hanna <ayman@...ence.com>, Cesar Rodriguez <rcesar@...ence.com>,
"Mariam Flayyan [C]" <mariamf@...ence.com>
Subject: Concerns about MUSL sqrt function math implementation in Formal
Verification
Hi MUSL team,
I am a Software Engineer at Cadence Design Systems working on Formal Verification for chip designs.
We use the MUSL math library in our internal code base and we detected issues from the math functions (specifically sqrt)
We have a linting app called "C Autoformal" aka CAF and we have noticed that we detect ArithmeticOverflow from sqrt function MUSL implementation.
When compiling the following code within our tool:
int main()
{
int arr[3] = {1, 2, 3};
int* ptr = arr;
ptr += 4;
int k = *ptr;
double y = my_sqrt(k);
return 0;
}
Attached below is a screenshot from out linting app (CAF), showing possible design overflows:
On the left panel: we show the possible overflow from the design (i.e: cpp_ArithmeticOverflow_3)
On the right panel: we show the source code line of the design that caused the overflow.
As you can see below, the detected ArithmeticOverflow points to a line (inside of math/sqrt.c : double sqrt(double x) ) that decreases 1 from top and then compares it to another value, this seems to cause ArithmeticOverflow:
[cid:image003.png@...C9F65.AF9393F0]
We want to know if this would affect the effeciency of the math funcitons?
Should this be a top concern for us or is it something under control and should be ignored?
Regards,
Mahmoud
Content of type "text/html" skipped
Download attachment "image003.png" of type "image/png" (121145 bytes)
Powered by blists - more mailing lists
Confused about mailing lists and their use?
Read about mailing lists on Wikipedia
and check out these
guidelines on proper formatting of your messages.
