Skip to content

Commit

Permalink
add same test to affeq because it also fails there
Browse files Browse the repository at this point in the history
  • Loading branch information
reb-ddm committed Jan 12, 2024
1 parent 51359ef commit 8767785
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 2 deletions.
25 changes: 25 additions & 0 deletions tests/regression/63-affeq/20-svcomp-signextension.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
// SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none

#include <stdio.h>
int main() {

unsigned short int allbits = -1;
short int signedallbits = allbits;
int unsignedtosigned = allbits;
unsigned int unsignedtounsigned = allbits;
int signedtosigned = signedallbits;
unsigned int signedtounsigned = signedallbits;

/*
printf ("unsignedtosigned: %d\n", unsignedtosigned);
printf ("unsignedtounsigned: %u\n", unsignedtounsigned);
printf ("signedtosigned: %d\n", signedtosigned);
printf ("signedtounsigned: %u\n", signedtounsigned);
*/

if (signedtounsigned == 4294967295) {
return (-1);
}

return (0);
}
3 changes: 1 addition & 2 deletions tests/regression/77-lin2vareq/34-svcomp-signextension.c
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,7 @@ int main() {
printf ("signedtounsigned: %u\n", signedtounsigned);
*/

if (unsignedtosigned == 65535 && unsignedtounsigned == 65535 &&
signedtosigned == -1 && signedtounsigned == 4294967295) {
if (signedtounsigned == 4294967295) {
return (-1);
}

Expand Down

0 comments on commit 8767785

Please sign in to comment.