E Gilli
email: e.gilli@wanadoo.fr

A Levret
email: agnes.levret@ipsn.fr

P Sollogoub
email: sollogoub@dmt.cea.fr

P Delange

Research on the February 18, 1996 earthquake in the caves of Saint-Paul-de-Fenouillet area (Pyrénées Orientales, France)

Research on the February 18, 1996 earthquake in the caves of Saint-Paul-de-Fenouillet area (Pyrénées Orientales, France). Recherches sur le séisme du 18 février 1998 dans les grottes de la région de Saint-Paul-de-Fenouillet (Pyrénées Orientales, France). RESUME: Afin d'évaluer les effets d'un séisme sur le concrétionnement des grottes, huit cavités ont été visitées en France, dans les Pyrénées Orientales prés de Saint-Paul-de-Fenouillet après le séisme du 18 février 1996. Cet événement de magnitude 5,2 associé au mouvement d'une faille est-ouest à une dizaine de kilomètres de profondeur, a provoqué des dégâts de surface réduits. Les grottes choisies dans la zone épicentrale n'avaient pas été visitées depuis le séisme. Quelques dégâts y ont été observés. Il s'agit principalement de chutes de fistuleuses et de petits blocs. Parmi les cavités de la zone épicentrale, la plus intéressante est le Barrenc du Paradet qui est aligné sur une faille active récente. Il présente de nombreux dégâts ayant affecté les fistuleuses à la suite du séisme. On y observe aussi de très nombreux dégâts anciens. Parmi eux, des stalagmites cisaillées horizontalement et dont les différents tronçons, restés en place, sont décalés et ont subi une rotation. En l'absence d'autre explication ces formes pourraient être attribuables à des séismes passés. L'étude des fistuleuses qui sont de véritables pendules naturels peut donner des indications sur la direction et le seuil de l'amplitude du mouvement sismique ayant provoqué leur chute lors d'un séisme, permettant ainsi d'obtenir des informations pour calibrer les dommages engendrés par des séismes anciens. Une étude statistique montre que la direction principale des débris de fistuleuses est est-ouest. L'analyse des enregistrements accélérométriques recueillis au barrage de l'Agly montre une accélération amplifiée dans cette direction. Une modélisation confirme que les fistuleuses sont des objets relativement résistants mais qui peuvent rompre dans certaines conditions pendant un séisme.

MOTS CLES: dégâts, fistuleuse, intensité, séisme, spéléothème ABSTRACT: Eight caves have been investigated near Saint-Paul-de-Fenouillet after the magnitude 5.2 earthquake of February 1996 which occurred in the Eastern Pyrenees (France) and caused moderate damage at the ground surface. The earthquake has been associated with the movement of a E-W fault. The caves were not visited since the earthquake. Some damage, mainly collapses of soda straws and small rocks, could be attributed to this earthquake. The most interesting cave in the epicentral area is the Paradet cave which is situated on a recently activated fault plane. In this cave, soda straw falls could be assigned to the earthquake, but other more ancient damage were observed also. Analysis of the azimuth of fallen speleothems which are natural pendulums, may indicate the directions and an estimation of their mechanical properties gives the threshold of the seismic ground motion amplitude responsible for their collapse and thus supply information to calibrate damage due to past earthquakes. A statistical study indicates that the main direction of the collapsed soda straws is E-W. Numerical simulations confirm that soda straws are relatively strong objects that may break under certain conditions during earthquakes. KEY WORDS: damage, earthquake, seismic ground motion, soda straw, speleothem

I. SEISMOTECTONIC CONTEXT

On February 18, 1996 a magnitude 5.2 (Ms) earthquake occurred in the Saint-Paul -de-Fenouillet area, SW France. It was felt over a radius of about 150 km. The earthquake recorded by numerous seismic stations, was followed by hundreds of aftershocks during two months. The epicentre is located between Saint-Paul-de-Fenouillet et Caramany with an intensity of VI (MSK). This earthquake is one of the most important known of the eastern Pyrenees and of the Aude district where five historical earthquakes [START_REF] Levret-Albaret A. ; | Mille ans de séismes en France. Catalogue d'épicentres: paramètres et références[END_REF] have induced slight damages in the Fenouillèdes massif (1920,1922), in the Têt valley (1755,1922) and in the Corbières (1950). Several major faults with a E-W direction (North Pyrenean Frontal thrust to the north of the epicentre, North Pyrenean fault, Agly fault to the south of the epicentre) exist in the area (figure 1). Moreover, geological investigations have shown several evidences of ground surface ruptures, such as the one of Caramany [START_REF] Philip | Présence de failles inverses d'âge quaternaire dans l'est des Pyrénées: implications sismotectoniques[END_REF]. The interpretation (Rigo et al., 1997) of the numerous records of the main shock gives a precise determination of the epicentre location: 42° 47.81' N, 2° 32.30' E and a focal depth in the range of 6 to 11 km depending on the observatories. It is therefore located at 8 km north of the North Pyrenean fault, inside the strongly fractured Agly massif. A published focal mechanism study (Rigo et al., 1997) shows an E-W or N-S, left-lateral strike-slip fault plane solution. The most significant aftershocks recorded during two months following the main shock, cluster within the Agly massif, immediately south of the main shock, with depths ranging from 0 to 11 km. To reach a magnitude of 5.2, a rupture plane of about 25 km 2 (5 km x 5 km) is required [START_REF] Kanamori | Theoretical basis of some empirical relations in seismology[END_REF]. Such a vertical fault plane oriented E-W, crossing the aftershock cluster, exists in the Agly massif (figure 2). Position des épicentres et des plans de failles déduits (hémisphére inferieure) de la secousse principale et des répliques de l'épisode du 18 février 1996.

In contrast with the main shock, the aftershock mechanisms indicate reverse faulting with a predominantly right lateral component. This is consistent with the complexity of the structures in the Agly massif and the reactivation by the main shock of several smaller structures (Rigo et al., 1997). The slight damage observed between Saint-Paul-de-Fenouillet and l'Ille-sur-Têt: widening of preexisting cracks and new cracks in old masonry walls, cracks in ceilings, fall of large pieces of plaster, particularly in the church of Saint-Paul-de-Fenouillet are of a degree VI on the MSK intensity scale. The vibration was felt over a radius of about 150 km as far as Auch to the east, Villefranchede-Rouergue to the north, Montpellier to the west and Barcelone to the south (figure 3) indicating a focus relatively deep [START_REF] Levret A | Atlas of macroseismic maps for French earthquakes with their principal characteristics[END_REF].

The damage area covers a surface of a mean radius of 10 km from north to south in a karstic area that motivated the investigation of potential damage inside the caves. Eight caves situated between 2 and 10 km from the epicenter have been investigated (figure 4). Carte des isoséistes du séisme du 18 février 1996 à Saint Paul de Fenouillet (Pyrénées Orientales, France).

II. METHOD AND FIRST RESULTS:

A. Damage scale

We have defined a scale for underground damages [START_REF] Blevins R. ; R | Formulas for natural frequency and mode shape[END_REF] Tableau 1 : underground seismic or tectonic damage scale. degree damage 0 no visible damage 1 broken soda straws, fall of dust 2 broken stalactites, collapse of stalagmites on clay, collapse of rocks 3 broken stalagmites, collapse of parts of the roof 4 decimetric to metric displacement of gallery sections 5 destruction of cave

The caves had not been explored since the earthquake. To make the difference between natural damages and human caused ones, we have mainly looked for fragments of soda straws coming from places situated out of the reach of cavers: niches difficult of access or roofs several meters high.

B. Results of caves visits (figure. 3)

The different caves show variability in the intensity ot the present damage, but also ancient ones. The most interesting phenomena was found in the Barrenc du Paradet, (B on the map) where many soda straw collapses and massive speleothem destructions are observed. This cave, the highest one, is located on a limestone crest. This led us to suppose a site effect that could have amplified the ground motion, augmenting the damages.

Tableau 2: Quantification of the underground evidences C. Earthquake study from the macroseismic observations. The macroseismic inquery following the earthquake gathered more than 850 observations spread over France and Spain, from which isoseismals separating areas whom intensity vary of one degree, have been drawn (figure 4). The intensity VI epicentral area is spread over a mean radius of 10 km and the vibration was felt over a radius of about 150 km as far as Auch to the east, Villefranche de Rouergue to the north, Montpellier to the west and Barcelone to the south.

From the spatial distribution of macroseismic intensities, the earthquake characteristics can be determined [START_REF] Levret A | Atlas of macroseismic maps for French earthquakes with their principal characteristics[END_REF]. The macroseismic epicenter which corresponds to the barycentre of the maximal intensity area, is located slightly to the north of Caramany (42°45' N, 2°34' E) at 6 km south of the instrumental epicenter (figure 3). The decreasing intensity with distance (Sponheuer relationship) allows the focal depth to be calculated. The great spreading of the effects indicates a focus relatively deep of 5 to 10 km consistent with the values given by the analysis of the records. The magnitude has been calculated from a correlation [START_REF] Levret A | Atlas of macroseismic maps for French earthquakes with their principal characteristics[END_REF] based on 140 earthquakes which occurred in France for which the macroseismic intensity and the instrumental magnitude are known: M = 0.44 I + 1.48 log R + 0.48 linking the magnitude (M) with the focal distance (R in km) of the isoseismal mean radius of intensity I (on MSK scale). This correlation applied to the February 18 earthquake isoseismals yields the following results: The mean value is: M = 5, consistent with the instrumental value (Rigo et al., 1997). The February 18 earthquake for which moderate damages have been observed on the ground surface (new cracks, widening of old cracks) generated very slight effects in the caves. The main damages have been observed in one cave (Barrenc du Paradet) situated at 840 m height, while the caves located at the foot of the relief remained intact. Amplification of the underground damage must have been induced due to the altitude of the cave. In fact, at the ground surface, no damage is produced at, Prugnanes, Camps-sur-l'Agly, Cubières-sur-Cinoble, in spite of the fact that they are the closest ones to the epicenter. Presumably, the reason could be that they are situated in the valleys at altitudes less than 400 m (figure 3). Site amplifications on top of steep slops of rocky spurs are, frequently, observed. One explanation [START_REF] Bard | Diffracted waves and displacement field over two dimensionnal elevated topography[END_REF] is that seismic waves are trapped and this effect is strongest in the presence of geological layers with strong impedance contrast. Similar site effects can be observed on the isoseismal maps where the Miocene and Oligocene sedimentary are responsible for the NE-SW direction of the earthquake isoseismals (figure 4).

III. THE BARRENC DU PARADET

A. The cave characteristics (figure. 5) The Barrence du Paradet is a shaft that begins with a narrow 26 m deep pit giving access to a succession of 3 inclined rooms up 60 m deep. The cave is well decorated and rarely visited, allowing precise observations as cave formations are well preserved from human damages. An accurate survey of the cave, as well as inside and outside observations, indicate that the Barrenc du Paradet is a tectonic cavity. It is organized on an active fault zone that cuts the North-Pyrenean Thrust fault in Chaînon de Galamus area. Its direction is roughly N40°. The space in which we circulate has been created by the relative displacement of the fault edges. This accident has moved during Holocene causing the breakage of speleothems.

