Project

General

Profile

Bug #65

integer division (euclidein division)

Added by Hamza Bourbouh 10 months ago. Updated 9 months ago.

Status:
Closed
Priority:
High
Category:
Bug
Start date:
05/08/2018
Due date:
% Done:

0%


Description

node top(x, y:int)
returns(z:int);
let
z = x/y;
tel

This is translated as x/y in C, which is different from Simulink coder approch (verifying the sign of numerator and denominator).
top(-4, 3) Simulink/Kind2 is giving -2 and Lustrec is giving -1.
-4 = 3*(-2) + 2; or -4 = 3*(-1) -1;
I think the modulo should be positive. So I go with Simulink/Kind2 result.

History

#1 Updated by Pierre-Loïc Garoche 10 months ago

Comment

Considering producing valid integer division and modulo instead of C ones. To be discussed.

#2 Updated by Hamza Bourbouh 9 months ago

  • Status changed from New to Closed
Comment

Solved in unstable branch

Also available in: Atom PDF