CBMC

cbmc:noexcept

  1. Git
  2. lp:cbmc
  3. noexcept
Last commit made on 2019-01-19
Get this branch:
git clone -b noexcept https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
noexcept
Repository:
lp:cbmc

Recent commits

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

add noexcept to frequently used constructors

0f7a99d... by Daniel Kroening <email address hidden>

added constructor for goto_symex_statet::framet

This enables removing the default constructor for sourcet.

fca695a... by Michael Tautschnig

Merge pull request #3832 from tautschnig/function-as_string

as_string() on instructions now takes function identifier [blocks: #3126]

8fe6120... by Michael Tautschnig

Merge pull request #3830 from tautschnig/function-goto_check

goto_check() now gets function identifier [blocks: #3126]

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

goto_check() now gets function identifier

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required. Consequently the mode is no
longer required as we can obtain it from the symbol table.

3b1b45f... by Daniel Kroening <email address hidden>

as_string() on instructions now takes function identifier

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.

dcbda65... by Joel Allred <email address hidden>

Merge pull request #3827 from allredj/disable-loopless-init-for-bool

Skip simple nondet initialization for arrays of bool

12bce17... by Chris Smowton <email address hidden>

Merge pull request #3826 from smowton/smowton/fix/json-expr-simplify-pointers

Fix json_expr simplification of pointers

d141953... by Chris Smowton <email address hidden>

Install jq under Travis and CodeBuild

This means CI will run the new jbmc-json-ui test group.

d14be45... by Chris Smowton <email address hidden>

Add a test for JBMC's JSON-formatted trace

The new test directory is unique in that it uses a chain.sh that passes the result through 'jq',
making it much easier to phrase tests like "this should result in JSON that contains a 'trace'
that itself has many records, all of which have a given property"