diff --git a/.gitmodules b/.gitmodules index 7c299f97..f8ce2b45 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "test/unit-test/CMock"] path = test/unit-test/CMock url = https://github.com/ThrowTheSwitch/CMock +[submodule "test/cbmc/aws-templates-for-cbmc-proofs"] + path = test/cbmc/aws-templates-for-cbmc-proofs + url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git diff --git a/test/cbmc/.gitignore b/test/cbmc/.gitignore index cb6ef5cd..55a5c751 100644 --- a/test/cbmc/.gitignore +++ b/test/cbmc/.gitignore @@ -9,6 +9,7 @@ TAGS-* # Emitted by Arpa arpa_cmake/ +arpa-validation-logs/ Makefile.arpa # These files should be overwritten whenever prepare.py runs diff --git a/test/cbmc/aws-templates-for-cbmc-proofs b/test/cbmc/aws-templates-for-cbmc-proofs new file mode 160000 index 00000000..ca24f065 --- /dev/null +++ b/test/cbmc/aws-templates-for-cbmc-proofs @@ -0,0 +1 @@ +Subproject commit ca24f0651a8ae68145d965f0fadec2e5a32dfe8a diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/.gitignore b/test/cbmc/aws-templates-for-cbmc-proofs/.gitignore deleted file mode 100644 index 8025bc04..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -__pycache__ -*~ diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/CODE_OF_CONDUCT.md b/test/cbmc/aws-templates-for-cbmc-proofs/CODE_OF_CONDUCT.md deleted file mode 100644 index 5b627cfa..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,4 +0,0 @@ -## Code of Conduct -This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct). -For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact -opensource-codeofconduct@amazon.com with any additional questions or comments. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/CONTRIBUTING.md b/test/cbmc/aws-templates-for-cbmc-proofs/CONTRIBUTING.md deleted file mode 100644 index 914e0741..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/CONTRIBUTING.md +++ /dev/null @@ -1,61 +0,0 @@ -# Contributing Guidelines - -Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional -documentation, we greatly value feedback and contributions from our community. - -Please read through this document before submitting any issues or pull requests to ensure we have all the necessary -information to effectively respond to your bug report or contribution. - - -## Reporting Bugs/Feature Requests - -We welcome you to use the GitHub issue tracker to report bugs or suggest features. - -When filing an issue, please check existing open, or recently closed, issues to make sure somebody else hasn't already -reported the issue. Please try to include as much information as you can. Details like these are incredibly useful: - -* A reproducible test case or series of steps -* The version of our code being used -* Any modifications you've made relevant to the bug -* Anything unusual about your environment or deployment - - -## Contributing via Pull Requests -Contributions via pull requests are much appreciated. Before sending us a pull request, please ensure that: - -1. You are working against the latest source on the *master* branch. -2. You check existing open, and recently merged, pull requests to make sure someone else hasn't addressed the problem already. -3. You open an issue to discuss any significant work - we would hate for your time to be wasted. - -To send us a pull request, please: - -1. Fork the repository. -2. Modify the source; please focus on the specific change you are contributing. If you also reformat all the code, it will be hard for us to focus on your change. -3. Ensure local tests pass. -4. Commit to your fork using clear commit messages. -5. Send us a pull request, answering any default questions in the pull request interface. -6. Pay attention to any automated CI failures reported in the pull request, and stay involved in the conversation. - -GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and -[creating a pull request](https://help.github.com/articles/creating-a-pull-request/). - - -## Finding contributions to work on -Looking at the existing issues is a great way to find something to contribute on. As our projects, by default, use the default GitHub issue labels (enhancement/bug/duplicate/help wanted/invalid/question/wontfix), looking at any 'help wanted' issues is a great place to start. - - -## Code of Conduct -This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct). -For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact -opensource-codeofconduct@amazon.com with any additional questions or comments. - - -## Security issue notifications -If you discover a potential security issue in this project we ask that you notify AWS/Amazon Security via our [vulnerability reporting page](http://aws.amazon.com/security/vulnerability-reporting/). Please do **not** create a public github issue. - - -## Licensing - -See the [LICENSE](LICENSE) file for our project's licensing. We will ask you to confirm the licensing of your contribution. - -We may ask you to sign a [Contributor License Agreement (CLA)](http://en.wikipedia.org/wiki/Contributor_License_Agreement) for larger changes. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/LICENSE b/test/cbmc/aws-templates-for-cbmc-proofs/LICENSE deleted file mode 100644 index 67db8588..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/LICENSE +++ /dev/null @@ -1,175 +0,0 @@ - - Apache License - Version 2.0, January 2004 - http://www.apache.org/licenses/ - - TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION - - 1. Definitions. - - "License" shall mean the terms and conditions for use, reproduction, - and distribution as defined by Sections 1 through 9 of this document. - - "Licensor" shall mean the copyright owner or entity authorized by - the copyright owner that is granting the License. - - "Legal Entity" shall mean the union of the acting entity and all - other entities that control, are controlled by, or are under common - control with that entity. For the purposes of this definition, - "control" means (i) the power, direct or indirect, to cause the - direction or management of such entity, whether by contract or - otherwise, or (ii) ownership of fifty percent (50%) or more of the - outstanding shares, or (iii) beneficial ownership of such entity. - - "You" (or "Your") shall mean an individual or Legal Entity - exercising permissions granted by this License. - - "Source" form shall mean the preferred form for making modifications, - including but not limited to software source code, documentation - source, and configuration files. - - "Object" form shall mean any form resulting from mechanical - transformation or translation of a Source form, including but - not limited to compiled object code, generated documentation, - and conversions to other media types. - - "Work" shall mean the work of authorship, whether in Source or - Object form, made available under the License, as indicated by a - copyright notice that is included in or attached to the work - (an example is provided in the Appendix below). - - "Derivative Works" shall mean any work, whether in Source or Object - form, that is based on (or derived from) the Work and for which the - editorial revisions, annotations, elaborations, or other modifications - represent, as a whole, an original work of authorship. For the purposes - of this License, Derivative Works shall not include works that remain - separable from, or merely link (or bind by name) to the interfaces of, - the Work and Derivative Works thereof. - - "Contribution" shall mean any work of authorship, including - the original version of the Work and any modifications or additions - to that Work or Derivative Works thereof, that is intentionally - submitted to Licensor for inclusion in the Work by the copyright owner - or by an individual or Legal Entity authorized to submit on behalf of - the copyright owner. For the purposes of this definition, "submitted" - means any form of electronic, verbal, or written communication sent - to the Licensor or its representatives, including but not limited to - communication on electronic mailing lists, source code control systems, - and issue tracking systems that are managed by, or on behalf of, the - Licensor for the purpose of discussing and improving the Work, but - excluding communication that is conspicuously marked or otherwise - designated in writing by the copyright owner as "Not a Contribution." - - "Contributor" shall mean Licensor and any individual or Legal Entity - on behalf of whom a Contribution has been received by Licensor and - subsequently incorporated within the Work. - - 2. Grant of Copyright License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - copyright license to reproduce, prepare Derivative Works of, - publicly display, publicly perform, sublicense, and distribute the - Work and such Derivative Works in Source or Object form. - - 3. Grant of Patent License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - (except as stated in this section) patent license to make, have made, - use, offer to sell, sell, import, and otherwise transfer the Work, - where such license applies only to those patent claims licensable - by such Contributor that are necessarily infringed by their - Contribution(s) alone or by combination of their Contribution(s) - with the Work to which such Contribution(s) was submitted. If You - institute patent litigation against any entity (including a - cross-claim or counterclaim in a lawsuit) alleging that the Work - or a Contribution incorporated within the Work constitutes direct - or contributory patent infringement, then any patent licenses - granted to You under this License for that Work shall terminate - as of the date such litigation is filed. - - 4. Redistribution. You may reproduce and distribute copies of the - Work or Derivative Works thereof in any medium, with or without - modifications, and in Source or Object form, provided that You - meet the following conditions: - - (a) You must give any other recipients of the Work or - Derivative Works a copy of this License; and - - (b) You must cause any modified files to carry prominent notices - stating that You changed the files; and - - (c) You must retain, in the Source form of any Derivative Works - that You distribute, all copyright, patent, trademark, and - attribution notices from the Source form of the Work, - excluding those notices that do not pertain to any part of - the Derivative Works; and - - (d) If the Work includes a "NOTICE" text file as part of its - distribution, then any Derivative Works that You distribute must - include a readable copy of the attribution notices contained - within such NOTICE file, excluding those notices that do not - pertain to any part of the Derivative Works, in at least one - of the following places: within a NOTICE text file distributed - as part of the Derivative Works; within the Source form or - documentation, if provided along with the Derivative Works; or, - within a display generated by the Derivative Works, if and - wherever such third-party notices normally appear. The contents - of the NOTICE file are for informational purposes only and - do not modify the License. You may add Your own attribution - notices within Derivative Works that You distribute, alongside - or as an addendum to the NOTICE text from the Work, provided - that such additional attribution notices cannot be construed - as modifying the License. - - You may add Your own copyright statement to Your modifications and - may provide additional or different license terms and conditions - for use, reproduction, or distribution of Your modifications, or - for any such Derivative Works as a whole, provided Your use, - reproduction, and distribution of the Work otherwise complies with - the conditions stated in this License. - - 5. Submission of Contributions. Unless You explicitly state otherwise, - any Contribution intentionally submitted for inclusion in the Work - by You to the Licensor shall be under the terms and conditions of - this License, without any additional terms or conditions. - Notwithstanding the above, nothing herein shall supersede or modify - the terms of any separate license agreement you may have executed - with Licensor regarding such Contributions. - - 6. Trademarks. This License does not grant permission to use the trade - names, trademarks, service marks, or product names of the Licensor, - except as required for reasonable and customary use in describing the - origin of the Work and reproducing the content of the NOTICE file. - - 7. Disclaimer of Warranty. Unless required by applicable law or - agreed to in writing, Licensor provides the Work (and each - Contributor provides its Contributions) on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or - implied, including, without limitation, any warranties or conditions - of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A - PARTICULAR PURPOSE. You are solely responsible for determining the - appropriateness of using or redistributing the Work and assume any - risks associated with Your exercise of permissions under this License. - - 8. Limitation of Liability. In no event and under no legal theory, - whether in tort (including negligence), contract, or otherwise, - unless required by applicable law (such as deliberate and grossly - negligent acts) or agreed to in writing, shall any Contributor be - liable to You for damages, including any direct, indirect, special, - incidental, or consequential damages of any character arising as a - result of this License or out of the use or inability to use the - Work (including but not limited to damages for loss of goodwill, - work stoppage, computer failure or malfunction, or any and all - other commercial damages or losses), even if such Contributor - has been advised of the possibility of such damages. - - 9. Accepting Warranty or Additional Liability. While redistributing - the Work or Derivative Works thereof, You may choose to offer, - and charge a fee for, acceptance of support, warranty, indemnity, - or other liability obligations and/or rights consistent with this - License. However, in accepting such obligations, You may act only - on Your own behalf and on Your sole responsibility, not on behalf - of any other Contributor, and only if You agree to indemnify, - defend, and hold each Contributor harmless for any liability - incurred by, or claims asserted against, such Contributor by reason - of your accepting any such warranty or additional liability. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/NOTICE b/test/cbmc/aws-templates-for-cbmc-proofs/NOTICE deleted file mode 100644 index 616fc588..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/NOTICE +++ /dev/null @@ -1 +0,0 @@ -Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/README.md b/test/cbmc/aws-templates-for-cbmc-proofs/README.md deleted file mode 100644 index b2666b7c..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/README.md +++ /dev/null @@ -1,59 +0,0 @@ -# AWS Templates for CBMC Proofs - -This repository includes templates and scripts intended to make it -easy to get started writing CBMC proofs for your code. The first -script installs proof infrastructure in the form of a few directories -containing code, templates, and Makefiles that facilitate writing CBMC proofs -in general. The second script installs, for a particular proof, a directory -containing skeletons of all the files needed to start writing that proof. - -## Proof infrastructure set up - -The script scripts/setup.py will set up the infrastructure for CBMC proofs. - -* Choose the path to the source root (eg, /usr/project) -* Choose the path to a directory under the source root that should hold - the infrastructure (eg, /usr/project/cbmc) -* Submodule the AWS-templates-for-CBMC repository into this directory (eg, - /usr/project/cbmc/aws-templates-for-cbmc) - ``` - cd /usr/project/cbmc - git submodule add https://github.com/awslabs/aws-templates-for-cbmc-proofs.git aws-templates-for-cbmc-proofs - ``` -* Use the script `aws-templates-for-cbmc-proofs/scripts/setup.py` to - setup the standard directory structure for CBMC proof. - ``` - cd /usr/project/cbmc - python3 aws-templates-for-cbmc-proofs/scripts/setup.py - ``` - The script will ask for the path to the source root `/usr/project`. - The script will install the directories - * include: contains include files for the proofs - * sources: contains source code for the proofs - * stubs: contains stubs for the proofs - * proofs: contains the proofs themselves (the proof root). - -## Proof set up - -The script scripts/setup-proof.py will set up a directory for a CBMC proof. - -* Change to a directory under the proof root (/usr/project/cbmc/proofs) -* Run the script `aws-templates-for-cbmc/scripts/setup-proof.py` and give - * The name of the function under test. - * The path to the source file defining the function under test. - * The path to the source root - -The script will create a directory named for the function, and will -install files needed to run the proof. - -You can cut and paste into the files, and type `make` to run and debug -the proof. For more details, see [the instructions in the training -materials repository](github.com/awslabs/aws-training-materials-for-cbmc/SETUP.md). - -## Security - -See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information. - -## License - -This project is licensed under the Apache-2.0 License. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/scripts/setup-proof.py b/test/cbmc/aws-templates-for-cbmc-proofs/scripts/setup-proof.py deleted file mode 100755 index e4a3fd6d..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/scripts/setup-proof.py +++ /dev/null @@ -1,74 +0,0 @@ -#!/usr/bin/env python3 - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -"""Set up a CBMC proof.""" - -import logging -import os -import shutil - -import util - -def proof_template_filenames(): - directory = os.path.join(util.templates_root(), util.PROOF_TEMPLATES) - return os.listdir(directory) - -def read_proof_template(filename): - directory = os.path.join(util.templates_root(), util.PROOF_TEMPLATES) - with open(os.path.join(directory, filename)) as data: - return data.read().splitlines() - -def write_proof_template(lines, filename, directory): - with open(os.path.join(directory, filename), "w") as data: - data.write('\n'.join(lines)) - -def rename_proof_harness(function, directory): - shutil.move(os.path.join(directory, "FUNCTION_harness.c"), - os.path.join(directory, "{}_harness.c".format(function))) - -def patch_function_name(lines, function): - return [line.replace("<__FUNCTION_NAME__>", function) for line in lines] - -def patch_path_to_makefile(lines, proof_root, proof_dir): - path = os.path.relpath(proof_root, proof_dir) - return [line.replace("<__PATH_TO_MAKEFILE__>", path) for line in lines] - -def patch_path_to_proof_root(lines, proof_root, source_root): - path = os.path.relpath(proof_root, source_root) - return [line.replace("<__PATH_TO_PROOF_ROOT__>", path) for line in lines] - -def patch_path_to_source_file(lines, source_file, source_root): - path = os.path.relpath(source_file, source_root) - return [line.replace("<__PATH_TO_SOURCE_FILE__>", path) for line in lines] - -def main(): - """Set up CBMC proof.""" - - logging.basicConfig(format='%(levelname)s: %(message)s') - - print("What is the function name? ", end="") - function = input() - - print("What is the source file that defines the function? ", end="") - source_file = os.path.abspath(os.path.expanduser(input())) - - source_root = util.read_source_root() - proof_root = util.read_proof_root() - - proof_dir = os.path.abspath(function) - os.mkdir(proof_dir) - - for filename in proof_template_filenames(): - lines = read_proof_template(filename) - lines = patch_function_name(lines, function) - lines = patch_path_to_makefile(lines, proof_root, proof_dir) - lines = patch_path_to_proof_root(lines, proof_root, source_root) - lines = patch_path_to_source_file(lines, source_file, source_root) - write_proof_template(lines, filename, proof_dir) - - rename_proof_harness(function, proof_dir) - -if __name__ == "__main__": - main() diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/scripts/setup.py b/test/cbmc/aws-templates-for-cbmc-proofs/scripts/setup.py deleted file mode 100755 index c242d8e3..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/scripts/setup.py +++ /dev/null @@ -1,38 +0,0 @@ -#!/usr/bin/env python3 - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -"""Set up the CBMC proof instrastructure.""" - -import logging -import os - -import util - -def create_makefile_template_defines(source_root, proof_root): - """Create Makefile-template-defines in the proof root.""" - - makefile = os.path.join(proof_root, "Makefile-template-defines") - if os.path.exists(makefile): - logging.warning("Overwriting %s", makefile) - - with open(makefile, "w") as fileobj: - print("SRCDIR ?= $(abspath $(PROOF_ROOT)/{})" - .format(os.path.relpath(source_root, proof_root)), - file=fileobj) - -def main(): - """Set up the CBMC proof infrastructure.""" - - logging.basicConfig(format='%(levelname)s: %(message)s') - - source_root = util.read_source_root() - cbmc_root = os.path.abspath('.') - proof_root = util.proof_root(cbmc_root) - - util.copy_repository_templates(cbmc_root) - create_makefile_template_defines(source_root, proof_root) - -if __name__ == "__main__": - main() diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/scripts/util.py b/test/cbmc/aws-templates-for-cbmc-proofs/scripts/util.py deleted file mode 100644 index e440e8cb..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/scripts/util.py +++ /dev/null @@ -1,128 +0,0 @@ -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -"""Methods of manipulating the templates repository.""" - -import logging -import os -import shutil - -REPOSITORY_TEMPLATES = "template-for-repository" -PROOF_TEMPLATES = "template-for-proof" - -PROOF_DIR = "proofs" - -# There are some files that we should copy to the project repository rather than -# symlinking. This is because users are expected to modify these files. If the -# files were symlinks, then modifying them would dirty up this submodule, which -# would prevent project owners from cleanly updating it. -COPY_INSTEAD = [ - "Makefile-project-defines", - "Makefile-project-targets", - "Makefile-project-testing", - ".gitignore", -] - -################################################################ - -def script_dir(): - """Directory containing setup scripts.""" - - return os.path.dirname(os.path.abspath(__file__)) - -def templates_root(): - """Directory containing the AWS-templates-for-CBMC repository.""" - - return os.path.dirname(script_dir()) - -def proof_root(cbmc_root): - """Directory containing the CBMC proofs.""" - - return os.path.abspath(os.path.join(cbmc_root, PROOF_DIR)) - -################################################################ - -def read_source_root(): - """Read path to source root from console.""" - - print("What is the path to the source root: ", end="") - return os.path.abspath(os.path.expanduser(input())) - -def read_cbmc_root(): - """Read path to cbmc root from console, default to '.'.""" - - print("What is the path to the cbmc root " - "(containing the proofs directory): ", - end="") - return os.path.abspath(os.path.expanduser(input())) - -def read_proof_root(): - """Read path to cbmc root from console, default to '.'.""" - - print("What is the path to the proof root (the 'proofs' directory): ", - end="") - return os.path.abspath(os.path.expanduser(input())) - -################################################################ - -def files_under_root(root): - """The list of files in the filesystem under root.""" - - cwd = os.getcwd() - try: - os.chdir(root) - return [os.path.join(path, name) - for path, _, files in os.walk('.') for name in files] - finally: - os.chdir(cwd) - - -def link_files(name, src, dst): - """Link file dst/name to file src/name, return number skipped""" - - src_name = os.path.normpath(os.path.join(src, name)) - dst_name = os.path.normpath(os.path.join(dst, name)) - - os.makedirs(os.path.dirname(dst_name), exist_ok=True) - src_link = os.path.relpath(src_name, os.path.dirname(dst_name)) - - if os.path.basename(name) in COPY_INSTEAD: - install_method = ("copy", shutil.copyfile) - src_link = src_name - else: - install_method = ("symlink", os.symlink) - - if os.path.exists(dst_name): - logging.warning("Skipping %s %s -> %s: file exists", - install_method[0], name, src_link) - return 1 - - logging.warning( - "Creating %s %s -> %s", install_method[0], name, src_link) - install_method[1](src_link, dst_name) - return 0 - -def copy_directory_contents(src, dst): - """Link the contents of one directory into another.""" - - src = os.path.normpath(src) - dst = os.path.normpath(dst) - - assert os.path.isdir(src) - assert os.path.isdir(dst) - - skipped = 0 - for name in files_under_root(src): - name = os.path.normpath(name) - skipped += link_files(name, src, dst) - - if skipped: - logging.warning("To overwrite a skipped file, " - "delete the file and rerun the script.") - -def copy_repository_templates(cbmc_root): - """Copy the files in the repository template into the CBMC root.""" - - copy_directory_contents(os.path.join(templates_root(), - REPOSITORY_TEMPLATES), - cbmc_root) diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/FUNCTION_harness.c b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/FUNCTION_harness.c deleted file mode 100644 index 262ac329..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/FUNCTION_harness.c +++ /dev/null @@ -1,25 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 - -/* - * Insert copyright notice - */ - -/** - * @file <__FUNCTION_NAME__>_harness.c - * @brief Implements the proof harness for <__FUNCTION_NAME__> function. - */ - -/* - * Insert project header files that - * - include the declaration of the function - * - include the types needed to declare function arguments - */ - -void harness() -{ - - /* Insert argument declarations */ - - <__FUNCTION_NAME__>( /* Insert arguments */ ); -} diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/Makefile b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/Makefile deleted file mode 100644 index bbeb8a9c..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -HARNESS_ENTRY=harness -HARNESS_FILE=<__FUNCTION_NAME__>_harness - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/<__PATH_TO_SOURCE_FILE__> - -include <__PATH_TO_MAKEFILE__>/Makefile.common diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/README.md b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/README.md deleted file mode 100644 index 36cf46d3..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/README.md +++ /dev/null @@ -1,20 +0,0 @@ -<__FUNCTION_NAME__> proof -============== - -This directory contains a memory safety proof for <__FUNCTION_NAME__>. - -To run the proof. -------------- - -* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path. -* Run "make". -* Open html/index.html in a web browser. - -To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. -------------- - -* Run "make arpa" to generate a Makefile.arpa that contains relevant build information for the proof. -* Use Makefile.arpa as the starting point for your proof Makefile by: - 1. Modifying Makefile.arpa (if required). - 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/cbmc-viewer.json b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/cbmc-viewer.json deleted file mode 100644 index 0efa41ac..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-proof/cbmc-viewer.json +++ /dev/null @@ -1,7 +0,0 @@ -{ "expected-missing-functions": - [ - - ], - "proof-name": "<__FUNCTION_NAME__>", - "proof-root": "<__PATH_TO_PROOF_ROOT__>" -} diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/.gitignore b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/.gitignore deleted file mode 100644 index 55a5c751..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/.gitignore +++ /dev/null @@ -1,16 +0,0 @@ -# Emitted when running CBMC proofs -proofs/**/logs -proofs/**/gotos -proofs/**/report -proofs/**/html - -# Emitted by CBMC Viewer -TAGS-* - -# Emitted by Arpa -arpa_cmake/ -arpa-validation-logs/ -Makefile.arpa - -# These files should be overwritten whenever prepare.py runs -cbmc-batch.yaml diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md deleted file mode 100644 index 36bdd94e..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md +++ /dev/null @@ -1,6 +0,0 @@ -CBMC proof include files -======================== - -This directory contains include files written for CBMC proof. It is -common to write some code to model aspects of the system under test, -and the header files for this code go here. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-defines b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-defines deleted file mode 100644 index f6f7681f..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-defines +++ /dev/null @@ -1,37 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Use this file to give project-specific definitions of the command -# line arguments to pass to CBMC tools like goto-cc to build the goto -# binaries and cbmc to do the property and coverage checking. -# -# Use this file to override most default definitions of variables in -# Makefile.common. -################################################################ - -# Flags to pass to goto-cc for compilation (typically those passed to gcc -c) -# COMPILE_FLAGS = - -# Flags to pass to goto-cc for linking (typically those passed to gcc) -# LINK_FLAGS = - -# Preprocessor include paths -I... -# Consider adding -# INCLUDES += -I$(CBMC_ROOT)/include -# You will want to decide what order that comes in relative to the other -# include directories in your project. -# -# INCLUDES = - -# Preprocessor definitions -D... -# DEFINES = - -# Path to arpa executable -# ARPA = - -# Flags to pass to cmake for building the project -# ARPA_CMAKE_FLAGS = diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-targets b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-targets deleted file mode 100644 index 2d4d4602..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-targets +++ /dev/null @@ -1,10 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Use this file to give project-specific targets, including targets -# that may depend on targets defined in Makefile.common. -################################################################ diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-testing b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-testing deleted file mode 100644 index dc0c2097..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile-project-testing +++ /dev/null @@ -1,11 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Use this file to define project-specific targets and definitions for -# unit testing or continuous integration that may depend on targets -# defined in Makefile.common -################################################################ diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common deleted file mode 100644 index 02bc49de..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common +++ /dev/null @@ -1,464 +0,0 @@ -# -*- mode: makefile -*- -# The first line sets the emacs major mode to Makefile - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - -################################################################ -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# -# Licensed under the Apache License, Version 2.0 (the "License"). You -# may not use this file except in compliance with the License. A copy -# of the License is located at -# -# http://aws.amazon.com/apache2.0/ -# -# or in the "license" file accompanying this file. This file is -# distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF -# ANY KIND, either express or implied. See the License for the -# specific language governing permissions and limitations under the -# License. - -################################################################ -# This file Makefile.common defines the basic work flow for cbmc proofs. -# -# The intention is that the goal of your project is to write proofs -# for a collection of functions in a source tree. -# -# To use this file -# 1. Edit the variable definitions in Section I below as appropriate for -# your project, your proofs, and your source tree. -# 2. For each function for which you are writing a proof, -# a. Create a subdirectory . -# b. Write a proof harness (a function) with the name -# in a file with the name /.c -# c. Write a makefile with the name /Makefile that looks -# something like -# -# HARNESS_FILE= -# HARNESS_ENTRY= -# -# PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c -# PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c -# -# PROOF_SOURCES += $(PROOFDIR)/harness.c -# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c -# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c -# -# UNWINDSET += foo.0:3 -# UNWINDSET += bar.1:6 -# -# REMOVE_FUNCTION_BODY += api_stub_a -# REMOVE_FUNCTION_BODY += api_stub_b -# -# DEFINES = -DDEBUG=0 -# -# include ../Makefile.common -# -# d. Change directory to and run make -# -# Dependency handling in this file may not be perfect. Consider -# running "make clean" or "make veryclean" before "make report" if you -# get results that are hard to explain. - -SHELL=/bin/bash - -default: report - -################################################################ -################################################################ -## Section I: This section gives common variable definitions. -## -## Feel free to edit these definitions for your project. -## -## Definitions specific to a proof (generally definitions defined -## below with ?= like PROJECT_SOURCES listing the project source files -## required by the proof) should be defined in the proof Makefile. -## -## Remember that this Makefile is intended to be included from the -## Makefile in your proof directory, so all relative pathnames should -## be relative to your proof directory. -## - -# Absolute path to the directory containing this Makefile.common -# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html -PROOF_ROOT = $(dir $(abspath $(filter %/Makefile.common,$(MAKEFILE_LIST)))) -CBMC_ROOT = $(shell dirname $(PROOF_ROOT)) -PROOF_STUB = $(CBMC_ROOT)/stubs -PROOF_SOURCE = $(CBMC_ROOT)/sources - -# Project-specific definitions to override default definitions below -# * Makefile-project-defines will never be overwritten -# * Makefile-template-defines will be overwritten each time the -# proof templates are updated -sinclude $(PROOF_ROOT)/Makefile-project-defines -sinclude $(PROOF_ROOT)/Makefile-template-defines - -# SRCDIR is the path to the root of the source tree -SRCDIR ?= $(abspath $(../..) - -# PROOFDIR is the path to the directory containing the proof harness -PROOFDIR ?= $(abspath .) - -# Path to the root of the cbmc project. -# -# Projects generally have a directory $(CBMCDIR) with subdirectories -# $(CBMCDIR)/proofs containing the proofs and maybe $(CBMCDIR)/stubs -# containing the stubs used in the proof. This Makefile is generally -# at $(CBMCDIR)/proofs/Makefile.common. -CBMCDIR ?= $(PROOF_ROOT)/cbmc - -# Default CBMC flags used for property checking and coverage checking -CBMCFLAGS += --unwind 1 $(CBMC_UNWINDSET) - -# Additional CBMC flags used for property checking -CHECKFLAGS += --bounds-check -CHECKFLAGS += --conversion-check -CHECKFLAGS += --div-by-zero-check -CHECKFLAGS += --float-overflow-check -CHECKFLAGS += --nan-check -CHECKFLAGS += --pointer-check -CHECKFLAGS += --pointer-overflow-check -CHECKFLAGS += --signed-overflow-check -CHECKFLAGS += --undefined-shift-check -CHECKFLAGS += --unsigned-overflow-check - -# Additional CBMC flags used for coverage checking -COVERFLAGS += - -# Additional CBMC flag to CBMC control verbosity. -# -# Meaningful values are -# 0 none -# 1 only errors -# 2 + warnings -# 4 + results -# 6 + status/phase information -# 8 + statistical information -# 9 + progress information -# 10 + debug info -# -# Uncomment the following line or set in Makefile-project-defines -# CBMC_VERBOSITY ?= --verbosity 4 - -# Additional CBMC flag to control how CBMC treats static variables. -# -# NONDET_STATIC is a list of flags of the form --nondet-static -# and --nondet-static-exclude VAR. The --nondet-static flag causes -# CBMC to initialize static variables with unconstrained value -# (ignoring initializers and default zero-initialization). The -# --nondet-static-exclude VAR excludes VAR for the variables -# initialized with unconstrained values. -NONDET_STATIC ?= - -# Flags to pass to goto-cc for compilation and linking -COMPILE_FLAGS ?= -LINK_FLAGS ?= - -# Preprocessor include paths -I... -INCLUDES ?= - -# Preprocessor definitions -D... -DEFINES ?= - -# CBMC object model -# -# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for -# the id of the object to which a pointer is pointing. CBMC uses 8 -# bits for the object id by default. The remaining bits in the pointer -# are used for offset into the object. This limits the size of the -# objects that CBMC can model. This Makefile defines this bound on -# object size to be CBMC_MAX_OBJECT_SIZE. You are likely to get -# unexpected results if you try to malloc an object larger than this -# bound. -CBMC_OBJECT_BITS ?= 8 - -# CBMC loop unwinding (Normally set in the proof Makefile) -# -# UNWINDSET is a list of pairs of the form foo.1:4 meaning that -# CBMC should unwind loop 1 in function foo no more than 4 times. -# For historical reasons, the number 4 is one more than the number -# of times CBMC actually unwinds the loop. -UNWINDSET ?= - -# CBMC function removal (Normally set set in the proof Makefile) -# -# REMOVE_FUNCTION_BODY is a list of function names. CBMC will "undefine" -# the function, and CBMC will treat the function as having no side effects -# and returning an unconstrained value of the appropriate return type. -# The list should include the names of functions being stubbed out. -REMOVE_FUNCTION_BODY ?= - -# The project source files (Normally set set in the proof Makefile) -# -# PROJECT_SOURCES is the list of project source files to compile, -# including the source file defining the function under test. -PROJECT_SOURCES ?= - -# The proof source files (Normally set in the proof Makefile) -# -# PROOF_SOURCES is the list of proof source files to compile, including -# the proof harness, and including any function stubs being used. -PROOF_SOURCES ?= - -################################################################ -################################################################ -## Section II: This section is for project-specific definitions - - -################################################################ -################################################################ -## Section II: This section defines the process of running a proof -## -## There should be no reason to edit anything below this line. - -################################################################ -# Paths - -CBMC ?= cbmc -GOTO_ANALYZER ?= goto-analyzer -GOTO_CC ?= goto-cc -GOTO_INSTRUMENT ?= goto-instrument -VIEWER ?= cbmc-viewer -MAKE_SOURCE ?= make-source -VIEWER2 ?= cbmc-viewer -CMAKE ?= cmake -ARPA ?= @echo "You must set ARPA in Makefile-project-defines to run arpa in this project"; false - -GOTODIR ?= $(PROOFDIR)/gotos -LOGDIR ?= $(PROOFDIR)/logs - -PROJECT ?= project -PROOF ?= proof - -HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE) -PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT) -PROOF_GOTO ?= $(GOTODIR)/$(PROOF) - -ARPA_BLDDIR ?= $(abspath $(PROOFDIR)/arpa_cmake) -ARPA_COMP_CMDS ?= $(ARPA_BLDDIR)/compile_commands.json - -################################################################ -# Useful macros for values that are hard to reference -SPACE :=$() $() -COMMA :=, - -################################################################ -# Useful macros for running commands - -#1: command, 2: flags, 3: log file -DO_AND_LOG_COMMAND = $(1) $(2) 2>&1 | tee $(3); exit $${PIPESTATUS[0]} - -#1: command, 2: flags, 3: log file - -# CBMC uses the special error-code 10 to signify that it detected an -# assertion violation. Continue the build so we can output the trace. -DO_AND_LOG_IGNORING_ERROR_10 = $(1) $(2) 2>&1 | tee $(3); if [ $${PIPESTATUS[0]} -ne 10 ]; then exit $${PIPESTATUS[0]}; fi - -#1: flags, 2: source, 3: target -DO_GOTO_ANALYZER = $(call DO_AND_LOG_COMMAND,$(GOTO_ANALYZER),$(CBMC_VERBOSITY) $(1) $(2) $(3), $(call LOG_FROM_ENTRY,$(3))) - -#1: flags, 2: source, 3: target -DO_GOTO_CC = $(call DO_AND_LOG_COMMAND,$(GOTO_CC),$(CBMC_VERBOSITY) $(1) $(2) -o $(3), $(call LOG_FROM_ENTRY,$(3))) - -#1: flags, 2: source, 3: target -DO_GOTO_INSTRUMENT = $(call DO_AND_LOG_COMMAND,$(GOTO_INSTRUMENT),$(CBMC_VERBOSITY) $(1) $(2) $(3), $(call LOG_FROM_ENTRY,$(3))) - -#1: flags, 2: source, 3: logfile -DO_CBMC = $(call DO_AND_LOG_IGNORING_ERROR_10,$(CBMC),$(CBMC_VERBOSITY) --flush $(1) $(2), $(3)) - -#1: message 2: source 3: dest -DO_NOOP_COPY = cp $(2) $(3); echo $(1) | tee $(call LOG_FROM_ENTRY,$(3)) - -################################################################ -# Useful macros translating filenames - -C_FROM_GOTO = $(patsubst $(GOTODIR)%,$(SRCDIR)%,$(1:.goto=.c)) -GOTO_FROM_C = $(patsubst $(SRCDIR)%,$(GOTODIR)%,$(1:.c=.goto)) -LOG_FROM_ENTRY = $(LOGDIR)/$(notdir $(1:.goto=.txt)) -LOG_FROM_GOTO = $(patsubst $(GOTODIR)%,$(LOGDIR)%,$(1:.goto=.txt)) - -################################################################ -# Set C compiler defines - -CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS) - -DEFINES += -DCBMC=1 -DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS) -DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))" - -# CI currently assumes cbmc invocation has at most one --unwindset -ifdef UNWINDSET - ifneq ($(strip $(UNWINDSET)),"") - CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) - endif -endif -CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) - -################################################################ -# Build targets that make the relevant .goto files - -# Compile project sources -$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) - mkdir -p $(dir $@) - mkdir -p $(dir $(call LOG_FROM_ENTRY,$@)) - $(call DO_GOTO_CC,--export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES),$^,$@) - -# Compile proof sources -$(PROOF_GOTO)1.goto: $(PROOF_SOURCES) - mkdir -p $(dir $@) - mkdir -p $(dir $(call LOG_FROM_ENTRY,$@)) - $(call DO_GOTO_CC,--export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES),$^,$@) - -# Optionally remove function bodies from project sources -$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto -ifeq ($(REMOVE_FUNCTION_BODY),"") - $(call DO_NOOP_COPY,"Not removing function bodies",$<,$@) -else - $(call DO_GOTO_INSTRUMENT,$(CBMC_REMOVE_FUNCTION_BODY),$<,$@) -endif - -# Don't remove function bodies from proof sources -$(PROOF_GOTO)2.goto: $(PROOF_GOTO)1.goto - $(call DO_NOOP_COPY,"Not removing function bodies",$<,$@) - -# Link project and proof sources into the proof harness -$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)2.goto $(PROJECT_GOTO)2.goto - $(call DO_GOTO_CC,--function $(HARNESS_ENTRY),$^,$@) - -# Optionally fill static variable with unconstrained values -$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto -ifeq ($(NONDET_STATIC),"") - $(call DO_NOOP_COPY,"Not applying --nondet-static",$<,$@) -else - $(call DO_GOTO_INSTRUMENT,$(NONDET_STATIC),$<,$@) -endif - -# Omit unused functions (sharpens coverage calculations) -$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto - $(call DO_GOTO_INSTRUMENT,--drop-unused-functions,$<,$@) - -# Omit initialization of unused global variables (reduces problem size) -$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto - $(call DO_GOTO_INSTRUMENT,--slice-global-inits,$<,$@) - -# Final name for proof harness -$(HARNESS_GOTO).goto: $(HARNESS_GOTO)4.goto - cp $< $@ - -goto: $(HARNESS_GOTO).goto - echo $(DEPENDENT_GOTOS) - -################################################################ -# Targets to run Arpa - -$(ARPA_BLDDIR): - $(CMAKE) $(ARPA_CMAKE_FLAGS) \ - -DCMAKE_EXPORT_COMPILE_COMMANDS=1 \ - -B $(ARPA_BLDDIR) \ - -S $(SRCDIR) - -arpa: $(ARPA_BLDDIR) - $(ARPA) run -cc $(ARPA_COMP_CMDS) -r $(SRCDIR) - -################################################################ -# Targets to run the analysis commands - -$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto - $(call DO_CBMC,$(CBMCFLAGS) $(CHECKFLAGS) --unwinding-assertions --trace,$<,$@) - -$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto - $(call DO_CBMC,$(CBMCFLAGS) $(CHECKFLAGS) --unwinding-assertions --trace --xml-ui,$<,$@) - -$(LOGDIR)/property.xml: $(HARNESS_GOTO).goto - $(call DO_CBMC,$(CBMCFLAGS) $(CHECKFLAGS) --unwinding-assertions --show-properties --xml-ui,$<,$@) - -$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto - $(call DO_CBMC,$(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui,$<,$@) - -result: $(LOGDIR)/result.txt - -property: $(LOGDIR)/property.xml - -coverage: $(LOGDIR)/coverage.xml - -report: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml - $(VIEWER) \ - --result $(LOGDIR)/result.txt \ - --block $(LOGDIR)/coverage.xml \ - --property $(LOGDIR)/property.xml \ - --srcdir $(SRCDIR) \ - --goto $(HARNESS_GOTO).goto \ - --htmldir html \ - -# Caution: run make-source before running property and coverage checking -# The current make-source script removes the goto binary -$(LOGDIR)/source.json: - mkdir -p $(dir $@) - $(RM) -r $(GOTODIR) - $(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@ - $(RM) -r $(GOTODIR) - -# Omit logs/source.json from report generation until make-sources -# works correctly with Makefiles that invoke the compiler with -# mutliple source files at once. -report2: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml - $(VIEWER2) \ - --result $(LOGDIR)/result.xml \ - --coverage $(LOGDIR)/coverage.xml \ - --property $(LOGDIR)/property.xml \ - --srcdir $(SRCDIR) \ - --goto $(HARNESS_GOTO).goto \ - --reportdir report \ - -################################################################ -# Targets to clean up after ourselves -clean: - -$(RM) $(DEPENDENT_GOTOS) - -$(RM) TAGS* - -$(RM) *~ \#* - -$(RM) Makefile.arpa - -$(RM) -r $(ARPA_BLDDIR) - -veryclean: clean - -$(RM) -r html report - -$(RM) -r $(LOGDIR) $(GOTODIR) - -.PHONY: setup_dependencies arpa result property coverage report clean veryclean testdeps - -################################################################ - -# Rule for generating cbmc-batch.yaml, used by the CI at -# https://github.com/awslabs/aws-batch-cbmc/ - -JOB_OS ?= ubuntu16 -JOB_MEMORY ?= 32000 - -define yaml_encode_options - "$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')" -endef - -CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS) --unwinding-assertions - -cbmc-batch.yaml: - @$(RM) $@ - @echo 'build_memory: $(JOB_MEMORY)' > $@ - @echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@ - @echo 'coverage_memory: $(JOB_MEMORY)' >> $@ - @echo "expected: SUCCESSFUL" >> $@ - @echo "goto: $(HARNESS_GOTO).goto" >> $@ - @echo "jobos: $(JOB_OS)" >> $@ - @echo 'property_memory: $(JOB_MEMORY)' >> $@ - @echo 'report_memory: $(JOB_MEMORY)' >> $@ - -.PHONY: cbmc-batch.yaml - -################################################################ - -# Project-specific targets requiring values defined above -sinclude $(PROOF_ROOT)/Makefile-project-targets - -# CI-specific targets to drive cbmc in CI -sinclude $(PROOF_ROOT)/Makefile-project-testing - -################################################################ diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md deleted file mode 100644 index 5e22aa01..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md +++ /dev/null @@ -1,27 +0,0 @@ -CBMC proofs -=========== - -This directory contains the CBMC proofs. Each proof is in its own -directory. - -This directory includes four Makefiles. - -One Makefile describes the basic workflow for building and running proofs: - -* Makefile.common: - * make: builds the goto binary, does the cbmc property checking - and coverage checking, and builds the final report. - * make goto: builds the goto binary - * make result: does cbmc property checking - * make coverage: does cbmc coverage checking - * make report: builds the final report - -Three included Makefiles describe project-specific settings and can override -definitions in Makefile.common: - -* Makefile-project-defines: definitions like compiler flags - required to build the goto binaries, and definitions to override - definitions in Makefile.common. -* Makefile-project-targets: other make targets needed for the project -* Makefile-project-testing: other definitions and targets needed for - unit testing or continuous integration. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py deleted file mode 100644 index d58805ca..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py +++ /dev/null @@ -1,54 +0,0 @@ -#!/usr/bin/env python3 - -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 - - -"""Prepare the source tree for proofs in continuous integration.""" - - -import os -import subprocess - - -MAKEFILE = "Makefile" -CBMC_BATCH_YAML = "cbmc-batch.yaml" - - -def create_cbmc_batch_yaml(folder): - """Run make to create cbmc-batch.yaml in folder.""" - - try: - subprocess.run( - ["make", "-B", CBMC_BATCH_YAML], - cwd=folder, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, - universal_newlines=True, - check=True - ) - except subprocess.CalledProcessError as error: - raise UserWarning("Failed to create {} in {}: " - "command was '{}': " - "error was '{}'" - .format(CBMC_BATCH_YAML, folder, - ' '.join(error.cmd), - error.stderr.strip())) from None - - -def create_cbmc_batch_yaml_files(root='.'): - """Create cbmc-batch.yaml in all directories under root.""" - - for folder, _, files in os.walk(root): - if CBMC_BATCH_YAML in files and MAKEFILE in files: - create_cbmc_batch_yaml(folder) - - -def prepare(): - """Prepare the source tree for proofs in continuous integration.""" - - create_cbmc_batch_yaml_files() - - -if __name__ == "__main__": - prepare() diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md deleted file mode 100644 index 4f706b23..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md +++ /dev/null @@ -1,6 +0,0 @@ -CBMC proof source code -====================== - -This directory contains source code written for CBMC proofs. It is -common to write some code to model aspects of the system under test, -and this code goes here. diff --git a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md b/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md deleted file mode 100644 index 3b7823dd..00000000 --- a/test/cbmc/aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md +++ /dev/null @@ -1,6 +0,0 @@ -CBMC proof stubs -====================== - -This directory contains the stubs written for CBMC proofs. It is -common to stub out functionality like network send and receive methods -when writing a CBMC proof, and the code for these stubs goes here. diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md index b655718b..4086b9eb 120000 --- a/test/cbmc/include/README.md +++ b/test/cbmc/include/README.md @@ -1 +1 @@ -../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md \ No newline at end of file +../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md \ No newline at end of file diff --git a/test/cbmc/include/mqtt_config.h b/test/cbmc/include/core_mqtt_config.h similarity index 61% rename from test/cbmc/include/mqtt_config.h rename to test/cbmc/include/core_mqtt_config.h index 2d79dc98..f32a8e8b 100644 --- a/test/cbmc/include/mqtt_config.h +++ b/test/cbmc/include/core_mqtt_config.h @@ -1,24 +1,5 @@ -#ifndef MQTT_CONFIG_H_ -#define MQTT_CONFIG_H_ - -/**************************************************/ -/******* DO NOT CHANGE the following order ********/ -/**************************************************/ - -/* Logging related header files are required to be included in the following order: - * 1. Include the header file "logging_levels.h". - * 2. Define LIBRARY_LOG_NAME and LIBRARY_LOG_LEVEL. - * 3. Include the header file "logging_stack.h". - */ - -/* Include header that defines log levels. */ -#include "logging_levels.h" - -/* Configure name and log level for the MQTT library. */ -#define LIBRARY_LOG_NAME "MQTT" -#define LIBRARY_LOG_LEVEL LOG_NONE - -#include "logging_stack.h" +#ifndef CORE_MQTT_CONFIG_H_ +#define CORE_MQTT_CONFIG_H_ /* Mock a network context for the CBMC proofs. */ struct NetworkContext @@ -26,15 +7,13 @@ struct NetworkContext int NetworkContext; }; -/************ End of logging configuration ****************/ - /** * @brief Determines the maximum number of MQTT PUBLISH messages, pending - * acknowledgment at a time, that are supported for incoming and outgoing + * acknowledgement at a time, that are supported for incoming and outgoing * direction of messages, separately. * - * QoS 1 and 2 MQTT PUBLISHes require acknowledgment from the server before - * they can be completed. While they are awaiting the acknowledgment, the + * QoS 1 and 2 MQTT PUBLISHes require acknowledgement from the server before + * they can be completed. While they are awaiting the acknowledgement, the * client must maintain information about their state. The value of this * macro sets the limit on how many simultaneous PUBLISH states an MQTT * context maintains, separately, for both incoming and outgoing direction of @@ -65,4 +44,4 @@ struct NetworkContext */ #define MQTT_PINGRESP_TIMEOUT_MS ( 500U ) -#endif /* ifndef MQTT_CONFIG_H_ */ +#endif /* ifndef CORE_MQTT_CONFIG_H_ */ diff --git a/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c b/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c index 199ebcc2..5393249b 100644 --- a/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c +++ b/test/cbmc/proofs/MQTT_Connect/MQTT_Connect_harness.c @@ -23,7 +23,7 @@ * @file MQTT_Connect_harness.c * @brief Implements the proof harness for MQTT_Connect function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Connect/Makefile b/test/cbmc/proofs/MQTT_Connect/Makefile index cbcac365..fe14a6b1 100644 --- a/test/cbmc/proofs/MQTT_Connect/Makefile +++ b/test/cbmc/proofs/MQTT_Connect/Makefile @@ -22,7 +22,7 @@ HARNESS_ENTRY=harness HARNESS_FILE=MQTT_Connect_harness -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 # Bound on the timeout in receiveConnack. This timeout is bounded because @@ -31,7 +31,7 @@ MAX_NETWORK_SEND_TRIES=3 # time out of 3 we can get coverage of the entire function. Another iteration # performed will unnecessarily duplicate the proof. MQTT_RECEIVE_TIMEOUT=3 -# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more +# Please see test/cbmc/include/mqtt_config.h for more # information on these defines. MQTT_STATE_ARRAY_MAX_COUNT=11 MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT=3 @@ -44,40 +44,40 @@ INCLUDES += # the function bodies to improve coverage accuracy. REMOVE_FUNCTION_BODY += MQTT_ProcessLoop REMOVE_FUNCTION_BODY += MQTT_ReceiveLoop -REMOVE_FUNCTION_BODY += __CPROVER_file_local_mqtt_c_handleIncomingPublish -REMOVE_FUNCTION_BODY += __CPROVER_file_local_mqtt_c_handleKeepAlive +REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_mqtt_c_handleIncomingPublish +REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_mqtt_c_handleKeepAlive # The loops below are unwound once more than the timeout. The loops below use # the user passed in timeout to break the loop. -UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) # If the user passed in timeout is zero, then the loop will run until the # MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT is reached. -UNWINDSET += __CPROVER_file_local_mqtt_c_receiveConnack.0:$(MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_receiveConnack.0:$(MQTT_MAX_CONNACK_RECEIVE_RETRY_COUNT) # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in # sendPacket will continue until all the bytes are sent or a network error # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) # The loops are unwound 5 times because these functions divides a size_t # variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_getRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_getRemainingLength.0:5 # This loop will run for the maximum number of publishes pending -# acknowledgments plus one. This value is set in -# libraries/standard/mqtt/cbmc/include/mqtt_config.h. -UNWINDSET += __CPROVER_file_local_mqtt_state_c_stateSelect.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +# acknowledgements plus one. This value is set in +# test/cbmc/include/mqtt_config.h. +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_stateSelect.0:$(MQTT_STATE_ARRAY_MAX_COUNT) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/memcpy.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memcpy.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Connect/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Connect/cbmc-viewer.json index 2ca9f7f9..d72d49bf 100644 --- a/test/cbmc/proofs/MQTT_Connect/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Connect/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Connect", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c index 53fa2967..f427ca7b 100644 --- a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c +++ b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c @@ -23,7 +23,7 @@ * @file MQTT_DeserializeAck_harness.c * @brief Implements the proof harness for MQTT_DeserializeAck function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_DeserializeAck/Makefile b/test/cbmc/proofs/MQTT_DeserializeAck/Makefile index 7984d21b..60f89c4b 100644 --- a/test/cbmc/proofs/MQTT_DeserializeAck/Makefile +++ b/test/cbmc/proofs/MQTT_DeserializeAck/Makefile @@ -30,10 +30,10 @@ DEFINES += -DREMAINING_LENGTH_MAX=$(REMAINING_LENGTH_MAX) INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_readSubackStatus.0:$(REMAINING_LENGTH_MAX) +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_readSubackStatus.0:$(REMAINING_LENGTH_MAX) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_DeserializeAck/cbmc-viewer.json b/test/cbmc/proofs/MQTT_DeserializeAck/cbmc-viewer.json index 2b5117a6..d8dd5d7e 100644 --- a/test/cbmc/proofs/MQTT_DeserializeAck/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_DeserializeAck/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_DeserializeAck", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c b/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c index c4b034e8..545974d3 100644 --- a/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c +++ b/test/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c @@ -24,7 +24,7 @@ * @brief Implements the proof harness for MQTT_DeserializePublish function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_DeserializePublish/Makefile b/test/cbmc/proofs/MQTT_DeserializePublish/Makefile index 07a4db8a..90c6bb06 100644 --- a/test/cbmc/proofs/MQTT_DeserializePublish/Makefile +++ b/test/cbmc/proofs/MQTT_DeserializePublish/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_DeserializePublish/cbmc-viewer.json b/test/cbmc/proofs/MQTT_DeserializePublish/cbmc-viewer.json index 0c9f5752..075de93e 100644 --- a/test/cbmc/proofs/MQTT_DeserializePublish/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_DeserializePublish/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_DeserializePublish", - "proof-root": "libraries/standard/mqtt/cbmc" + "proof-root": "test/cbmc" } diff --git a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c index 6f59a53f..9819272e 100644 --- a/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c +++ b/test/cbmc/proofs/MQTT_Disconnect/MQTT_Disconnect_harness.c @@ -23,7 +23,7 @@ * @file MQTT_Disconnect_harness.c * @brief Implements the proof harness for MQTT_Disconnect function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Disconnect/Makefile b/test/cbmc/proofs/MQTT_Disconnect/Makefile index b105017c..bea17289 100644 --- a/test/cbmc/proofs/MQTT_Disconnect/Makefile +++ b/test/cbmc/proofs/MQTT_Disconnect/Makefile @@ -22,7 +22,7 @@ HARNESS_ENTRY=harness HARNESS_FILE=MQTT_Disconnect_harness -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES) @@ -34,15 +34,15 @@ REMOVE_FUNCTION_BODY += # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Disconnect/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Disconnect/cbmc-viewer.json index a0f83370..b1c2b594 100644 --- a/test/cbmc/proofs/MQTT_Disconnect/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Disconnect/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Disconnect", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c b/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c index 138fba49..af4907ac 100644 --- a/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c +++ b/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c @@ -23,7 +23,7 @@ * @file MQTT_GetIncomingPacketTypeAndLength_harness.c * @brief Implements the proof harness for MQTT_GetIncomingPacketTypeAndLength function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "network_interface_stubs.h" #include "mqtt_cbmc_state.h" diff --git a/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile b/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile index 1a654626..e2aead71 100644 --- a/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile +++ b/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile @@ -29,11 +29,11 @@ REMOVE_FUNCTION_BODY += # The getRemainingLength loop is unwound 5 times because getRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_getRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_getRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/cbmc-viewer.json b/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/cbmc-viewer.json index 80ed87a5..968269c5 100644 --- a/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_GetIncomingPacketTypeAndLength", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c b/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c index 25cdec94..0e1ea91e 100644 --- a/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c +++ b/test/cbmc/proofs/MQTT_GetPacketId/MQTT_GetPacketId_harness.c @@ -24,7 +24,7 @@ * @brief Implements the proof harness for MQTT_GetPacketId function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_GetPacketId/Makefile b/test/cbmc/proofs/MQTT_GetPacketId/Makefile index 38cfc600..dff98e31 100644 --- a/test/cbmc/proofs/MQTT_GetPacketId/Makefile +++ b/test/cbmc/proofs/MQTT_GetPacketId/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_GetPacketId/cbmc-viewer.json b/test/cbmc/proofs/MQTT_GetPacketId/cbmc-viewer.json index fdd2429c..4f988b90 100644 --- a/test/cbmc/proofs/MQTT_GetPacketId/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_GetPacketId/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_GetPacketId", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c b/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c index 8ca65023..c8ce14b5 100644 --- a/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c +++ b/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/MQTT_GetSubAckStatusCodes_harness.c @@ -24,7 +24,7 @@ * @brief Implements the proof harness for MQTT_GetSubAckStatusCodes function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile b/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile index 3c8ad8d0..3d3e9f97 100644 --- a/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile +++ b/test/cbmc/proofs/MQTT_GetSubAckStatusCodes/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c b/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c index 75729fe5..1f91b3f8 100644 --- a/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c +++ b/test/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c @@ -24,7 +24,7 @@ * @brief Implements the proof harness for MQTT_Init function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Init/Makefile b/test/cbmc/proofs/MQTT_Init/Makefile index 8b21e51f..2ea6cc4a 100644 --- a/test/cbmc/proofs/MQTT_Init/Makefile +++ b/test/cbmc/proofs/MQTT_Init/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Init/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Init/cbmc-viewer.json index 8c1d680c..47835920 100644 --- a/test/cbmc/proofs/MQTT_Init/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Init/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Init", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c b/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c index b8344a29..a799a512 100644 --- a/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c +++ b/test/cbmc/proofs/MQTT_MatchTopic/MQTT_MatchTopic_harness.c @@ -24,7 +24,7 @@ * @brief Implements the proof harness for MQTT_MatchTopic function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_MatchTopic/Makefile b/test/cbmc/proofs/MQTT_MatchTopic/Makefile index 96459013..019f6867 100644 --- a/test/cbmc/proofs/MQTT_MatchTopic/Makefile +++ b/test/cbmc/proofs/MQTT_MatchTopic/Makefile @@ -31,12 +31,12 @@ DEFINES += -DMAX_TOPIC_NAME_FILTER_LENGTH=$(MAX_TOPIC_NAME_FILTER_LENGTH) INCLUDES += REMOVE_FUNCTION_BODY += -UNWINDSET += __CPROVER_file_local_mqtt_c_matchTopicFilter.0:$(MAX_TOPIC_NAME_FILTER_LENGTH) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_matchTopicFilter.0:$(MAX_TOPIC_NAME_FILTER_LENGTH) UNWINDSET += strncmp.0:$(MAX_TOPIC_NAME_FILTER_LENGTH) -UNWINDSET += __CPROVER_file_local_mqtt_c_matchWildcards.0:$(MAX_TOPIC_NAME_FILTER_LENGTH) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_matchWildcards.0:$(MAX_TOPIC_NAME_FILTER_LENGTH) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Ping/MQTT_Ping_harness.c b/test/cbmc/proofs/MQTT_Ping/MQTT_Ping_harness.c index 559da9a1..fcab96ae 100644 --- a/test/cbmc/proofs/MQTT_Ping/MQTT_Ping_harness.c +++ b/test/cbmc/proofs/MQTT_Ping/MQTT_Ping_harness.c @@ -23,7 +23,7 @@ * @file MQTT_Ping_harness.c * @brief Implements the proof harness for MQTT_Ping function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Ping/Makefile b/test/cbmc/proofs/MQTT_Ping/Makefile index 50711f78..2a04ae6e 100644 --- a/test/cbmc/proofs/MQTT_Ping/Makefile +++ b/test/cbmc/proofs/MQTT_Ping/Makefile @@ -22,7 +22,7 @@ HARNESS_ENTRY=harness HARNESS_FILE=MQTT_Ping_harness -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES) @@ -31,15 +31,15 @@ INCLUDES += # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in # sendPacket will continue until all the bytes are sent or a network error # occurs. Please see NetworkInterfaceReceiveStub in -# libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c for more +# test/cbmc/stubs/network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Ping/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Ping/cbmc-viewer.json index 7ee974b2..55cbfa74 100644 --- a/test/cbmc/proofs/MQTT_Ping/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Ping/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Ping", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c b/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c index a9de5f98..91be5ba6 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c +++ b/test/cbmc/proofs/MQTT_ProcessLoop/MQTT_ProcessLoop_harness.c @@ -23,7 +23,7 @@ * @file MQTT_ProcessLoop_harness.c * @brief Implements the proof harness for MQTT_ProcessLoop function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile index 2461c353..9ae5ec62 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/Makefile +++ b/test/cbmc/proofs/MQTT_ProcessLoop/Makefile @@ -28,10 +28,10 @@ HARNESS_FILE=MQTT_ProcessLoop_harness # out of 2 we can get coverage of the entire function. Another iteration will # performed unnecessarily duplicating of the proof. MQTT_RECEIVE_TIMEOUT=3 -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 -# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more +# Please see test/cbmc/include/mqtt_config.h for more # information. MQTT_STATE_ARRAY_MAX_COUNT=11 DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT) @@ -44,31 +44,31 @@ REMOVE_FUNCTION_BODY += MQTT_DeserializeAck REMOVE_FUNCTION_BODY += MQTT_SerializeAck UNWINDSET += MQTT_ProcessLoop.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT) # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in # sendPacket will continue until all the bytes are sent or a network error # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) # The getRemainingLength loop is unwound 5 times because getRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_getRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_getRemainingLength.0:5 # These loops will run for the maximum number of publishes pending -# acknowledgments plus one. This value is set in -# libraries/standard/mqtt/cbmc/include/mqtt_config.h. -UNWINDSET += __CPROVER_file_local_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) -UNWINDSET += __CPROVER_file_local_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +# acknowledgements plus one. This value is set in +# test/cbmc/include/mqtt_config.h. +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json b/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json index ba8c554a..8f4faa1b 100644 --- a/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_ProcessLoop/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_ProcessLoop", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_Publish/MQTT_Publish_harness.c b/test/cbmc/proofs/MQTT_Publish/MQTT_Publish_harness.c index eae41cd5..7c09b05d 100644 --- a/test/cbmc/proofs/MQTT_Publish/MQTT_Publish_harness.c +++ b/test/cbmc/proofs/MQTT_Publish/MQTT_Publish_harness.c @@ -23,7 +23,7 @@ * @file MQTT_Publish_harness.c * @brief Implements the proof harness for MQTT_Publish function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Publish/Makefile b/test/cbmc/proofs/MQTT_Publish/Makefile index 74f701a1..b2b9df30 100644 --- a/test/cbmc/proofs/MQTT_Publish/Makefile +++ b/test/cbmc/proofs/MQTT_Publish/Makefile @@ -22,10 +22,10 @@ HARNESS_ENTRY=harness HARNESS_FILE=MQTT_Publish_harness -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 -# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more +# Please see test/cbmc/include/mqtt_config.h for more # information. MQTT_STATE_ARRAY_MAX_COUNT=11 DEFINES += -DMAX_NETWORK_SEND_TRIES=$(MAX_NETWORK_SEND_TRIES) @@ -38,23 +38,23 @@ REMOVE_FUNCTION_BODY += # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) -# These loops will run for the maximum number of publishes pending acknowledgment. -# This is set in libraries/standard/mqtt/cbmc/include/mqtt_config.h. -UNWINDSET += __CPROVER_file_local_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) -UNWINDSET += __CPROVER_file_local_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +# These loops will run for the maximum number of publishes pending acknowledgement. +# This is set in test/cbmc/include/mqtt_config.h. +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Publish/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Publish/cbmc-viewer.json index 36e61072..2a3f7d76 100644 --- a/test/cbmc/proofs/MQTT_Publish/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Publish/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Publish", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c b/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c index ed74110f..96666fe2 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/MQTT_ReceiveLoop_harness.c @@ -23,7 +23,7 @@ * @file MQTT_ReceiveLoop_harness.c * @brief Implements the proof harness for MQTT_ReceiveLoop function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile index 4c4cc0a3..579091e3 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/Makefile @@ -10,10 +10,10 @@ HARNESS_FILE=MQTT_ReceiveLoop_harness # out of 2 we can get coverage of the entire function. Another iteration will # performed unnecessarily duplicating of the proof. MQTT_RECEIVE_TIMEOUT=3 -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 -# Please see libraries/standard/mqtt/cbmc/include/mqtt_config.h for more +# Please see test/cbmc/include/mqtt_config.h for more # information. MQTT_STATE_ARRAY_MAX_COUNT=11 DEFINES += -DMQTT_RECEIVE_TIMEOUT=$(MQTT_RECEIVE_TIMEOUT) @@ -26,30 +26,30 @@ REMOVE_FUNCTION_BODY += MQTT_SerializeAck # The loops below are unwound once more than the exclusive timeout bound. UNWINDSET += MQTT_ReceiveLoop.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) -UNWINDSET += __CPROVER_file_local_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_discardPacket.0:$(MQTT_RECEIVE_TIMEOUT) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_recvExact.0:$(MQTT_RECEIVE_TIMEOUT) # Unlike recvExact, sendPacket is not bounded by the timeout. The loop in # sendPacket will continue until all the bytes are sent or a network error # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) # The getRemainingLength loop is unwound 5 times because getRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_getRemainingLength.0:5 -# These loops will run for the maximum number of publishes pending acknowledgment. -# This is set in libraries/standard/mqtt/cbmc/include/mqtt_config.h. -UNWINDSET += __CPROVER_file_local_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) -UNWINDSET += __CPROVER_file_local_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_getRemainingLength.0:5 +# These loops will run for the maximum number of publishes pending acknowledgement. +# This is set in test/cbmc/include/mqtt_config.h. +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_addRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) +UNWINDSET += __CPROVER_file_local_core_mqtt_state_c_findInRecord.0:$(MQTT_STATE_ARRAY_MAX_COUNT) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json b/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json index 05e9d9b5..882c3810 100644 --- a/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_ReceiveLoop/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_ReceiveLoop", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c b/test/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c index 54bf9e97..d8a38756 100644 --- a/test/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c +++ b/test/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializeAck_harness.c * @brief Implements the proof harness for MQTT_SerializeAck function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializeAck/Makefile b/test/cbmc/proofs/MQTT_SerializeAck/Makefile index 861bd7c9..9d7b2d25 100644 --- a/test/cbmc/proofs/MQTT_SerializeAck/Makefile +++ b/test/cbmc/proofs/MQTT_SerializeAck/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json index a69c3ae7..6d6d3794 100644 --- a/test/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializeAck", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c b/test/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c index 648d2222..f45f7288 100644 --- a/test/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c +++ b/test/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializeConnect_harness.c * @brief Implements the proof harness for MQTT_SerializeConnect function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializeConnect/Makefile b/test/cbmc/proofs/MQTT_SerializeConnect/Makefile index a12eaf20..1347917c 100644 --- a/test/cbmc/proofs/MQTT_SerializeConnect/Makefile +++ b/test/cbmc/proofs/MQTT_SerializeConnect/Makefile @@ -33,11 +33,11 @@ REMOVE_FUNCTION_BODY += MQTT_GetIncomingPacketTypeAndLength # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/memcpy.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/memcpy.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializeConnect/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializeConnect/cbmc-viewer.json index 57f66a9d..54cff91e 100644 --- a/test/cbmc/proofs/MQTT_SerializeConnect/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializeConnect/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializeConnect", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c b/test/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c index 595b9b47..814638bf 100644 --- a/test/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c +++ b/test/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializeDisconnect_harness.c * @brief Implements the proof harness for MQTT_SerializeDisconnect function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializeDisconnect/Makefile b/test/cbmc/proofs/MQTT_SerializeDisconnect/Makefile index ac0d7e3e..491609e7 100644 --- a/test/cbmc/proofs/MQTT_SerializeDisconnect/Makefile +++ b/test/cbmc/proofs/MQTT_SerializeDisconnect/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json index 858f3ae8..ffffb16f 100644 --- a/test/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializeDisconnect", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c b/test/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c index 38bc2885..f5dba1cb 100644 --- a/test/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c +++ b/test/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializePingreq_harness.c * @brief Implements the proof harness for MQTT_SerializePingreq function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializePingreq/Makefile b/test/cbmc/proofs/MQTT_SerializePingreq/Makefile index 6b48b750..17103afc 100644 --- a/test/cbmc/proofs/MQTT_SerializePingreq/Makefile +++ b/test/cbmc/proofs/MQTT_SerializePingreq/Makefile @@ -29,7 +29,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json index 4e487fbe..6bcd3a31 100644 --- a/test/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializePingreq", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c b/test/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c index 529e0525..70be568c 100644 --- a/test/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c +++ b/test/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializePublish_harness.c * @brief Implements the proof harness for MQTT_SerializePublish function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializePublish/Makefile b/test/cbmc/proofs/MQTT_SerializePublish/Makefile index 4253601d..ba2a3d11 100644 --- a/test/cbmc/proofs/MQTT_SerializePublish/Makefile +++ b/test/cbmc/proofs/MQTT_SerializePublish/Makefile @@ -29,10 +29,10 @@ REMOVE_FUNCTION_BODY += # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json index f6464b32..6d7106f6 100644 --- a/test/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializePublish", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c b/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c index 3993cb32..9e2bed2c 100644 --- a/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c +++ b/test/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializePublishHeader_harness.c * @brief Implements the proof harness for MQTT_SerializePublishHeader function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializePublishHeader/Makefile b/test/cbmc/proofs/MQTT_SerializePublishHeader/Makefile index 10ea76cc..1302e599 100644 --- a/test/cbmc/proofs/MQTT_SerializePublishHeader/Makefile +++ b/test/cbmc/proofs/MQTT_SerializePublishHeader/Makefile @@ -29,10 +29,10 @@ REMOVE_FUNCTION_BODY += # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json index 1ddfd34e..fe85e6f3 100644 --- a/test/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializePublishHeader", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c b/test/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c index 9ec6da09..a7c371f6 100644 --- a/test/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c +++ b/test/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializeSubscribe_harness.c * @brief Implements the proof harness for MQTT_SerializeSubscribe function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializeSubscribe/Makefile b/test/cbmc/proofs/MQTT_SerializeSubscribe/Makefile index eb81c7aa..4e1f3c5c 100644 --- a/test/cbmc/proofs/MQTT_SerializeSubscribe/Makefile +++ b/test/cbmc/proofs/MQTT_SerializeSubscribe/Makefile @@ -32,15 +32,15 @@ INCLUDES += REMOVE_FUNCTION_BODY += UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += MQTT_SerializeSubscribe.0:$(SUBSCRIPTION_COUNT_MAX) # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json index 5b0c51c4..11c4b413 100644 --- a/test/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializeSubscribe", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c b/test/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c index f31eb28a..1399cd28 100644 --- a/test/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c +++ b/test/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c @@ -23,7 +23,7 @@ * @file MQTT_SerializeUnsubscribe_harness.c * @brief Implements the proof harness for MQTT_SerializeUnsubscribe function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile b/test/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile index 40538e73..dea8b7d1 100644 --- a/test/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile +++ b/test/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile @@ -32,15 +32,15 @@ INCLUDES += REMOVE_FUNCTION_BODY += UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += MQTT_SerializeUnsubscribe.0:$(SUBSCRIPTION_COUNT_MAX) # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json index 166638dc..a0323b93 100644 --- a/test/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_SerializeUnsubscribe", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_Subscribe/MQTT_Subscribe_harness.c b/test/cbmc/proofs/MQTT_Subscribe/MQTT_Subscribe_harness.c index 3745dd7a..1c81e42e 100644 --- a/test/cbmc/proofs/MQTT_Subscribe/MQTT_Subscribe_harness.c +++ b/test/cbmc/proofs/MQTT_Subscribe/MQTT_Subscribe_harness.c @@ -23,7 +23,7 @@ * @file MQTT_Subscribe_harness.c * @brief Implements the proof harness for MQTT_Subscribe function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Subscribe/Makefile b/test/cbmc/proofs/MQTT_Subscribe/Makefile index fe9d39f7..f7e6de85 100644 --- a/test/cbmc/proofs/MQTT_Subscribe/Makefile +++ b/test/cbmc/proofs/MQTT_Subscribe/Makefile @@ -22,7 +22,7 @@ HARNESS_ENTRY=harness HARNESS_FILE=MQTT_Subscribe_harness -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 # Bound on the the subscription count. Please see the default value in @@ -40,23 +40,23 @@ REMOVE_FUNCTION_BODY += # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += MQTT_SerializeSubscribe.0:$(SUBSCRIPTION_COUNT_MAX) # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Subscribe/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Subscribe/cbmc-viewer.json index 1223d9d3..7b8ce0f7 100644 --- a/test/cbmc/proofs/MQTT_Subscribe/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Subscribe/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Subscribe", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/MQTT_Unsubscribe/MQTT_Unsubscribe_harness.c b/test/cbmc/proofs/MQTT_Unsubscribe/MQTT_Unsubscribe_harness.c index 3f17faa3..bc0396f4 100644 --- a/test/cbmc/proofs/MQTT_Unsubscribe/MQTT_Unsubscribe_harness.c +++ b/test/cbmc/proofs/MQTT_Unsubscribe/MQTT_Unsubscribe_harness.c @@ -23,7 +23,7 @@ * @file MQTT_Unsubscribe_harness.c * @brief Implements the proof harness for MQTT_Unsubscribe function. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" void harness() diff --git a/test/cbmc/proofs/MQTT_Unsubscribe/Makefile b/test/cbmc/proofs/MQTT_Unsubscribe/Makefile index 892ebb0a..15d30886 100644 --- a/test/cbmc/proofs/MQTT_Unsubscribe/Makefile +++ b/test/cbmc/proofs/MQTT_Unsubscribe/Makefile @@ -22,7 +22,7 @@ HARNESS_ENTRY=harness HARNESS_FILE=MQTT_Unsubscribe_harness -# Please see libraries/standard/mqtt/cbmc/stubs/network_interface_subs.c for +# Please see test/cbmc/stubs/network_interface_subs.c for # more information on MAX_NETWORK_SEND_TRIES. MAX_NETWORK_SEND_TRIES=3 # Bound on the the subscription count. Please see the default value in @@ -40,23 +40,23 @@ REMOVE_FUNCTION_BODY += # occurs. Please see NetworkInterfaceReceiveStub in # libraries\standard\mqtt\cbmc\stubs\network_interface_stubs.c for more # information. -UNWINDSET += __CPROVER_file_local_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) +UNWINDSET += __CPROVER_file_local_core_mqtt_c_sendPacket.0:$(MAX_NETWORK_SEND_TRIES) UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) UNWINDSET += MQTT_SerializeUnsubscribe.0:$(SUBSCRIPTION_COUNT_MAX) # The encodeRemainingLength loop is unwound 5 times because encodeRemainingLength() # divides a size_t variable by 128 until it reaches zero to stop the loop. # log128(SIZE_MAX) = 4.571... -UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:5 +UNWINDSET += __CPROVER_file_local_core_mqtt_lightweight_c_encodeRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/get_time_stub.c -PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/event_callback_stub.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c -PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/get_time_stub.c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/event_callback_stub.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_lightweight.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_state.c include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_Unsubscribe/cbmc-viewer.json b/test/cbmc/proofs/MQTT_Unsubscribe/cbmc-viewer.json index 7d278ab8..f0cf459a 100644 --- a/test/cbmc/proofs/MQTT_Unsubscribe/cbmc-viewer.json +++ b/test/cbmc/proofs/MQTT_Unsubscribe/cbmc-viewer.json @@ -3,5 +3,5 @@ ], "proof-name": "MQTT_Unsubscribe", - "proof-root": "libraries/standard/mqtt/cbmc/proofs" + "proof-root": "test/cbmc/proofs" } diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines index 82e9b5b4..36179148 100644 --- a/test/cbmc/proofs/Makefile-project-defines +++ b/test/cbmc/proofs/Makefile-project-defines @@ -18,11 +18,10 @@ COMPILE_FLAGS += -std=gnu90 LINK_FLAGS = # Preprocessor include paths -I... -INCLUDES += -I$(SRCDIR)/libraries/standard/mqtt/cbmc/include -INCLUDES += -I$(SRCDIR)/libraries/standard/mqtt/include -INCLUDES += -I$(SRCDIR)/libraries/standard/mqtt/src -INCLUDES += -I$(SRCDIR)/demos/logging-stack -INCLUDES += -I$(SRCDIR)/platform/include +INCLUDES += -I$(SRCDIR)/test/cbmc/include +INCLUDES += -I$(SRCDIR)/source/include +INCLUDES += -I$(SRCDIR)/source/src +INCLUDES += -I$(SRCDIR)/source/portable # Preprocessor definitions -D... DEFINES += -Dmqtt_EXPORTS diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets index bf681eed..2d4d4602 100644 --- a/test/cbmc/proofs/Makefile-project-targets +++ b/test/cbmc/proofs/Makefile-project-targets @@ -1,6 +1,9 @@ # -*- mode: makefile -*- # The first line sets the emacs major mode to Makefile +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + ################################################################ # Use this file to give project-specific targets, including targets # that may depend on targets defined in Makefile.common. diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing index 03b9a052..dc0c2097 100644 --- a/test/cbmc/proofs/Makefile-project-testing +++ b/test/cbmc/proofs/Makefile-project-testing @@ -1,6 +1,9 @@ # -*- mode: makefile -*- # The first line sets the emacs major mode to Makefile +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + ################################################################ # Use this file to define project-specific targets and definitions for # unit testing or continuous integration that may depend on targets diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines index f8c68bed..ee131a06 100644 --- a/test/cbmc/proofs/Makefile-template-defines +++ b/test/cbmc/proofs/Makefile-template-defines @@ -1 +1 @@ -SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../..) +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..) diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common index 71c36926..69d247eb 120000 --- a/test/cbmc/proofs/Makefile.common +++ b/test/cbmc/proofs/Makefile.common @@ -1 +1 @@ -../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common \ No newline at end of file +../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common \ No newline at end of file diff --git a/test/cbmc/proofs/README.md b/test/cbmc/proofs/README.md index 090da1de..cac5275b 120000 --- a/test/cbmc/proofs/README.md +++ b/test/cbmc/proofs/README.md @@ -1 +1 @@ -../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md \ No newline at end of file +../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md \ No newline at end of file diff --git a/test/cbmc/proofs/prepare.py b/test/cbmc/proofs/prepare.py index 220e7221..97c77e98 120000 --- a/test/cbmc/proofs/prepare.py +++ b/test/cbmc/proofs/prepare.py @@ -1 +1 @@ -../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py \ No newline at end of file +../aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py \ No newline at end of file diff --git a/test/cbmc/sources/README.md b/test/cbmc/sources/README.md index bfcee2de..969d1dee 120000 --- a/test/cbmc/sources/README.md +++ b/test/cbmc/sources/README.md @@ -1 +1 @@ -../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md \ No newline at end of file +../aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md \ No newline at end of file diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index c5240c93..8f2e0b71 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -20,7 +20,7 @@ */ #include #include -#include "mqtt.h" +#include "core_mqtt.h" #include "mqtt_cbmc_state.h" #include "network_interface_stubs.h" #include "get_time_stub.h" diff --git a/test/cbmc/stubs/README.md b/test/cbmc/stubs/README.md index 107ab230..327d6f6b 120000 --- a/test/cbmc/stubs/README.md +++ b/test/cbmc/stubs/README.md @@ -1 +1 @@ -../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md \ No newline at end of file +../aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md \ No newline at end of file diff --git a/test/cbmc/stubs/event_callback_stub.c b/test/cbmc/stubs/event_callback_stub.c index d645572d..924ddb2d 100644 --- a/test/cbmc/stubs/event_callback_stub.c +++ b/test/cbmc/stubs/event_callback_stub.c @@ -18,7 +18,7 @@ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "event_callback_stub.h" void EventCallbackStub( MQTTContext_t * pContext, diff --git a/test/cbmc/stubs/get_time_stub.c b/test/cbmc/stubs/get_time_stub.c index 6468371c..40ddb698 100644 --- a/test/cbmc/stubs/get_time_stub.c +++ b/test/cbmc/stubs/get_time_stub.c @@ -19,7 +19,7 @@ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "get_time_stub.h" uint32_t GetCurrentTimeStub( void ) diff --git a/test/cbmc/stubs/network_interface_stubs.c b/test/cbmc/stubs/network_interface_stubs.c index 6a0c1da1..5881cc9b 100644 --- a/test/cbmc/stubs/network_interface_stubs.c +++ b/test/cbmc/stubs/network_interface_stubs.c @@ -19,7 +19,7 @@ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. */ -#include "mqtt.h" +#include "core_mqtt.h" #include "network_interface_stubs.h" /* An exclusive bound on the times that the NetworkInterfaceSendStub will be