SV-Comp incorrect result in no-overflow tasks

[DrMichaelPetter]

Straight from no-overflow  on ldv-regression/test_overflow.i ; we are not flagging any overflow here.

#include <stdlib.h>
#include <stdio.h>

void __blast_assert()
{
 ERROR: {reach_error();abort();}
}

ssize_t getService();
int globalSize;

int
main(int argc, char* argv[]) {
 long int retVal;
 retVal = getService();
 ((sizeof(retVal)==globalSize) ? (0) : __blast_assert ());
 printf("returned value: %ld\n", retVal);
 return 0;
}

ssize_t getService() {
 ssize_t localVar = 999999999999;
 globalSize = sizeof(localVar);
 printf("localVar: %zd\n", localVar);
 return localVar;
}

Correct me if I am wrong, but I thought that ssize_t localVar = 999999999999; is the culprit on 32bit architectures. However, we do not flag an overflow even on

//SKIP PARAM: --sets  exp.architecture 32bit  --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" --conf conf/svcomp22.json

#include <sys/types.h>

int main(){
    ssize_t a = 999999999999; // WARN
    return a?0:1;
}

If we let gcc -Wall -c -m32 test.c try with this minimal example, it flags the overflow in that line. Is this what the sv-comp task would require us to do, too?

[sim642]

exp.architecture only applies to preprocessing (which isn't used in SV-COMP anyway) right now. If this is based on 32bit architecture, then it's just another instance of #54 revealing itself.

[sim642]

According to SV-COMP community meeting discussion and decision, we are right here: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1552.

[sim642]

The task was fixed upstream, so it's not longer incorrect: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1552.