nagini_contracts/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_contracts/adt.py,sha256=RpUq7sbSZuTdrNXd1EKTRFeWzXFF-tB9XlgGjIwgMLA,1086
nagini_contracts/contracts.py,sha256=m27DV2N8qF8xfVhzKEsiB-Qf9fHtmd4ftOdVNUKXjf8,11734
nagini_contracts/importer.py,sha256=vp5-hIaRIzYCDp-ZQenV9M4yJV3qVFEZ8YzB4M24P_o,2536
nagini_contracts/io_builtins.py,sha256=a60RIfUjVCfUEgLPkCqD0A5yVaLoQrAiIUFSPHsrCjo,5523
nagini_contracts/io_contracts.py,sha256=1Bpk8Hohhw9I73IaHaGOGLePEfLG6p59Ac5iBISl-jQ,10478
nagini_contracts/lock.py,sha256=WjKZKGy11MubeFlJY3JhWucq7nLU6yXVoD0RDGhF9ac,2645
nagini_contracts/obligations.py,sha256=F0H2K5FyeYrU1ZFFPIpLsIG3z-e7ruWAN40LuvDIgZE,1257
nagini_contracts/thread.py,sha256=pItAzf2Rprn1yzrsb_kjsCOqvNuU6_fDMEGQTscbmd8,3022
nagini_contracts/transformer.py,sha256=eRis83NFvelv1Xb1JI7kruWGXKY5DrSZOkTP3i-wCYQ,7674
nagini_translation/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/analyzer.py,sha256=LvinkvCY1Zrz8aSWOb2_dxlzWM8v89mSf3uaosyFXJc,67342
nagini_translation/analyzer_io.py,sha256=rQGNNXmu3sdWKsVTz-QTvwO-TlbqzrrnrDlNRu-W0EY,11983
nagini_translation/client.py,sha256=lDGNfgFIB2JuKS-6cFdpLKWr1EYJ9DiqbjTqKwg_bkg,627
nagini_translation/conftest.py,sha256=HXSJM6F6bvRjo3NDsRXewcNZCilmWGJPRFhFXAtGZxc,8826
nagini_translation/main.py,sha256=pGCD2awh5FiCxnIEKAq9FfsHpXBM656dCcYBJID7fA8,14423
nagini_translation/sif_translator.py,sha256=mPZLl3UjctXgZV75XXJU10HpmLmuHi7Beq9KQnjCYeU,3963
nagini_translation/tests.py,sha256=3K2BqAUEJbbUfv41_mipnESXLX_OrLBOFXGaihEhvig,22530
nagini_translation/translator.py,sha256=NG-NduiTQ-8ab1AvnjtrzB5rjhX2YlJau0c3C4cZ6gM,6968
nagini_translation/verifier.py,sha256=pr_zxLnV2Fwo1W9I_WfVDKgdnh9fVCxAZC0wWpsge2Y,5685
nagini_translation/lib/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/lib/config.py,sha256=HrTOo0NcKoUEzhDJTPIMnm0hy_3-AUscbpgPao2uMsw,8073
nagini_translation/lib/constants.py,sha256=avJVJY4ddC7EM866-ZQKqU8ZuAUguYxyXiLXUv3z0v8,5762
nagini_translation/lib/context.py,sha256=jREwW_r5GABVgcKRZ2vDubh42uxrxWqaqZx9BQuOtXs,7486
nagini_translation/lib/guard_collectors.py,sha256=tjcdxc8VE3TH7tL7kcx0Jsfin02wWDIRlmxVLkKKc1A,1802
nagini_translation/lib/io_checkers.py,sha256=obiahAuq55k15fPymtxrS9Qc1N6-T_SnpPF-Gb-jTBw,3328
nagini_translation/lib/io_context.py,sha256=qU5EZR3d8vhNsB4S2h7NYUpDSMchuKxdGwmKqnQEIsE,3137
nagini_translation/lib/jvmaccess.py,sha256=eG-VYKgMHZ4yj8JNHgudi_ntjbgLfEAPJ6qYDamXk5k,836
nagini_translation/lib/obligation_context.py,sha256=TVrKa9slDZxWEnMleMlb87qSp6o-Khgiqu5BV7U_SC8,1958
nagini_translation/lib/program_nodes.py,sha256=yKmSQ8MpTBS1_3mCyDD2QSEHeH17a7xY4_77ORVOPro,68267
nagini_translation/lib/resolver.py,sha256=XZ1Hc2EQXeb7Id5eLcO44ExbI85kIIoU0x1_8xShIag,26027
nagini_translation/lib/typedefs.py,sha256=-8LBk0JvubyAdLXBTa3DjmuiU_RqaPkcJT_IY6hHh74,984
nagini_translation/lib/typeinfo.py,sha256=t8nfMSuEA3PR4s0Xq1rmP80WdqndcMP_DyYZvIhB0d0,14410
nagini_translation/lib/util.py,sha256=-IScjiinNYREtGesxVuThx61cyofkLW8pbPKno0nZ9g,12416
nagini_translation/lib/views.py,sha256=5kQDtYeFEn39sEz7-nukpO_r26UNDzHMoSZnst1O3-M,4503
nagini_translation/lib/viper_ast.py,sha256=7ITZyw12Zm1CbWVFVRxxGM6wvs_3taCoWXTl3f5q4SY,22247
nagini_translation/lib/errors/__init__.py,sha256=dxnhRw4P5qgkoYUBtAtdIQNplDeDCYkG6OQOoaJDJc4,480
nagini_translation/lib/errors/manager.py,sha256=yPc6DmxVAagXUyUDXAvezJkCv7WAZvvjqRtzgLoYCGk,4710
nagini_translation/lib/errors/messages.py,sha256=wXkC_xJ7mPnoZuUtLRQ4wyYS_C-kvoR4qIB5yblVmYM,8409
nagini_translation/lib/errors/rules.py,sha256=4SKculC4AS7sQWMLdwNISk2GmOEUXV9mEnWh5cWAE7I,4906
nagini_translation/lib/errors/wrappers.py,sha256=-u2Ovm_tCmHYeYFdv97kWnwNVpw7RuaLc6VH8Kuf3so,5795
nagini_translation/lib/silver_nodes/__init__.py,sha256=d1AhR_WGirIGBU6BAFrOAm3qXZM_zVp_OTVem2VXh1o,1076
nagini_translation/lib/silver_nodes/base.py,sha256=wudYu-FlMzPC6cKC-ZH8Y4dnrQDvWUCVKqGYCLp1Tp0,1150
nagini_translation/lib/silver_nodes/bool_expr.py,sha256=JyQsgamxP5imMbkUzZHF9p_SIFW5QIMSI9kYZvNsApY,10265
nagini_translation/lib/silver_nodes/call.py,sha256=ayBBXs36luDdnHhKk2EayAcStyr5_lo68iuiMtp3sP0,2357
nagini_translation/lib/silver_nodes/expression.py,sha256=jhEJMgiSKX6WODrgyMoxYnIVbHsyb3SrwjO7j_UMa7k,1476
nagini_translation/lib/silver_nodes/int_cmp_expr.py,sha256=q_LVN7yvCMraqpZSlMIBqad0lcbxSLKZaIv-bSsYYcc,3752
nagini_translation/lib/silver_nodes/int_expr.py,sha256=FJ9orVJ3Wvvw-gXezxoOfewHjafXNiABr8kUKCaO4V0,6612
nagini_translation/lib/silver_nodes/location_expr.py,sha256=PxMqFF0Ssz7j_mGikznn9GFwcnzA88FnIYMVtNvQrnQ,2825
nagini_translation/lib/silver_nodes/perm_cmp_expr.py,sha256=dx-Y_gGJc8wD3fCSuB-fDWFcNrEv9MwdRaGp_mscil0,2853
nagini_translation/lib/silver_nodes/perm_expr.py,sha256=F3aAKIiuv-9huWdv-9dlf4Q3BhO40RizdEG93Ny5_js,4797
nagini_translation/lib/silver_nodes/program.py,sha256=W_IKLf5gToEth2LQROCzwEhv7sKwng-iwVIuXPhQ1iA,1521
nagini_translation/lib/silver_nodes/reference_expr.py,sha256=N9STwmSZf9Doxn1qCr7Uimyl4uVbCe8yyhtUGOICBcg,2442
nagini_translation/lib/silver_nodes/statement.py,sha256=iEC7MV7-FUUpbnUu4pY6CGb69ValZsRdld-GfisefuY,3204
nagini_translation/lib/silver_nodes/types.py,sha256=jiYTHqmSXbCN_eTj6T5GQ7NF0lKosOtWOLbPK-1orZQ,4637
nagini_translation/mypy_patches/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/mypy_patches/column_info_patch.py,sha256=HroJ06Wy1Vpqi-GCaFQfg6JVth7AmScb0oeswBoz1pw,1472
nagini_translation/mypy_patches/optional_patch.py,sha256=Y6UR-BBZuqlNt_E8-Yv_6jWghFrwhwV0_SruRPH7k0o,1056
nagini_translation/sif/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/sif/lib/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/sif/lib/util.py,sha256=5UZAbbHiGg1q0koytXh1c7JNlz4uYYa2ELen6Y-bKEM,3369
nagini_translation/sif/lib/viper_ast_extended.py,sha256=Q685sArW7yoy-6tedYuvIrEXH8mCAnDLjhXl6ekRL40,5598
nagini_translation/sif/translators/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/sif/translators/call.py,sha256=JcX1Tjh_xYGjUJeU66sO3Fr6InqomUyM6MfL93ikJag,1216
nagini_translation/sif/translators/contract.py,sha256=9DtNCxT3DcSoJADCVI-0KW1nxojtBdIg4055bczeHnI,4870
nagini_translation/sif/translators/expression.py,sha256=2I2wthSW9CqVDeDGWL6d40GnmzZ5HI6uuOXCD6QKZFc,1478
nagini_translation/sif/translators/method.py,sha256=F4Z6lGvOlu_vkIdsqoeENUUwQphgPiGtQU2mzExYlvo,3441
nagini_translation/sif/translators/program.py,sha256=dlcYi6Yw0KJOQIf546M_A7lAFIubgs0JQFDUWyqjsAs,728
nagini_translation/sif/translators/statement.py,sha256=9Je-B_lEt6FxNwyCOo86uo5gWSjXe_H8OtIm8sb4PZk,14609
nagini_translation/translators/__init__.py,sha256=1zIVDe34wl5haB4LKuZV8RmWoXrPbAG724oI2znTtzg,200
nagini_translation/translators/abstract.py,sha256=Sb34tNDS8oAiJMIa7UWDERYkZEkZRZm5hnBnVpVXguY,17109
nagini_translation/translators/call.py,sha256=bNl3bVqxu2kx0PFz692hRNhWJSHWNxmUualhU9buTfQ,80745
nagini_translation/translators/common.py,sha256=cfFz7_C4w2czjgdv1fW7S0iPtPeWFfFAJBKJM0FvRXA,41439
nagini_translation/translators/contract.py,sha256=YwmNhnHQIVG0-gvF4_OsiF75U5RoakyjApbsEkZRq5Q,45572
nagini_translation/translators/expression.py,sha256=IMhogy7f4C60Vi4h1XR77LEcLPEfMSs0-cFxNcq5q8Q,60017
nagini_translation/translators/method.py,sha256=e3dOP08sihGPuy94li3oX4jDod96rX2KviRAxCqiZgE,44227
nagini_translation/translators/permission.py,sha256=LxXsNsoyu3UoqTE2HRa37QJudKIfDHREYyXN2HcspuQ,8372
nagini_translation/translators/predicate.py,sha256=_svBWi_t7Rnu48MocSBOamZWs_UaeoNypbIbPC6n3hQ,6726
nagini_translation/translators/program.py,sha256=mO_vGpx6Cc1da6T5vAabD50M0962Hd6TOIRWsDIcSGY,69443
nagini_translation/translators/pure.py,sha256=1M4C6MnJ4XR1ctvG4PwnM5ltL1nriYZinoVv9O1Z9Fo,12834
nagini_translation/translators/statement.py,sha256=jXfl5vPMm1gMb9vexg0ilxTEunqgOoUvSDYq4vfxWNo,69624
nagini_translation/translators/type.py,sha256=ef31YW-ZZwCWfXuvhzjL8jz1Vwqgp2k-0w_LNFQFbGc,3750
nagini_translation/translators/type_domain_factory.py,sha256=OeqI6fuk9y_K9pBLZOqtOYm0kGK9XG-8Z044uELaHIc,51127
nagini_translation/translators/io_operation/__init__.py,sha256=s6n4Jb6Qw_BB6fz4LF_c6j9lACrcbtYuEXFxtigWre8,4855
nagini_translation/translators/io_operation/common.py,sha256=xCDAD3aKWzhGV_riQ__iV2HFdh70khZbmIDzUXSsyyg,3205
nagini_translation/translators/io_operation/definition.py,sha256=DIClrCSP2-vBkUB5Cb3dTFNNURdb105grPMtUBnkc_Q,7446
nagini_translation/translators/io_operation/interface.py,sha256=xPljJuNutv4sixHSe1lhy5pNeoQKkvlwWZwgog-s_oc,3131
nagini_translation/translators/io_operation/opener.py,sha256=McTa307AeJBkzbIWs1NmQ6jB3YO36yHwsU6G7Jpqx-w,7609
nagini_translation/translators/io_operation/result_translator.py,sha256=rMBn8CvMjy63Fn7JHw8Qxr_LV9A2X1HNr8Lrx0J8qjg,7431
nagini_translation/translators/io_operation/termination_check.py,sha256=o6AjU283ZR9JreE7yt3eZZ_eeWmxNmvQIsUwphSlFL4,7688
nagini_translation/translators/io_operation/use.py,sha256=V8yo_ZsTF0OjwKMEs2B1iK81uHHk2vdVsqkJacVRVvk,11915
nagini_translation/translators/io_operation/utils.py,sha256=vVvqC3fru8rhDzsi4cqs2QJj3AauK2VD7Sdhb00m2zk,2589
nagini_translation/translators/obligation/__init__.py,sha256=Kp8w6l5QySA7-MhuB1Bemb_Miq3OIXU9tnHNKpxUCuQ,340
nagini_translation/translators/obligation/common.py,sha256=wD20S97dqdPjyEvqHgKN-BUV4HPApJtXcr3osQsskrk,4431
nagini_translation/translators/obligation/fork.py,sha256=9l0BFWStxGH3gSaITo1bX3WS_5yHnSCI1N1QIgymMf4,11202
nagini_translation/translators/obligation/inexhale.py,sha256=JvxT_gzFI6jUmeqbXPNjx3FqbrFwMaU3mbPIwEGWmgc,8509
nagini_translation/translators/obligation/interface.py,sha256=BHPX3btoJEa4m6v0eIrnFSfpW5xjgHscVH2vkySXdwo,9581
nagini_translation/translators/obligation/loop.py,sha256=6Jjnn0dp_V2hG_CcK0XnkJAsrSKKKZ5HQrBjLfaPV_w,2600
nagini_translation/translators/obligation/loop_node.py,sha256=L7mhSNaMn6cnEUB7NbbHzFQ6FBo03Blt5UnxAgPLCsE,11131
nagini_translation/translators/obligation/manager.py,sha256=csy6fKIjjtu1EfKRNO5lxnGsZytoi_VKjQzdLIXyhRE,3045
nagini_translation/translators/obligation/measures.py,sha256=ZYkCsdP-ZyBPj06c_-KpjvaK7ArjCH-xoMaj9Y0aRx4,3273
nagini_translation/translators/obligation/method.py,sha256=q_vE0PM-PH5MVc9nsIiLoYH9an0yAk5rYMXHFWSN1n4,4570
nagini_translation/translators/obligation/method_call_node.py,sha256=nuQwM7ownlNL766OH8_OnyyKWcdbnIQul6-w-zNFkI4,4243
nagini_translation/translators/obligation/method_node.py,sha256=hL6W8XlfX0lRK6pSQT4JjEnsBz8D1M5c6L4FMwBNUag,14163
nagini_translation/translators/obligation/node_constructor.py,sha256=A0SIL0cbwvLqB98rXoXj0FsjO3DIB3DXxF3U7Y84_Tw,5139
nagini_translation/translators/obligation/obligation_info.py,sha256=TMXmlnMvrdX3_SFmw08QgV5WHE_1aZm4L_6mU6Lnt40,19565
nagini_translation/translators/obligation/utils.py,sha256=kpBT25Rw9Fw5HOI1o_C9HKsK-phR70dWIohFf_42yyw,1615
nagini_translation/translators/obligation/waitlevel.py,sha256=P-qILFgUC8MfRkx5vLPTGGwgsH__Fu7dAtJGK9rVarc,8692
nagini_translation/translators/obligation/types/__init__.py,sha256=9gj1KLREYiixyll21IJdLX45KpzLYS48VhAvjGxV9jc,408
nagini_translation/translators/obligation/types/base.py,sha256=mjV2mk85ZhMywnpjwqxBcmdtbcxhiOo6T25ZylMcZhk,5213
nagini_translation/translators/obligation/types/must_invoke.py,sha256=vj5jPHFOriFsfashK213ZbUruwrfToYLr7yoJzbUwyE,3902
nagini_translation/translators/obligation/types/must_release.py,sha256=WuypI3SMXWMiyGkh703rk6KkkCp54EEGjiTPOpJE1Rw,3220
nagini_translation/translators/obligation/types/must_terminate.py,sha256=4zXz03vL-sqWMqqdsyiJDoLGvU-0651cqas1VoJAWNw,10753
nagini-0.8.dist-info/LICENSE.txt,sha256=HyVuytGSiAUQ6ErWBHTqt1iSGHhLmlC8fO7jTCuR8dU,16725
nagini-0.8.dist-info/METADATA,sha256=5VCiNJvYomKccWERvNP6vC7mZk_UNFL7Rd8ILU-EhCo,766
nagini-0.8.dist-info/WHEEL,sha256=U88EhGIw8Sj2_phqajeu_EAi3RAo8-C6zV3REsWbWbs,92
nagini-0.8.dist-info/entry_points.txt,sha256=Zsve3MFCPY1fHEiusrUqS1hERnh4DPtlz1hTP4hiyYc,57
nagini-0.8.dist-info/top_level.txt,sha256=DPm_IoHgncWTKcHdQunxbwj2nTx3_Z_QbBkbAqgiNzs,36
nagini-0.8.dist-info/RECORD,,