In the entire cave, places with soda straws show broken fragments on the floor (phot. 1). Some fragments that we observed last year, are now soldered to the floor by an imperceptible calcite cloak which is probably about 0.01 mm thick.. Except these numerous collapses of soda straws, the Barrenc du Roc Paradet presents also many big speleothems breakdowns, rocks collapses, and stalagmites ruptures. A human cause is impossible due to the importance of the calcite shield that covers these evidences. Moreover, the entrance of the Barrenc du Paradet is a vertical narrow pit. These ancient phenomena have not been dated. b.-Modeling.

Sodastraws are like natural pendulums. A mechanical modeling of their behaviour has allowed to evaluate the conditions necessary for breaking under seismic vibration. Soda straws are considered as beams working in breaking and solicited by a seismic motion at their fixing point to the cave roof.

We have essentially taken into account the soda straw measurements in the caves of Rasiguères and Barrenc du Paradet. The stalactites are constituted of a root whose length varies between 3 cm to 30 cm with a mean value of 10 cm, Beyond the soda straw cylindrical body begins with a variable length. A mean value of 20 cm can be considered. The section is empty and the average thickness of the face is about 0.5 mm. The outside diameter is 5 mm. The density is close to 2.5.

In order to evaluate the sensitivity of soda straws to ground shaking, we first have to determine the fundamental frequency. [START_REF] Blevins R. ; R | Formulas for natural frequency and mode shape[END_REF] gives the following formula for the natural frequency of a cantilever beam:

3,52 L E.I m f =
where f, is the frequency L, is the length of the beam E, is the Young modulus I, is the section inertia of the beam m, is the mass per unit length

The formula applies for a elastic material which can be assumed in order to appreciate the sensitivity to earthquake loads. In the formula all the parameters are known for a given geometry, except the Young modulus. It is shown that the frequency is proportional to the square root of the Young modulus. It was not possible to measure the calcite elasticity Young modulus on the available samples. Therefore, we have used, in this preliminary study, an approximate value: E = 400 MPa, which is one per cent of the concrete value. This value has been assumed by judgment, and is considered as lower bound. An in situ investigation is in progress to precise the Young modulus of the calcite. We obtained the frequency of the fundamental mode at 7.8 Hz, which is right in the middle of the amplification range of seismic motion. As shown on figure 7, the 5% damping response spectrum of the horizontal ground motion component measured in Agly dam site, during the Saint-Paul-de-Fenouillet earthquake, presents a peak between 4 and 10 Hz with a maximum acceleration of 1,37 m/s 2 . Moreover, the frequency is inversely proportional to the square length and proportional to the square Young modulus, this allows to extrapolate to other values. Another result obtained from this elementary analysis is that the place where the bending force is the most important, is the soda straw root, and this for all modes. The fractures should be observed there, for an homogeneous soda straw. Other fractures may result from structural anomalies. The other important parameter to quantify seismic behavior is the rupture stress of calcitic stalactites. Some tests have been realized at the laboratory of Ecole des Mines de Paris on some samples. They give values between 0.93 et 2.8 MPa but on a few samples. With a minimum value of 0.9 MPa it is possible to define the following points:

