| Description | ==== test.c ====
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR: goto ERROR;
}
return;
}
#define a (2)
int main(unsigned int loop1, unsigned int m1) {
int sn=0;
unsigned int x=0;
while(1){
sn = sn + a;
x++;
__VERIFIER_assert(sn==x*a || sn == 0);
}
}
==========
$ frama-c -pdg test.c
[pdg] computing for function __VERIFIER_assert
[pdg] done for function __VERIFIER_assert
[pdg] computing for function main
[kernel] Current source was: sum03_safe.c:5
The full backtrace is:
Called from file "set.ml", line 216, characters 18-33
Called from file "list.ml", line 195, characters 17-20
Called from file "src/kernel/stmts_graph.ml", line 418, characters 6-65
Called from file "src/pdg/ctrlDpds.ml", line 217, characters 35-59
Called from file "list.ml", line 86, characters 24-34
Called from file "src/pdg/ctrlDpds.ml", line 237, characters 29-39
Called from file "src/pdg/ctrlDpds.ml", line 257, characters 22-31
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
Called from file "src/pdg/ctrlDpds.ml", line 261, characters 11-21
|