Skip to content

Commit d037058

Browse files
author
Daniel Kroening
committed
move developer tips from COMPILING to CODING_STANDARD
1 parent 47f413a commit d037058

File tree

2 files changed

+94
-93
lines changed

2 files changed

+94
-93
lines changed

CODING_STANDARD.md

+94
Original file line numberDiff line numberDiff line change
@@ -240,3 +240,97 @@ or use a symbolic link. Then, when running git commit, you should get the
240240
linter output (if any) before being prompted to enter a commit message. To
241241
bypass the check (e.g. if there was a false positive), add the option
242242
`--no-verify`.
243+
244+
# CODE COVERAGE
245+
246+
Code coverage metrics are provided using gcov and lcov. Ensure that you have
247+
installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for
248+
ubuntu lcov is available in the standard apt-get repos.
249+
250+
To get coverage metrics run the following script from the regression directory:
251+
```
252+
get_coverage.sh
253+
```
254+
This will:
255+
1) Rebuild CBMC with gcov enabled
256+
2) Run all the regression tests
257+
3) Collate the coverage metrics
258+
4) Provide an HTML report of the current coverage
259+
260+
# USING CLANG-FORMAT
261+
262+
CBMC uses clang-format to ensure that the formatting of new patches is readable
263+
and consistent. There are two main ways of running clang-format: remotely, and
264+
locally.
265+
266+
## RUNNING CLANG-FORMAT REMOTELY
267+
268+
When patches are submitted to CBMC, they are automatically run through
269+
continuous integration (CI). One of the CI checks will run clang-format over
270+
the diff that your pull request introduces. If clang-format finds formatting
271+
issues at this point, the build will be failed, and a patch will be produced
272+
in the CI output that you can apply to your code so that it conforms to the
273+
style guidelines.
274+
275+
To apply the patch, copy and paste it into a local file (`patch.txt`) and then
276+
run:
277+
```
278+
patch -p1 -i patch.txt
279+
```
280+
Now, you can commit and push the formatting fixes.
281+
282+
## RUNNING CLANG-FORMAT LOCALLY
283+
284+
### INSTALLATION
285+
286+
To avoid waiting until you've made a PR to find formatting issues, you can
287+
install clang-format locally and run it against your code as you are working.
288+
289+
Different versions of clang-format have slightly different behaviors. CBMC uses
290+
clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and
291+
Homebrew.
292+
To install on a Unix-like system, try installing using the system package
293+
manager:
294+
```
295+
apt-get install clang-format-3.8 # Run this on Ubuntu, Debian etc.
296+
brew install [email protected] # Run this on a Mac with Homebrew installed
297+
```
298+
299+
If your platform doesn't have a package for clang-format, you can download a
300+
pre-built binary, or compile clang-format yourself using the appropriate files
301+
from the [LLVM Downloads page](http://releases.llvm.org/download.html).
302+
303+
An installer for Windows (along with a Visual Studio plugin) can be found at
304+
the [LLVM Snapshot Builds page](http://llvm.org/builds/).
305+
306+
### FORMATTING A RANGE OF COMMITS
307+
308+
Clang-format is distributed with a driver script called git-clang-format-3.8.
309+
This script can be used to format git diffs (rather than entire files).
310+
311+
After committing some code, it is recommended to run:
312+
```
313+
git-clang-format-3.8 upstream/develop
314+
```
315+
*Important:* If your branch is based on a branch other than `upstream/develop`,
316+
use the name or checksum of that branch instead. It is strongly recommended to
317+
rebase your work onto the tip of the branch it's based on before running
318+
`git-clang-format` in this way.
319+
320+
### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS
321+
322+
If your works spans several commits and you'd like to keep the formatting
323+
correct in each individual commit, you can automatically rewrite the commits
324+
with correct formatting.
325+
326+
The following command will stop at each commit in the range and run
327+
clang-format on the diff at that point. This rewrites git history, so it's
328+
*unsafe*, and you should back up your branch before running this command:
329+
```
330+
git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
331+
-- upstream/develop..HEAD
332+
```
333+
*Important*: `upstream/develop` should be changed in *both* places in the
334+
command above if your work is based on a different branch. It is strongly
335+
recommended to rebase your work onto the tip of the branch it's based on before
336+
running `git-clang-format` in this way.

COMPILING.md

-93
Original file line numberDiff line numberDiff line change
@@ -278,96 +278,3 @@ To work with Eclipse, do the following:
278278
5. Click "Finish"
279279
6. Select Project -> Build All
280280
281-
# CODE COVERAGE
282-
283-
Code coverage metrics are provided using gcov and lcov. Ensure that you have
284-
installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for
285-
ubuntu lcov is available in the standard apt-get repos.
286-
287-
To get coverage metrics run the following script from the regression directory:
288-
```
289-
get_coverage.sh
290-
```
291-
This will:
292-
1) Rebuild CBMC with gcov enabled
293-
2) Run all the regression tests
294-
3) Collate the coverage metrics
295-
4) Provide an HTML report of the current coverage
296-
297-
# USING CLANG-FORMAT
298-
299-
CBMC uses clang-format to ensure that the formatting of new patches is readable
300-
and consistent. There are two main ways of running clang-format: remotely, and
301-
locally.
302-
303-
## RUNNING CLANG-FORMAT REMOTELY
304-
305-
When patches are submitted to CBMC, they are automatically run through
306-
continuous integration (CI). One of the CI checks will run clang-format over
307-
the diff that your pull request introduces. If clang-format finds formatting
308-
issues at this point, the build will be failed, and a patch will be produced
309-
in the CI output that you can apply to your code so that it conforms to the
310-
style guidelines.
311-
312-
To apply the patch, copy and paste it into a local file (`patch.txt`) and then
313-
run:
314-
```
315-
patch -p1 -i patch.txt
316-
```
317-
Now, you can commit and push the formatting fixes.
318-
319-
## RUNNING CLANG-FORMAT LOCALLY
320-
321-
### INSTALLATION
322-
323-
To avoid waiting until you've made a PR to find formatting issues, you can
324-
install clang-format locally and run it against your code as you are working.
325-
326-
Different versions of clang-format have slightly different behaviors. CBMC uses
327-
clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and
328-
Homebrew.
329-
To install on a Unix-like system, try installing using the system package
330-
manager:
331-
```
332-
apt-get install clang-format-3.8 # Run this on Ubuntu, Debian etc.
333-
brew install [email protected] # Run this on a Mac with Homebrew installed
334-
```
335-
336-
If your platform doesn't have a package for clang-format, you can download a
337-
pre-built binary, or compile clang-format yourself using the appropriate files
338-
from the [LLVM Downloads page](http://releases.llvm.org/download.html).
339-
340-
An installer for Windows (along with a Visual Studio plugin) can be found at
341-
the [LLVM Snapshot Builds page](http://llvm.org/builds/).
342-
343-
### FORMATTING A RANGE OF COMMITS
344-
345-
Clang-format is distributed with a driver script called git-clang-format-3.8.
346-
This script can be used to format git diffs (rather than entire files).
347-
348-
After committing some code, it is recommended to run:
349-
```
350-
git-clang-format-3.8 upstream/develop
351-
```
352-
*Important:* If your branch is based on a branch other than `upstream/develop`,
353-
use the name or checksum of that branch instead. It is strongly recommended to
354-
rebase your work onto the tip of the branch it's based on before running
355-
`git-clang-format` in this way.
356-
357-
### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS
358-
359-
If your works spans several commits and you'd like to keep the formatting
360-
correct in each individual commit, you can automatically rewrite the commits
361-
with correct formatting.
362-
363-
The following command will stop at each commit in the range and run
364-
clang-format on the diff at that point. This rewrites git history, so it's
365-
*unsafe*, and you should back up your branch before running this command:
366-
```
367-
git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
368-
-- upstream/develop..HEAD
369-
```
370-
*Important*: `upstream/develop` should be changed in *both* places in the
371-
command above if your work is based on a different branch. It is strongly
372-
recommended to rebase your work onto the tip of the branch it's based on before
373-
running `git-clang-format` in this way.

0 commit comments

Comments
 (0)