From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lf1-x133.google.com (mail-lf1-x133.google.com [IPv6:2a00:1450:4864:20::133]) by sourceware.org (Postfix) with ESMTPS id 15B8D3858D39 for ; Tue, 5 Oct 2021 08:26:30 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 15B8D3858D39 Received: by mail-lf1-x133.google.com with SMTP id x27so82944418lfu.5 for ; Tue, 05 Oct 2021 01:26:30 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=wnbhjQDTDcAruUu4TwAuaLNQfucuGoyA5E32fTmWZc8=; b=CsErm0XaTMY6EaeP54/cQFz23LbX0r9JXzi5WfXgKNIgt/ZMz/dDbjb+AeOoKHdKIx MXnaXQO0vx00nxPo5j4eJFETBwM9UDecdo2DFaTG4cdpq5eisLpnvq9ly4Ax0j4LU5QN 3eo+AYssxHv5kP6spWPtUTPYEdG4iBxC2h+kFvPvEOnpIMEESrNb0AaaAtq5iFUAE3AI tDDelRzDAzoA8Cu7f9ete8OcXJ10Pa3ALShV6s/t4+ndy9Ce2Z1OXPwCwLQIphgeGHlb p5f4Erg0nUEyTofHV0oEHsNFSQs/e2muMrzUsVRfHz/riL7we44JpmxfqXZridV4RDfW +IRg== X-Gm-Message-State: AOAM532Ps6itiBANr0lvE69EFGexGBrR76Y83QDZdyVj2Eh+FucCMeW7 Mcm5ozzAtOMmxAdKKlB74DEMmynWRNLmqQ== X-Google-Smtp-Source: ABdhPJzcflzLUuevSq/nU3tyIqaQxC6k++BSrEfWojYCX+K937ubZ60f7z1iBUkIGoSMcyCz5KZYOA== X-Received: by 2002:a05:6512:2398:: with SMTP id c24mr2192139lfv.298.1633422388278; Tue, 05 Oct 2021 01:26:28 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id s9sm1859578lfp.291.2021.10.05.01.26.26 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 05 Oct 2021 01:26:27 -0700 (PDT) Date: Tue, 5 Oct 2021 08:26:26 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Proof of Ada.Characters.Handling Message-ID: <20211005082626.GA2693302@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="TB36FDmn/VVEgNH/" Content-Disposition: inline X-Spam-Status: No, score=-7.0 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 05 Oct 2021 08:26:35 -0000 --TB36FDmn/VVEgNH/ Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Complete functional specification of this unit based on the Ada RM requirements in Ada RM A.3.2. This includes also obsolete subprograms moved to Ada.Characters.Conversions in Ada 2005. GNATprove proves both absence of runtime errors and that the code correctly implements the specified contracts. We add a ghost type and ghost function to the public interface of Ada.Strings.Maps to be able to express the specification of Value. In order to minimize the risk of a naming conflict when Ada.Strings.Maps is with'ed/use'd, we prefix the name of such ghost entities with "SPARK_Proof". Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-chahan.adb: Add loop invariants as needed to prove subprograms. Also use extended return statements where appropriate and not done already. Mark data with Relaxed_Initialization where needed for initialization by parts. Convert regular functions to expression functions where needed for proof. * libgnat/a-chahan.ads: Add postconditions. * libgnat/a-strmap.ads (Model): New ghost function to create a publicly visible model of the private data Character_Mapping, needed in order to prove subprograms in Ada.Characters.Handling. --TB36FDmn/VVEgNH/ Content-Type: application/gzip Content-Disposition: attachment; filename="patch.diff.gz" Content-Transfer-Encoding: base64 H4sICLAKXGEAA3BhdGNoLTAwMC5kaWZmAOVdbVPjOLb+zq9Q1X5IUiRpEiBAc3trGJaeoZuh qX7Z3blfUo6jEFc7dq7tNM3U/vh7zpEsS7L8koTZO3eHmaLBkY6PnvMqHUnMg8WCDQaPQca8 V4++/8qbe6/CYPYYedkrb+AvvaUXDb35jM1qPz4YDAYNFA4ODw+bqPzwAxuML/qjETvEfy7Y Dz8cAHvsxb4GA6T3kl8H7OAQObyL4zULom9eEnhRlsKPLFsGKdtEiG3C2YrDc7aIE+ZFXvic wmdxFD73WRSLx8kmGmTBigt6/pL7X4Posc88IJaxp3gTztmMsyyOmR+nWfjM4mzJk6cg5UP2 Gd8F//MISPkcWj6zlGcZUBD0oClQSnmSBXHE1nEY+M9Ai90+RnHChweHB4frxHtceewqbzV9 EK26OLbpbT429uavslfvErqxpyBbsqu5N7xeeonnZzxJh3cevHk6uiTQNymv+lzr/SlLgNl0 +Iu3Ti81keW9jc8r+g2v4yjNEP9LZz/tc5DbYO35X71Hzmbx/Nnm8GcvmofQEUAFZFo0PDhk gqlPD1cf309/iecgSejMDoTitVElasgUcXYdgsiCReB7JLXP3izkqMPCTi76F+zw+OisfwZ2 wtoOxs2NZHOxiXx61W06Ldjo3mZ8xV6zfwRzXjzusYRnmyRiP8ZxCMqNxNFUZ/wxiA6k0com Zs/OQ5wKoj32X2x8Ormk5jyaG++9REjhq9vQu3dZAXIOKBKNoyyJwxy845MTAu/0aH/wHNDd fvownZxMFHA7YUZ9wY1IYgZG6plEyGqrIcLYfZzx12y18ZdsBUbL+AIUKuBgyH48x3HFC/IO izgM4yd8oIYCDmUdgwaC2ily4FgynqJjAQfzjSdeyEaTv5wf/YXNAuH3PCC8Woc84+C1krl4 lEIHUN54DT2QthDD6Vl/AmKYjPrn24pBfAULgVP3XY8caYEBjinSWhbAvvXClF9qHyGowSIH E7+kKzQdn/Y5QE6ePAzZe3on8NB5GyRpxoZD9o5cpK0G3fe9Xk+9Ft8ZAvlcUgV7n5MNcIfw nJxOEJ6TyXgPeKqMByHrsb++QQv6A2Ble5sd0Do77Y9OAa7z4/5oa7zqbfpzPP3RSwO/xqKL AdTY9N+9cMNZl2hNISL1CY1eYdv5ixTA3YouysSreRSRTzEofs3H6+LuI083YaZ6su4IJUTy uuPRY7bssXmcM9a+D0XFjzz0vvM5aEiQBV4Y/CZCGtAr9ATV5J1SkY9eBLJDqZuaKd/YfccG YqhSmQZsBAr9+k0FyKTvl4ZetlBdlED+wpHQ14GuwYfw0o4aE5/v9oYG+7DbayC8d4LwxlYG 05pMgyoeCJGKR6Yyon2djkb98Qk7PB2P++PTbe1LV1PpF+WrBYfiSzMsxdmnzQzCTbaBcPJa OXcQc4d1lG7nFFGfa8yvm4cLK0yIhxxcnfY20yqNiAtxcVtSZWOtQ0EY01YQiC7UQyJQqEmN dcIgy/6g0hCLqViTFR7os7auHqadgOEHbvwNZR04Pdbli/ukwuAqoTBsshEN2+J3BOTP4b0c PZhmMYVP6+voGMwXKnNYPHD4N2XWrhmEcHvHE0orTk/Of4+04i5+0mZY+6UVRGt67aW8Kreg FmrWUNfN6bJMZv/k+YULtj9dkqFrxM5JhtRKsjaYER5jknE27p8cbT/pMcMozX3qYmlhXX/s aIoolWZI70z/9x8cLluN/iWMrsTMH9DsqqKjYwa9f3xUxuOMZvQIm31Zr+G96pEV81AJ9TBC raVqtoh8TVm99MdEtTb6UQsx4hI7bUOwGTqd73SGTjFmZozZGUBzn8MqRvufFURdAP7pgqiu gDsHUancGEQnR2f9EQTRyfhcFNF2nqlrAbRed+2GjqCpNfk3R05zCVRb/tw/ZNYPqlCHGvPK G/0OcbRh8H+WiFkNgzC27cOimVge0OMKs7o8ODiYtyyzp/UF8rS5zJ42l9lTUXo57p+xQ/g+ mvz/qLKram1doRZH8RCnmR9H8wCN6yUL8UApTuagPNgwi1kaxk9gtU8Rlc/4d+5vyG+KelrK lSdN68vryLBVVD+sK6oTsXowKovRhRE+bBJZ2MFR3kbM830Ynhf5XBXX2fjo6JRd3Q6OJ2MQ AVVZRv1TnJ8d9ccXEz20NC6EVNe13+Y4uTPIerVgVtVaFnotn9JUiL0sEfop8dbLwN+f0B3P cMwvQIjm2i9ASOQbL0BIlBhegNDfAvSNOxA6LPQXjXDOUz8J1kR2xtE+0aC55y+L12VLL5N0 UublpBSlhGJJX9j0YsH9DJf7BeEZp2o2cLJK87K55mo2EXqHJ9CapSKHTb5RrouVSiQlXs3n kCrkjkKjgR4K/cuKCx5oXIqaGkTOP9Vnh/Jz1ewGB1wq6/um1SnvxJYeAgFIrbxQm3bl1Nbw ANjhiUjP++A352UAJXDk6l7GJokOuiIZjJWfVBQ7MvAXc+Kuc5sIyOwI04fjEfsXG43P8OfR 6UWv0B8hnLykk9IeBsG0nxMcsqvyQ9m2hNnTMga5ruM0yDdSYPSIeC6VBDO6lB0Nh8ATqCgw NRwCSy74dvRENfBJilvAdzwmzMYTBHBCYI5PT2sBfJRsGwCWHu4J4PEYYAOuEMIJoAlMuSDc 0QfXQCgoOhDMi4Kdqw6i1PnvDkDW8cQvv3W0ZBM9E1Z4qjAfXRDoY5jK/Qu+T+iXE5TA+OS8 jQRC4hFhFz9ZWAtPaCNbOEKBMIxjOMRRALswDPj5t04ff2knIUUORgPiGZ30cSjw08mEqMBQ qqW2W8CrkxpSrBPaLnIaj4+3Fw0yMvA9IKtJyX5YZRya4BTSewkHhkAiaZLIjplDjUSIYisz 2tdyxuM6iURsg5xYInE8pdaKjtOYNJloxlMlEkXL9Gy5vZBIyGLGY5dIdszBakRCFLcVSZWT g+dy3jL8cj29uoFUb73MlrGYo5Qb3bVpBJRufR5CHhL40xs1hjKpFq0MWp+XcRK1oFbf7ifI D71o+gmwX08/1fqBGUmvcAH67y53rUhVBUSlcZikGS4hV1DRx0hQVY74mllC6rM7+4ENfl+R sgG32hJofVYGEtnTiZj4uZR+x/lCjdITRaX0mrIfCaW+6NTKcc79ALPnOZJBQRoPbEkGUTnS 4ptAWBcdHC+zxyuoWeNuHq9ol/AIEvhUDbM8//qZf/fmpXfsMJG7CtdLL9qseKI7pR0IfVoD O94LzOPvgohPP4NGBZGXxcnuhH7xkq8llduF0Ac8tjF9i9OtbC9CD/jzhmZzOCOKYK4a1xWy asD2fP4SQ7t/+/56J4zKJr6jStaYeImiK8bZtiaTCsDVDn9v9cR+Ue8elsWrCxdRetiU7vEA Ncf2NrpvrwkJbztFopFn8ouOy7nuaMM1yOsU3aDLCZqGtlsQ9Smcp3OuzzurPsorukjPNTNS iMuIHJfQdwG4o++qAVBSdGOXrw9I8DDw4wqSLclmAFkqGXdO3Ss/1HMSx7RfgYlM6WJwTvl2 89Z1Uz6T4hZrHiNa5hgd45LH8XH9YpEaLC2dqyR/dDQcAoEuMfGW87mWLBFf3mwTkgPvMwwI og279pIk8B759CONkgwCWGDde/49oxH1XODtGKFqwEOKRVIkD4PkI7jH4z8CjG4Uy1VOdD3P a21qRquLvpfxxzgJwBshyT67j6MBRh1Zq8jdkvhQfsCu49UsiLDM7BrtjmG0ZrQ6RS0VdOrH GzY621EnzkCQn+JFNv35eb3kkXNwO4b2msE5Kba1hjfson49o2qwF6es25nCBORrhIUyUIW7 +Ik0WM/5v+DCeepj9cvtT3dKT2r9KVBsErFY9qT1zp3GDp27tKdQLE4qCt37ePpjwr2vgg3n kHdMpGqGjBTbilucpDML7bjqi1ic4/cz+vnslL6LJxf4/fzInBSPzmnF/fyEvlPzc1pCPqdO 59TpohJePz/0vE54iicWxVFCsd0ionoFbjPAYuy9/K3YUoHU0JYZINn1sISzALWjk9HXoYfH g8cjdFe3nz68ur25Bl89OZm8Hh+NznqXomQcRH64mWvLZLgrQUkbsoPvPl9n0BYXdgzZpwhX H9HqI1j47RS/0a8XRRAAwPoIEn47wW/Y6nyC37Dp+YUotgBEwy0OEpeqpOJtYPXgsFOz4or1 scJX48vkbpYtS7E1VdltdrlfujcL7ta19ZG9Qv30ypmYNOfc9xUzQiaKfsIXqAygg9lTXKrU pa8pI6ccyCcBZAB6Eq801KGr+oWIG4szdMrfRUAKCnqLn/AWAC7LcDgGLHsqSuoFgyweFK/W j/oWNU4qnfb1UqfBkV8okrdeh4GwQFEbxDPAdiWxqCASi1apNWdVjgL5kyPT3oPrVrPMyw0Y X/us5w7wfqLBQ75CR5EXP+XwOmmOlmJFjiQBJtZYftWIVWBVsHMppleCfWCNtGUDziE/A2FW UorMiNbaCJyCj3J/IUiqBrBZvAFls0sz4s3qxAUblWLINkZXFTVyGo6wgR461W2zJ84Qa96/ iCx/h/G6A82hGWP0Q3Va/cymbJEnejCh7bFB6elVp2f1xMJBEzF9MRqnV9+4TYVcY1W3L0W3 ntbRfrPcoJwL9aOsqJf0Uq8LCVVaqOWIQgwC0SK06EV6alvcFtLooJ0bk5tcc8tOLc4o77FF u0aVqypNAkMNAEPWCGNxKk9eMVC51u/QEv3LqBL8Ov1b4HEQs9pVztj/tRFdOY3I28uIvuxm RHcvbERaIc9pRKQAmvxzG6ImtEPGKAaiG+/XGVnhw4tiYVFFTMt1DiJm6gWbx6RyS0BBvJxo FEkGMJG6XH/rzKfGXqrKgACXXF4qLdpRUVbVJCviAj6tlmeXQJKTK0tfntAOy2qFGm48/Yjy pi8YCeh0v4EO/MfnQRh6Je3Mv5DOdSOdGyc/N5o8kc5NI51bJ51bi85tI5376ecgnJdnzua4 7hvpfHDy88Hi50MLOh9mYfA/G9o6HX91MNaOzhcnP18sfr400vl1euXjOcB6fH6tp3Pn1MO7 sh56jXTa6aHfSMehh3dlPeSNdBx6eFfWw6CRTjs9jBrpOPTwrqyHcQs6bfSwmY5DD+/Kerhp pNNOD59b0CnevDUdilzEceJB/GIPSfwIU5TpTZLESa8ixMqyiBlp5VyQzTaZWBWJYjYPPJhb ZoEPWcwKF3mLokF5xxr1pGqBsR/isjKfbZr7uA/atZv1yKMkb9hIoaZyQrupOPYDbbVDQKVe GvjqqAsd9bGpiVM/9oEXe1KGF0WUj2IbB9/ofNCoJ866NOTW20KlZ9UNUBlN94bKoFYJlZH0 K6iMA3dbQNVi7tIyoWqAymi6N1QGtUqojHxPQWXcIlQJ1c5rk3XLlcZ2ddpvj4MtVjFT9iPP njiPrAXM208fGF4TsvsKppOrYona2FWfclptKnbT4+14NLlY8dUMOF0G63xToOSsmBAovqlU T9u05Bofm8mx5aOhsat6rNwjlG5mVG3Lb0ZR9yBcm5TteeRRD4OW9XA0PiNR2ps6Wt9mWN4P YnfNTYax8g6QXd9aU/OQNBzbuoqLEg2p5u8XezXtpbr8/EOQOsqcMjZV1omkClgSc9V+WoO2 xciL6ZvhHMigc4/guLLwXa+3N0RylbISH/VSemf3ttfD3vSxOrxzazI73PI6LatGwLa6VEyd Bd3mIrLqKFAtGQMMffZcdadYnVzISW+jwNrispZklQXUM1c9UKc1YPTxmx7OWH7cRnj6QmJL KejLiFt1aS23hvhtNd47glv0KmO4pVwUxe1Ft/JFWs6w7ro7ZF9l00DWNY10SHgJQVCMj+oa Qw0ygorLCh21VKRk3YfuwH4MvoEUZs/6SNVhPX2ikheLpG/Zo8Ran7ZYZ8+NSJ7mVxKPjo77 53gl8Yl1zVjzwVr2D44rhUuYAHyjDTff8Jpwtgi9R3nAUBSk8qO/9zFMgFMIIakPw5++5R7I gRfk4GeQhqoLwosBUdZNOceT9vQRcMT9rwYZPCs8vYlAY557pRLDDvdJO7apCh1hzKSwRVKx LQ81EbZInsqevObC6jf2enfx652XZq6Jdh4py1QV0XLpkj62aDv31myJaQ0iok9NynHrTDls mWAGUIOC3mP7jGFP29bmHnl+XmfcyrbHo/4Ir1s4H/dPLtoadylKFrHaFSdNRtzxsuDMCn/W Vojt+9VEzjpLsQTaspZcaV81hSJn5qSvZemFftdylkv3euZ2jYqk6LpdEuS4Z8eQbV0iVCmg ulSooVONSA1Tb8iFzLZ7p0ImucpMyHRGVYlQ2fdskwp9rMpfkhfLXzTV2SKDKV3hVJjpQNMu 16Ta9iKHW7WvURnLZkuuwPq8stxdgb/lhv8JE23AmXZNuUJmETFdvuSfvUokpWmYMFZfhmUD WHNtVgN025ico8PeduegWWl85baVFui+l6l6TbZK9L+T/VnsNRihIqeMcZ0E37yM6xfv3EYh bn/uWuczei0uioLce+WtKy+KKj6uvChKa1J1UZTWRPyNDvGXUvqjY7ooSlwV9ZDwl7ljiZl3 LKWxsFlxo9KaA+pzuc9WXY9C9am5828e0bjzP3zkEFXtX0Dauat95RSlBEjtcYlG7MdzztIl 7WXG8c/yy6KAZbyKZhMhErg3/omHofueKUGv5WVTeFlW5WVTCTfvmqptyYq2dtFQ/yJf1a7p T0v7titW/yek5L1T49ER6iFeIDE+sTNo/W88Meuaq4Tz0JvFCf7tJPtiyyLA4O2Ta/TMxZVY H7ncdS6vy6GzX9qpplj7ZSV6v5ZVArHYQVdvPSRxvJiW3kNXcoXFFhcvSbxnjZ8eCrYcVgV8 hRt82MxAWOEz+xbQX+lhKyKLpRJWeqc9+9MZJHbyWAXt9VivsMnFmmeJzQOsZPw64V6uvx5b bzkMIzLTTaJ51oys45eDfZU430h/3WJLeNvWVcGbeCvKDyXEieEe68qXVC2zictSE+dkRWxm A22ke6cUu6CRxVo7SQB9Gd5mhRvVgYJUWXgs1VzsrAZ+8tznds5pNQeG7su/m+ZCVdrn+Sn9 Kaejk/5oTPaZRz6iZa41551pdalW8y+lRf3blba46reNHZMYxZ/DQ9cjXdOdOnlf7dtaA43X Yh8c/C+VHoW/sXEAAA== --TB36FDmn/VVEgNH/--