{ "info": { "author": "Viper Team", "author_email": "viper@inf.ethz.ch", "bugtrack_url": null, "classifiers": [ "Development Status :: 3 - Alpha", "Environment :: Console", "Intended Audience :: Developers", "License :: OSI Approved :: Mozilla Public License 2.0 (MPL 2.0)", "Operating System :: OS Independent", "Programming Language :: Python :: 3 :: Only", "Topic :: Software Development" ], "description": "\nNagini is an automatic verifier for statically typed Python programs, based on the `Viper `_ verification infrastructure. Nagini is being developed at the `Chair of Programming Methodology `_ at ETH Zurich as part of the `VerifiedSCION `_ project.\n\nOur CAV 2018 tool paper describing Nagini can be found `here `_. See `the Wiki `_ for the documentation of Nagini's specification language. \n\nYou can try a (rather slow) online version of Nagini `on this website `_.\n\nFor use with the PyCharm IDE, try the `Nagini PyCharm plugin `_.\n\nDependencies (Ubuntu Linux)\n===================================\n\n1. Install Java 8 (64 bit), Mercurial, Git and Python 3.6 (64 bit, newer versions should work but are currently untested) and the required libraries::\n\n sudo apt-get install python3-dev libzmq3-dev\n\n For usage with the Viper's verification condition generation backend Carbon, you will also need to install the Mono runtime.\n\n2. Download and extract `ViperToolsLinux `_\n\nDependencies (Windows)\n==========================\n\n1. Install Java (64 bit), Mercurial, Git and Python 3.5 (64 bit), s.t. java, hg, git and python are all available from the command line.\n\n2. Install either Visual C++ Build Tools 2015 (http://go.microsoft.com/fwlink/?LinkId=691126) or Visual Studio 2015. For the latter, make sure to choose the option \"Common Tools for Visual C++ 2015\" in the setup (see https://blogs.msdn.microsoft.com/vcblog/2015/07/24/setup-changes-in-visual-studio-2015-affecting-c-developers/ for an explanation).\n\n3. Download and extract `ViperToolsWin `_\n\nGetting Started\n===============\n\n1. Create a virtual environment::\n\n virtualenv --python=python3 \n\n2. Install Nagini::\n\n .//bin/pip install nagini\n\n\nCommand Line Usage\n==================\n\nTo verify a specific file from the nagini directory, run::\n\n .//bin/nagini [OPTIONS] path-to-file.py\n\n\nThe options ``--z3`` and ``--viper-jar-path`` are mandatory and must point to a Z3 executable and a JAR file containing the desired Viper backend. E.g., to use the Symbolic Execution backend (Silicon) from the provided Viper Tools file, call ::\n\n .//bin/nagini --z3 /z3/bin/z3 --viper-jar-path /backends/silicon.jar path-to-file.py\n\nThe following command line options are available::\n\n ``--verifier`` \n Selects the Viper backend to use for verification.\n Possible options are ``silicon`` (for Symbolic Execution) and ``carbon`` \n (for Verification Condition Generation based on Boogie). \n Default: ``silicon``.\n\n ``--select`` \n Select which functions/methods/classes to verify. Expects a comma-\n separated list of names.\n\n ``--z3`` \n Sets the path of the Z3 executable. Always required. Alternatively, the\n ``Z3_EXE`` environment variable can be set.\n\n ``--boogie`` \n Sets the path of the Boogie executable. Required if the Carbon backend\n is selected. Alternatively, the ``BOOGIE_EXE`` environment variable can be\n set.\n\n ``--viper-jar-path`` \n Sets the path to the required Viper binaries (``silicon.jar`` or\n ``carbon.jar``). Only the binary for the selected backend is\n required. You can either use the provided binary packages\n (see above) or compile your own from source (see below).\n Expects either a single path or a colon- (Unix) or semicolon-\n (Windows) separated list of paths. Alternatively, the environment\n variables ``SILICONJAR``, ``CARBONJAR`` or ``VIPERJAR`` can be set.\n\nTo see all possible command line options, invoke ``./bin/nagini`` without arguments.\n\n\nAlternative Viper Versions\n==========================\n\nTo use a more recent or custom version of the Viper infrastructure, follow the\n`instructions here `_. Look for\n``sbt assembly`` to find instructions for packaging the required JAR files. Use the\nparameters mentioned above to instruct Nagini to use your custom Viper version.\n\n\nTroubleshooting\n=======================\n\n1. On Windows: During the setup, you get an error like ``Microsoft Visual C++ 14.0 is required.`` or ``Unable to fnd vcvarsall.bat``: \n\n Python cannot find the required Visual Studio 2015 C++ installation, make sure you have either installed the Build Tools or checked the \"Common Tools\" option in your regular VS 2015 installation (see above).\n\n2. While verifying a file, you get a stack trace ending with something like ``No matching overloads found``:\n\n The version of Viper you're using does not match your version of Nagini. Try updating both to the newest version.\n\n3. When using the Carbon backend, Boogie crashes:\n\n The Boogie binaries in ViperToolsWin don't seem to work on all systems; in this case, compile Boogie from scratch and set the Boogie path point to the new (or an existing) Boogie installation.\n\nBuild Status\n============\n\n.. image:: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=nagini&style=plastic\n :alt: Build Status\n :target: https://pmbuilds.inf.ethz.ch/job/nagini\n\n\n", "description_content_type": "", "docs_url": null, "download_url": "", "downloads": { "last_day": -1, "last_month": -1, "last_week": -1 }, "home_page": "http://www.pm.inf.ethz.ch/research/nagini.html", "keywords": "", "license": "MPL-2.0", "maintainer": "", "maintainer_email": "", "name": "nagini", "package_url": "https://pypi.org/project/nagini/", "platform": "", "project_url": "https://pypi.org/project/nagini/", "project_urls": { "Homepage": "http://www.pm.inf.ethz.ch/research/nagini.html" }, "release_url": "https://pypi.org/project/nagini/0.8.3/", "requires_dist": [ "mypy-lang (==0.4.5)", "toposort (==1.5)", "jpype1 (==0.6.2)", "astunparse (==1.6.2)", "typed-ast (==0.6.3)", "pytest (==3.3.0)", "z3-solver" ], "requires_python": "", "summary": "Static verifier for Python 3, based on Viper.", "version": "0.8.3" }, "last_serial": 5999229, "releases": { "0.8": [ { "comment_text": "", "digests": { "md5": "2b4cac051004e6455230f04927a1bbe9", "sha256": "13869330c1c9af423ba7286403783a2be13e8cc640d61160bf627e83a12e30e4" }, "downloads": -1, "filename": "nagini-0.8-py3-none-any.whl", "has_sig": false, "md5_digest": "2b4cac051004e6455230f04927a1bbe9", "packagetype": "bdist_wheel", "python_version": "py3", "requires_python": null, "size": 290367, "upload_time": "2019-02-20T10:56:03", "url": "https://files.pythonhosted.org/packages/ed/d0/4d7547b5f2d5675880010b4f77291def5b4090cc5369ab60b7079322d2d0/nagini-0.8-py3-none-any.whl" }, { "comment_text": "", "digests": { "md5": "e23dca2bfda7f08928867a42cf3a7372", "sha256": "e74c0b8e0c011c0e1b46e443fa8b7d6d408c6d01f74be692f60e494d9e938c47" }, "downloads": -1, "filename": "nagini-0.8.tar.gz", "has_sig": false, "md5_digest": "e23dca2bfda7f08928867a42cf3a7372", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 219837, "upload_time": "2019-02-20T10:56:05", "url": "https://files.pythonhosted.org/packages/9f/43/3525e2244cb186f430f1c4d2d7a3be67ede97c3a59b3009e80c1808b415a/nagini-0.8.tar.gz" } ], "0.8.1": [ { "comment_text": "", "digests": { "md5": "ea4c80d61df748d424dac6e6972283bb", "sha256": "bdf4b43f8c94b5675e4561666c7e41e5675c8a130539bc7abba9d5ead1070457" }, "downloads": -1, "filename": "nagini-0.8.1-py3-none-any.whl", "has_sig": false, "md5_digest": "ea4c80d61df748d424dac6e6972283bb", "packagetype": "bdist_wheel", "python_version": "py3", "requires_python": null, "size": 311185, "upload_time": "2019-02-20T11:15:00", "url": "https://files.pythonhosted.org/packages/c3/5a/e366ee797b84260b07463dc05a9272a14c6c5f4e5220f895d759f4032d30/nagini-0.8.1-py3-none-any.whl" }, { "comment_text": "", "digests": { "md5": "239fe0204331a24522acea10f44db3d0", "sha256": "8aad7fa121176f03290bbfeb27eca05ff7efd56a57806bc8553661d6e306ed5e" }, "downloads": -1, "filename": "nagini-0.8.1.tar.gz", "has_sig": false, "md5_digest": "239fe0204331a24522acea10f44db3d0", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 233138, "upload_time": "2019-02-20T11:15:04", "url": "https://files.pythonhosted.org/packages/54/5b/ca19ca7d7e53a9c653680b9c0b461c76320ce7c7ffc6d0e0d1b767fe8b64/nagini-0.8.1.tar.gz" } ], "0.8.2": [ { "comment_text": "", "digests": { "md5": "6f9babe3c5b70cadef0e1f9ff9cd16c9", "sha256": "76b5eb56bdefb4690a2248db6a7e7f4e4fe031240596c960de23ee115ef3885a" }, "downloads": -1, "filename": "nagini-0.8.2-py3-none-any.whl", "has_sig": false, "md5_digest": "6f9babe3c5b70cadef0e1f9ff9cd16c9", "packagetype": "bdist_wheel", "python_version": "py3", "requires_python": null, "size": 313441, "upload_time": "2019-02-20T13:21:31", "url": "https://files.pythonhosted.org/packages/02/2f/7cd1ab776916527cd31601ece46bb0f6ecfd5c7ff649f6d34d8b3d6db231/nagini-0.8.2-py3-none-any.whl" }, { "comment_text": "", "digests": { "md5": "33a87503c38de4a93673ea0a9162082a", "sha256": "e678091c2cfb841829a20a7a63bd86d53785bb283ea4e8fc3050d1a0657c30b1" }, "downloads": -1, "filename": "nagini-0.8.2.tar.gz", "has_sig": false, "md5_digest": "33a87503c38de4a93673ea0a9162082a", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 232828, "upload_time": "2019-02-20T13:21:33", "url": "https://files.pythonhosted.org/packages/98/27/8e78dd495702acab6cd31dd30a42d242b3983542f7ddf16c883a502a69ed/nagini-0.8.2.tar.gz" } ], "0.8.3": [ { "comment_text": "", "digests": { "md5": "809f7ee7d93a68354209b600a8d54e6d", "sha256": "a161ec6308ed4fa98821dde29d1d8f34756682c038c366256579129c1ae3d3ff" }, "downloads": -1, "filename": "nagini-0.8.3-py3-none-any.whl", "has_sig": false, "md5_digest": "809f7ee7d93a68354209b600a8d54e6d", "packagetype": "bdist_wheel", "python_version": "py3", "requires_python": null, "size": 55915530, "upload_time": "2019-03-22T14:20:12", "url": "https://files.pythonhosted.org/packages/96/50/941bc59b3c50bcbc1fab88409caf11b1b90bd9f30fec156f3eb256899a71/nagini-0.8.3-py3-none-any.whl" }, { "comment_text": "", "digests": { "md5": "c3a5ae643f56c08fb7ed50c744a20668", "sha256": "28cb9660f805c54d8f94f265f09900ad4eb95b3fae8ec5fd655062189fcbc219" }, "downloads": -1, "filename": "nagini-0.8.3.tar.gz", "has_sig": false, "md5_digest": "c3a5ae643f56c08fb7ed50c744a20668", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 55816441, "upload_time": "2019-03-22T14:20:21", "url": "https://files.pythonhosted.org/packages/ee/d4/f56c3c440a7f6196b915e99d3be8589f1b2ba7b562767eb1455835aae284/nagini-0.8.3.tar.gz" } ] }, "urls": [ { "comment_text": "", "digests": { "md5": "809f7ee7d93a68354209b600a8d54e6d", "sha256": "a161ec6308ed4fa98821dde29d1d8f34756682c038c366256579129c1ae3d3ff" }, "downloads": -1, "filename": "nagini-0.8.3-py3-none-any.whl", "has_sig": false, "md5_digest": "809f7ee7d93a68354209b600a8d54e6d", "packagetype": "bdist_wheel", "python_version": "py3", "requires_python": null, "size": 55915530, "upload_time": "2019-03-22T14:20:12", "url": "https://files.pythonhosted.org/packages/96/50/941bc59b3c50bcbc1fab88409caf11b1b90bd9f30fec156f3eb256899a71/nagini-0.8.3-py3-none-any.whl" }, { "comment_text": "", "digests": { "md5": "c3a5ae643f56c08fb7ed50c744a20668", "sha256": "28cb9660f805c54d8f94f265f09900ad4eb95b3fae8ec5fd655062189fcbc219" }, "downloads": -1, "filename": "nagini-0.8.3.tar.gz", "has_sig": false, "md5_digest": "c3a5ae643f56c08fb7ed50c744a20668", "packagetype": "sdist", "python_version": "source", "requires_python": null, "size": 55816441, "upload_time": "2019-03-22T14:20:21", "url": "https://files.pythonhosted.org/packages/ee/d4/f56c3c440a7f6196b915e99d3be8589f1b2ba7b562767eb1455835aae284/nagini-0.8.3.tar.gz" } ] }