Relevant variable not recognized
Verification of verifythis/duplets.c fails because a relevant variable mkdup:x
is not in relevant var set.
Bash: scripts/cpa.sh -svcomp20 -heap 10000M -timelimit '900 s' -stats -spec ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/verifythis/duplets.c
UPDATE 28.09.20: The issue with relevant variables not being tracked is responsible for (at least some) false alarms in the AWS benchmarks as well. memset_using_uint64_harness.i for example uses a second pointer to modify array content, that is used for reach ability check. This second pointer is not in the Relevant-Var-Set, so the modification is not tracked. A MWE is:
typedef unsigned char __uint8_t;
typedef __uint8_t unit8_t;
void reach_error(){}
extern void abort(void);
void __VERIFIER_assert(_Bool cond) {
if(!cond) {reach_error();abort();}
}
int main() {
short d1[1];
char *s = (char *) d1;
s[0] = 1;
unit8_t *r = (unit8_t *) d1;
__VERIFIER_assert(r[0] == 1);
return 0;
}
Edited by Stephan Holzner