Skip to content

Add CBMC Mini Projects list #3930

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 6, 2019
Merged

Conversation

karkhaz
Copy link
Collaborator

@karkhaz karkhaz commented Jan 25, 2019

This list is intended to be a central repository of small, focussed CBMC
'nice-to-have' features that would be suitable for first-time CBMC
contributors to get their feet wet with. Projects on this list should
have the following features:

  • Small (e.g. <200 LOC) or easy to implement

    • This is so that time-constrained contributors (like interns or
      students) can use these projects to ramp up before starting their
      main CBMC work
  • Focussed, touching only one part of the codebase

    • This is so that people wanting to learn about one aspect of CBMC
      (solver, front-end, symex) can pick a project that involves that
      part of the codebase.
  • Genuinely useful to somebody

    • This is so that somebody will be keen to quickly review and merge
      the code, and guide the new contributor in polishing the PR. This
      leads to a more rewarding experience for the contributor.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 0944cdc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98560297
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

Copy link
Contributor

@danpoe danpoe left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That looks very useful! I like the suggested projects as well and hope we'll add more in the future.

This list is intended to be a central repository of small, focussed CBMC
'nice-to-have' features that would be suitable for first-time CBMC
contributors to get their feet wet with. Projects on this list should
have the following features:

- Small (e.g. <200 LOC) or easy to implement

  - This is so that time-constrained contributors (like interns or
    students) can use these projects to ramp up before starting their
    main CBMC work

- Focussed, touching only one part of the codebase

  - This is so that people wanting to learn about one aspect of CBMC
    (solver, front-end, symex) can pick a project that involves that
    part of the codebase.

- Genuinely useful to somebody

  - This is so that somebody will be keen to quickly review and merge
    the code, and guide the new contributor in polishing the PR. This
    leads to a more rewarding experience for the contributor.
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 5764b81).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98656572
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@martin-cs
Copy link
Collaborator

Years ago (on the old Wiki) I wrote a bunch of these:

https://web.archive.org/web/20150530010030/http://www.cprover.org/wiki/doku.php?id=starter_projects

I don't know how many of them are still relevant / interesting.

@karkhaz
Copy link
Collaborator Author

karkhaz commented Feb 6, 2019

Thanks! @martin-cs please feel free to add any that are still relevant? It looks like some of them were already assigned to people, and a couple of them look complete.

Also, many of those projects look interesting and useful, but are larger than the ones I envisioned for that list. I do think it's worth keeping a record of larger starter projects though. I now wonder whether this would be better maintained as a page under the official documentation, split into subsections (<= 2 weeks, <= 6 weeks, <= 3 month projects)?

I don't mind either way, perhaps we could merge this and then add some longer projects in a separate PR.

@kroening kroening merged commit 55302b7 into diffblue:develop Feb 6, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants