blob: 83a1c722d6086644d1ef09b50b4074b694877923 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
/* lv6 -2cgc -node main convertible.lus */
/* on vanoise the 08/05/2019 at 23:54:11 */
#ifndef _SOC2C_PREDEF_TYPES
#define _SOC2C_PREDEF_TYPES
typedef int _boolean;
typedef int _integer;
typedef char* _string;
typedef double _real;
typedef double _double;
typedef float _float;
#define _false 0
#define _true 1
#endif
// end of _SOC2C_PREDEF_TYPES
// User typedef
#ifndef _convertible_main_TYPES
#define _convertible_main_TYPES
typedef _integer convertible_eq_case;
typedef _integer convertible_roof_speed_state;
typedef _integer convertible_roof_state;
typedef struct {
_integer i;
_integer j;
_real v;
} convertible_update_acc;
typedef _integer convertible_vehicle_state;
#endif // enf of _convertible_main_TYPES
// Memoryless soc ctx typedef
// Memoryfull soc ctx typedef
/* Lustre_pre_ctx */
typedef struct {
/*Memory cell*/
_integer _memory ;
} Lustre_pre_ctx_type;
/* Lustre_arrow_ctx */
typedef struct {
/*Memory cell*/
_boolean _memory ;
} Lustre_arrow_ctx_type;
/* Lustre_pre_2_ctx */
typedef struct {
/*Memory cell*/
_real _memory ;
} Lustre_pre_2_ctx_type;
/* Lustre_arrow_2_ctx */
typedef struct {
/*Memory cell*/
_boolean _memory ;
} Lustre_arrow_2_ctx_type;
/* convertible_roof_speed_ctx */
typedef struct {
/*INSTANCES*/
Lustre_pre_2_ctx_type Lustre_pre_2_ctx_tab[2];
Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
Lustre_arrow_2_ctx_type Lustre_arrow_2_ctx_tab[2];
Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
} convertible_roof_speed_ctx_type;
/* convertible_roof_ctx */
typedef struct {
/*INSTANCES*/
convertible_roof_speed_ctx_type convertible_roof_speed_ctx_tab[1];
Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
} convertible_roof_ctx_type;
/* Lustre_pre_3_ctx */
typedef struct {
/*Memory cell*/
_real _memory[50] ;
} Lustre_pre_3_ctx_type;
/* Lustre_arrow_3_ctx */
typedef struct {
/*Memory cell*/
_boolean _memory ;
} Lustre_arrow_3_ctx_type;
/* sum_50_0d0_ctx */
typedef struct {
/*INSTANCES*/
Lustre_pre_3_ctx_type Lustre_pre_3_ctx_tab[1];
Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
Lustre_arrow_3_ctx_type Lustre_arrow_3_ctx_tab[1];
Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
} sum_50_0d0_ctx_type;
/* sum_50_0d1_ctx */
typedef struct {
/*INSTANCES*/
Lustre_pre_3_ctx_type Lustre_pre_3_ctx_tab[1];
Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
Lustre_arrow_3_ctx_type Lustre_arrow_3_ctx_tab[1];
Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
} sum_50_0d1_ctx_type;
/* convertible_speed_kmh_ctx */
typedef struct {
/*INSTANCES*/
sum_50_0d1_ctx_type sum_50_0d1_ctx_tab[1];
sum_50_0d0_ctx_type sum_50_0d0_ctx_tab[1];
Lustre_pre_2_ctx_type Lustre_pre_2_ctx_tab[3];
Lustre_arrow_2_ctx_type Lustre_arrow_2_ctx_tab[3];
} convertible_speed_kmh_ctx_type;
/* convertible_vehicle_ctx */
typedef struct {
/*INSTANCES*/
Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
} convertible_vehicle_ctx_type;
/* convertible_may_collide_ctx */
typedef struct {
/*INSTANCES*/
Lustre_pre_2_ctx_type Lustre_pre_2_ctx_tab[1];
Lustre_arrow_2_ctx_type Lustre_arrow_2_ctx_tab[1];
} convertible_may_collide_ctx_type;
/* convertible_main_ctx */
typedef struct {
/*INSTANCES*/
convertible_vehicle_ctx_type convertible_vehicle_ctx_tab[1];
convertible_speed_kmh_ctx_type convertible_speed_kmh_ctx_tab[1];
convertible_roof_ctx_type convertible_roof_ctx_tab[1];
convertible_may_collide_ctx_type convertible_may_collide_ctx_tab[1];
} convertible_main_ctx_type;
// Defining array and extern types assignments
#ifndef _assign_rp50
#define _assign_rp50(dest, source, size) memcpy(dest, source, size)
#endif
|
