Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / clocks7 / clocks7_opt2.c @ 6a93d814

History | View | Annotate | Download (1.09 KB)

1
#include <assert.h>
2
#include "clocks7.h"
3

    
4
/* C code generated by lustrec
5
   SVN version number 0.1-382M
6
   Code is C99 compliant */
7
   
8
/* Import dependencies */
9

    
10
/* Global constants (definitions) */
11

    
12
/* Struct definitions */
13

    
14

    
15
void toto_step (int x, 
16
                int (*b2)
17
                ) {
18
  choice2 d;
19
  choice1 c;
20
  _Bool __toto_1;
21
  //@ ghost _Bool ck_b1 = 0;
22
  //@ ghost _Bool disj_b2 = 0;
23
  //@ ghost _Bool ck_b2 = 0;
24
  //@ ghost _Bool ck_b3 = 0;
25
  if ((x > 0)) {
26
    d = Up;
27
    __toto_1 = (0 == x);
28
    if (__toto_1) {
29
      c = Off;
30
      // z -> b2
31
      // y -> b2
32
      // b2 = 2; (cst prop)
33
      // z = b2; (id assign)
34
      *b2 = 2;
35
      //@ ghost ck_b2 = 1;
36
    } else {
37
      c = On;
38
      // z -> b2
39
      // b1 -> #b2
40
      // y -> b2
41
      // b1 = 1; (cst prop)
42
      //@ ghost (disj_b2 == 1) ;
43
      // z = b1; (id assign)
44
      *b2 = 1;
45
      //@ ghost ck_b2 = 1;
46
    }
47
  } else {
48
    d = Down;
49
    // b3 -> #b2
50
    // y  -> b2
51
    // b3 = 3; (cst prop)
52
    //@ ghost (disj_b2 == 1) ;
53
    *b2 = 3;
54
    //@ ghost ck_b2 = 1;
55
  }
56
  //@ assert ((disj_b2 == 0) || (ck_b2 == 0)) ;
57
  return;
58
}
59