CBMC

cbmc:value_set_code

  1. Git
  2. lp:cbmc
  3. value_set_code
Last commit made on 2021-11-08
Get this branch:
git clone -b value_set_code https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
value_set_code
Repository:
lp:cbmc

Recent commits

f98ccce... by Daniel Kroening <email address hidden>

expand value_sett::apply_code_rec

The method value_sett::apply_code_rec is expanded at its call site; this
removes the invocation of get_code(), which is earmarked for removal.

d0e6b9a... by Thomas Spriggs <email address hidden>

Merge pull request #6445 from thomasspriggs/tas/smt_codeowners

Update CODEOWNERS to facilitate work on SMT2 solver support

a229942... by Thomas Andrew Spriggs

Add codeowners of `/src/solvers/makefile`

So that those who can approve changes to the smt2 solver support can
also approve adding / removing / renaming `.cpp` files in those
subdirectories. The list of codeowners is based on the global code
owners plus the smt2 code owners. This is as suggested by Michael
Tautschnig here -
https://github.com/diffblue/cbmc/pull/6415#issuecomment-951813494

73e271e... by Thomas Andrew Spriggs

Update codeowners of `/src/solvers/smt2` to those working on it

Removing @allredj @romainbrenguier as these people do not currently work
on SMT2 support. Adding @thomasspriggs @NlightNFotis @TGWDB due to
current experience of working on SMT2 support.

ff9082a... by Thomas Andrew Spriggs

Remove `@tautschnig` from code ownership of `/src/solvers/smt2`

As requested by Michael Tautschnig in a review comment -
https://github.com/diffblue/cbmc/pull/6422/files#r740281493

1b8ceee... by Michael Tautschnig <email address hidden>

Merge pull request #6441 from diffblue/goto_program_OTHER_nl

goto_programt::output: add missing newline

d250cce... by Daniel Kroening <email address hidden>

goto_programt::output: add missing newline

74963e7... by Fotis Koutoulakis <email address hidden>

Merge pull request #6434 from NlightNFotis/implication_statement_checks

Refinement of guard based on antecedent of implication statement

4c40cd0... by Fotis Koutoulakis

Add a `PRECONDITION` for the types of expressions that `check_rec_logical_op` can handle.

It should only handle `and`, `or` or `==>`.

6dfd3f7... by TGWDB <email address hidden>

Merge pull request #6395 from remi-delmas-3000/pointer-primitive-pragma

enabling `#pragma disable "pointer-primitive"`