~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/jessie/test6_floats.c

• browse files at revision 1
• compare with another revision
• download diff
• download tarball
• view history from revision 1

Show diffs side-by-side

added

removed

tests/jessie/test6_floats.c

 

1

 

 

2

 

 

3

/*@  predicate my_killing_prop(double uc, double up, int n) */

 

4

 

 

5

 

 

6

 

 

7

/*@ requires 2 <= N <= 2^^26 && 

 

8

  @      \exact(u0)==u0 && \exact(u1)==u1 &&

 

9

  @      \forall int k; 0 <= k <= N =>  |u0+k*(u1-u0)| <= 1

 

10

  @ ensures  \exact(\result)==u0+N*(u1-u0) &&

 

11

  @          \round_error(\result) <= (N)*(N+1)/2.*2^^(-53)

 

12

  @*/

 

13

 

 

14

 

 

15

double comput_seq(double u0, double u1, int N) {

 

16

  int i;

 

17

  double uprev, ucur,tmp;

 

18

  uprev=u0;

 

19

  ucur=u1;

 

20

 

 

21

  /*@ invariant 2 <= i && i <= N+1 && 

 

22

    @   \exact(ucur) ==u0+(i-1)*(u1-u0) &&

 

23

    @   \exact(uprev)==u0+(i-2)*(u1-u0) &&

 

24

    @   my_killing_prop(ucur,uprev,i-2) 

 

25

    @ variant N-i*/ 

 

26

  for (i=2; i<=N; i++) {

 

27

    tmp=2*ucur;

 

28

    /*@ assert tmp==2*ucur */

 

29

    tmp-=uprev;

 

30

    uprev=ucur;

 

31

    ucur=tmp;

 

32

  }

 

33

  return ucur;

 

34

}

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1