File: div.i

package info (click to toggle)
frama-c 20220511-manganese-5
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 66,492 kB
  • sloc: ml: 278,834; ansic: 47,093; sh: 4,823; makefile: 3,613; javascript: 2,436; python: 1,919; perl: 897; lisp: 293; xml: 62
file content (13 lines) | stat: -rw-r--r-- 333 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
 
volatile v;

void main() {
  double d1, d2;
  if (v) {
    d1 = v ? 0 : 4;
    d2 = v ? 0 : 3;
    //@ assert d1 / d2 >= 0; // Does not hold, but we want to test the division itself. In the logic this is tricky
    //@ assert !\is_finite((double)(d1 / d2));
    //@ assert \is_finite((double)(d1 / d2));
    //@ assert \false;
  }
}