Skip to content

Commit 54f4af2

Browse files
author
Mark R. Tuttle
committed
Initial commit
0 parents  commit 54f4af2

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

57 files changed

+10821
-0
lines changed

‎.eslintrc.json

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{
2+
"root": true,
3+
"parser": "@typescript-eslint/parser",
4+
"parserOptions": {
5+
"ecmaVersion": 6,
6+
"sourceType": "module"
7+
},
8+
"plugins": [
9+
"@typescript-eslint"
10+
],
11+
"rules": {
12+
"@typescript-eslint/naming-convention": "warn",
13+
"@typescript-eslint/semi": "warn",
14+
"curly": "warn",
15+
"eqeqeq": "warn",
16+
"no-throw-literal": "warn",
17+
"semi": "off"
18+
}
19+
}

‎.gitignore

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
out
2+
dist
3+
node_modules
4+
.vscode-test/
5+
.vscode/
6+
*.vsix
7+
*~

‎.vscodeignore

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
**/*.map
2+
**/*.ts
3+
**/.eslintrc.json
4+
**/tsconfig.json
5+
.gitignore
6+
.vscode-test/**
7+
.vscode/**
8+
.yarnrc
9+
CHANGELOG.md
10+
Makefile
11+
demo/**
12+
docs/**
13+
out/test/**
14+
src/**

‎CHANGELOG.md

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
# Change Log
2+
3+
All notable changes to the "mctracedebugger" extension will be documented in this file.
4+
5+
Check [Keep a Changelog](http://keepachangelog.com/) for recommendations on how to structure this file.
6+
7+
## [Unreleased]
8+
9+
- Initial release

‎CODE_OF_CONDUCT.md

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
## Code of Conduct
2+
This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
3+
For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
4+
[email protected] with any additional questions or comments.

‎CONTRIBUTING.md

+59
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
# Contributing Guidelines
2+
3+
Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional
4+
documentation, we greatly value feedback and contributions from our community.
5+
6+
Please read through this document before submitting any issues or pull requests to ensure we have all the necessary
7+
information to effectively respond to your bug report or contribution.
8+
9+
10+
## Reporting Bugs/Feature Requests
11+
12+
We welcome you to use the GitHub issue tracker to report bugs or suggest features.
13+
14+
When filing an issue, please check existing open, or recently closed, issues to make sure somebody else hasn't already
15+
reported the issue. Please try to include as much information as you can. Details like these are incredibly useful:
16+
17+
* A reproducible test case or series of steps
18+
* The version of our code being used
19+
* Any modifications you've made relevant to the bug
20+
* Anything unusual about your environment or deployment
21+
22+
23+
## Contributing via Pull Requests
24+
Contributions via pull requests are much appreciated. Before sending us a pull request, please ensure that:
25+
26+
1. You are working against the latest source on the *main* branch.
27+
2. You check existing open, and recently merged, pull requests to make sure someone else hasn't addressed the problem already.
28+
3. You open an issue to discuss any significant work - we would hate for your time to be wasted.
29+
30+
To send us a pull request, please:
31+
32+
1. Fork the repository.
33+
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.
34+
3. Ensure local tests pass.
35+
4. Commit to your fork using clear commit messages.
36+
5. Send us a pull request, answering any default questions in the pull request interface.
37+
6. Pay attention to any automated CI failures reported in the pull request, and stay involved in the conversation.
38+
39+
GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and
40+
[creating a pull request](https://help.github.com/articles/creating-a-pull-request/).
41+
42+
43+
## Finding contributions to work on
44+
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.
45+
46+
47+
## Code of Conduct
48+
This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
49+
For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
50+
[email protected] with any additional questions or comments.
51+
52+
53+
## Security issue notifications
54+
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.
55+
56+
57+
## Licensing
58+
59+
See the [LICENSE](LICENSE) file for our project's licensing. We will ask you to confirm the licensing of your contribution.

‎INSTALLATION.md

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
## Installation
2+
3+
On MacOS, use the [homebrew](https://brew.sh/) package manager to install with
4+
5+
```
6+
brew install node
7+
git clone https://model-checking/cbmc-proof-debugger.git cbmc-proof-debugger
8+
cd cbmc-proof-debugger
9+
npm install
10+
make
11+
make install
12+
```
13+
14+
The [homebrew](https://brew.sh/) page gives instructions for
15+
installing `brew`.
16+
The command `brew install node` installs the [Node.js](https://nodejs.org)
17+
runtime for [JavaScript](https://en.wikipedia.org/wiki/JavaScript),
18+
including the [npm](https://docs.npmjs.com/about-npm) package manager.
19+
The command `npm install` installs the dependencies listed in
20+
packages.json into the directory `node_modules`.
21+
The command `make` builds the extension into a file
22+
named `proof-debugger-VERSION.vsix` where `VERSION` is the version number
23+
given in package.json.
24+
The command `make install` runs `code` from the command line to
25+
install the extension in Code.
26+
27+
On other platforms, you can download a Node.js installer for your platform
28+
from the [Node.js download page](https://nodejs.org/en/download),
29+
and the remaining instructions should work.
30+
On Ubuntu, you can install Node.js with just `apt install nodejs`.
31+
If you learn how to build and install this package on your platform,
32+
please submit a pull request to contribute your instructions.

‎LICENSE.md

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
3+
Permission is hereby granted, free of charge, to any person obtaining a copy of
4+
this software and associated documentation files (the "Software"), to deal in
5+
the Software without restriction, including without limitation the rights to
6+
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
7+
the Software, and to permit persons to whom the Software is furnished to do so.
8+
9+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
10+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
11+
FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
12+
COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
13+
IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
14+
CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
15+

‎Makefile

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
default:
2+
./node_modules/.bin/vsce package
3+
4+
install:
5+
code --install-extension proof-debugger-*.vsix
6+
7+
format:
8+
./node_modules/.bin/tsfmt -r src/*.ts
9+
10+
clean:
11+
$(RM) *~
12+
cd demo && make clean
13+
14+
veryclean: clean
15+
$(RM) -r out
16+
$(RM) src/*.js
17+
$(RM) *.vsix
18+
19+
.PHONY: default install format clean veryclean

‎README.md

+43
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
## CBMC Proof Debugger
2+
3+
The
4+
[CBMC Proof Debugger](https://github.com/model-checking/cbmc-proof-debugger)
5+
is a debugger for
6+
[Visual Studio Code](https://code.visualstudio.com/)
7+
for debugging error traces from
8+
[CBMC](https://github.com/diffblue/cbmc).
9+
10+
[CBMC](https://github.com/diffblue/cbmc)
11+
is a model checker for C. CBMC will explore all possible paths
12+
through your code on all possible inputs, and will check that all
13+
assertions in your code are true. CBMC can also check for the
14+
possibility of security issues (like buffer overflow) and for
15+
instances of undefined behavior (like signed integer overflow).
16+
If CBMC finds a code issue, it generates an error trace demonstrating how that
17+
issue could occur.
18+
If CBMC terminates without finding any issues, the result is
19+
assurance that your code behaves as expected.
20+
CBMC is a *bounded* model checker, however, so getting CBMC to terminate
21+
may require restricting inputs to some bounded size,
22+
and CBMC's assurance is restricted to these bounded inputs.
23+
24+
[CBMC Viewer](https://github.com/model-checking/cbmc-viewer)
25+
is a tool that scans the output of CBMC and produces a browsable summary
26+
of its findings, making it easy to root cause the issues CBMC finds using
27+
any web browser. Viewer also produces a summary of its findings in the
28+
form of a collection of json blobs.
29+
30+
The
31+
[CBMC Proof Debugger](https://github.com/model-checking/cbmc-proof-debugger)
32+
loads the json summaries produced by CBMC Viewer,
33+
and lets a developer explore the error traces produced by CBMC using
34+
the Visual Studio Code's debugger.
35+
36+
## Security
37+
38+
See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
39+
40+
## License
41+
42+
This library is licensed under the MIT-0 License. See the [LICENSE](LICENSE.md)
43+
file.

‎demo/.gitignore

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
*.goto
2+
*.xml
3+
*.json
4+
/report/

‎demo/.vscode-backup/launch.json

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
// Use IntelliSense to learn about possible attributes.
3+
// Hover to view descriptions of existing attributes.
4+
// For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
5+
"version": "0.2.0",
6+
"configurations": [
7+
{
8+
"type": "viewer",
9+
"request": "launch",
10+
"name": "Viewer debug",
11+
"stopOnEntry": true,
12+
"trace": true
13+
}
14+
]
15+
}

‎demo/Makefile

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
default: report
2+
3+
4+
#CBMC_FLAGS= --pointer-check --bounds-check --signed-overflow-check --unwind 1
5+
CBMC_FLAGS= --pointer-check --bounds-check --unwind 1
6+
7+
%.goto: %.c
8+
goto-cc -c -o $@ $<
9+
10+
test.goto: foo.goto main.goto
11+
goto-cc -o $@ $?
12+
13+
result.xml: test.goto
14+
-cbmc $(CBMC_FLAGS) --unwinding-assertions --xml-ui $< > $@
15+
16+
coverage.xml: test.goto
17+
-cbmc --cover location --xml-ui $< > $@
18+
19+
property.xml: test.goto
20+
-cbmc --show-properties $(CBMC_FLAGS) --unwinding-assertions --xml-ui $< > $@
21+
22+
report: test.goto result.xml coverage.xml property.xml
23+
cbmc-viewer \
24+
--result result.xml \
25+
--coverage coverage.xml \
26+
--property property.xml \
27+
--srcdir . \
28+
--goto test.goto
29+
30+
loop.xml: test.goto
31+
cbmc --show-loops --xml-ui $< > $@
32+
33+
viewer-property.json: property.xml
34+
make-property --srcdir . $< > $@
35+
36+
viewer-coverage.json: coverage.xml
37+
make-coverage --srcdir . $< > $@
38+
39+
viewer-result.json: result.xml
40+
make-result $< > $@
41+
42+
viewer-loop.json: loop.xml
43+
make-loop --srcdir . $< > $@
44+
45+
clean:
46+
$(RM) *~
47+
$(RM) *.goto
48+
$(RM) *.json
49+
$(RM) *.xml
50+
$(RM) -r report
51+
$(RM) *.vsix
52+
$(RM) -r .vscode
53+
54+
.PHONY: report demo
55+
56+
demo:
57+
$(MAKE) clean
58+
$(RM) -r .vscode
59+
- code --uninstall-extension mrtuttle.proof-debugger
60+
make -C ..
61+
cp ../proof-debugger-*.vsix .
62+
@echo
63+
@echo 'Do: make report'
64+
@echo 'Do: code --install-extension proof-debugger-*.vsix'
65+
@echo 'Do: code .'
66+
@echo 'Configure'
67+
@echo 'Load traces'
68+
@echo 'Debug'

0 commit comments

Comments
 (0)