/*
* Copyright (c) 2005-2006 Institute for System Programming
* Russian Academy of Sciences
* All rights reserved.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*/
/*
* Portions of this text are reprinted and reproduced in electronic form
* from IEEE Std 1003.1, 2004 Edition, Standard for Information Technology
* -- Portable Operating System Interface (POSIX), The Open Group Base
* Specifications Issue 6, Copyright (C) 2001-2004 by the Institute of
* Electrical and Electronics Engineers, Inc and The Open Group. In the
* event of any discrepancy between this version and the original IEEE and
* The Open Group Standard, the original IEEE and The Open Group Standard
* is the referee document. The original Standard can be obtained online at
* http://www.opengroup.org/unix/online.html.
*/
#include "math/integer/integer_model.seh"
#include <limits.h>
#pragma SEC subsystem integer "math.integer"
/*
The group of functions 'math.integer' consists of:
abs [1]
div [1]
imaxabs [1]
imaxdiv [1]
labs [1]
ldiv [1]
llabs [1]
lldiv [1]
*/
/********************************************************************/
/** Interface Functions **/
/********************************************************************/
/*
Linux Standard Base Core Specification 3.1
Copyright (c) 2004, 2005 Free Standards Group
refers
The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved.
NAME
abs - return an integer absolute value
SYNOPSIS
#include <stdlib.h>
int abs(int i);
DESCRIPTION
The functionality described on this reference page is aligned with the
ISO C standard. Any conflict between the requirements described here and
the ISO C standard is unintentional. This volume of IEEE Std 1003.1-2001
defers to the ISO C standard.
The abs() function shall compute the absolute value of its integer
operand, i. If the result cannot be represented, the behavior is undefined.
RETURN VALUE
The abs() function shall return the absolute value of its integer operand.
*/
specification
IntT abs_spec( CallContext context, IntT i )
{
pre
{
/* If the result cannot be represented, the behavior is undefined. */
/* [INFORMATIVE SECTION: APPLICATION USAGE]
* [In two's-complement representation, the absolute value of the negative
* integer with largest magnitude {INT_MIN} might not be representable.]
*/
/* [Checking is implicit to avoid overflow] */
REQ("app.abs.02","Absolute value shall be representable", (i >= 0) || (i + max_IntT) >=0 );
return true;
}
coverage C
{
if( i==0 )
return { Zero, "Zero parameter" };
else if( i>0 )
{
if( i==max_IntT )
return { IntMax, "INT_MAX" };
return { Positive, "Positive value" };
}
else /* [i<0] */
return { Negative, "Negative value" };
}
post
{
/* The abs() function shall compute the absolute value of its integer operand, i. */
/* [Function shall return non-negative result] */
REQ("abs.01", "Function shall return non-negative result", abs_spec >=0 );
if( i>=0 )
{
/* [For non-negative i function abs() shall return i] */
REQ( "abs.01","For non-negative i function abs() shall return i", i==abs_spec );
}
else
{
/* [For negative i expression i+abs(i) shall equal to zero] */
REQ( "abs.01", "For negative i expression i+abs(i) shall equal to zero", i+abs_spec == 0 );
}
return true;
}
}
/*
Linux Standard Base Core Specification 3.1
Copyright (c) 2004, 2005 Free Standards Group
refers
The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved.
NAME
div - compute the quotient and remainder of an integer division
SYNOPSIS
#include <stdlib.h>
div_t div(int numer, int denom);
DESCRIPTION
The functionality described on this reference page is aligned with the ISO
C standard. Any conflict between the requirements described here and the
ISO C standard is unintentional. This volume of IEEE Std 1003.1-2001 defers
to the ISO C standard.
The div() function shall compute the quotient and remainder of the division
of the numerator numer by the denominator denom. If the division is
inexact, the resulting quotient is the integer of lesser magnitude that is
the nearest to the algebraic quotient. If the result cannot be represented,
the behavior is undefined; otherwise, quot* denom+ rem shall equal numer.
RETURN VALUE
The div() function shall return a structure of type div_t, comprising both
the quotient and the remainder. The structure includes the following
members, in any order:
int quot; / * quotient * /
int rem; / * remainder * /
*/
specification
DivT * div_spec( CallContext context, IntT numer, IntT denom )
{
pre
{
/* If the result cannot be represented, the behavior is undefined; */
/* [In two's-complement representation (INT_MIN/-1) may be greater than INT_MAX] */
REQ("app.div.02","Shall not divide INT_MIN into -1", (numer!=min_IntT) || (denom!=-1) );
/* [The denominator shall be non zero] */
REQ("app.div.02","The denominator is non zero", denom != 0);
return true;
}
coverage C
{
if ( numer == 0 )
return { NumerZero, "The numerator is zero" };
else
if ( numer > 0 )
{
if( numer == max_IntT )
return { NumerMAX , "The numerator is INT_MAX"};
if( denom > 0 )
{
if ( denom == max_IntT )
return {NumerPositiveDenomIntMax, "The numerator is positive, the denominator is INT_MAX"};
return { NumerPositiveDenomPositive, "The numerator is positive, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_IntT )
return {NumerPositiveDenomIntMin, "The numerator is positive, the denominator is INT_MIN" };
return { NumerPositiveDenomNegative, "The numerator is positive, the denominator is negatve" };
}
}
else
if ( numer < 0 )
{
if( numer == min_IntT )
return { NumerMIN , "The numerator is INT_MIN"};
if( denom > 0 )
{
if ( denom == max_IntT )
return {NumerNegativeDenomIntMax, "The numerator is negative, the denominator is INT_MAX"};
return { NumerNegativeDenomPositive, "The numerator is negative, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_IntT )
return {NumerNegativeDenomIntMin, "The numerator is negative, the denominator is INT_MIN"};
return { NumerNegativeDenomNegative, "The numerator is negative, the denominator is negative" };
}
}
}
post
{
/* If the division is inexact, the resulting quotient is the integer of
* lesser magnitude that is the nearest to the algebraic quotient.
*/
/* [Therefore, the numerator and the remainder shall have the same sign] */
if( numer == 0 )
{
REQ("div.05","Reminder shall be zero", div_spec->rem == 0);
}
else if( numer > 0 )
{
REQ("div.05","The numerator and the remainder shall have the same sign", div_spec->rem >= 0);
}
else /* [if( numer < 0 )] */
{
REQ("div.05","The numerator and the remainder shall have the same sign", div_spec->rem <= 0);
}
/* [The remainder shall be less than the denominator by absolute value] */
if( denom<0 )
{
REQ("div.05","The remainder shall be less than the denominator by absolute value", div_spec->rem > denom );
}
else
{
REQ("div.05","The remainder shall be less than the denominator by absolute value", div_spec->rem < denom );
}
/* quot* denom+ rem shall equal numer. */
/* [Checking is implicit to avoid overflow.
* We check the remainder and the quotient separately. % operator is used for calculating the remainder,
* integer division is used for calculating the quotient] */
/* [Checking the remainder] */
REQ("div.03","rem shall equal numer % denom", div_spec->rem == numer % denom);
/* [Checking the quotient] */
REQ("div.03","quot shall equal (numer- rem)/denom", div_spec->quot == (numer-div_spec->rem) / denom);
/* The div() function shall compute the quotient and remainder of the division of the numerator numer
* by the denominator denom.
*/
/* [This requirement is already checked due to {div.03}] */
REQ("div.01","div() shall compute the quotient and remainder",true);
return true;
/* The div() function shall return a structure of type div_t, comprising both the quotient and the remainder.
*/
/* [This requirement is already checked due to {div.03}] */
REQ("div.04","div() shall return the structure, comprising the quotient and the remainder",true);
return true;
}
}
/*
Linux Standard Base Core Specification 3.1
Copyright (c) 2004, 2005 Free Standards Group
refers
The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved.
NAME
imaxabs - return absolute value
SYNOPSIS
#include <inttypes.h>
intmax_t imaxabs(intmax_t j);
DESCRIPTION
The functionality described on this reference page is aligned with the ISO
C standard. Any conflict between the requirements described here and the
ISO C standard is unintentional. This volume of IEEE Std 1003.1-2001 defers
to the ISO C standard.
The imaxabs() function shall compute the absolute value of an integer j. If
the result cannot be represented, the behavior is undefined.
RETURN VALUE
The imaxabs() function shall return the absolute value.
*/
specification
IntMaxT imaxabs_spec( CallContext context, IntMaxT i )
{
pre
{
/* If the result cannot be represented, the behavior is undefined. */
/* [In two's-complement representation, the absolute value of the negative
* integer with largest magnitude {INTMAX_MIN} might not be representable.]
*/
/* If the result cannot be represented, the behavior is undefined. */
/* [Checking is implicit to avoid overflow] */
REQ( "app.imaxabs.02","Absolute value shall be representable", (i >= 0) || (i + max_IntMaxT >=0 ) );
return true;
}
coverage C
{
if( i==0 )
return { Zero, "Zero parameter" };
else if( i>0 )
{
if( i==max_IntMaxT )
return { IntMaxMax, "INTMAX_MAX" };
return { Positive, "Positive value" };
}
else /* [if( i<0 )] */
{
return { Negative, "Negative value" };
}
}
post
{
/* The imaxabs() function shall compute the absolute value of an integer j. */
/* [Function shall return non-negative result] */
REQ( "imaxabs.01","Function shall return non-negative result", imaxabs_spec >=0 );
if( i>=0 )
{
/* [For non-negative i function imaxabs() shall return i] */
REQ( "imaxabs.01","For non-negative i function imaxabs() shall return i", i == imaxabs_spec );
}
else
{
/* [For negative i expression i+imaxabs(i) shall equal to zero] */
REQ( "imaxabs.01","For negative i expression i+imaxabs(i) shall equal to zero", i + imaxabs_spec == 0 );
}
return true;
}
}
/*
Linux Standard Base Core Specification 3.1
Copyright (c) 2004, 2005 Free Standards Group
refers
The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved.
NAME
imaxdiv - return quotient and remainder
SYNOPSIS
#include <inttypes.h>
imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom);
DESCRIPTION
[CX] The functionality described on this reference page is aligned with
the ISO C standard. Any conflict between the requirements described here
and the ISO C standard is unintentional. This volume of IEEE Std
1003.1-2001 defers to the ISO C standard.
The imaxdiv() function shall compute numer / denom and numer % denom in a
single operation.
RETURN VALUE
The imaxdiv() function shall return a structure of type imaxdiv_t,
comprising both the quotient and the remainder. The structure shall contain
(in either order) the members quot (the quotient) and rem (the remainder),
each of which has type intmax_t.
If either part of the result cannot be represented, the behavior is
undefined.
*/
specification
IMaxDivT * imaxdiv_spec( CallContext context, IntMaxT numer, IntMaxT denom )
{
pre
{
/* If either part of the result cannot be represented, the behavior is undefined. */
/* [In two's-complement representation (INTMIN_MIN/-1) may be greater than INTMIN_MAX] */
REQ("app.imaxdiv.03","Shall not divide INTMAX_MIN into -1", (numer!=min_IntMaxT) || (denom!=-1) );
/* [The denominator shall be non zero] */
REQ("app.imaxdiv.03","The denominator is non zero", denom != 0);
return true;
}
coverage C
{
if ( numer == 0 )
{
return { NumerZero, "The numerator is zero" };
}
else if ( numer > 0 )
{
if( numer == max_IntMaxT )
return { NumerMAX , "The numerator is INTMAX_MAX"};
if( denom > 0 )
{
if ( denom == max_IntMaxT )
return {NumerPositiveDenomIntMax, "The numerator is positive, the denominator is INTMAX_MAX"};
return { NumerPositiveDenomPositive, "The numerator is positive, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_IntMaxT )
return {NumerPositiveDenomIntMin, "The numerator is positive, the denominator is INTMAX_MIN" };
return { NumerPositiveDenomNegative, "The numerator is positive, the denominator is negatve" };
}
}
else if ( numer < 0 )
{
if( numer == min_IntMaxT )
return { NumerMIN , "The numerator is INTMAX_MIN"};
if( denom > 0 )
{
if ( denom == max_IntMaxT )
return {NumerNegativeDenomIntMax, "The numerator is negative, the denominator is INTMAX_MAX"};
return { NumerNegativeDenomPositive, "The numerator is negative, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_IntMaxT )
return {NumerNegativeDenomIntMin, "The numerator is negative, the denominator is INTMAX_MIN"};
return { NumerNegativeDenomNegative, "The numerator is negative, the denominator is negative" };
}
}
}
post
{
/* The imaxdiv() function shall compute numer / denom and numer % denom in a single operation.*/
/* [Therefore, the numerator and the remainder shall have the same sign] */
if( numer == 0 )
{
REQ("imaxdiv.01","Reminder shall be zero", imaxdiv_spec->rem == 0);
}
else if( numer > 0 )
{
REQ("imaxdiv.01","The numerator and the remainder shall have the same sign", imaxdiv_spec->rem >= 0);
}
else /* [if( numer < 0 )] */
{
REQ("imaxdiv.01","The numerator and the remainder shall have the same sign", imaxdiv_spec->rem <= 0);
}
/* [And the remainder shall be less than the denominator by absolute value] */
if( denom<0 )
{
REQ("imaxdiv.01","The remainder shall be less than the denominator by absolute value", imaxdiv_spec->rem > denom );
}
else
{
REQ("imaxdiv.01","The remainder shall be less than the denominator by absolute value", imaxdiv_spec->rem < denom );
}
/* [Checking is implicit to avoid overflow
* We check the remainder and the quotient separately. % operator is used for calculating the remainder,
* integer division is used for calculating the quotient] */
/* [Checking the remainder] */
REQ("imaxdiv.01","quot* denom+ rem shall equal numer", imaxdiv_spec->rem == numer % denom);
/* [Checking the quotient] */
REQ("imaxdiv.01","quot shall equal (numer- rem)/denom", imaxdiv_spec->quot == (numer-imaxdiv_spec->rem) / denom);
return true;
}
}
/*
Linux Standard Base Core Specification 3.1
Copyright (c) 2004, 2005 Free Standards Group
refers
The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved.
NAME
labs, llabs - return a long integer absolute value
SYNOPSIS
#include <stdlib.h>
long labs(long i);
long long llabs(long long i);
DESCRIPTION
The functionality described on this reference page is aligned with the ISO
C standard. Any conflict between the requirements described here and the
ISO C standard is unintentional. This volume of IEEE Std 1003.1-2001 defers
to the ISO C standard.
The labs() function shall compute the absolute value of the long integer
operand i. The llabs() function shall compute the absolute value of the
long long integer operand i. If the result cannot be represented, the
behavior is undefined.
RETURN VALUE
The labs() function shall return the absolute value of the long integer
operand. The labs() function shall return the absolute value of the long
long integer operand.
*/
specification
LongT labs_spec( CallContext context, LongT i )
{
pre
{
/* If the result cannot be represented, the behavior is undefined. */
/* [In two's-complement representation, the absolute value of the negative
* long integer with largest magnitude {LONG_MIN} might not be
* representable.]
*/
/* [Checking is implicit to avoid overflow] */
REQ( "app.labs.03","Absolute value shall be representable", (i >= 0) || (i + max_LongT >=0 ) );
return true;
}
coverage C
{
if( i==0 )
return { Zero, "Zero parameter" };
else if( i>0 )
{
if( i==max_LongT )
return { LongMax, "LONG_MAX" };
return { Positive, "Positive value" };
}
else /* [if( i<0 )] */
{
return { Negative, "Negative value" };
}
}
post
{
/* The labs() function shall compute the absolute value of the long integer operand i. */
/* [Function shall return non-negative result] */
REQ( "labs.01","Function shall return non-negative result", labs_spec >=0 );
/* The labs() function shall return the absolute value of its long integer
* operand.
*/
if( i>=0 )
{
/* [For non-negative i function labs() shall return i] */
REQ( "labs.01","For positve i function labs() shall return i", i==labs_spec );
}
else
{
/* [For negative i expression i+labs(i) shall equal to zero] */
REQ( "labs.01","For negative i expression i+labs(i) shall equal to zero", i+labs_spec == 0 );
}
return true;
}
}
specification
LLongT llabs_spec( CallContext context, LLongT i )
{
pre
{
/* If the result cannot be represented, the behavior is undefined. */
/* [In two's-complement representation, the absolute value of the negative
* long long integer with largest magnitude {LLONG_MIN} might not be
* representable.]
*/
/* If the result cannot be represented, the behavior is undefined. */
/* [Checking is implicit to avoid overflow] */
REQ( "app.llabs.03","Absolute value shall be representable", (i >= 0) || (i + max_LLongT >=0 ) );
return true;
}
coverage C
{
if( i==0 )
return { Zero, "Zero parameter" };
else if( i>0 )
{
if( i==max_LLongT )
return { LLongMax, "LLONG_MAX" };
return { Positive, "Positive value" };
}
else /* [if( i<0 )] */
{
return { Negative, "Negative value" };
}
}
post
{
/* The llabs() function shall compute the absolute value of the long long integer operand i. */
/* [Function shall return non-negative result] */
REQ( "llabs.01","Function shall return non-negative result", llabs_spec >=0 );
/* The llabs() function shall return the absolute value of its long long
* integer operand.
*/
if( i>=0 )
{
/* [For non-negative i function llabs() shall return i] */
REQ( "llabs.01","For positve i function llabs() shall return i", i==llabs_spec );
}
else
{
/* [For negative i expression i+llabs(i) shall equal to zero] */
REQ( "llabs.01","For negative i expression i+llabs(i) shall equal to zero", i+llabs_spec == 0 );
}
return true;
}
}
/*
Linux Standard Base Core Specification 3.1
Copyright (c) 2004, 2005 Free Standards Group
refers
The Open Group Base Specifications Issue 6
IEEE Std 1003.1, 2004 Edition
Copyright (c) 2001-2004 The IEEE and The Open Group, All Rights reserved.
NAME
ldiv, lldiv - compute quotient and remainder of a long division
SYNOPSIS
#include <stdlib.h>
ldiv_t ldiv(long numer, long denom);
lldiv_t lldiv(long long numer, long long denom);
DESCRIPTION
The functionality described on this reference page is aligned with the ISO
C standard. Any conflict between the requirements described here and the
ISO C standard is unintentional. This volume of IEEE Std 1003.1-2001 defers
to the ISO C standard.
These functions shall compute the quotient and remainder of the division of
the numerator numer by the denominator denom. If the division is inexact,
the resulting quotient is the long integer (for the ldiv() function) or
long long integer (for the lldiv() function) of lesser magnitude that is
the nearest to the algebraic quotient. If the result cannot be represented,
the behavior is undefined; otherwise, quot * denom+rem shall equal numer.
RETURN VALUE
The ldiv() function shall return a structure of type ldiv_t, comprising
both the quotient and the remainder. The structure shall include the
following members, in any order:
long quot; / * Quotient * /
long rem; / * Remainder * /
The lldiv() function shall return a structure of type lldiv_t, comprising
both the quotient and the remainder. The structure shall include the
following members, in any order:
long long quot; / * Quotient * /
long long rem; / * Remainder * /
*/
specification
LDivT * ldiv_spec( CallContext context, LongT numer, LongT denom )
{
pre
{
/* If the result cannot be represented, the behavior is undefined */
/* [In two's-complement representation (LONG_MIN/-1) may be greater than LONG_MAX] */
REQ("app.ldiv.03","Shall not divide LONG_MIN into -1", (numer!=min_LongT) || (denom!=-1) );
/* [The denominator shall be non zero] */
REQ("app.ldiv.03","The denominator is non zero", denom != 0);
return true;
}
coverage C
{
if ( numer == 0 )
{
return { NumerZero, "The numerator is zero" };
}
else if ( numer > 0 )
{
if( numer == max_LongT )
return { NumerMAX , "The numerator is LONG_MAX"};
if( denom > 0 )
{
if ( denom == max_LongT )
return {NumerPositiveDenomIntMax, "The numerator is positive, the denominator is LONG_MAX"};
return { NumerPositiveDenomPositive, "The numerator is positive, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_LongT )
return {NumerPositiveDenomIntMin, "The numerator is positive, the denominator is LONG_MIN" };
return { NumerPositiveDenomNegative, "The numerator is positive, the denominator is negatve" };
}
}
else /* [if ( numer < 0 )] */
{
if( numer == min_LongT )
return { NumerMIN , "The numerator is LONG_MIN"};
if( denom > 0 )
{
if ( denom == max_LongT )
return {NumerNegativeDenomIntMax, "The numerator is negative, the denominator is LONG_MAX"};
return { NumerNegativeDenomPositive, "The numerator is negative, the denominator is positive" };
}
else
{ /* denom < 0 */
if ( denom == min_LongT )
return {NumerNegativeDenomIntMin, "The numerator is negative, the denominator is LONG_MIN"};
return { NumerNegativeDenomNegative, "The numerator is negative, the denominator is negative" };
}
}
}
post
{
/* If the division is inexact, the resulting quotient is the long
* integer (for the ldiv() function) or long long integer (for the
* lldiv() function) of lesser magnitude that is the nearest to the
* algebraic quotient.
*/
/* [Therefore, the numerator and the remainder shall have the same sign] */
if( numer == 0 )
{
REQ("ldiv.02","Reminder shall be zero", ldiv_spec->rem == 0);
}
else if( numer > 0 )
{
REQ("ldiv.02","The numerator and the remainder shall have the same sign", ldiv_spec->rem >= 0);
}
else /* [if( numer < 0 )] */
{
REQ("ldiv.02","The numerator and the remainder shall have the same sign", ldiv_spec->rem <= 0);
}
/* [The remainder shall be less than the denominator by absolute value] */
if( denom<0 )
{
REQ("ldiv.02","The remainder shall be less than the denominator by absolute value", ldiv_spec->rem > denom );
}
else
{
REQ("ldiv.02","The remainder shall be less than the denominator by absolute value", ldiv_spec->rem < denom );
}
/* quot* denom+ rem shall equal numer */
/* [Checking is implicit to avoid overflow
* We check the remainder and the quotient separately. % operator is used for calculating the remainder,
* integer division is used for calculating the quotient] */
/* [Checking the remainder] */
REQ("ldiv.04","quot* denom+ rem shall equal numer", ldiv_spec->rem == numer % denom);
/* [Checking the quotient] */
REQ("ldiv.04","quot shall equal (numer- rem)/denom", ldiv_spec->quot == (numer-ldiv_spec->rem) / denom);
/* These functions shall compute the quotient and remainder of the division of the numerator numer
* by the denominator denom.
*/
/* [This requirement is already checked due to {ldiv.04}] */
REQ("ldiv.01","ldiv() shall compute the quotient and remainder",true);
return true;
}
}
specification
LLDivT * lldiv_spec( CallContext context, LLongT numer, LLongT denom )
{
pre
{
/* If the result cannot be represented, the behavior is undefined; */
/* [In two's-complement representation (LLONG_MIN/-1) may be greater than LLONG_MAX] */
REQ("app.lldiv.03","Shall not divide LLONG_MIN into -1", (numer!=min_LLongT) || (denom!=-1) );
/* [The denominator shall be non zero] */
REQ("app.lldiv.03","The denominator is non zero", denom != 0);
return true;
}
coverage C
{
if ( numer == 0 )
{
return { NumerZero, "The numerator is zero" };
}
else if ( numer > 0 )
{
if( numer == max_LLongT )
return { NumerMAX , "The numerator is LLONG_MAX"};
if( denom > 0 )
{
if ( denom == max_LLongT )
return {NumerPositiveDenomIntMax, "The numerator is positive, the denominator is LLONG_MAX"};
return { NumerPositiveDenomPositive, "The numerator is positive, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_LLongT )
return {NumerPositiveDenomIntMin, "The numerator is positive, the denominator is LLONG_MIN" };
return { NumerPositiveDenomNegative, "The numerator is positive, the denominator is negatve" };
}
}
else /* if ( numer < 0 ) */
{
if( numer == min_LLongT )
return { NumerMIN , "The numerator is LLONG_MIN"};
if( denom > 0 )
{
if ( denom == max_LLongT )
return {NumerNegativeDenomIntMax, "The numerator is negative, the denominator is LLONG_MAX"};
return { NumerNegativeDenomPositive, "The numerator is negative, the denominator is positive" };
}
else
{ /* [denom < 0] */
if ( denom == min_LLongT )
return {NumerNegativeDenomIntMin, "The numerator is negative, the denominator is LLONG_MIN"};
return { NumerNegativeDenomNegative, "The numerator is negative, the denominator is negative" };
}
}
}
post
{
/* If the division is inexact, the resulting quotient is the long
* integer (for the ldiv() function) or long long integer (for the
* lldiv() function) of lesser magnitude that is the nearest to the
* algebraic quotient.
*/
/* [Therefore, the numerator and the remainder shall have the same sign] */
if( numer == 0 )
{
REQ("lldiv.02","Reminder shall be zero", lldiv_spec->rem == 0);
}
else if( numer > 0 )
{
REQ("lldiv.02","The numerator and the remainder shall have the same sign", lldiv_spec->rem >= 0);
}
else /* [if( numer < 0 )] */
{
REQ("lldiv.02","The numerator and the remainder shall have the same sign", lldiv_spec->rem <= 0);
}
/* [The remainder shall be less than the denominator by absolute value] */
if( denom<0 )
{
REQ("lldiv.02","The remainder shall be less than the denominator by absolute value", lldiv_spec->rem > denom );
}
else
{
REQ("lldiv.02","The remainder shall be less than the denominator by absolute value", lldiv_spec->rem < denom );
}
/* quot* denom+ rem shall equal numer */
/* [Checking is implicit to avoid overflow
* We check the remainder and the quotient separately. % operator is used for calculating the remainder,
* integer division is used for calculating the quotient] */
/* [Checking the remainder] */
REQ("lldiv.04","quot* denom+ rem shall equal numer", lldiv_spec->rem == numer % denom);
/* [Checking the quotient] */
REQ("lldiv.04","quot shall equal (numer- rem)/denom", lldiv_spec->quot == (numer-lldiv_spec->rem) / denom);
/* These functions shall compute the quotient and remainder of the division of the numerator numer
* by the denominator denom.
*/
/* [This requirement is already checked due to {lldiv.04}] */
REQ("lldiv.01","lldiv() shall compute the quotient and remainder",true);
return true;
}
}
/********************************************************************/
/** Specification Types **/
/********************************************************************/
specification typedef struct DivT DivT = {};
specification
typedef struct IMaxDivT IMaxDivT = {};
specification
typedef struct LDivT LDivT = {};
specification
typedef struct LLDivT LLDivT = {};
/********************************************************************/
/** Helper Functions **/
/********************************************************************/
DivT* create_DivTObj( IntT quot, IntT rem )
{
return create( &type_DivT, quot, rem );
}
IMaxDivT* create_IMaxDivTObj( IntMaxT quot, IntMaxT rem )
{
return create( &type_IMaxDivT, quot, rem );
}
LDivT* create_LDivTObj( LongT quot, LongT rem )
{
return create( &type_LDivT, quot, rem );
}
LLDivT* create_LLDivTObj( LLongT quot, LLongT rem )
{
return create( &type_LLDivT, quot, rem );
}
Specifications source code for LSB Core 3.1