mirror of
https://github.com/FreeRTOS/coreMQTT
synced 2025-07-02 01:18:51 +08:00
Enable CBMC proof builds (#16)
This commit is contained in:
Archit Aggarwal
GitHub
parent
3ab7316bad
commit
09fbf71a3f
3
.gitmodules
vendored
3
.gitmodules
vendored
@ -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
|
||||
|
||||
1
test/cbmc/.gitignore
vendored
1
test/cbmc/.gitignore
vendored
@ -9,6 +9,7 @@ TAGS-*
|
||||
|
||||
# Emitted by Arpa
|
||||
arpa_cmake/
|
||||
arpa-validation-logs/
|
||||
Makefile.arpa
|
||||
|
||||
# These files should be overwritten whenever prepare.py runs
|
||||
|
||||
1
test/cbmc/aws-templates-for-cbmc-proofs
Submodule
1
test/cbmc/aws-templates-for-cbmc-proofs
Submodule
@ -0,0 +1 @@
|
||||
Subproject commit ca24f0651a8ae68145d965f0fadec2e5a32dfe8a
|
||||
@ -1,2 +0,0 @@
|
||||
__pycache__
|
||||
*~
|
||||
@ -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.
|
||||
@ -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.
|
||||
@ -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.
|
||||
@ -1 +0,0 @@
|
||||
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
||||
@ -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.
|
||||
@ -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()
|
||||
@ -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()
|
||||
@ -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)
|
||||
@ -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 */ );
|
||||
}
|
||||
@ -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
|
||||
@ -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`).
|
||||
@ -1,7 +0,0 @@
|
||||
{ "expected-missing-functions":
|
||||
[
|
||||
|
||||
],
|
||||
"proof-name": "<__FUNCTION_NAME__>",
|
||||
"proof-root": "<__PATH_TO_PROOF_ROOT__>"
|
||||
}
|
||||
@ -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
|
||||
@ -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.
|
||||
@ -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 =
|
||||
@ -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.
|
||||
################################################################
|
||||
@ -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
|
||||
################################################################
|
||||
@ -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 <DIR>.
|
||||
# b. Write a proof harness (a function) with the name <HARNESS_ENTRY>
|
||||
# in a file with the name <DIR>/<HARNESS_FILE>.c
|
||||
# c. Write a makefile with the name <DIR>/Makefile that looks
|
||||
# something like
|
||||
#
|
||||
# HARNESS_FILE=<HARNESS_FILE>
|
||||
# HARNESS_ENTRY=<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 <DIR> 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
|
||||
|
||||
################################################################
|
||||
@ -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.
|
||||
@ -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()
|
||||
@ -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.
|
||||
@ -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.
|
||||
@ -1 +1 @@
|
||||
../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/include/README.md
|
||||
../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md
|
||||
@ -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_ */
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Connect",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_DeserializeAck",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_DeserializePublish",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc"
|
||||
"proof-root": "test/cbmc"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Disconnect",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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"
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_GetIncomingPacketTypeAndLength",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_GetPacketId",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Init",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Ping",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_ProcessLoop",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Publish",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_ReceiveLoop",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializeAck",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializeConnect",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializeDisconnect",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializePingreq",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializePublish",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializePublishHeader",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializeSubscribe",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_SerializeUnsubscribe",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Subscribe",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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()
|
||||
|
||||
@ -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
|
||||
|
||||
@ -3,5 +3,5 @@
|
||||
|
||||
],
|
||||
"proof-name": "MQTT_Unsubscribe",
|
||||
"proof-root": "libraries/standard/mqtt/cbmc/proofs"
|
||||
"proof-root": "test/cbmc/proofs"
|
||||
}
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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.
|
||||
|
||||
@ -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
|
||||
|
||||
@ -1 +1 @@
|
||||
SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../..)
|
||||
SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
|
||||
|
||||
@ -1 +1 @@
|
||||
../../../../../tools/aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common
|
||||
../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
x
Reference in New Issue
Block a user