-
Notifications
You must be signed in to change notification settings - Fork 262
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix multiplication and division of complex numbers
Multiplication and division of complex numbers are not just pointwise applications of those operations. Fixes: #8375
- Loading branch information
1 parent
629dbcd
commit 9f1160a
Showing
4 changed files
with
131 additions
and
40 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
#include <complex.h> | ||
|
||
int main() | ||
{ | ||
char choice; | ||
float re = choice ? 1.3f : 2.1f; // a non-constant well-behaved float | ||
float complex z1 = I + re; | ||
float complex z2 = z1 * z1; | ||
float complex expected = 2 * I * re + re * re - 1; // (a+i)^2 = 2ai + a^2 - 1 | ||
float complex actual = | ||
re * re + I; // (a1 + b1*i)*(a2 + b2*i) = (a1*a2 + b1*b2*i) | ||
__CPROVER_assert(z2 == expected, "right"); | ||
__CPROVER_assert(z2 == actual, "wrong"); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
|
||
^\[main.assertion.1\] line 12 right: SUCCESS$ | ||
^\[main.assertion.2\] line 13 wrong: FAILURE$ | ||
^VERIFICATION FAILED$ | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters