Nikolai Kosmatov
email: nikolaikosmatov@gmail.com

Fonenantsoa Maurica

Julien Signoles

Efficient Runtime Assertion Checking for Properties over Mathematical Numbers

Keywords: typing, runtime assertion checking, numerical properties, rational numbers, optimized code generation

Runtime assertion checking is the discipline of detecting at runtime violations of program properties written as formal code annotations. These properties often include numerical properties, which may rely on either (bounded) machine representations or (unbounded) mathematical numbers. The verification of the former is easier to implement and more efficient at runtime, while the latter are more expressive and often more adequate for writing specifications. This short paper explains how the runtime assertion checker E-ACSL reconciles both approaches by presenting a type system that allows the tool to generate efficient machine-number based code when it is safe to do so, while generating arbitrary-precision code when it is necessary. This type system and the code generator not only handle integers but also rational arithmetics. As far as we know, it is the first runtime verification tool that supports the verification of properties over rational numbers.

Introduction

Runtime assertion checking is the discipline of detecting at runtime violations of program properties written as formal code annotations [START_REF] Clarke | A Historical Perspective on Runtime Assertion Checking in Software Development[END_REF][START_REF] Kosmatov | A Lesson on Runtime Assertion Checking with Frama-C[END_REF]. This way, it allows the developer to better support testing, to make debugging easier by reducing the distance between the execution of a bug and the manifestation of its effects, to serve as executable comments about preconditions and postconditions 1 , and can act as an intermediate step before applying formal proof. Its main drawback is the slowdown of the program execution. It may also lead to additional runtime failures when used incorrectly by a developer.

Formal code annotations usually express properties about program variables or/and program inputs and outputs. Most of them are mathematical properties or, at least, involve some mathematical operations. The semantics of these properties may involve either bounded machine representations (e.g., machine integers and floating-point numbers), or unbounded mathematical numbers (e.g., mathematical integers in Z and real numbers in R). The former one allows for efficient runtime checking and remains close to the semantics of the underlying programming language, so easy to grasp for a developer. However, it is less expressive than the latter and, most often, it does not correspond to the informal specifications that writers or readers have in mind because they usually think in terms of usual mathematics [START_REF] Chalin | JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics[END_REF]. It can lead to incorrect specifications [START_REF] Chalin | Improving JML: For a Safer and More Effective Language[END_REF]. Yet the latter is harder to implement and leads to less efficient code [START_REF] Delahaye | Common Specification Language for Static and Dynamic Analysis of C Programs[END_REF].

The oldest formal specification languages such as Eiffel [START_REF] Meyer | Eiffel: The Language[END_REF] and Spec# [START_REF] Barnett | The Spec# Programming System: An Overview[END_REF] rely on a bounded semantics. JML [START_REF] Leavens | In: JML: A Notation for Detailed Design[END_REF] historically used this semantics but now accepts three different modes (bounded integers with modulo when overflowing, bounded integers that raises exceptions when overflowing, and unbounded integers). Spark2014 [START_REF] Dross | Correct Code Containing Containers[END_REF] also offers both bounded and unbounded integer modes. ACSL [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF] and Why3 [START_REF] Filliâtre | Why3 -Where Programs Meet Provers[END_REF] rely on an unbounded semantics. Kosmatov et al. [START_REF] Kosmatov | Static vs Dynamic Verification in Why3, Frama-C and SPARK[END_REF] provide a more complete comparison of Spark2014, ACSL and Why3.

This paper presents a type system that allows to rely on the unbounded mathematical semantics when writing formal specifications, while soundly using bounded machine integers most of the time when executing the code. This way, it reconciles both approaches by combining the expressiveness of the mathematical semantics and the efficiency of machine integers. It supports not only integers, but also rational numbers in Q, thus making it possible to conveniently express and verify at runtime many useful numerical accuracy properties. This technique is implemented in E-ACSL [START_REF] Signoles | E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs[END_REF], the runtime assertion checker of Frama-C [START_REF] Kirchner | Frama-C: A Software Analysis Perspective[END_REF]. This type system has also been adapted to Spark2014 by Adacore (but only for integers). As far as we know, E-ACSL is the only tool that supports runtime assertion checking of properties over rational numbers. The paper also provides initial experiments that demonstrate the gain of efficiency of E-ACSL because of its type system. To sum up, the contributions of this paper are threefold:

a type system that allows a runtime assertion checker to soundly rely on machine code for evaluating mathematical integers and rational numbers; an implementation of this type system in E-ACSL that allows the tool to efficiently check at runtime properties over both integer and rational numbers; an initial evaluation of this type system to measure the gain of efficiency.

The outline of the paper is as follows. Section 2 gives a general overview and a motivating example. Section 3 introduces a small formal specification language on which the type system is designed in Section 4. Section 5 provides some insights about our evaluation and experiments before concluding in Section 6.

Overview and Motivating Example

To illustrate a property with mathematical numbers, consider a simple example of Fig. 1, broadly inspired by well-known numerical accuracy issues (in critical software 2 or in computations of stock prices 3 ). It computes, given daily prices of a merchandise (say, in cents), its average price (as a floating-point value) over a week. The considered property states that, for a given ε > 0, the computed short Mo , Tu , We , Th , Fr , Sa , Su ; // daily prices in cents int main { ... // read recorded prices over a week // compute the average price as a floating -point number float avg =( Mo + Tu + We + Th + Fr + Sa + Su ) /7.0; // check the error is at most 0.0001 /* @ assert ( Mo + Tu + We + Th + Fr + Sa + Su ) /7.0 -0.0001 ≤ avg ≤ ( Mo + Tu + We + Th + Fr + Sa + Su ) /7.0+0.0001; */ } Fig. 1. Toy example computing an average, and an ACSL assertion on its precision.

average avg has a maximal (absolute) error ε with respect to the exact (ideal) average A id : A id -ε ≤ avg ≤ A id + ε. For ε = 0.0001, this property can fail: e.g., 17293/7 ≈ 2470.428571 while the division result in a float is 2470.428467.

The ACSL semantics guarantees that all computations in annotations remain mathematically precise. It allows us to specify the numerical accuracy property of the result in the simplest form, as in the assertion. Indeed, unlike ACSL, in C code, a sum of integers can overflow, and a division in floating-point numbers can be rounded. In our example, the developer avoids the risk of an integer overflow by taking the prices in short, automatically promoted to int to compute the sum (line 5), but the rounding cannot be avoided.

The expression (Mo + ... + Su)/7.0 in the assertion (lines 7-8) can have a different value than in the code (line 5) because it assumes mathematical numbers and operators in Z or R. To verify the assertion at runtime, it cannot be translated into C by the same expression in machine numbers. In our example, the property translated in such a way would be always true, while the assertion can in fact fail. Precise computations in mathematical integer and rational numbers can rely e.g. on the GMP library4 for C programs, but its usage has a cost.

The purpose of our work is twofold. First, we present a pre-analysis step that allows to identify computations for which machine numbers (of a suitable type) can be used without loss of precision. In our example, the sums on lines 7-8 can be safely computed in an int variable without GMP calls. Second, we add a support for rational numbers that makes it possible to easily specify and verify at runtime properties over rational numbers, including some accuracy properties.

Formal Specification Language

Our work is based on the E-ACSL specification language [15], derived from the ACSL specification language [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF]. The differences between both languages [START_REF] Delahaye | Common Specification Language for Static and Dynamic Analysis of C Programs[END_REF] are of no importance for our work. This section introduces a small common sublanguage sufficient for presenting our type system. It is rich enough to express the assertion at lines 7-8 of Fig. 1. Its formal syntax is shown in Fig. 2.

Logic statements are assertions enclosed in special comments /*@ ...*/ that may be written before any C instruction. Assertions are typed predicates which include logical relations, comparison operators over terms, local bindings à la ML and bounded first-order quantifiers over integers. Terms are logic binders, C left-values (variables, pointer dereferences, array and struct accesses, etc.), mathematical constants (either integers or rationals; e.g., the constant 7.0 on a ::= /*@ assert p; */ lines 7-8 in Fig. 1 is seen as a rational number because of the decimal notation) 5 , numerical operators, and (explicit) casts. Terms are typed. Types are the standard C types extended with mathematical integers and rationals. The typing rules are left implicit here, but are straightforward. A numerical operation is an integer one if both arguments are integers; otherwise it is an operation over rational numbers (and the integer argument, if any, is automatically promoted to the corresponding rational number).

assertion p ::= p rel p rel ∈ {∧, ∨, ⇒} | ¬p negation | t cmp t cmp ∈ {≡, <, >, ≤, ≥} | let x = t; p local binding | τ x; t ≤ x < t, p ∈ {∀, ∃} τ ::= γ | Z | Q γ ∈ C types t ::= x logic binder | lv left-values | zcst zcst ∈ Z | qcst qcst ∈ Q | t op t op ∈ {+, -, ×, /} | (τ )t cast
It is worth noting that all constants and numerical operators are over mathematical numbers (either integers in Z, or rationals in Q depending on the context). C integers and floating-point values (that come from C left values) are implicitly coerced to their mathematical counterparts. For the sake of simplicity, we assume no NaN, -0.0 nor ±∞ values, as well as no runtime errors when evaluating C left-values. In practice, the necessary code for checking the absence of runtime errors is generated by an independent mechanism [START_REF] Delahaye | Common Specification Language for Static and Dynamic Analysis of C Programs[END_REF][START_REF] Signoles | From Static Analysis to Runtime Verification with Frama-C and E-ACSL[END_REF]. Illustrative examples. Consider the assertion /*@ assert x + 1 ≤ 127; */ with x of type int. When x = 127, it is invalid. Yet, using machine-integer code for evaluating it would be unsound since x + 1 would overflow. To circumvent this issue, a code generator should rely on a dedicated mathematical library such as GMP in C. For instance, the E-ACSL runtime assertion checker [START_REF] Signoles | E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs[END_REF] of Frama-C [START_REF] Kirchner | Frama-C: A Software Analysis Perspective[END_REF] would generate the (slightly simplified) code of Fig. 3.

While sound, the generated arbitrary-precision code is not as efficient as machine-number based code, while not being always necessary. Consider for instance the assertion /*@ assert c + 1 ≡ 0; */ with c of type char: it would be more efficient and fully sound to use machine-number based code for evaluating the assertion since c + 1 cannot overflow if computed over type int (the values of c vary from -32 to 31, thus the values of c + 1 are included in [-128; 127]).

Based on (over-approximated) intervals of possible values of integer-valued expressions, our type system decides whether the code generator can soundly rely on machine-number based code. On our small examples, it infers that the type of x + 1 should be Z because its possible values vary from -128 to 128, so does not fit in any existing type of our toy architecture, while the type of c + 1 can be int because its possible values vary from -32 to 32. The domains of values are computed thanks to a simple interval analysis. In most cases, using a machine-number based code instead of arbitrary-precision code is possible.

Our type system also supports rational arithmetics. Yet, our type system allows to optimize only comparisons between floating-point variables (e.g., f ≤ g) but no rational operations. Indeed, an interval-based reasoning does not allow optimizing rational arithmetics (e.g., f +1.) by floating-point operations without being unsound (as any non-singular interval of rationals contains an infinite number of values non-representable as floating-point numbers). It explains why the rational extension of our type system does not rely on interval arithmetics: it directly infers either a floating-point type for variables and comparisons between them, or type Q for any other rational number or operator. Language type system. We assume the existence of a type system at the level of the formal specification language: Σ(t) denotes the type of a term t and the primitive isinteger(t) (resp., isfloat(t)) is true if and only if Σ(t) is a subtype of Z (resp., a floating-point type). The relation τ is the subtyping relation (expressing that all values of one type are also values of the other). On our illustrative examples, Σ(x) = int and Σ(c) = char because x (resp. c) is an int (resp. a char), while Σ(x + 1) = Σ(c + 1) = Z since any logical integer operation relies on an unbounded semantics. Furthermore, char τ int τ Z. Integer intervals. We consider (unbounded) integer intervals with partial order I . Let ∅ be the empty interval, T(I) be the smallest C integral type containing interval I (e.g., int if I = [18; 42] since I [-32; 31]), or Z otherwise, and I(t) be an interval that contains all the possible values of the term t. On our illustrative examples, I(x + 1) = [-128; 128] and I(c + 1) = [-32; 32], thus T(x+1) = Z and T(c+1) = int. In practice, E-ACSL relies on a simple syntactic type-based inference system to compute I(t) [START_REF] Jakobsson | Rester statique pour devenir plus rapide, plus précis et plus mince[END_REF].

Kinds. Kinds extend integer intervals to floating-point and rational numbers. They are required since integer arithmetics and rational arithmetics should re-main separated: as already explained, integer type inference relies on interval arithmetics, while it is not the case for rationals. Kinds define a lattice structure. They are the core information used by our type system. More formally, let (K, ) be the lattice of kinds defined as follows:

K ::= Z I an integer interval I | F γ a floating-point type γ | Q the set of rationals Q Z I 1 Z I 2 ⇐⇒ I 1 I I 2 F γ 1 F γ 2 ⇐⇒ γ 1 τ γ 2 Z I F γ ⇐⇒ T(I) τ γ K Q (for all K ∈ K).
The kind Z ∅ (resp., Q) is the minimum (resp., maximum) element of the lattice. Let (resp., ) denote the union (resp., intersection) over kinds induced by their lattice structure. The kind of a term t, denoted κ(t), and the type of a kind k, denoted θ(k), are defined as follows:

κ(t) = Z I(t) if isinteger(t) κ(t) = F Σ(t) if isfloat(t) κ(t) = Q if ¬ isfloat(t) θ(Z I) = T(I) θ(F τ ) = τ θ(Q) = Q.
While we will use an integer interval I for soundly representing a range of machine-integer values as soon as T(I) is not Z, it would be unsound to use a non-singular rational interval R to do the same for a range of floating-point values since R contains (an infinite number of) rationals that are not representable as floating-point values. The operator κ naturally extends from terms to types. The operator θ converts a kind to a type. For integers, it means converting intervals to types, while, for rationals, it means choosing between a floating-point types and rationals. On our illustrative examples, one gets:

θ(κ(x + 1)) = θ(Z [-128; 128]) = Z θ(κ(c + 1)) = θ(Z [-32; 32]) = int θ(κ(f + 1.)) = θ(Q) = Q.
Type system. Fig. 4 presents the type system. An earlier version limited to integers has already been published in French [START_REF] Jakobsson | Rester statique pour devenir plus rapide, plus précis et plus mince[END_REF]. A type judgment, written Γ t : τ 1 ← τ 2 for terms (resp., Γ p p : τ 1 ← τ 2 for predicates), means "in the typing environment Γ , the C expression generated for t (resp., p) may soundly have type τ 1 , but, in the case of an operator (resp., a comparison), it must be computed over type τ 2 ". The type τ 2 is omitted when irrelevant (e.g. for constants). Actually, it may only differ from τ 1 for comparisons and decreasing arithmetic operators (the division "/" in our formal specification language). Predicates return an int. For instance, assuming two variables x and y of type int, the term x/(y + 1) requires GMP code because y + 1 does not fit into any C type of our toy architecture. However, its result fits into an int, so it may soundly be compared to 42 with the usual C equality. Therefore, its type is int ← Z. Fig. 5 details the derivation tree of x/(y + 1) ≡ 42 (with both x and y of type int) and f -0.1 ≤ g (with both f and g of type float).

A constant is evaluated within the smallest possible type with respect to its value (rule [Cst]), but this type is actually never more precise than int (e.g., never char). This optimization avoids superfluous casts in the generated code,

Γ cst : θ(κ(cst) κ(int)) [Cst] Γ lv : Σ(lv) [Lv] Γ x : Γ (x) [Bind] Γ t : τt τ = θ(κ((τ )t)) Γ (τ )t : τ [Cast] τ = θ(κ(t1) κ(t2) κ(t1 op t2)) Γ t1 : τ Γ t2 : τ Γ t1 op t2 : τ ← τ [Op] Γ t : τ τ τ τ Γ t : τ [Sub] Γ t : τ ← τ τ ≺τ τ θ(κ(t)) τ τ Γ t : τ ← τ [↓] Γ p p1 : int p p2 : int Γ p p1 rel p2 : int [Rel] Γ p p : int Γ p ¬p : int [Neg] τ = θ(κ(t1) κ(t2)) Γ t1 : τ Γ t2 : τ Γ p t1 cmp t2 : int ← τ [Cmp] Γ t : τ Γ, x : τ p p : int Γ p let x = t; p : int [Let] τ = θ(κ(t1) κ(t2)) Γ t1 : τ Γ t2 : τ Γ, x : θ(κ(τ ) κ(τ )) p p : int Γ p τ x; t1 ≤ x < t2, p : int [Quantif]
Fig. 4. Type system inferring the types of terms and predicates for the generated code.

because of the C99 promotion rule [18, §6.3.1.1] that states (among others) that any expression more precise than int is automatically promoted to int when used in arithmetic operands. A left-value keeps its C type ([Lv]), while a logic binder takes it from the typing context ([Bind]). A cast (τ )t uses the interval inference system to downcast the resulting type of t to a possibly more precise type τ (e.g. char for both (int)4 and (char)42, cf. rule [Cast]). As usual with explicit coercions, it is up to the user to enforce safety. E-ACSL is also able to verify this safety property but that is outside the scope of this paper. The typing rule [Op] for an operator computes the kind of its operands and its result, merges them to get the most precise interval containing all of their possible values, and converts the result into the corresponding C type. The last two rules for terms are coercion rules. Rule [Sub] is a standard subsumption rule [START_REF] Pierce | Types and Programming Languages[END_REF] (e.g., stating that any term of type char may have type int as well), while rule [↓] soundly downcasts a term to a smaller type than its own type if its inferred kind fits in. For instance, the term x/(y+1) of Fig. 5 has type Z ← Z after applying rule [Op], but since any possible result of the division fits into an int (i.e., θ(κ(x/(y + 1))) τ int), it may soundly be coerced to this type. Yet its operands are still computed over Z.

Typing rules [Rel] and [Neg] for relations are straightforward. Rule [Cmd] for comparisons is similar to rule [Op], but the result is necessarily an int (actually either 0 or 1). A let-binding extends the typing context when evaluating the predicate ([Let]). A quantifier does the same ([Quantif]). In this latter case, the type associated to x is the smallest possible type with respect to its declared type and the one of its bounds. For instance, the inferred type of x is char for both ∀ char x; -3 ≤ x < 4, 2×x ≤ 6 and ∀ int x; 0 ≤ x < 4, 2×x ≤ 6 because x fits in [0; 4] in each case. Fig. 5 shows the derivation for the latter formula. As for casts, it is up to the user to enforce safety of the type declaration, but this property may be verified independently.

Code generation. Generating code from the information computed by the type system is quite straightforward. Yet we may notice that the inference system is not an algorithm since several rules can be applied for a given term because of the coercion rules. A good implementation strategy consists in applying these coercions rules only when no other rules apply. This way, a cast must be introduced

x : int x : Z y : int y : Z 1 : char 1 : Z [Sub] y + 1 : Z ← Z [Op]
x/(y + 1) :

Z ← Z [Op] int ≺τ Z θ(κ(x/(y + 1))) τ int x/(y + 1) : int ← Z [↓] 42 : int 42 : Z p x/(y + 1) ≡ 42 : int [Cmp] f : float f : Q [Sub] 0.1 : Q f -0.1 : Q ← Q [Op] g : float g : Q [Sub] p f -0.1 ≤ g : int ← Q [Cmp] 0 : int 0 : char [↓] 4 : int 4 : char [↓]
x : char 2 : int

x : char x : char

x : char x : int

[Sub]

x : char 2 × x : int

[Op]

x : char 6 : int in the generated code if and only if a coercion rule is applied. Thus, this strategy introduces a minimal number of casts in the generated code. For instance, the code generated for the assertion /*@ assert x/(y + 1) ≡ 42 ∧ f -0.1 ≤ g; */ with the first operand of ≡ of type int ← Z, and f and g of type double would be as follows (the comments are manually added for readibility).

x : char p 2 × x ≤ 6 : int ← int [Cmp] p ∀ int x; 0 ≤ x < 4, 2 × x ≤ 6 : int [Quantif]
/* compute x /( y +1) with GMP intege rs */ mpz_t _x , _y , _cst_1 , _add , _div ; int _div2 , _and ; m pz _i n it _s et _ si ( _x , x ) ; mp z _i ni t _s et _s i ( _y , y ) ; mp z _i ni t_ s et _s i ( _cst_1 , 1) ; mpz_init ( _add ) ; mpz_add ( _add , _y , _cst_1 ) ; mpz_init ( _div ) ; mpz_tdiv_q ( _div , _x , _add ) ; /* soundly downcast the result of the division from GMP to int ; It is worth noting that, at line 9, the code uses the C equality "==" to compare the result of the division to 42 thanks to our type system. The rational operations (lines 10-20) cannot be optimized because of the rational subtraction that cannot be soundly computed in any floating-point type, as we explained above. If the comparison were f ≤ g, then the generated code would use a floatingpoint comparison. The effect of the type system is even clearer for the assertion /*@ assert c + 1 ≡ 0; */ in which the term c + 1 has type int: the generated code is as simple as the C assertion assert(c+1 == 0);

Experiments

We evaluate the benefits of the optimized code generation on several simple examples (cf. Fig. 6). The first one is a simple computational program similar to Fig. 1. It computes, given daily prices of a merchandise, its average price (as a floating-point value) over a year. The considered property states that the returned average has a maximal error ε with respect to the exact average. The other four examples are simple C programs with ACSL annotations involving integer numbers: three programs manipulating an array (binary search, search for a maximal element, search for repetitions), and a program dealing with a matrix (checking if a matrix is symmetric).

Since these examples are rather simple and their execution is very fast, we perform N runs (for various values of parameter N ) of the computational part of each example, including annotations to be evaluated. This is done for two reasons. First, a unique execution is always instantaneous and thus the speedup computed for it is meaningless. Second, performing several iterations of the computational part simulates more complex examples where the evaluation of annotations represents a more significant part of the whole execution.

Figure 6 shows the execution time of the non-optimized (all-GMP) and optimized versions for different values of parameter N . It shows that the optimized code brings a speedup between 88% and 99% by replacing GMP code by machinenumber based code. Moreover, some of the executions of the non-optimized version ran out-of-memory because of numerous heap allocations performed by the GMP code. Thanks to our optimization, this problem did not happen on the optimized version, where no GMP calls were required. Finally, the results of both versions were identical, giving confidence in the soundness of the optimization. Regarding the average example, it was executed with ε = 0.001. Our experiments also demonstrate that if the result type is float, the specified precision property is true for ε = 0.001, but fails for ε = 0.0001. If the computation result type is double, a much greater precision is achieved.

