[EVA] Question about \tainted
Hi,
I know the taint analysis is still in experimental phase, but I was wondering why Frama-C cannot prove the following assertion in this program.
#include "__fc_builtin.h"
int tainted;
int main(void){
tainted = Frama_C_nondet(0, 1);
//@ taint tainted;
//@ assert \tainted(tainted);
return 0;
}
Frama-C commit 437130a79253e90571fc44a90732290da5957f07
using the command frama-c -eva -eva-domains taint -eva-msg-key=d-taint,-d-c-value test.c
says
Assertions 0 valid 1 unknown 0 invalid 1 total
Even though Frama_C_domain_show_each
shows that the variable is indeed tainted.
Frama_C_domain_show_each:
tainted : # cvalue: {0; 1}
# taint: true
Is \tainted
just a placeholder to be implemented for now ?