ACSL Language Reference 1.9 с указанием, какие возможности ACSL не реализованы в Frama-C из проекта Astraver (1185160), страница 4
Текст из файла (страница 4)
LOGIC EXPRESSIONS• |d × q| ≤ |n|, and |q| is maximal for this property;• q is zero if |n| < |d|;• q is positive if |n| ≥ |d| and n and d have the same sign;• q is negative if |n| ≥ |d| and n and d have opposite signs;• q × d + r = n;• |r| < |d|;• r is zero or has the same sign as n.Example 2.2 The following examples illustrate the results of division and modulo dependingon the sign of their arguments:• 5/3 is 1 and 5%3 is 2;• (-5)/3 is -1 and (-5)%3 is -2;• 5/(-3) is -1 and 5%(-3) is 2;• (-5)/(-3) is 1 and (-5)%(-3) is -2.Hexadecimal octal and binary constantsHexadecimal, octal and binary constants are always non-negative.
Suffixes u and l for Cconstants are allowed but meaningless.Casts and overflowsIn logic expressions, casting from mathematical integers to an integral C type t (such as char ,short , int , etc.) is allowed and is interpreted as follows: the result is the unique value of thecorresponding type that is congruent to the mathematical result modulo the cardinal of thistype, that is 28× sizeof (t) .Example 2.3 (unsigned char)1000 is 1000 mod 256 i.e. 232.To express in the logic the value of a C expression, one has to add all the necessarycasts. For example, the logic expression denoting the value of the C expression x*y+z is( int )((int)(x*y)+z). Note that there is no implicit cast from integers to C integral types.Example 2.4 The declaration//@ logic int f(int x) = x+1 ;is not allowed because x+1, which is a mathematical integer, must be casted to int .
One shouldwrite either//@ logic integer f(int x) = x+1 ;or//@ logic int f(int x) = (int)(x+1) ;21CHAPTER 2. SPECIFICATION LANGUAGEQuantification on C integral typesQuantification over a C integral type corresponds to integer quantification over the corresponding interval.Example 2.5 Thus the formula\forall char c; c <= 1000is equivalent to\forallinteger c; CHAR_MIN <= c <= CHAR_MAX ==> c <= 1000where the the bounds CHAR_MIN and CHAR_MAX are defined in limits.hSize of C integer typesThe size of C types is architecture-dependent. ACSL does not enforce these sizes either,hence the semantics of terms involving such types is also architecture-dependent.
The sizeofoperator may be used in annotations and is consistent with its C counterpart. For instance,it should be possible to verify the following code:12/*@ ensures \result <= sizeof ( int ); */int f() { return sizeof (char); }Constants giving maximum and minimum values of those types may be provided in a library.Enum typesEnum types are also interpreted as mathematical integers. Casting an integer into an enumin the logic gives the same result as if the cast was performed in the C code.Bitwise operationsLike arithmetic operations, bitwise operations apply to any mathematical integer: any mathematical integer has a unique infinite 2-complement binary representation with infinitelymany zeros (for non-negative numbers) or ones (for negative numbers) on the left.
Bitwiseoperations apply to this representation.Example 2.6• 7 & 12 == · · ·00111 & · · ·001100 == · · ·00100 == 4• -8 | 5 == · · ·11000 | · · ·00101 == · · ·11101 == -3• ~5 == ~· · · 00101 == · · ·111010 == -6• -5 << 2 == · · ·11011 << 2 == · · ·11101100 == -20• 5 >> 2 == · · ·00101 >> 2 == · · ·0001 == 1• -5 >> 2 == · · ·11011 >> 2 == · · ·1110 == -2222.2.
LOGIC EXPRESSIONS2.2.5Real numbers and floating point numbersFloating-point constants and operations are interpreted as mathematical real numbers: aC variable of type float or double is implicitly promoted to a real. Integers are promotedto reals if necessary. Usual binary operations are interpreted as operators on real numbers,hence they never involve any rounding nor overflow.Example 2.7 In an annotation, 1e+300 * 1e+300 is equal to 1e+600, even if that last numberexceeds the largest representable number in double precision: there is no "overflow".2 ∗ 0.1 is equal to the real number 0.2, and not to any of its floating-point approximation:there is no "rounding".Unlike the promotion of C integer types to mathematical integers, there are special floatvalues which do not naturally map to a real number, namely the IEEE-754 special values for“not-a-number”, +∞ and −∞.
See below for a detailed discussion on such special values.However, remember that ACSL’s logic has only total functions. Thus, there are implicitpromotion functions real_of_float and real_of_double whose results on the 3 values aboveis left unspecified.In logic, real literals can also be expressed under the hexadecimal form of C99: 0xhh.hhp±ddwhere h are hexadecimal digits and dd is in decimal, denotes number hh.hh × 2dd , e.g.0x1.Fp-4 is (1 + 15/16) × 2−4 .Usual operators for comparison are interpreted as real operators too. In particular,equality operation ≡ of float (or double) expressions means equality of the real numbersthey represent respectively.
Or equivalently, x ≡ y for x, y two float variables meansreal_of_float(x) ≡ real_of_float(y) with the mathematical equality of real numbers.Special predicates are also available to express the comparison operators of float (resp. double) numbers as in C: \eq_float , \gt_float , \ge_float , \le_float , \lt_float , \ne_float (resp. fordouble).Casts, infinity and NaNsCasting from a C integer type or a float type to a float or a double is as in C: the sameconversion operations apply.Conversion of real numbers to float or double values indeed depends on various possiblerounding modes defined by the IEEE 754 standard [24, 26].
These modes are defined by alogic type (see section 2.6.8):/*@ type rounding_mode = \Up | \Down | \ToZero | \NearestAway | \NearestEven;*/Then rounding a real number can be done explicitly using functionslogic float \round_float(rounding_mode m, real x);logic double \round_double(rounding_mode m, real x);Cast operators ( float ) and (double) applied to a mathematical integer or real number x areequivalent to apply rounding functions above with the nearest-even rounding mode (which isthe default rounding mode in C programs) If the source real number is too large, this mayalso result into one of the special values +infinity and -infinity.23CHAPTER 2.
SPECIFICATION LANGUAGEExample 2.8 We have ( float )0.10.10000000149011611938476562513421773 × 2−27≡whichisequaltoNotice also that unlike for integers, suffixes f and l are meaningful, because they implicitlyadd a cast operator as above.This semantics of casts ensures that the float result r of a C operation e1 op e2 on floats, ifthere is no overflow and if the default rounding mode is not changed in the program, has thesame real value as the logic expression ( float )(e1 op e2 ).
Notice that this is not true for theequality \eq_float of floats: -0.0 + -0.0 in C is equal to the float number -0.0, which is not\eq_float to 0.0, which is the value of the logic expression ( float )(-0.0 + -0.0).Finally, additional predicates are provided on float and double numbers, which check thattheir argument is NaN or a finite number respectively:1234predicate \is_NaN(float x);predicate \is_NaN(double x);predicate \is_finite ( float x);predicate \is_finite (double x);QuantificationQuantification over a variable of type real is of course usual quantification over real numbers.Quantification over float (resp.
double) types is allowed too, and is supposed to range overall real numbers representable as floats (resp doubles). In particular, this does not includeNaN, +infinity and -infinity in the considered range.Mathematical functionsClassical mathematical operations like exponential, sine, cosine, and such are available asbuilt-in:integer \min(integer x, integer y) ;integer \max(integer x, integer y) ;real \min(real x, real y) ;real \max(real x, real y) ;integer \abs( integer x) ;real \abs( real x) ;real \sqrt ( real x) ;real \pow(real x, real y) ;integer \ceil ( real x) ;integer \floor ( real x) ;real \exp( real x) ;real \log( real x) ;real \log10( real x) ;real \cos( real x) ;real \sin( real x) ;real \tan( real x) ;real \cosh( real x) ;real \sinh( real x) ;242.2. LOGIC EXPRESSIONSreal \tanh( real x) ;real \acos( real x) ;real \asin( real x) ;real \atan( real x) ;real \atan2( real y, real x) ;real \hypot( real x, real y) ;Exact computationsIn order to specify properties of rounding errors, it is useful to express something about theso-called exact computations [3]: the computations that would be performed in an ideal modewhere variables denote true real numbers.To express such exact computations, two special constructs exist in annotations:• \exact(x) denotes the value of the C variable x (or more generally any C left-value) asif the program was executed with ideal real numbers.• \round_error(x) is a shortcut for |x − \exact(x)|Example 2.9 Here is an example of a naive approximation of cosine [2]./*@ requires \abs(\exact(x)) <= 0x1p-5;@ requires \round_error(x) <= 0x1p-20;@ ensures \abs(\exact( \result ) - \cos(\exact(x))) <= 0x1p-24;@ ensures \round_error( \result ) <= \round_error(x) + 0x3p-24;@*/float cosine(float x) {return 1.0f - x * x * 0.5f;}2.2.6C arrays and pointersAddress operator, array access, pointer arithmetic and dereferencingThese operators are similar to their corresponding C operators.address-of operator should be used with caution.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