In general, the benefit of the proposed optimization for other programs can depend on the considered annotations and the amount of computation necessary to evaluate them with respect to the rest of the code. An evaluation of this optimization on real-life programs is left as future work, even if this optimization was already turned-on when benchmarking [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of block-level properties[END_REF] or experimenting [START_REF] Pariente | Static Analysis and Runtime Assertion Checking: Contribution to Security Counter-Measures[END_REF] E-ACSL.

These experiments also suggest that runtime assertion checking with the E-ACSL tool can be a very useful and easily performed step to empirically identify numerical properties (in particular, with respect to the exact result in mathematical numbers specified in ACSL) of a given code before attempting to perform their formal proof.

Conclusion and Future Work

We presented a type system parameterized by an interval analysis in order to rely on machine-number based code as often as possible when checking at runtime N = 100 N = 1, 000 N = 10, 000 N = 100, 000 N = 1, 000, 000 average All-GMP 0.008s 0.070s 0.719s where "-" indicates that the execution exceeded the heap allocation limit of 128MB and thus the speedup cannot be computed.

properties over integer and rational numbers. It is implemented in the E-ACSL tool and has been adapted (for integers only) by Adacore to Spark2014. To the best of our knowledge, E-ACSL is the only runtime verification tool that is able to verify numerical properties over rational numbers. Our initial experiments confirm the soundness and the efficiency of our approach. More generally, it has already been used on large use cases a number of times without detecting soundness issues. Yet, evaluating the precise efficiency gain on larger use cases, as well as proving the soundness of the type system, are left as future work. Future work also includes more efficient generated code when dealing with Q, and a richer support when dealing with numbers in R.

Code generation. When dealing with rationals, arbitrary-precision code can be further reduced by using floating-point arithmetics when appropriate. Indeed, floating-point computations are exact under precisely defined circumstances. First, any multiplication and division by an integer power of two is exact: it simply corresponds to a change of the exponent in the binary representation of the floating-point number. Then, the Hauser theorem states that any floatingpoint addition is exact if both operands are small enough, while the Sterbenz lemma states that any floating-point subtraction is exact if the second operand is small enough [22, Theorem 3 and Lemma 2]. Several other floating-point number properties can be used in a similar way.

Expressiveness. The Richardson theorem states that equality over rational expressions extended with the sine function is undecidable [START_REF] Richardson | The identity problem for elementary functions and constants[END_REF]. Hence formal specifications that use the sin function, and any other trigonometric function by extension, cannot always be translated into terminating code. More generally, exact runtime assertion checking of properties over real numbers is not possible in finite time. To circumvent this issue, we could rely on sound approximations and partial verdicts (i.e., the tool would sometimes answer "I don't know").

Fig. 2 .

 2 Fig. 2. Formal syntax of the specification language.

  The illustrative examples of this section assume a toy architecture that supports a set of C types limited to {char, int, float} in which the values of type char are included in the interval [-32; 31], while those of type int are included in[-128; 127]. The possible floating-point values are left unspecified.

  Fig.3. GMP code generated by E-ACSL for /*@ assert x + 1 ≤ 127; */ on a toy architecture. The comments have been manually inserted for readibility.

Fig. 5 .

 5 Fig. 5. Derivation trees for predicates x/(y + 1) ≡ 42 (top), f -0.1 ≤ g (middle) and ∀ int x; 0 ≤ x < 4, 2 × x ≤ 6 (bottom). The unlabeled rules are axioms or [Sub].

  it corresponds to the application of rule [↓] in Fig 5. */ _div2 = mpz_get_si ( _div ) ; if ( _div2 == 42) { /* compute f -0.1 ≤ g with GMP rationals */ mpq_t _f , _cst , _g , _sub ; int _le ; mpq_init ( _cst ) ; mpq_set_str ( _cst , " 01/10 " ,10) ; mpq_init ( _f ) ; mpq_set_d ( _f , f ) ; mpq_init ( _sub ) ; mpq_sub ( _sub , _f , _cst ) ; mpq_init ( _g ) ; mpq_set_d ( _g , g ) ; /* getting the result of the predicate as an int */ _le = mpq_cmp ( _sub , _g ) ; _and = _le ≤ 0;/* de -allocate the allocated GMP variables for rationals */ mpq_clear ( _cst ) ; mpq_clear ( _f ) ; mpq_clear ( _sub ) ; mpq_clear ( _g ) ; } else _and = 0; /* runtime check the conjunction */ assert ( _and ) ; /* de -allocate the allocated GMP variables for intege rs */ mpz_clear ( _x ) ; mpz_clear ( _y ) ; mpz_clear ( _cst_1 ) ; mpz_clear ( _add ) ; mpz_clear ( _div ) ;

Fig. 6 .

 6 Fig. 6. Execution time of the intrumented examples with and without optimization,where "-" indicates that the execution exceeded the heap allocation limit of 128MB and thus the speedup cannot be computed.

https://blog.regehr.org/archives/1091

See e.g. http://www-users.math.umn.edu/∼arnold/disasters/patriot.html

See e.g. https://en.wikipedia.org/wiki/Vancouver Stock Exchange

https://gmplib.org/

E-ACSL also supports floating-point constants such as 0.1f but they are excluded here for the sake of simplicity.

Acknowledgment. The authors thank Thales Research & Technology for support of this work, the Frama-C team for providing the tool, as well as the anonymous reviewers for their helpful comments.