-to break under its proper weight a soda straw must have more than 20 m of length; -to break in bending during an earthquake the spectral acceleration must be close to 7 m/s 2 . This value is 5 times higher than the one observed on the spectrum (figure 7), with a 5% damping, but a smaller damping tends to increase the spectral acceleration. Nevertheless, this value may be achieved with moderate size earthquakes where site effects may increase the movements up to 10 times more. For such event (magnitude 5 and a distance of 10 km), accelerations up to 3 to 4 m/s 2 are commonly observed with a 5% damping and more with a smaller damping. It could be possible to get these stresses for longer soda straws, as moment varies with the square length, but frequency will decrease in the same way. A more accurate estimate of Young modulus and a better statistical knowledge of calcite rupture stress would be interesting. With this model we confirm the extreme fragility of a soda straw when a static charge is applied at its end and also the relative resistance concerning the action of lateral winds. In order to explain the preferential direction E-W of the stalactite falls observed in the cave of Barrenc du Paradet (figure 6), the seismic ground motion and its response spectrum have been calculated in different directions (each 22°5 from 0° = E-W to -90° = N-S). The maximum ground acceleration is in the direction E-W (angle 0° and 180° and the minimum near the N-S direction (figure 8). This directivity of the maximum ground motion could explain the preferential E-W fall of the soda straws. In conclusion, these preliminary calculations indicate that soda straws are not breakable under the effect of their proper weight or with strains caused by a lateral wind. If they are homogeneous, they need an important acceleration (7 m/s 2) to break during an earthquake, but such a value is not far from the maximum spectral accelerations observed for similar earthquakes and soda straws are rarely homogeneous. The break of soda straws observed in the Barrenc du Paradet situated at 840 m height could be explained by an amplification of the seismic ground motion or/and by structural anomalies in the sodastraw body as it can be deduced from the modeling. It is interesting to note that only some soda straws were broken in the Barrenc du Paradet, probably the ones with structural anomalies. To confirm these results we need more complete information concerning the Young modulus, the damping, and more accurate statistics on rupture stresses. A more precise modeling could be done using these new data, associated with a seismic ground motion analysis it would allow a more complete quantification of the effects observed.

C. Description of old damage

In several parts of the cave, we observe soda straw fragments that are cemented with calcite. Due to the thin layer of calcite, they could be attributed to the 1922 earthquake (phot 2). As a matter of fact, they are small objects and the calcite coating thickness is reduced, about 1 mm. Now we have seen that during one year, a coating of probably 0.01 mm had been deposed on the 1997 fragments, 1 mm of calcite could represent 100 years. Even without accurate measures we remain in a time scale which is compatible with the 1922 earthquake. Much more important damage are visible in the whole cave (phot.3) :

-Type A (figure 9) : objects in touch with the walls are crushed or sheared. This implies a subvertical movement of the fault. Some features are very spectacular (stalactite that vertically penetrates its facing stalagmite, causing its breakage; stalagmite embedded into the roof) (phot.4).

-Type B (figure 10) : speleothems are broken without any contact with the wall or a rock (phot.5). The surface of the speleothems is free of impact. The most interesting are stalagmites that are horizontally broken at different levels. The broken parts remain in place with a displacement and a rotation. These signs are similar to the ones observed on tomb stones or antique columns after an earthquake. An important shake or a vibration are the only explanations for such forms in a cave.

IV. CONCLUSION

This study shows that a 5.2 earthquake causes only few underground damage in the caves located in the epicentral area. A special attention should be given to soda straws. They are simple objects easy to model under seismic solicitation. The first results of the calculation are consistent with the observed effects.

The Barrenc de Paradet that shows modern and ancient damage, is a very interesting cave for quantitative and qualitative analysis of seismotectonic movements that cause disorders in this area.

The comparison with other caves in the same area, shows the importance of site effects. The damage have now to be dated and quantified.

Fig. 1 :

 1 Fig. 1: Map of the historical seismicity of Oriental Pyreneous, with location of the 18/2/1996 earthquake (star). Carte de la sismicité historique des Pyrénées Orientales avec position de l'épicentre du séisme du 18/2/1996 (étoile).

Fig. 2 :

 2 Fig. 2: Epicentral locations and fault plane solutions (lower hemisphere) of the 18 february, 1996 main shock and of the aftershocks. The locations are given for the 37 aftershocks of magnitude of duration M l above 1.8. The shaded fault plane solutions are determined with at least one P polarity of the temporary stations and the black fault plane solutions are determined without data from the temporary network, not yet installed. Compressional (P-) and extensional (T-) axes for the main shock are shown as black and white arrows respectively.

Fig. 3 :

 3 Fig. 3: Main caves around the epicentre of the 18 february, 1996 earthquake. Principales cavités signalées autour de l'épicentre du séisme du 18 février 1996.

Fig. 4 :

 4 Fig. 4: Isoseismal map of the 18 february, 1996 earthquake in Saint Paul de Fenouillet (Pyrénées Orientales, France).Carte des isoséistes du séisme du 18 février 1996 à Saint Paul de Fenouillet (Pyrénées Orientales, France).

Fig. 5 :Fig. 6 :

 56 Fig. 5: Block diagramm of the Barrenc du Paradet and its geological environment. The shaft is aligned on a N40° tear fault . Bloc diagramme du Barrenc du Paradet et de son environnement géologique. Le gouffre est aligné sur un décrochement N40°.

Fig. 7 :Fig. 8 :

 78 Fig.7: 5% damping response spectrum of the horizontal ground motion componante measured in Agly dam site. Spectre de réponse avec un amortissement de 5% du signal horizontal mesuré au barrage de l'Agly (Pyrénées Orientales, France)

  Phot. 2: Two fragments of soda straws in the Barrenc du Paradet. The upper one has collapsed during 1996 seism. The lower one, now covered with calcite is probably from 1922 earthquake. Deux débris de fistuleuses dans le Barrenc du Paradet. Celui du dessus est tombé pendant le séisme de 1996, l'autre remonte probablement au séisme de 1922. Phot. 3: Old massive speleothems collapsed in the Barrenc du Paradet. Concrétions anciennes et massives effondrées dans le Barrenc du Paradet.

Fig. 9 :

 9 Fig. 9: Some type A ancient damage observed in Barrenc du Paradet. The speleothems are in contact with the walls or the roof. Quelques dégâts anciens de type A observés dans le Barrenc du Paradet. Les concrétions sont en contact avec le plafond ou les parois.

Fig. 10 :

 10 Fig. 10: Some type B ancient damage observed in Barrenc du Paradet. The stalagmites are not in contact with the walls or the roof. Quelques dégâts anciens de type B observés dans le Barrenc du Paradet. Les stalagmites ne sont pas en contact avec le plafond ou les parois.

Fig. 11 :

 11 Fig. 11: Origin of type A damage in the Barrenc of Paradet. Origine des dégâts de type A dans le Barrenc du Paradet


Eric Gilli
email: e.gilli@wanadoo.fr

P Delange

Recent, slow and aseismic movement of an overthrust observed in the Abel sink hole

Keywords: overthrust, Provence, sodastraw stalactite, speleothems, tectonics

The main galeries of the Abel sinkhole near Grasse (Alpes Maritimes -France) are developped along a main thrust fault. The study of speleothems proves clearly a recent movement of this fault. The fractures indicate a north-south movement, they are not fossilised by new calcite. A large rock placed under the fault plane rotated during the movement. The sodastraws fixed to the rock are curved. This allows an estimation of the movement speed.

L'inspection d'un petit gouffre donnant accès à un vaste réseau de galeries a permis de constater que ces dernières s'étaient formées sous un plan de chevauchement. L'analyse du concrétionnement montre de façon très nette un mouvement récent du chevauchement qui a cisaillé de nombreux spéléothèmes. Les fractures traduisent un mouvement nord-sud et ne sont pas fossilisées par de la calcite nouvelle. Parmi les indices, un bloc auquel sont fixées des fistuleuses a été mis en rotation. Les fistuleuses se sont courbées sous l'effet du mouvement, enregistrant ainsi la vitesse du déplacement.

MOTS CLES: chevauchement, fistuleuse, Provence, spéléothème, tectonique 1. -DESCRIPTION.

A. -Location (fig. 1) The Abel sink hole (inventory number 129 O2) or Lèque sink hole, is located in south eastern France, in Alpes Maritimes, 3.5 km south-west of Saint Vallier-de-Thiey and a few hundred meters before La Lèque pass. [START_REF] Mangan Ch | Synthèse hydrogéologique du bassin de la Hte Siagne (Alpes Maritimes)[END_REF].

Schéma géologique du secteur de Saint Vallier où se situe l'Aven Abel (d'après [START_REF] Mangan Ch | Synthèse hydrogéologique du bassin de la Hte Siagne (Alpes Maritimes)[END_REF] B. -Description (fig. 2) Several vertical pits lead to a network of galleries, at a depth of 80 m deep. Toward the north, after a small room, a large gallery steadily descends until a vertical passage with several pits at a depth of 150 m. From this point a gallery which is roughly symetrical to the previous one, goes up to a depth of 106 m. The series of pits conducts to several muddy and narrow passages till a depth of 326 m. This part, which is close to the local karstic water table, is flooded during high water periods.

-GEOLOGY

A. -Geological environnement (from [START_REF] Mangan Ch | Synthèse hydrogéologique du bassin de la Hte Siagne (Alpes Maritimes)[END_REF] The area of Saint Vallier and Saint Cézaire plateaux is part of the sedimentary cover of Tanneron metamorphic block and is more or less folded by the progression, toward the south, of the sedimentary cover of the Alps (Préalples) (fig. 3).

-STUDY OF TECTONIC MOVEMENT SIGNS

A. -Classical signs.

The possibility to follow the thrust fault plane for several hundred meters, as was done in the Calernaum sink hole [START_REF]Au coeur d'un chevauchement dans les gouffres du Calernaum et des Baoudillouns[END_REF], allows to see if the fault has moved since the digging of the cave. Many signs were observed, similar to previously described ones (Bini et al., 1992;[START_REF]Néotectonique dans les massifs karstiques. Un exemple dans les Préalpes de Nice: la grotte des Deux Gourdes[END_REF]:

-limestone fractured after the karstification. Before arriving to the main gallery, several fractures that affect the limestone wall of the last pits are visible. These fractures cut karstic features and are neither enlarged by karstic erosion, nor covered with calcite. -broken and tilted columns.

In the main gallery some speleothems are established between the roof (thrust fault plane) and the soil (impervious crushed formation). The movement of the fault has broken or tilted these formations. The shape and the direction of the fractures indicate that it is not possible to invoke a subsidence movement that could have affected the lower formation.

-decapitated stalagmites (ph. 2).

During the fault movement speleothems that were fixed to the roof struck the top of stalagmites and caused their rupture.

-fractured flowstones.

Flowstones that cover the lower formation are fractured by the fault movement. In a same way as for previous observations, the shape of the fractures is not compatible with subsidence . The figure 6 synthesizes these observations. Principaux indices affectant les spéléothèmes de l'Aven Abel.

Near the depth of 140 m, a stalagmitic floor laying on the gallery substratum shows a reverse fault (fig. 7). A similar observation was made in Calernaum without being sure that it was the result of tectonic movement. Calernaum is located in Préalpes, in Calern limestone unit, 12 km north-east of the Abel sink hole.

The previous features look very young because of the absence of calcite covering the fractures. Calcite precipitation is active in this geographical area. Recent and active speleothems are visible in the whole cave. Near the evidence, water drips from the stalactites and recent calcite is visible. The age could be less than 100 years The observed displacement is some centimeters and the speed should be about 1 mm per year. The previous observations are classical, but a very unusual sign has been observed in Abel sink hole. At the base of the first pits series, in a small room, a pluri-metric rock is wedged under the thrust fault plane. Several soda straws have grown below the rock. The movement of the thrust fault has induced a rotation of the rock, tilting its soda straws. As they continued their vertical growth during the fault movement, the soda straws are now curved (fig. 8) (photo. 3). Their form is proof of a slow movement. Studying the rock geometry and the soda straw ages could permit the precise calculation of the speed of the thrust fault movement. Similar observations were done in Chemin-de-Castellaras cave [START_REF] Mangan | Enregistrement des mouvements d'un versant par les spéléothèmes de la grotte du chemin du Castellaras[END_REF] which was affected by a landslide. Photographie 3: Abel sink hole. Curved sodastraws below a rock that rotates during the fault mouvement. Aven Abel. Fistuleuses courbes fixées sous un bloc en rotation à cause du mouvement de la faille.

-CONCLUSION:

The inspection of the speleothems proves the present activity of the Lèque thrust fault with a possible speed of 1mm per year. The movement has stopped in the past, allowing the growth of speleothems, then a new movement has affected the cave formations. Among the speleothems, the soda straws are very interesting movement recorders. Such geological environment is not rare in Alpes Maritime where several sink holes cross thrust faults: Aven du Calernaum (Calern Plateau), Réseau Claude (Caussols Plateau), Gouffre Samson (La Brigue). Their study could help to describe the kinematics of folds and faults in the Nice Prealps.

Figure 1 :

 1 Figure1: geological sketch of Saint-Vallier area where Abel sink hole is located (from[START_REF] Mangan Ch | Synthèse hydrogéologique du bassin de la Hte Siagne (Alpes Maritimes)[END_REF].Schéma géologique du secteur de Saint Vallier où se situe l'Aven Abel (d'après[START_REF] Mangan Ch | Synthèse hydrogéologique du bassin de la Hte Siagne (Alpes Maritimes)[END_REF]

Figure 2 :

 2 Figure 2: Map and cross section of Abel sink hole (galleries from -191 m to -326 m are not figured) (from Hotz, 1997). Plan et coupe de l'Aven Abel (les galeries entre -191 m et -326 ne sont pas figurées) (d'aprèsHotz, 1997).

Figure 3 :

 3 Figure 3: Simplified structural sketch of Alpes Maritimes between Mercantour and Tanneron. Schéma structural simplifié des Alpes Maritimes entre le Mercantour et le Tanneron.

Figure 4 :Figure 5 :

 45 Figure 4: Simplified geological cross section of Abel sink hole.Coupe géologique simplifiée de l'Aven Abel.

Figure 6 :

 6 Figure 6 : Main signs affecting the speleothems of Abel sink hole.Principaux indices affectant les spéléothèmes de l'Aven Abel.

Figure 7 :

 7 Figure 7: Reverse fault affecting a flowstone in Abel sink hole. Faille inverse affectant un plancher stalagmitique de l'Aven Abel.

Figure 8 :

 8 Figure 8: Curved sodastraws under a rock that rotates under the thrust fault plane. Fistuleuses courbées sous un bloc en rotation sous le plan de chevauchement de l'Aven Abel.

Photographie 1: General aspect of the thrust fault plane in the main gallery of Abel sink hole. The passage is digged in the impervious crushed formation, the ceiling is formed by the lower part of a limestone bed. Aspect général du plan de chevauchement dans la galerie principale de l'aven Abel. Le passage est creusé aux dépens de la formation broyée imperméable. Le plafond est formé d'une surface inférieur de banc.


Keywords: Arizona, Nouveau-Mexique, grottes, séismes, concrétions, Arizona, New Mexico, cave, earthquake, speleothem Version française abrégée

Plusieurs grottes ont été visitées dans le sud-ouest des Etats Unis pour rechercher d'éventuels dégâts d'origine sismique ou tectonique. La Californie est dépourvue de grottes. En Arizona, des indices attribuables au séisme de Sonora (Mexique, 1887) ont été vus dans la grotte de Sutherland Peak. Au Nouveau Mexique, les grottes des Monts Guadalupe renferment de nombreuses concrétions brisées qui pourraient traduire l'existence d'au moins un paléoséisme important.

PRESENTATION

Plusieurs grottes ont été visitées dans l'Ouest Américain, entre la côte Californienne et les Montagnes Rocheuses, à la recherche de dégâts souterrains attribuables à des séismes. Dans les différentes cavités, des lieux peu accessibles (sommets d'escalades, passages très étroits, …) ont été inspectés pour éliminer au maximum l'hypothèse de dégâts humains (figure 1). Les observations les plus intéressantes ont été effectuées en Arizona et au Nouveau Mexique.

GROTTES DU SUD DE L'ARIZONA

Un séisme majeur à Sonora, au Mexique, a causé d'important dégâts en 1887, à proximité de la frontière avec l'Arizona et le Nouveau Mexique (figure 2 et 3). La magnitude supposée est de 7,2. L'intensité des dégâts près de Sierra Vista a été comprise entre VII et VIII (Stover et Coffman, 1993). Dans ce secteur, à Sutherland Peak dans les monts Huachuca, la grotte de S.P. Cave contient des concrétions variées dont de nombreuses fistuleuses. On peut observer d'importants dégâts affectant le concrétionnement: colonnes et coulées fracturées, piliers basculés. Ils résultent pour l'essentiel de tassements du substratum argileux de ces concrétions. En plusieurs points on peut cependant constater la présence au sol, de concrétions brisées. Certaines sont encore plantées verticalement dans l'argile ce qui indique un âge relativement récent. Ces chutes pourraient donc être attribuables au séisme de 1887.

GROTTES DU SUD DU NOUVEAU MEXIQUE

3. 1. Géologie des Monts Guadalupe et du secteur de Carlsbad. (d'après Jagnow. et al., 1992) L'élément directeur de la géologie de cette zone est l'unité de Guadalupe qui culmine à 2665 m au Pic Guadalupe. Cette unité est un vaste plateau sédimentaire incliné vers le nord-est où il s'ennoie sous la plaine de Carlsbad. Au Miocène, tout le secteur a connu une phase de plissement, suivie au début du Pliocène, d'une rupture de l'unité de Guadalupe à la faveur d'une importante faille nord-sud, verticale. Le compartiment Est de l'unité de Guadalupe a alors commencé à se soulever. Le mouvement se poursuit aujourd'hui. La vitesse est très importante, plusieurs centaines de mètres depuis 6 millions d'années (figure 6). La région de Carlsbad possède de nombreuses et importantes cavités dont le réseau touristique de Carlsbad et la grotte de Lechuguilla. La plupart de ces grottes sont de véritables labyrinthes où les différents niveaux sont le reflet de différentes étapes du soulèvement de l'unité Est de Guadalupe. Malgré les traces évidentes d'une activité tectonique actuelle (failles actives), seuls des séismes mineurs ont été enregistrés depuis le début des mesures (figure 8).

2. Visite des cavités

Près de Carlsbad, les grottes d'Endless, de Sand et de Mac Kittrick (Mac Kittrick Hills) sont des grottes labyrinthes dans lesquelles on observe de nombreuses chutes de concrétions. En plusieurs endroits, on peut voir des débris de fistuleuses, soudés au sol par de la calcite. Il en existe aussi de nombreux, libres, sur le sol, donc plus récents et provenant très vraisemblablement de saccages. Dans la grotte de Sand, sur de la calcite fossilisant des fistuleuses, on peut voir une signature avec une date: 1917, montrant que la vitesse du concrétionnement est très lente et que les premières chutes sont antérieures à la présence des colons (figure 7).

Plus à l'ouest, la caverne de Carlsbad, grotte touristique, est le phénomène endokarstique majeur de ce secteur. Elle comprend trois niveaux de galeries de grande taille qui montrent, sur le sol, des fistuleuses brisées et recouvertes de calcite. Beaucoup plus à l'ouest, dans le gouffre de Hidden on observe de nombreuses chutes de fines concrétions avec deux époques distinctes: une ancienne où les débris sont soudés au sol et une récente où les débris sont libres.

CONCLUSION

Une visite sommaire de la grotte de Sutherland Peak (SP cave), grotte bien préservée du vandalisme dans la région de Sierra Vista a montré des indices que l'on pourrait rattacher au séisme de 1887. De la même façon, dans la région de Carlsbad, l'étude succincte des grottes a permis l'observation générale d'indices convergeant vers la définition d'au moins un épisode sismique ancien qui a affecté la zone comprise entre le Mont Guadalupe et la ville de Carlsbad. La faille limitant à l'ouest les Monts Guadalupe, et dont le mouvement a causé l'importante surrection de ce secteur, est très certainement responsable de cette sismicité.

PRESENTATION AND METHOD

Speleothems are good indicators of paleoseismicity [START_REF] Postpichl | Paleosismicity from karst sediments: the Grotta del Cervo cave case study (Central Italy)[END_REF][START_REF]Recording of earth movements in karst[END_REF]1996;[START_REF] Quinif | Enregistrement et datation des effets sismo-tectoniques par l'étude des spéléothèmes[END_REF][START_REF] Forti | Speleothems and Earthquakes[END_REF]1998;[START_REF] Davenport | Karst as a record of Palaeoseismicity, Speleochronos h.s[END_REF]. In certain conditions they break during an earthquake, and it is possible to see fragments on the soil of the caves [START_REF] Becker | Höhle und Erdbeben: Mitt. über Höhlen[END_REF]Gospodaric, 1977;[START_REF] Moser | Seismospeläologie-Erdbebenzerstörungen in Höhlen am Beispiel des Gailoches bei Oberfellendorf (Oberfranken, Bayern)[END_REF]Geyer, 1979, Gilli 1998a) and to obtain informations on the paleoearthquakes [START_REF] Becker | Höhle und Erdbeben: Mitt. über Höhlen[END_REF]Schillat, 1977, Agostini and[START_REF] Agostini | Gli studi sismotettonici e paleosismici effetuati nelle grotta del Cervo di Petrasecca nel periodo 1987-1991[END_REF]Gilli, 1998b, Gilli andal, 1998). We have looked for paleoseismicity signs in several caves in south western USA. Places with an important present seismic activity like California is, have in fact no cave, but we have obtained some results in south-eastern Arizona and south-eastern New Mexico, that are places with reduced present seismic activity.

In the USA the exploration of caves is quite recent. It began at the end of the 19th century when prospectors were looking everywhere, including caves, to find guano or gold. It is difficult to know if natives used to go underground as antique signs in deep caves are rare. For indian people, during the colonist period, the underground world was a sacred place haunted by ghosts and only the large cave entrances were inhabited. Meanwhile, it is possible that Archeoindians had different habits. Therefore, during our study, we have specially explored places that were difficult to reach (tops of climbs, very narrow passages, niches… ) to eliminate human caused damages (figure 1).

S. P. Cave (Sutherland Peak cave)

SP Cave is a well decorated cave located on Sutherland peak, in Huachuca mounts near Sierra Vista. It contains an important quantity of speleothems, including shelters, helictites and sodastraws.

The cave is in a limestone lens included in a volcanic [START_REF] Hayes | Geological map of the Huachuca and Mustang moutains southeastern Arizona[END_REF]). It has functioned like a natural drain for the surrounding fractured rhyolites.

The contact between the rhyolite and the limestone is a fault with many parallel joints. A climb down in an open joint gives access to an horizontal phreatic maze level (figure 4).

Several fractures affect the speleothems near these joints. These fractures were probably caused by a recent fault movement. In the horizontal level, damage affect the cave formations (broken flowstones and stalagmites, fractured pillars, tilted stalagmites). They result from clay subsidence below the speleothems.

In some places the clay has been washed out by water circulation and the speleothem basis is well visible (figure 5). But in several places, small broken stalactites and sodastraws are present on the soil. Some of them are vertically stuck in the clay. The signs are recent as no new calcite is visible on them. These collapses could be the effect of the 1887 earthquake.

The local intensity was VII and these evidences are similar to the effects observed in France after the February 18, 1996 earthquake (Ms 5.2 and intensity VI) that caused the collapse of sodastraws and small rocks (Gilli and al, 1998).

It would be interesting to realize a bore hole in the clay to see if older signs are observable.

CAVES IN SOUTHERN NEW MEXICO

3. 1. Geology of the Guadalupe Mountains and Carlsbad area (from Jagnow and Rohwer-Jagnow, 1992) (figure 6).

The main element the geological environment is Guadalupe block whose highest point is Guadalupe Peak (8.749 feet). The block, that contains limestone formations (Capitan limestone), deeps towards north-east, where it disappears beneath the plain of Carlsbad. It is bordered, on the west, by an important escarpment over salt lakes and on the south by another escarpment, the reef escarpment, over the Delaware evaporitic basin. Capitan limestone is a permian reef that was probably covered with Mesozoic rocks. In the Miocene period this place began to arch. At Early Pliocene, a main fault line broke the block and the eastern part began to rise up until the present time (figure 6). The western escarpment results from this movement. It extended several hundred meters for the past 6 million years. There is no evidence of faulting in the reef escarpment area that results from a differential erosion process between the gypsum of Delaware basin and the Capitan limestone. The area around Carlsbad contains many important limestone caves. Most of them are mazes with different levels and they usually contain gypsum deposit. Among them, are Lechuguilla, the deepest cave of USA, and Carlsbad cavern a world famous touristic cave. It is probable that these caves began to form during the Late Miocene or Early Pliocene when the Capitan reef started to arch and rise up. The Mesozoic cover eroded away, allowing the action of water on the limestone. The water is now flowing towards Carlsbad springs in the Pecos River, but the functioning of water flow and caves digging, inside Capitan limestone, is difficult to understand as several phenomenon are involved:

-uplift movement, -connections between the Delaware basin aquifer and the karstic aquifer, -presence of sulfuric acid [START_REF] Hill | Geology of Carlsbad cavern and other caves in the Guadalupe Mountains, New Mexico and Texas[END_REF].

The importance of the western escarpment and the presence of active faults, prove that the uplift of the Guadalupe block is continuing today and the existence of different levels in the caves could indicate different steps in the uplift. At present time there is no evidence of a seismic risk in that area, as only small earthquakes have been recorded (figure 8). We have visited several caves near Carlsbad to search evidence of paleo-earthquakes.

2. Evidences of speleothem collapses in the caves near Carlsbad

• Endless cave This cave is a maze with three different levels. It can be an hydrothermal cave as it is located at the top of a limestone anticline which was probably covered with an impervious layer.

There are many broken speleothems. It is possible to observe two kinds of signs:

-ancient broken sodastraws that are now soldered with calcite onto the flowstone, -more recent broken pieces, that are loose on the soil and were certainly broken by men.

In some parts between the upper level and the entrance level, it is possible to observe collapsed limestone beds. The collapse have broken flowstone and big stalagmites.

• Sand cave Sand cave is also a maze located at the top of a hill. Unfortunately, in the early part of the century, the formations of the cave were destroyed to be sold at Carlsbad tourist shops. Meanwhile, two different ages of broken formations are visible in niches or inaccessible places, excluding a human cause. A signature with a date ( 1917) is engraved on a flowstone where some of the older collapsed sodastraws are included (figure 7). This observation indicates that the calcite formation is very slow and the age of the first collapse is older than the commercial activity. • Mac Kittrick cave Like the previous ones, Mac Kittrick cave is a maze located at the top of a hill. We also have observed in it, two periods of speleothem collapses.

• Carlsbad Cavern In the whole cave, broken sodastraws, rocks collapses and fractures are visible. Some of these evidences have a speleogenetic origin:

-one of the most important collapse is Iceberg Rock, but the movement seems to have been a slow slip as the formations that were on the rock before the collapse, are not broken (figure 9), -in the Colonel Boles Formations a large crack in the soil was caused by clay subsidence. But in several places, damage with a probable seismic origin are visible. For instance, between Crystal Spring Dome and the Rock of Ages, a little basin is full of ancient broken stalactites. In Lower cave, broken sodastraws are now covered with calcite, forming hundreds cave pearls. • Hidden cave. Hidden cave is a small shaft located near the summit of the Guadalupe Mounts. The entrance is a vertical pit that conducts to two horizontal galleries. The cave is aligned on a fault line but no evidence of a recent movement was observed. In both galleries, many collapses are visible and, as for the previous examples, two different ages may be observed. For the oldest collapse, the presence of several pieces located behind unbroken columns (figure 1) proves that the breaks were not caused by human action. Hidden cave contains only short sodastraws and several stalactites have broken extremities with new calcite growth. It is mostly certain that this cave was affected by an important earthquake.

Paleoseismicity

This place was recently inhabited and no data are available concerning its seismic history. This succint study of some caves near Carlsbad tends to prove the existence of an ancient seismic activity in the whole area between Guadalupe Mountains and the city of Carlsbad.

The Western fault that causes the uplift of the Guadalupe block was probably responsible for some earthquakes in the past times. Unfortunately some of the caves have been partially destroyed by human activity. It would be very interesting to check the presence of two generations of broken sodastraws in well preserved caves. By comparison with the similar effects observed in the Barrenc du Paradet (Gilli and al, 1998) the magnitude of the paleoearthquake could be close to 6.

CONCLUSION

The study of speleothems for paleosesimicity studies in the USA is a new approach that has to be developped with precautions. There are not enough caves in California for such studies.

In Arizona some evidences in SP Cave could be attributed to the 1887 Sonora earthquake. In New Mexico, this short trip revealed that caves in Carlsbad area were probably affected by a paleoseismic activity. Most of the caves have been destroyed by human action and the observations have to be controlled in preserved caves. It would be worthwhile to check for the same evidences in other caves, like Lechuguilla near Carlsbad, or Kartchner Caverns near Sierra Vista, These caves are well protected against vandalism, but the permits are difficult to obtain.

As the seismic history of several places in the United States is too recent, seismic hazard is difficult to approach and cave studies could be a good tool. A project of nuclear waste disposal, is in progress near Carlsbad. The knowledge of the recurence and intensity of ancient seisms could be beneficial. These informations are certainly recorded in the caves of Guadalupe Mountains and Carlsbad area.

Figure 1 :Figure 2 :

 12 Figure 1: Location of signs in places protected against human vandalism. Position des indices dans des endroits inaccessibles et préservés du vandalisme

Figure 3 :

 3 Figure 3: The Sonora, 1887 earthquake isoseists and the location of Sierra Vista where Sutherland Peak cave is.From Stover and Coffman (1993)

Figure 4 :

 4 Figure 4: geological context of Sutherland Peak Cave (Sierra Vista) Contexte géologique de la grotte de Sutherland Peak (Sierra Vista).

Figure 5 :

 5 Figure 5: Fractures caused by subsidence in S.P. CaveFractures liées à des tassements dans S.P. Cave

Figure 6 :

 6 Figure 6: Sketch of Guadalupe Mounts with location of the studied caves. Coupe schématique des Monts Guadalupe avec la position des grottes étudiées.

Figure 7 :

 7 Figure 7: Signs observed in Sand Cave (Mac Kitttrick hills, Carlsbad). The first collapses are older than 1917. Indices observés dans Sand Cave. Les premières chutes sont antérieures à 1917.

Figure 8 :

 8 Figure 8: Historical seismicity of New Mexico and location of Carlsbad area. From Stover et Coffman (1993) Sismicité historique du Nouveau Mexique et localisation de la zone de Carlsbad. Extrait de Stover et Coffman (1993).

Figure 9 :

 9 Figure 9: Rock that has slowly dipped in Carlsbad Cavern. Bloc ayant basculé lentement dans Carlsbad Cavern.

Acknowledgements:

Coronado National Forest (Arizona), Lincoln National Forest (N. Mexico), Bureau of Land Management (Carlsbad), Carlsbad Caverns National Park.


Antoine Miné
email: mine@di.ens.fr

Abstract Domains for Bit-Level Machine Integer and Floating-point Operations

come

Introduction

Semantic-based static analysis is an invaluable tool to help ensuring the correctness of programs as it allows discovering program invariants at compile-time and fully automatically. Abstract interpretation [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF] provides a systematic way to design static analyzers that are sound but approximate: they infer invariants which are not necessarily the tightest ones. A central concept is that of abstract domains, which consist of a set of program properties together with a computer representation and algorithms to compute sound approximations in the abstract of the effect of each language instruction. For instance, the interval domain [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF] allows inferring variable bounds. Bound properties allow expressing the absence of many run-time errors (such as arithmetic and array overflows) but, due to approximations, the inferred bounds may not be sufficiently precise to imply the desired safety assertions (e.g., in the presence of loops). An effective static analyzer for run-time errors, such as Astrée [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF], uses additional domains to infer local and loop invariants of a more complex form (e.g., octagons [START_REF] Miné | The octagon abstract domain[END_REF]) and derive tighter bounds.

Most numeric domains naturally abstract an ideal semantics based on perfect integers or rationals, while computers actually use binary numbers with a fixed number of digits. One solution is to adapt the domains to take into account hardware limitations: overflows are detected and treated as errors, while floating-point semantics is simulated by introducing rounding errors [START_REF] Miné | Relational abstract domains for the detection of floating-point run-time errors[END_REF]. While this works well in many cases, it is not sufficient to analyze programs that perform overflows on purpose (expecting a wrap-around semantics) or that rely on the precise binary representation of numbers. The goal of this article is to propose a set of simple, lightweight numeric abstract domains that are aware of these aspects. Figure 2: Floating-point computations exploiting the IEEE binary representation. On the right, c1 to c4 are unspecified constant coefficients of a polynomial approximation. A 32-bit big-endian processor is assumed (e.g., PowerPC).

Motivating Examples

Figure 1.a presents a small C function that adds two signed bytes (char) by casting them to unsigned bytes before the addition and casting the result back to signed bytes. The function systematically triggers an overflow on negative arguments, which is detected by an analyzer such as Astrée. Additionally, on widespread architectures, the return value equals x+y due to wrap-around. This programming pattern is used in popular industrial code generators such as TargetLink [START_REF] Dspace | TargetLink code generator[END_REF] and known as "compute-through-overflow." An analysis not aware of wraparound will either report dead code (if overflows are assumed to be fatal) or return [-128, 127] (if overflows produce full-range results). Even a wrapping-aware interval analysis will return an imprecise interval for arguments crossing zero, e.g. [-1, 0], as the first cast maps {-1, 0} to {255, 0} and intervals cannot represent non-convex properties (see Sec. 2.6).

A variant is shown in Fig. 1.b, where the casts are implicit and caused by copies between variables of different types. This pattern is used to ensure that arithmetic computations are performed in CPU registers only, using a pool of register variables with irrelevant signedness (i.e., register allocation is explicit and not entrusted to the compiler).

Figure 2.a presents a C function exploiting the binary representation of floating-point numbers based on the IEEE standard [START_REF]Standard for binary floating-point arithmetic[END_REF]. It implements a conversion from 32-bit integers to 64-bit floats by first constructing the float representation for x.d = 2 52 + 2 31 and y.d = 2 52 + 2 31 + i using integer operations and then computing y.dx.d = i as a float subtraction. This code is similar to the assembly code generated by compilers when targeting CPUs missing the conversion instruction (such as PowerPC). Some code generators choose to provide their own C implementation instead of relying on the compiler (for instance, to improve the traceability of the assembly code). Figure 2.b exploits the binary encoding of floats to implement a square root: the argument is split into an exponent e and a mantissa in [START_REF]GMP: The GNU multiple precision arithmetic library[END_REF][START_REF]Rationale for international standard, Programming languages[END_REF] (computed by masking the exponent in d); then the square root of the mantissa is evaluated through a polynomial, while the exponent is simply halved. In both examples, a sound analyzer not aware of the IEEE floating-point encoding will return the full float range.

These examples may seem disputable, yet they are representative of actual industrial codes (the examples have been modified for the sake of exposition). The underlying programming patterns are supported by many compilers and code generators. An industrial-strength static analyzer is expected to accept existing coding practices and handle them precisely.

Contribution

We introduce a refined concrete semantics taking bit manipulations into account, and present several abstractions to infer precise bounds for the codes in Figs. 12.

Section 2 focuses on integers with wrap-around: we propose an interval domain extended with a modular component and a bitfield domain abstracting each bit separately. Handling the union type and pointer cast from Fig. 2 requires a specific memory model, which is described in Sec. 3. Section 4 presents a bit-level float domain based on pattern matching enriched with predicate propagation. Section 5 presents experimental results using the Astrée and AstréeA static analyzers. Finally, Sec. 6 concludes.

The domains we present are very simple and lightweight; they have a limited expressiveness. They are intended to supplement, not replace, classic domains, when analyzing programs featuring bit-level manipulations. Moreover, they are often slight variations on existing domains [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF][START_REF] Masdupuy | Semantic analysis of interval congruences[END_REF][START_REF] Monniaux | Verification of device drivers and intelligent controllers: a case study[END_REF][START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF][START_REF] Miné | The octagon abstract domain[END_REF]. We stress the fact that these domains and the change of concrete semantics they require have been incorporated into existing industrial analyzers, to enrich the class of programs they can analyze precisely, at low cost and with no precision regression on previously analyzed codes.

Related Work

The documentation [START_REF]How do I get rid of red OVFL outside PolySpace for Model Link[END_REF] for the PolySpace analyzer suggests removing, prior to an analysis, all computes-through-overflows and provides a source filter based on regular expressions to do so. This solution is fragile and can miss casts (e.g., when they are not explicit, as in Fig. 1.b) or cause unsoundness (in case the pattern is too inclusive and transforms unrelated code parts), while the solution we propose is semantic-based.

Various domains supporting modular arithmetics have been proposed, such as simple [START_REF] Granger | Static analysis of arithmetic congruences[END_REF] and affine congruences [START_REF] Granger | Static analysis of linear congruence equalities among variables of a program[END_REF][START_REF] Müller-Olm | Analysis of modular arithmetic[END_REF]. Masdupuy introduced interval congruences [START_REF] Masdupuy | Semantic analysis of interval congruences[END_REF] to analyze array indices; our modular intervals are a slightly simpler restriction and feature operators adapted to wrap-around. Simon and King propose a wrap-around operator for polyhedra [START_REF] Simon | Taming the wrapping of integer arithmetic[END_REF]; in addition to being costly, it outputs convex polyhedra while our examples require the inference of nonconvex invariants locally. Abstracting each bit of an integer separately is a natural idea that has been used, for instance, by Monniaux [START_REF] Monniaux | Verification of device drivers and intelligent controllers: a case study[END_REF] and Regehr et al. [START_REF] Regehr | Deriving abstract transfer functions for analyzing embedded software[END_REF]. Brauer et al. [START_REF] Brauer | Transfer function synthesis without quantifier elimination[END_REF] propose a bit-blasting technique to design precise transfer functions for small blocks of integer operations, which can bypass the need for more expressive (e.g., disjunctive) local invariants.

We are not aware of any abstract domain able to handle bit-level operations on floatingpoint numbers. Unlike classic predicate abstraction [START_REF] Ball | Automatic predicate abstraction of C programs[END_REF], our floating-point predicate domain includes its own fast and ad-hoc (but limited) propagation algorithm instead of relying on an external generic tool. 2 Integer Abstract Domains

int-type

::= (signed | unsigned)? (char | short | int | long | long long) n? (n ∈ N * ) bitsize : int-type → N * signed : int-type → {true, false} range(t) def = [0, 2 bitsize(t) -1] if ¬signed(t) [-2 bitsize(t)-1 , 2 bitsize(t)-1 -1] if signed(t)

Concrete Integer Semantics

In this section, we focus on integer computations. Before designing a static analysis, we need to provide a precise, mathematical definition of the semantics of programs. We base our semantics on the C standard [START_REF]C standard[END_REF], extended with hypotheses on the representation of data-types necessary to analyze the programs in Fig. 1.

The C language mixes operators based on mathematical integers (addition, etc.) and operators based on the binary representation of numbers (bit-wise operators, shifts). At the hardware level, however, all integer computations are performed in registers of fixed bit-size. Thus, one way to define the semantics is to break it down at the bit level (i.e., "bit-blasting" [START_REF] Brauer | Transfer function synthesis without quantifier elimination[END_REF]). We choose another route and express the semantics using classic mathematical integers in Z. Our semantics is higher-level than a bit-based one, which provides some advantages: on the concrete level, it makes the classic arithmetic C operations (+, -, *, /, %) straightforward to express; on the abstract level, it remains compatible with abstract domains expressed on perfect numbers (such as polyhedra). We show that this choice does not preclude the definition of bit-wise operators nor bit-aware domains.

Integer Types

Integer types in C come in different sizes and can be signed or unsigned. We present in Fig. 3 the type grammar for integers, int-type, including bitfields that can only appear in structures (when a bit size n is specified). The bit size and signedness of types are partly implementationspecific. We assume that they are specified by two maps: bitsize : int-type → N * and signed : int-type → {true, false}. Moreover, we assume that unsigned integers are represented using a pure binary representation:

b n-1 • • • b 0 ∈ { 0, 1 } n represents n-1 i=0 2 i b i , and signed integers use two's complement representation: b n-1 • • • b 0 ∈ { 0, 1 } n represents n-2 i=0 2 i b i -2 n-1 b n-1 .
Although this is not required by the C standard, it is the case for all the popular architectures. 1The range (i.e., the set of acceptable values) of each type is derived as in Fig. 3.

Integer Expressions

We consider here only a pure, side-effect-free, integer fragment of C expressions, as depicted in Fig. 4. To stay concise, we include only arithmetic and bit-wise operators and casts. Moreover, statements are reduced to assignments and assertions (which are sufficient to model programs as control-flow graphs). We perform a static transformation that makes all wrap-around effects

expr ::= n (constant n ∈ Z) | V (variable V ∈ V) | (int-type) expr (cast)
| expr

τ : expr → int-type τ (n) ∈ int-type (given) τ (V ) ∈ int-type (given) τ ( e) def = promote(τ (e)) τ ((t) e) def = t τ (e 1 • e 2 ) def = lub(promote(τ (e 1 )), promote(τ (e 2 ))) if • ∈ { +, -, *, /, %, &, |, ^} promote(τ (e 1 )) if • ∈ { <<, >> }
where: explicit in expressions by first typing sub-expressions and then inserting casts. These steps are performed in a front-end and generally not discussed, but we present them to highlight of few subtle points.

promote(t) def =          int if rank(t) < rank(int) ∧ range(t) ⊆ range(int) unsigned else if rank(t) < rank(int) ∧ range(t) ⊆ range(unsigned) promote(t ) if t has bitfield type t n, based on t t otherwise lub(t, t ) def = when rank(t) ≥ rank(t ):      t if signed(t) = signed(t ) or ¬signed(t) ∧ signed(t ) or signed(t) ∧ ¬signed(t ) ∧ range(t ) ⊆ range(t) unsigned t if signed(t) ∧ ¬signed(t ) ∧ range(t ) ⊆ range(t) when rank(t) < rank(t ): lub(t , t) rank(char) def = 1 rank(short) def = 2 rank(int) def = 3 rank(long) def = 4 rank(long long) def = 5 rank(signed t) def = rank(unsigned t) def = rank(t)
Typing. The type τ (e) of an expression e is inferred as in Fig. 5 based on the given type of variables and constants. Firstly, a promotion rule (promote) states that values of type t smaller than int (where the notion of "smaller" is defined by the rank function) are promoted to int, if int can represent all the values in type t, and to unsigned otherwise. Values of bitfield type t n are promoted as their corresponding base type t. Secondly, for binary operators, the type of the result is inferred from that of both arguments (lub). Integer promotion causes values with the same binary representation but different types to behave differently. For instance,

V def = V n def = (τ (n)) n (t) e def = (t) e e def = let t = τ ( e) in (t) ( (t) e ) e 1 • e 2 def = if • ∈ { +, -, *, /, %, &, |, ^} then: let t = τ (e 1 • e 2 ) in (t) ((t) e 1 • (t) e 2 ) if • ∈ { <<, >> } then: let t = τ (e 1 ) in (t) ((t) e 1 • (unsigned 5) e 2 ) V = e def = V = (τ (V )) e assert(e) def =
assert( e )

Figure 6: Insertion of implicit casts.

expr : Integer promotion is said to be "value preserving", as opposed to "representation preserving" [START_REF]Rationale for international standard, Programming languages[END_REF]. This rule comforts us in our decision to focus on the integer value of variables instead of their binary representation.

E → P(Z) V ρ def = { ρ(V ) } n ρ def = { n } (t) e ρ def = { wrap(v, range(t)) | v ∈ e ρ } e ρ def = { v | v ∈ e ρ } e 1 • e 2 ρ def = { v 1 • v 2 | v 1 ∈ e 1 ρ ∧ v 2 ∈ e 2 ρ ∧ (v 2 = 0 ∨ • / ∈ { /, % }) } where wrap(v, [ , h]) def = min { v | v ≥ ∧ ∃k ∈ Z : v = v + k(h -+ 1) } stat : E → P(E) V = e ρ def = { ρ[V → v] | v ∈ e ρ } assert(e) ρ def = { ρ | ∃v ∈ e ρ : v = 0 }
Cast introduction. The translation of expressions, • , is presented in Fig. 6. Firstly, before applying an operator, its arguments are converted to the type of the result. This can lead to wrap-around effects. For instance, in (int)-1 + (unsigned)1, the left argument is converted to unsigned, which gives 2 32 -1 on a 32-bit architecture. The case of bit shift operators is special; as shifting by an amount exceeding the bit-size of the result is undefined in the C standard, we model instead the behavior of intel 32-bit hardware: the right argument is masked to keep only the lower 5 bits (abusing bitfield types). Secondly, casts are introduced to ensure that the value of the result lies within the range of its inferred type. Finally, before storing a value into a variable, it is converted to the type of the variable.

Operator Semantics

After translation, the semantics of expressions can be defined in terms of integers, without any reference to C types. The arithmetic operators (+,-,*,/,%) have their classic meaning in Z. 2 To define bit-wise operations ( ~, &, |, ^, <<, >>) on Z, we first associate an (infinite) bit pattern to each integer in Z. It is an element of the boolean algebra B = ({0, 1} N , ¬, ∧, ∨) with pointwise negation ¬, logical and ∧, and logical or ∨ operators. The pattern p(x) ∈ B of an integer x ∈ Z is defined using an infinite two's complement representation:

p(x) def = p(x) = (b i ) i∈N where b i = x/2 i mod 2, if x ≥ 0 p(x) = (¬b i ) i∈N where (b i ) i∈N = p(-x -1), if x < 0 (1)
The elements in B are reminiscent of 2-adic integers, but we restrict ourselves to those representing regular integers. The function p is injective, and we note p -1 its inverse, which is only defined on sequences that are stable after a certain index (∃i : ∀j ≥ i : b j = b i ). The bit-wise C operators are given a semantics in Z, based on their natural semantics in B, as follows:

~x def = p -1 (¬p(x)) = -x -1 x & y def = p -1 (p(x) ∧ p(y)) x | y def = p -1 (p(x) ∨ p(y))
x ^y def = p -1 (p(x) ⊕ p(y))

x <<

y def = x × 2 y x >> y def = x × 2 -y (2)
where ⊕ is the exclusive or and • rounds towards -∞. This semantics is compatible with that of existing arbitrary precision integer libraries [START_REF]GMP: The GNU multiple precision arithmetic library[END_REF][START_REF] Miné | ZArith: Arbitrary precision integers library for OCaml[END_REF].

Expression Semantics

Given environments ρ ∈ E def = V → Z associating integer values to variables, we can define the semantics • of expressions and statements as shown in Fig. 7. The semantics of wraparound is modeled by the wrap function. Our semantics is non-deterministic: expressions (resp. statements) return a (possibly empty) set of values (resp. environments). This is necessary to define the semantics of errors that halt the program (e.g., division by zero). Non-determinism is also useful to design analyses that must be sound with respect to several implementations at once. We could for instance relax our semantics and return a full range instead of the modular result in case of an overflow in signed arithmetics (as the result is undefined by the standard).

All it takes to adapt legacy domains to our new semantics is an abstraction of the wrap operator. A straightforward but coarse one would state that wrap (v, [ , h]) and[ , h] otherwise (see also [START_REF] Simon | Taming the wrapping of integer arithmetic[END_REF] for a more precise abstraction on polyhedra). In the following, we will introduce abstract domains specifically adapted to the wrap-around semantics.

def = {v} if v ∈ [ , h],

Integer Interval Domain D i

We recall very briefly the classic interval abstract domain [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF]. It maps each variable to an interval of integers:

D i def = { [ , h] | , h ∈ Z ∪ { ±∞ } }
As it is a non-relational domain, the abstract semantics of expressions, and so, of assignments, can be defined by structural induction, replacing each operator • on Z with an abstract version • i on intervals. Abstract assertions are slightly more complicated and require backward operators; we refer the reader to [18, § 2.4.4] for details. We recall [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF] that optimal abstract operators can be systematically designed with the help of a Galois connection (α, γ):

[ 1 , h 1 ] • i [ 2 , h 2 ] def = α i ({ v 1 • v 2 | v 1 ∈ γ i ([ 1 , h 1 ]), v 2 ∈ γ i ([ 2 , h 2 ]) } γ i ([ , h]) def = { x ∈ Z | ≤ x ≤ h } α i (X) def = [min X, max X] -m ([ , h] + kZ) def = [-h, -] + kZ ~ m ([ , h] + kZ) def = [-h -1, --1] + kZ ([ 1 , h 1 ] + k 1 Z) • m ([ 2 , h 2 ] + k 2 Z) def =      ([ 1 , h 1 ] • i [ 2 , h 2 ]) + gcd(k 1 , k 2 )Z if • ∈ { +, -, *, ∪, } ([ 1 , h 1 ] • i [ 2 , h 2 ]) + 0Z if k 1 = k 2 = 0, • ∈ { /, %, &, |, ^, >>, << } [-∞, +∞] + 0Z otherwise wrap m ([ , h] + kZ, [ , h ]) def = let k = gcd(k, h -+ 1) in [wrap( , [ , h ]), wrap(h, [ , h ])] + 0Z if ( + k Z) ∩ [ + 1, h] = ∅ [ , h] + k Z otherwise
where gcd is the greatest common divisor, and gcd(0, x) = gcd(x, 0) = x. For instance, [

1 , h 1 ] + i [ 2 , h 2 ] def = [ 1 + 2 , h 1 + h 2 ]
. Additionally, an abstraction ∪ i of the set union ∪, as well as a widening i [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF] enforcing termination are required. We note that the optimal abstraction of wrap is:

wrap i ([ , h], [ , h ]) = [wrap( , [ , h ]), wrap(h, [ , h ])] if ( + (h -+ 1)Z) ∩ [ + 1, h] = ∅ [ , h
] otherwise which returns the full interval [ , h ] when [ , h] crosses a boundary in + (h -+ 1)Z. This is the case when

{ wrap(v, [ , h ]) | v ∈ [ , h] } is not convex.
Example. Consider the function add1 in Fig. 1.a and assume that, in the abstract, the computed range for both arguments is [-

Modular Interval Domain D m

We now propose a slight variation on the interval domain that corrects the precision loss in wrap i . It is defined as intervals with an extra modular component:

D m def = { [ , h] + kZ | , h ∈ Z ∪ { ±∞ }, k ∈ N } γ m ([ , h] + kZ) def = { x + ky | ≤ x ≤ h, y ∈ Z }
The domain was mentioned briefly in [START_REF] Kästner | Astrée: Proving the absence of runtime errors[END_REF] but not defined formally. It is also similar to the interval congruences θ.[ , u] m by Masdupuy [START_REF] Masdupuy | Semantic analysis of interval congruences[END_REF], but with θ set to 1, which results in simpler abstract operations (abstract values with θ = 1 are useful when modeling array accesses, as in [START_REF] Masdupuy | Semantic analysis of interval congruences[END_REF], but not when modeling wrap-around).

Abstract operators • m are defined in Fig. 8. There is no longer a best abstraction in general (e.g., { 0, 2, 4 } could be abstracted as either [0, 4]+0Z or [0, 0]+2Z which are both minimal and yet incomparable), which makes the design of operators with a guaranteed precision difficult. We designed ~ m , -m , + m , -m , and ∪ m based on optimal interval and simple congruence operators [START_REF] Granger | Static analysis of arithmetic congruences[END_REF], using basic coset identities to infer modular information. The result may not be minimal (in the sense of minimizing γ m (x • m y )) but suffices in practice. For other operators, we simply revert to classic intervals, discarding any modulo information.

We now focus our attention on wrap m ([ , h] + kZ, [ , h ]). Similarly to intervals, wrapping [ , h]+kZ results in a plain interval if no [ , h]+ky, y ∈ Z crosses a boundary in +(h -+1)Z, in which case the operation is exact. Otherwise, it returns the interval argument [ , h] modulo both h -+ 1 and k. This forgets that the result is bounded by [ , h ] but keeps an important information: the values and h. In practice, we maintain the range [ , h ] by performing a reduced product between D m and plain intervals D i , which ensures that each operator (except the widening) is at least as precise as in an interval analysis.

Example. Consider again the function add1 from Fig. 1.a, with abstract arguments [-1, 1] + 0Z. Then, e = (unsigned char)[-1,1] is abstracted as [-1, 1]+256Z. Thus, e+e gives [-2, 2]+ 256Z. Finally, (char)(e+e) gives back the expected interval: [-2, 2] + 0Z.

Bitfield Domain D b

The interval domain D i is not very precise on bit-level operators. On the example of Fig. 2.b, (range(int) & 0x801fffff) | 0x3fe00000 is abstracted as range(int), which does not capture the fact that some bits are fixed to 0 and others to 1. This issue can be solved by a simple domain that tracks the value of each bit independently. A similar domain was used by Monniaux when analyzing unsigned 32-bit integer computations in a device driver [START_REF] Monniaux | Verification of device drivers and intelligent controllers: a case study[END_REF]. Our version, however, abstracts a Z-based concrete semantics, making it independent from bit-size and signedness. The domain associates to each variable two integers, z and o, that represent the bit masks for bits that can be set respectively to 0 and to 1:

D b def = Z × Z γ b (z, o) def = { b | ∀i ≥ 0 : (¬p(b) i ) ∧ p(z) i or p(b) i ∧ p(o) i } α b (S) def = (∨ { ¬p(b) | b ∈ S }, ∨ { p(b) | b ∈ S })
where p is defined in [START_REF]GMP: The GNU multiple precision arithmetic library[END_REF]. The optimal abstract operators can be derived through the Galois connection P(Z) ---→ ←---

α b γ b Z × Z.
We present the most interesting ones in Fig. 9. They use the bit-wise operators on Z defined in [START_REF]How do I get rid of red OVFL outside PolySpace for Model Link[END_REF]. For bit shifts, we only handle the case where the right argument represents a positive singleton (i.e., it has the form n b for some constant n ≥ 0). Wrapping around an unsigned interval [0, 2 n -1] is handled by masking high bits. Wrapping around a signed interval [-2 n , 2 n -1] additionaly performs a sign extension. Our domain has infinite increasing chains (e.g., X n = (-1, 2 n -1)), and so, requires a widening: b will set all the bits to 0 (resp. 1) if the mask for bits at 0 (resp. at 1) is not stable.

Efficiency. The three domains D i , D m , D b are non-relational, and so, very efficient. Using functional maps, even joins and widenings can be implemented with a sub-linear cost in practice [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF]§III.H.1]. Each abstract operation costs only a few integer operations. Moreover, the values encountered during an analysis generally fit in a machine word. Our analyzer uses an arbitrary precision library able to exploit this fact to improve the performance [START_REF] Miné | ZArith: Arbitrary precision integers library for OCaml[END_REF].

n b def = ( ~n, n) (n ∈ Z) ~ b (z, o) def = (o, z) (z 1 , o 1 ) & b (z 2 , o 2 ) def = (z 1 | z 2 , o 1 & o 2 ) (z 1 , o 1 ) | b (z 2 , o 2 ) def = (z 1 & z 2 , o 1 | o 2 ) (z 1 , o 1 ) ^ b (z 2 , o 2 ) def = ((z 1 & z 2 ) | (o 1 & o 2 ), (z 1 & o 2 ) | (o 1 & z 2 )) (z 1 , o 1 ) << b (z 2 , o 2 ) def = ((z 1 << n) | ((1 << n) -1), o 1 << n), when ∃n ≥ 0 : (z 2 , o 2 ) = n b (z 1 , o 1 ) >> b (z 2 , o 2 ) def = (z 1 >> n, o 1 >> n), when ∃n ≥ 0 : (z 2 , o 2 ) = n b (z 1 , o 1 ) ∪ b (z 2 , o 2 ) def = (z 1 | z 2 , o 1 | o 2 ) (z 1 , o 1 ) b (z 2 , o 2 ) def = (z 1 z 2 , o 1 o 2 ) with x y def = if x = x | y then x else -1 wrap b ((z, o), [0, 2 n -1]) def = (z | (-2 n ), o & (2 n -1)) wrap b ((z, o), [-2 n , 2 n -1]) def = ((z & (2 n -1)) | (-2 n z n ), (o & (2 n -1)) | (-2 n o n ))
Figure 9: Abstract operators in the bitfield domain D b . See also [START_REF]How do I get rid of red OVFL outside PolySpace for Model Link[END_REF].

synt : (L × P(L)) → expr synt((V, o, t), C) def =                    c if c = (V, o, t) ∈ C (t)c if c = (V, o, t ) ∈ C ∧ t, t ∈ int-type ∧ bitsize(t) = bitsize(t ) hi-word-of-dbl(c) if c = (V, o, t ) ∈ C ∧ t ∈ int-type ∧ t = double ∧ bitsize(t) = 32 dbl-of-word(c 1 , c 2 ) if c 1 = (V, o, t ) ∈ C ∧ c 2 = (V, o + 4, t ) ∈ C ∧ t = double ∧ t ∈ int-type ∧ bitsize(t ) = 32 range(t) otherwise

Memory Abstract Domain

A prerequisite to analyze the programs in Fig. 2 is to detect and handle physical casts, that is, the re-interpretation of a portion of memory as representing an object of different type through the use of union types (Fig. 2.a) or pointer casts (Fig. 2.b).

In this section, we are no longer restricted to integers and consider arbitrary C expressions and types. Nevertheless our first step is to reduce expressions to the following simplified grammar: Memory accesses (including field and array accesses, variable reads and modifications) are through typed dereferences * t e, and pointer arithmetics is reduced to arithmetics on bytebased memory addresses. The translation to such expressions can be performed statically by a front-end. For instance, in Fig. 2.a, the statement y.i[1] = i ^x.i [START_REF]GMP: The GNU multiple precision arithmetic library[END_REF] is translated into * int (&y + 4) = (* int &i) ^(* int (&x + 4)). We do not detail this translation further.

A low-level semantics would model memory states as maps in { (V, i) ∈ V × N | i < bitsize(τ (V )) } → { 0, 1 } from bit positions to bit values. We consider instead a slightly higher-level concrete semantics: the memory is a collection of cells in

L def = { (V, o, t) ∈ V × N × scalar-type | o + sizeof(t) ≤ sizeof(V ) },
where V is the variable the cell lives in, o is its offset in bytes from the start of V , and t is the cell type (integer, float, or pointer). A concrete environment ρ is a partial function from cells in L to values in V, where V contains all the integer, float, and pointer values. Pointer values are represented as pairs composed of a variable name V ∈ V and a byte offset o ∈ N from the start of the variable, and written as &V + o. Cells are added on-demand when writing into memory: an assignment * t e = e creates a cell (V, o, t) for each pointer &V + o pointed to by e. Reading a cell (V, o, t) from a memory with cell set

C ⊆ L returns ρ(V, o, t) if (V, o, t) ∈ C. If (V, o, t) /
∈ C, we try to synthesize its value. An example synthesis function, synt, is presented in Fig. 10: it returns an expression over-approximating the value of a cell (V, o, t) using only cells in C. Firstly, if t is an integer type and there is an integer cell (V, o, t ) ∈ C with the same size but t = t , its value is converted to t -i.e., a physical cast *((int*)&V) is treated as a regular cast (int)V. Secondly, selected bit-level manipulations of floats are detected and translated into expressions using two new operators: hi-word-of-dbl and dbl-of-word, that denote, respectively, extracting the most significant 32-bit integer word of a 64-bit double and building a 64-bit double from two words (this semantics is formalized in Sec. 4.1). Thirdly, if no synthesis can occur, the whole range of t is returned. This concrete semantics is then abstracted in a straightforward way: a specific memory domain maintains a set C ⊆ L of current cells and delegates the abstraction of P(C → V) to an underlying domain. Pointer values are abstracted by maintaining an explicit set of pointed-to variables C → P(V) and delegating the abstraction of offsets to a numeric domain. Given an expression and an abstract environment, the memory domain resolves pointer dereferences, synthesizes cell values, and translates dynamically expressions into simple numeric expressions, similar to Fig. 4 extended with the operators introduced during synthesis. Such expressions can then be handled directly by numeric domains, as shown in Sec. 4.2.

This memory domain was introduced in [19] and we will not discuss it further. Note however that the synthesis was limited to integer cells in [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF], while we extend it here to express some bit-level float manipulations. 3Example. In Fig. 2.a, writing into x.i[0] and x.i [START_REF]GMP: The GNU multiple precision arithmetic library[END_REF] creates the cells c 1 = (x, 0, int) and c 2 = (x, 4, int). Reading back x.d amounts to evaluating the expression dbl-of-word(c 1 , c 2 ). In Fig. 2.b, the expression (*p & 0x7fe00000) >> 20 is translated into (hi-word-of-dbl(c) & 0x7fe00000) >> 20, where the cell c = (d, 0, double) represents the variable d.

Floating-Point Abstract Domains 4.1 Concrete Bit-Level Floating-Point Semantics

We now consider the analysis of programs manipulating floating-point numbers. Due to the limited precision of computers, float arithmetics exhibits rounding errors. For many purposes, it is sufficient to model floats as reals, with rounding abstracted as a non-deterministic choice in an error interval. This permits the use of the classic abstract domains defined on rationals or reals (intervals, but also relational domains [START_REF] Miné | Relational abstract domains for the detection of floating-point run-time errors[END_REF]) to model floating-point computations. However, this is not sufficient when the bit representation of numbers is exploited, as in Fig. 2.

We introduce a bit-level semantics based on the ubiquitous IEEE 754-1985 standard [START_REF]Standard for binary floating-point arithmetic[END_REF]. We focus here on double-precision numbers, which occupy 64 bits: a 1-bit sign s, a 11-bit 4 FLOATING-POINT ABSTRACT DOMAINS dbl : {0, 1} 64 → V dbl(s, e 10 , . . . e 0 , m 0 . . . , m 51 ) exponent e 0 to e 10 , and a 52-bit mantissa m 0 to m 51 . The mapping from bit values to float values is described by the function dbl in Fig. 11. In addition to normalized numbers (of the form ±1.m 0 m 1 • • • × 2 x ), the standard allows denormalized (i.e., small) numbers, signed infinities ±∞, and N aN s (Not a Numbers, standing for error codes). This representation gives a concrete semantics to the operators dbl-of-word and hi-word-of-dbl introduced by cell synthesis. As in the case of integers, legacy abstract domains can be adapted to our new semantics by defining an abstraction for our new operators. Straightforward ones would state that dbl-of-word (e 1 , e 2 ) = range(double) and hi-word-of-dbl (e) = range(unsigned), but we propose more precise ones below.

def =          (-1) s × (1 + 51 i=0 2 -i-1 m i ) × 2 ( 10 i=0 2 i ei-1023) if 10 i=0 2 i e i / ∈ { 0, 2047 } (-1) s × ( 51 i=0 2 -i-1 m i ) × 2 -1022 if ∀i : e i = 0 (-1) s × ∞ if ∀i : e i =

Predicate Domain on Binary Floating-Point Numbers D p

The programs in Fig. 2 are idiomatic. It is difficult to envision a general domain that can reason precisely about arbitrary binary floating-point manipulations. Instead, we propose a lightweight and extensible technique based on pattern matching of selected expression fragments. However, matching each expression independently is not sufficient: it provides only a local view that cannot model computations spread across several statements precisely enough. We need to infer and propagate semantic properties to gain in precision.

To analyze Fig. 2.a, we use a domain D p of predicates of the form V = e, where V ∈ V and e is an expression chosen from a fixed list P with a parameter W ∈ V. At most one predicate is associated to each V , so, an abstract element is a map from V to P ∪ { }, where denotes the absence of a predicate:

D p def = V → (P ∪ { })
where:

P ::= W ^0x80000000 (W ∈ V) | dbl-of-word(0x43300000, W ) (W ∈ V) γ p (X p ) def = { ρ ∈ E | ∀V ∈ V : X p (V ) = ∨ ρ(V ) ∈ X p (V ) ρ } (3)
The concretization is the set of environments that satisfy all the predicates, and there is no Galois connection. Figure 12 presents a few example transfer functions. Assignments and tests operate on a pair of abstractions: a predicate X p and an interval X i . Sub-expressions from e are combined by combine with predicates from X p to form idioms. The assignment then removes (in Y p ) the predicates about the modified variable (var(p) is the set of variables appearing in p) and tries to infer a new predicate. The matching algorithm is not purely syntactic: it uses a semantic interval information from X i (e.g., to evaluate sub-expressions). Dually, successfully matched idioms refine the interval information. The join on D p removes the predicates that are not identical. As D p is flat, it has no need for a widening. Similarly to non-relational domains, the cost of each operation is sub-linear when implemented with functional maps [7, §III.H.1].

V = e p (X p , X i ) def = let Y i = V = combine(e, X p , X i ) i X i in let Y p = λW : if W = V or V ∈ var(X p (W )) then else X p (W ) in if e = W ^e1 ∧ e 1 i X i ∈ {[2 31 , 2 31 ], [-2 31 , -2 31 ]} then (Y p [V → W ^0x80000000], Y i ) else if e = dbl-of-word(e 1 , W ) ∧ e 1 i X i = [1127219200, 1127219200] then (Y p [V → dbl-of-word(0x43300000, W )], Y i ) otherwise (Y p , Y i ) assert(e) p (X p , X i ) def = (X p , assert(combine(e, X p , X i )) i X i ) X p ∪ Y p def = λV : if X p (V ) = Y p (V ) then X p (V ) else combine(e, X p , X i ) replaces sub-expressions V 1 -V 2 in e with (double)I when: ∃V 1 , V 2 : ∀j ∈ {1, 2} : X p (V j ) = dbl-of-word(0x43300000, V j ) ∧ X p (V 1 ) = I ^0x80000000 ∧ X i (V 2 ) = [-2 31 , -2 31 ]
To stay concise, we only present the transfer functions sufficient to analyze Fig. 2.a. It is easy to enrich P with new predicates and extend the pattern matching and the propagation rules to accommodate other idioms. For instance, Fig. 2.b can be analyzed by adding the predicate V = hi-word-of-dbl(W ) and using information gathered by the bitfield domain D b during pattern matching.

Exponent Domain D e

As last example, we consider the program in Fig. 13 that decomposes a float into its exponent and mantissa. Although it is possible to extract exponents using bit manipulations, as in Fig. 2.b, this function uses another method which illustrates the analysis of loops: when |d| ≥ 1 it computes r = 2 x iteratively, incrementing x until r ≥ |d|. This example is, as those in Figs. 12, inspired from actual industrial codes and out of scope of existing abstract domains.

To provide precise bounds for the returned value, a first step is to bound r. the case where |d| ≥ 1. To prove that r and d/r are bounded, it is necessary to infer at the loop invariant r ≤ 2d and use the loop exit condition d ≤ r. Several solutions exist to infer this invariant (such as using the polyhedra domain). We advocate the use of a variation D e of the, more efficient, zone domain [START_REF] Miné | A new numerical abstract domain based on difference-bound matrices[END_REF]. While the original domain infers invariants of the form V -W ∈ [ , h], we infer invariants of the form V /W ∈ [ , h]:

D e def = (V × V) → { [ , h] | , h ∈ R ∪ { ±∞ } } γ e (X e ) def = { ρ ∈ E | ∀V, W ∈ V : ρ(W ) = 0 ∨ ρ(V )/ρ(W ) ∈ X e (V, W ) } α e (X) def = λ(V, W ) : [min { ρ(V )/ρ(W ) | ρ ∈ X }, max { ρ(V )/ρ(W ) | ρ ∈ X }]
The domain is constructed by applying a straightforward log transformation to [START_REF] Miné | A new numerical abstract domain based on difference-bound matrices[END_REF]. A near linear cost can be achieved by using packing techniques [7, §III.H.5]. Now that r is bounded, in order to prove that x is also bounded, it is sufficient to infer a relationship between x and r, i.e., r = 2 x at , and r = 2 x-1 at . This is possible, for instance, by using the predicate domain D p from Sec. 4.2 enriched with a new predicate parameterized by a variable W and an integer i:

P ::= P | 2 W +i (W ∈ V, i ∈ Z)
To stay concise, we do not describe the adapted transfer functions.

Experimental Results

All the domains we presented have been incorporated into the Astrée static analyzer for synchronous embedded C programs [START_REF] Absint | Angewandte Informatik. Astrée run-time error analyzer[END_REF][START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF] and its extension AstréeA for multi-threaded programs [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel C programs[END_REF]. Both check for arithmetic and memory errors (integer and float overflows and invalid operations, array overflows, invalid pointer dereferences). Thanks to a modular design based on a partially reduced product of communicating domains, new domains can be easily added.

Figure 14 presents the running-time and number of alarms when analyzing large (up to 2.5 MLoc) C applications from the aeronautic industry. Figure 14.a corresponds to a family of control-command software; each one consists in a single very large reactive loop generated from a graphical specification language (similar to Lustre) and features much floating-point computations (integrations, digital filters, etc.). Figure 14.b is a software to perform hardware checks; it features many loops and is mainly integer-based. Figures 14.c-d are embedded communication software that manipulate strings and buffers; they feature much physical casts to pack, transmit, and unpack typed and untyped messages, as well as some amount of boolean and numeric control. Additionally, the applications in Fig. 14.d are multi-threaded. More details on the analyzed applications are available in [7, III.M] and [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel C programs[END_REF].

In all the tests, the default domains are enabled (intervals, octagons, binary decision trees, etc., we refer the reader to [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF] for an exhaustive list). The first and second columns show, respectively, the result with and without our new domains. In many cases (shown in boldface), our domains strictly improve the precision. Moreover, the improved analysis is between twice slower and twice faster. This variation can be explained as follows: adding new domains incurs a cost per abstract operation, but improving the precision may decrease or increase the number of loop iterations to reach a fixpoint. In the third column, our new domains are disabled but the code is pre-processed with ad-hoc syntactic scripts to (partially) remove their need (e.g., replacing the cast function in Fig. 1.b with a C cast), which is possibly unsound and incomplete (hence the remaining alarms). Comparing the first and last columns shows that being sound does not cause a significant loss of efficiency.

Conclusion

We presented several abstract domains to analyze C codes exploiting the binary representation of integers and floats. They are based on a concrete semantics that allows reasoning about these low-level implementation aspects in a sound way, while being compatible with legacy abstract domains. Each introduced domain focuses on a specific coding practice, so, they are not general. However, they are simple, fast to design and implement, efficient, and easy to extend. They have been included in the industrial-strength analyzer Astrée [START_REF] Absint | Angewandte Informatik. Astrée run-time error analyzer[END_REF] to supplement existing domains and enable the precise analysis of codes exploiting the binary representation of numbers without resorting to unsound source pre-processing.

Future work includes generalizing our domains and developing additional domains specialized to code patterns we will encounter when analyzing new programs, with the hope of building a library of domains covering most analysis needs.

1 INTRODUCTIONFigure 1 :

 11 Figure 1: Integer "compute-through-overflow" examples. char are assumed to be signed. union u { int i[2]; double d; }; double cast(int i) { union u x,y; x.i[0] = 0x43300000; y.i[0] = x.i[0]; x.i[1] = 0x80000000; y.i[1] = i ^x.i[1]; return y.d -x.d; } double sqrt(double d) { double r; unsigned* p = (unsigned*)&d; int e = (*p & 0x7fe00000) >> 20; *p = (*p & 0x801fffff) | 0x3fe00000; r = ((c1*d+c2)*d+c3)*d+c4; *p = (e/2 + 511) << 20; p[1] = 0; return d * r; } (a) (b)

Figure 3 :

 3 Figure 3: Integer C types and their characteristics.

(Figure 4 :

 4 Figure 4: Fragment of integer C syntax.

Figure 5 :

 5 Figure 5: Typing of integer expressions.

Figure 7 :

 7 Figure 7: Concrete semantics.

Figure 8 :

 8 Figure 8: Abstract operators in the modular interval domain D m .

Figure 10 :

 10 Figure 10: Cell synthesis to handle physical casts. A big endian architecture is assumed.

  expr ::= n | &V | expr | expr • expr | (scalar-type) expr | * scalar-type expr stat ::= (* scalar-type expr) = expr | assert(expr) scalar-type ::= int-type | float | double | char *

1 Figure 11 :

 111 Figure 11: Bit-level concrete semantics of floating-point numbers, extending Fig. 7.

Figure 12 :Figure 13 :

 1213 Figure 12: Abstract operator examples in the predicate domain D p .

The C standard allows some features that we do not handle: padding bits, trap representations, one's complement representations or sign-magnitude representations of negative numbers, and negative zeros.

Note that / rounds towards zero and that a % b def = a -(a/b)*b.

Our analyzer (Sec. 5) extends this further to synthesize and decompose integers, bitfields, and 32-bit floats (not presented here for the sake of conciseness).

This work is supported by the INRIA project "Abstraction" common to CNRS and ENS in France.