CBMC

cbmc:pull-request/arrays-in-trace

  1. Git
  2. lp:cbmc
  3. pull-request/arrays-in-trace
Last commit made on 2017-06-15
Get this branch:
git clone -b pull-request/arrays-in-trace https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
pull-request/arrays-in-trace
Repository:
lp:cbmc

Recent commits

8f192ae... by Romain Brenguier

Documentation for json_goto_trace in doxygen format

c45033c... by Romain Brenguier

Adding test to check that data field of strings are set in json

d7dde9c... by Romain Brenguier

Simplifying array access and expressions with pointer offsets

We simplify expressions containing array accesses before producing a
json representation of the trace.
This commit also adds comments on the functions in the cpp files

Includes improvements in json_goto_trace.cpp following review of PR#922

d353236... by Romain Brenguier

Simplifying expressions of the form &array[0] in json

We simplifying these expression so that these pointers appear correctly
in the trace in json.
This is related to issue diffblue/test-gen#21

Includes improvements in json_expr.cpp following review of PR#922

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

Merge pull request #1004 from smowton/smowton/feature/time_limit_minisat

Add simple time limiting to prop_conv and propt

0ee4933... by Chris Smowton <email address hidden>

Add simple time limiting to prop_conv and propt

Currently only minisat2 supports this.

38907fc... by Chris Smowton <email address hidden>

Merge pull request #1003 from smowton/smowton/cleanup/traces_to_status_out

Write traces to status() not cout

23e2c9b... by Chris Smowton <email address hidden>

Merge pull request #1012 from smowton/smowton/merge/master_20170614

Smowton/merge/master 20170614

4324bbd... by Chris Smowton <email address hidden>

Disable warnings that result from array-of with zero length

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

Merge remote-tracking branch 'origin/master' into smowton/merge/master_20170614