1

Integer division in LustreC

2


3

* Issue

4


5

Integer division / and associated modulo mod

6


7

a = (a / b) * b + (a mod b)

8


9

Division between two integers can be interpreted in different ways

10

 a C like division where sign(a mod b) = sign a

11

 a euclidean division where 0 <= a mod b < b

12

In both cases they satisfy the above equation.

13


14

Kind modelchecker or Horn encoding assumes the mathematical definition, ie. the

15

euclidean division, while lustreC or the Verimag compiler rely on the C

16

definition.

17


18

In the following we deonote by div_C/mod_C and div_M/mod_M the functions in C

19

and math, respectively.

20


21

As an example 4 div_C 3 = 1 while 4 div_M 3 = 2

22


23

Some properties:

24

 we have a div_M b = a div_C b when a = b * k

25

 we have a mod_C b = 0 \equiv a mod_M b = 0.

26


27

* From C to Euclidian

28


29

a mod_M b = (a mod_C b) + (a mod_C b < 0 ? abs(b) : 0)

30


31

a div_M b = (a  (a mod_M b)) div_C b

32

= (a  ((a mod_C b) + (a mod_C b < 0 ? abs(b) : 0))) div_C b

33


34

* From Euclidian to C

35


36

a mod_C b = a mod_M b  ((a mod_M b <> 0 && a <= 0) ? abs(b) : 0)

37


38

a div_C b = (a  (a mod_C b)) div_M b

39

= (a mod_M b <> 0 && a <= 0)?((a  a mod_M b + abs(b)) div_M b) :((a  a mod_M b) div_M b)
