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

Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking #1641

Merged
merged 6 commits into from Feb 21, 2018

Conversation

@karkhaz
Contributor

karkhaz commented Nov 29, 2017

CBMC can now model-check each path of a program one at a time, displaying the verification result for that path before continuing to symbolically execute other paths. This functionality is similar to what the symex tool provides, but uses the goto-symex core that is already used by CBMC rather than having a disjoint symbolic execution codebase. This functionality is enabled by passing the --paths flag to CBMC or JBMC.

When --paths is passed, CBMC does not perform path merging when it encounters a program join point. Instead, whenever it encounters a conditional goto instruction, it saves the state of the symbolic executor onto a workqueue and executes one of the branches. Once symbolic execution has finished and the verification result printed out, CBMC pops the workqueue and resumes executing the untaken branch.

This is all integrated with the existing bmc and goto_symext classes, with no change in CBMC's original model-checking functionality. Without the --paths flag, CBMC's full-program model-checking behaviour is an edge-case of path exploration, whereby no goto branch-points are saved and so the entire program is only symbolically executed once.

The main patch in this patchset is [path explore 5/6] Support path-based exploration. Other commits are fairly small and introduce features that are necessary for path exploration, but which are also desirable changes by themselves.

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Nov 29, 2017

Thanks for this patch set; it looks really exciting.

Paging @theyoucheng who has a similar patch set and @bjowac who was the original author of symex. Also cross linking against #749 for my last attempt at getting everyone who cared about per-path symex talking to each other so we didn't duplicate work.

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Nov 29, 2017

@martin-cs thanks for the comment. This is a complete implementation and is working well, but I'd like to braindump a few future refinements here for the record:

  • Different heuristics for deciding which path to execute next. The implementation in this pull request is a simple FIFO, i.e. whenever we get to a branch point, we save the path that we don't execute for now, and resume paths in the order that they were saved. It turns out that this isn't a great strategy. I should have better ones in the next few weeks.

  • Multithreaded CBMC. This is exciting! Every path that is symbolically executed could be done in a different thread. The only data structure that needs to be shared is the workqueue where upcomming paths are saved, so we'd need to lock that (and it's potentially a fairly hot data structure). Mark Tuttle suggests that to remedy this, we could experiment with every thread having its own local queue of paths to execute next, and pull paths from the global workqueue only when the local one gets emptied (and of course, every thread should contribute paths to resume to the global workqueue).
    Another way to avoid this issue entirely is to have all symbolic execution happen in the main thread, but fork off the SAT solver in a different thread or process (so that CBMC is symbolically executing one path while the SAT solver checks another).
    In either case, thread/process control would be done entirely from the method bmct::do_language_agnostic_bmc, which is a method that is introduced in this patchset. I expect that doing this wouldn't be too invasive, but we'd need to add an implementation of a thread or process pool to the codebase.

cheers!

@smowton

Some comments. Mostly doxy comments, style and some inconsistency in how the arguments are described. Most substantively I'd appreciate comments where appropriate about why namespaces are being re-initialised to point at different symbol tables, and at what stage they point to different places (therefore, if a future coder is editing goto_symext and adds an ns.lookup, what tables do they think they're referring to? Is it outright invalid (uninitialised) at any point?)

src/cbmc/bmc.cpp Outdated
const optionst &opts,
const goto_modelt &goto_model,
const ui_message_handlert::uit &ui,
messaget *const message)

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

Take by reference?

src/cbmc/bmc.cpp Outdated
result=bmc.run(goto_model.goto_functions);
}
INVARIANT(opts.get_bool_option("paths") || worklist.empty(),
"Some branches were unexplored when model-checking "

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

Recommend making a "should" statement here, as otherwise it's often confusing whether the statement says what should have been or what went wrong.

src/cbmc/bmc.cpp Outdated
worklist.pop_front();
}
}
catch(const char *error_msg)

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

Recommend throwing structured errors rather than plain strings wherever possible

This comment has been minimized.

@karkhaz

karkhaz Dec 1, 2017

Contributor

@smowton this catch is to deal with a throw from cbmc_solverst, i.e. it's code that predates this patchset. As far as I can see, that code only ever throws the number 0 (and it prints a message to messaget::error() just before it throws). I'm not familiar with cprover's error handling, what sort of error would you recommend that I throw from cbmc_solvert instead of 0? Or should I just leave that there?

This comment has been minimized.

@smowton

smowton Dec 1, 2017

Member

"Pretty crap," in brief ;) If it's old code you're catching from, I guess you intend to catch everything? In that case I'd catch const char * and const std::string & (perhaps mergable if exception catching permits implicit construction to catch, but I doubt it) and then catch(...) to catch other errors. If you specifically intend to catch some things but let others get by then you should at least document your intent in comments, and probably change the throwing code to throw something more specific.

This comment has been minimized.

@martin-cs

martin-cs Dec 16, 2017

Collaborator

#include "martin_comment_about_catch_all_vs_invariants.h"

If you are going to catch (...) please exit and / or throw upwards; many exceptions are non-recoverable.

src/cbmc/bmc.cpp Outdated
cbmc_solver=solvers.get_solver();
prop_convt &pc=cbmc_solver->prop_conv();
goto_symext::branch_pointt &resume=worklist.front();
path_explorert pe(opts,

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

If there are this many args, probably clearest to break after ( and then list one argument per line

@@ -596,3 +599,93 @@ void bmct::setup_unwind()
if(options.get_option("unwind")!="")
symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
}
int bmct::do_language_agnostic_bmc(

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

Please add function-level doxy comments

This comment has been minimized.

@karkhaz

karkhaz Nov 30, 2017

Contributor

The prevalent style seems to be having the doxy comments in header files, right? I already have one there, but it's a bit brief so I'll expand it.

src/goto-symex/symex_goto.cpp Outdated
goto_programt::const_targett tmp=new_state_pc;
new_state_pc=state_pc;
state_pc=tmp;
std::cerr << "Resuming from '" << state_pc->code.source_location() << "'\n";

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

If this is a debug message, guard with #ifdef DEBUG_GOTO_SYMEX or something (and the same for iostream include above). Otherwise, use a messaget or get one passed in.

This comment has been minimized.

@karkhaz

karkhaz Nov 30, 2017

Contributor

If #1625 gets merged in before this, symext will have a messaget mutable member as you suggested so I'll rebase and use that

This comment has been minimized.

@tautschnig

tautschnig Nov 30, 2017

Collaborator

FWIW I'll merge #1625 as soon as CI completes.

src/goto-symex/symex_goto.cpp Outdated
do_simplify(simpl_state_guard);
// No point executing both branches of an unconditional goto.
if(new_guard.is_true()&& // We have an unconditional goto, AND

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

Space before && and ||

src/goto-symex/symex_goto.cpp Outdated
// Goto is conditional, so figure out which branch to take before
// checking whether to do path exploration or model-checking, and before
// adjusting guards.
std::string gp=options.get_option("goto-priority");

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

As above, suggest using an enum type

src/goto-symex/symex_goto.cpp Outdated
branch_point.state.has_saved_target=true;
branch_point.state.saved_target_is_backwards=forward;
branch_worklist.push_back(branch_point);
std::cerr << "Saving '" << new_state_pc->source_location << "'\n";

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

Another use of std streams

src/goto-symex/symex_main.cpp Outdated
{
ns=namespacet(outer_symbol_table, state.symbol_table);

This comment has been minimized.

@smowton

smowton Nov 30, 2017

Member

As above, could you comment why namespaces are being re-initialised to point at different tables like this? What tables will ns refer to and at what stage in proceedings?

@smowton smowton changed the title from CBMC now supports path exploration in addition to full bounded model checking to Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking Nov 30, 2017

@smowton

This comment has been minimized.

Member

smowton commented Nov 30, 2017

Also edited title to the usual "voice" for such things :)

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Nov 30, 2017

@smowton thanks so much for the prompt review, I'll try and get this done within the next few days.

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Dec 1, 2017

@karkhaz Multi-threading certainly is exciting but may I add a small note of caution. SAT solvers are very sensitive to memory latency and cache sizes. Given parts of the memory subsystem are shared between cores, running a SAT solver in one core can adversely affect the performance of a SAT solver running in another. Before you start work, I'd recommend trying the following experiment.

*. Pick a benchmark that takes at least 30 seconds and uses at least at least 50 MB of memory in the SAT solver.
*. Try running 1, 2, ..., $NUMBER_OF_CORES copies simultaneously and record the wall clock time taken to finish the complete run.
*. Plot total time and total time / N (work-rate) against N and see where they peak.

If total time is flat and work-rate peaks at N; brilliant, my warning no longer applies. If the peak is elsewhere and the lower it is, consider if it is worth the investment of time to multi-thread stuff.

( Also, a seeded pseudo-random queuing policy, run as a portfolio could also give a lower bound / estimate on the performance of the multi-threading.)

The other exciting topic, with @DanielNeville can provide input on is when to merge and when to queue. I'm told that "merge forwards branches and queue backwards ones" does interesting things...

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Dec 1, 2017

@martin-cs thanks for this information! I'd certainly be interested in better merging heuristics. Something that I have working (not in this patchset) is the ability to put __CPROVER_begin_path_explore() and __CPROVER_end_path_explore() dummy function calls in the target codebase. The idea is to be able to do merging up until a point, and then do path exploration from that point onward, and switch merging back on. Or, the other way round. This very coarse-grained approach seems to work nicely for particular "shapes" of codebases. But obviously an automatic decision on when to merge would be extremely welcome.

Hopefully there's a lot of experimenting to be done here: what are the best heuristics for deciding when to merge, and what are the best heuristics for deciding on which path to explore next. I'm planning to gather some amount of empirical data about this, and would be very interested to read data gathered by others also.

@karkhaz karkhaz requested a review from forejtv as a code owner Dec 3, 2017

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Dec 4, 2017

@smowton I've addressed all your suggestions, thanks so much!

I've also added two commits to deal with the cpplint and clang-format. They're in this PR because linting won't pass without them.

src/cbmc/cbmc_parse_options.h Outdated
"(localize-faults)(localize-faults-method):" \
#define CBMC_OPTIONS \
OPT_BMC \
"(preprocess)(slice-by-trace):" OPT_FUNCTIONS \

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Keep OPT_FUNCTIONS and OPT_GOTO_CHECK on their own lines

src/goto-programs/safety_checker.h Outdated
safety_checkert::resultt const &r1,
safety_checkert::resultt const &r2)
{
return r1 == safety_checkert::resultt::SAFE

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

How about defining an operator< then simply returning std::min or std::max(r1, r2)?

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

(or a named comparator function, say result_worse_than, then using std::min(r1, r2, result_worse_than)

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Just realised this is only showing up at all due to clang-format, so can ignore this

src/jbmc/jbmc_parse_options.cpp Outdated
" --json-ui use JSON-formatted output\n"
" --verbosity # verbosity level\n"
"\n";
std::cout << "* * Daniel Kroening, Edmund Clarke * "

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

I'd avoid reformatting the whole help text / arg list if I were you, even if the linters complain -- this makes an annoying commit to rebase across

@smowton

Looks good! Couple of nitpicks; I'd probably drop commit #8 though (the wholesale linter patch), clang-format is introducing lots of pointless churn here. Though perhaps I'm doing a King Canute act -- @peterschrammel any opinion?

src/cbmc/bmc.cpp Outdated
statistics() << "size of program expression: "
<< equation.SSA_steps.size()
<< " steps" << eom;
statistics() << "size of program expression: " << equation.SSA_steps.size()

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Don't reformat unchanged lines

This comment has been minimized.

@martin-cs

martin-cs Feb 20, 2018

Collaborator

+1 what he said.

src/cbmc/bmc.cpp Outdated
if(cmdline.isset("goto-priority"))
{
const std::string &priority = cmdline.get_value("goto-priority");
if(priority == "jump")

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Braces around multi-line if (similarly below)

src/cbmc/bmc.h Outdated
#include <goto-programs/safety_checker.h>
#include <goto-symex/memory_model.h>
#include "symex_bmc.h"
class bmct:public safety_checkert
class goto_modelt;

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Header is included so probably unnecessary

@tautschnig

This comment has been minimized.

Collaborator

tautschnig commented Dec 4, 2017

Echoing @smowton's comment: please don't clang-format what hasn't been touched to avoid rebasing hell.

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Dec 4, 2017

@tautschnig and @smowton I've run into issues with clang format's incremental use not being that incremental.

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Dec 4, 2017

@smowton that's done. I removed the forward class declaration. All your other comments were about changes introduced in the clang-format commit, which I've dropped.

@smowton

This comment has been minimized.

Member

smowton commented Dec 4, 2017

Great, thanks! In that case my only other suggestion is to replace the exhaustive listing of resultt with a comparator and min and max calls in operator|| and && respectively. Otherwise all looks great!

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Dec 4, 2017

@smowton cheers, I did that. I think this implementation is actually better, as it uses a switch statement so that the compiler can warn if new values are added to the enum, rather than checking and throwing at runtime.

@smowton

Like the pattern, couple of problems with the implementation

src/goto-programs/safety_checker.h Outdated
@@ -45,4 +45,39 @@ class safety_checkert:public messaget
const namespacet &ns;
};
/// \brief is `r1` a worse result than `r2`?
inline bool operator<(
safety_checkert::resultt &r1,

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Take by value

src/goto-programs/safety_checker.h Outdated
switch(r1)
{
case safety_checkert::resultt::ERROR:
return true;

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

This is wrong, two things that are == must not be <. This should return true if r1 is strictly worse than r2.

src/goto-programs/safety_checker.h Outdated
}
/// \brief The worst of two results
inline safety_checkert::resultt &operator&=(

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Take and return by value

src/goto-programs/safety_checker.h Outdated
}
/// \brief The best of two results
inline safety_checkert::resultt &operator|=(

This comment has been minimized.

@smowton

smowton Dec 4, 2017

Member

Similar

karkhaz added some commits Feb 15, 2018

[path explore 3/7] Logical ops for resultt
The operators &= and |= can now be used between two
safety_checkert::resultt objects. They return the "best" or "worst" of
two results, and additionally assign that result to the LHS.  The
assignment operators are useful when repeatedly performing a safety
check and wanting to return a single error code that either describes
the best or worst outcome of all the safety checks combined.
[path explore 4/7] Factor out common BMC code
The CBMC and JBMC frontends included identical code for running BMC
after the language-specific preprocessing. This commit moves that common
code into a static method of bmct.

Parse options and help text related to bounded model checking are
defined in bmc.h.
@tautschnig

This comment has been minimized.

Collaborator

tautschnig commented Feb 20, 2018

@karkhaz Just state whether you'd like to review the code and make changes right away in light of @martin-cs' comments.

@martin-cs & @karkhaz: I'd like to merge this relatively soon to have a first implementation in place for everyone to use and then iterate to improve it.

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Feb 20, 2018

@tautschnig sorry, I pushed right before I saw your comment. @martin-cs I've removed 6/8, and I'll add a more general flag once I have my heuristics ready and it's more clear what the implementation will look like. Does that work?

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Feb 20, 2018

@tautschnig I think my question about what's happened to the output method is probably more of a blocker than the 6/8 question.

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Feb 20, 2018

@karkhaz Thank you that is most considerate of you.

karkhaz added some commits Nov 29, 2017

[path explore 5/7] Support path-based exploratio2
This commit introduces the --paths flag to CBMC, which makes CBMC
model-check each individual path of the program rather than merging
paths and model-checking the entire program.

The overall strategy involves allowing the "state" of symbolic
execution---i.e., a pair of goto_symex_statet and symex_target_equationt
---to be saved during an execution, and for an execution to be resumed
from a saved pair. By saving the state at every branch point and
disabling path merging, symbolic execution only runs along one path but
populates a worklist of saved states that should be executed later. At
the top level, CBMC or JBMC loops while the worklist of saved states is
non-empty, creating a new bmct object to resume executing each saved
path.

This commit includes the following supporting changes:

- goto_symex_statet now owns a symbol table, separate from the one
  supporting the goto_program, which is used for dynamically created
  objects during symbolic execution. goto_symex was previously using a
  symbol table that was passed to it by reference for this purpose, but
  that symbol table is needed when resuming symbolic execution from a
  saved point and so ought properly to be part of the symbolic execution
  state.

- goto_symex_statet now has a pointer to a symex_target_equationt, which
  can be updated with an equation from a previously-saved symbolic
  execution run. While equations are also conceptually part of the state
  of symbolic execution, they are heavily used after symbolic execution
  has completed (and the symex state has been deallocated) and so the
  equation is not owned by the state. An explicit copy constructor has
  been added to goto_symex_statet that initializes the equation member,
  so that symbolic execution can proceed either with an empty equation
  or with an equation that was earlier saved.

- goto_symex_statet no longer has a pointer to a dirtyt, as this was
  hindering it from being copied.
[path explore 6/7] cpplint & clang-fmt agree on :
cpplint now complains if a derived-class declaration is formatted as

  class derived: base

rather than complaining if it is formatted as

  class derived : base

(with a space on both sides of the colon). The latter style is the one
enforced by clang-format, meaning that the two linters were inconsistent.
@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Feb 20, 2018

Just pushed: removed the formatting fix, and reinstated the output method with a new namespacet argument. Not sure what to do about the hard-coded guard identifier, and I'm not sure how I would have implemented the bmc customization differently; it does appear to need some kind of callback as it currently stands. If the use-case is going away then we can simply omit that callback parameter from bmct::do_language_agnostic_bmc() when that happens, it shouldn't be a difficult change, but why not keep it for now---I think the avoidance of code duplication that do_language_agnostic_bmc gives us more than makes up for any custom callbacks that we need to pass into that function.

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Feb 20, 2018

Also, going to sleep now, I have a flight tomorrow that I need to wake up for...should have time to make any additional changes tomorrow early morning if needed.

@tautschnig

This comment has been minimized.

Collaborator

tautschnig commented Feb 21, 2018

@karkhaz Thanks a lot for all those updates! I'm inclined to merge once CI passes, unless @martin-cs tells me otherwise?

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Feb 21, 2018

@martin-cs

@tautschnig Nah; I think we're good here.

@tautschnig

This comment has been minimized.

Collaborator

tautschnig commented Feb 21, 2018

CI has passed successfully, just need @martin-cs to give the green light.

@tautschnig tautschnig merged commit 9d1e625 into diffblue:develop Feb 21, 2018

3 checks passed

Cpp Linter No linting problems found.
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details

@karkhaz karkhaz deleted the karkhaz:kk-big-6-6 branch Feb 21, 2018

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Feb 21, 2018

Thanks so much everyone for the detailed reviews and suggestions! Looking forward to continuing work on this.

message_handlert &_message_handler,
prop_convt &_prop_conv)
prop_convt &_prop_conv,
goto_symext::branch_worklistt &_branch_worklist)

This comment has been minimized.

@peterschrammel

peterschrammel Feb 21, 2018

Member

For more backwards compatibility, would it have been possible to provide a constructor that initialises branch_worklist to a default value here?

This comment has been minimized.

@tautschnig

tautschnig Feb 21, 2018

Collaborator

I'm not sure default values and references would be compatible?

@smowton

This comment has been minimized.

Member

smowton commented Feb 27, 2018

@karkhaz just coming to rebase my own work on top of this; a couple of questions:

  1. At the moment this looks like it will interact oddly with any of the reporting options (show-vcc, program-only, symex-coverage-report) by outputting a report each time bmc is run. Is that intentional, or should the iterative symex-then-bmc run until "done", then only run end-of-day reporting once?

  2. How should this interact with the (default) all-properties mode or with --cover, both of which try to cover multiple goals? At present it is only merging a single safe / not-safe return value, which feels as if it's designed for use with --stop-on-fail, and with --cover it would presumably repeatedly print reports saying that (for a particular symex path) goals X, Y and Z were reached, then for another path goals A, B and C were... and so on. Should we declare --paths currently only for use with --stop-on-fail, or is there pending work to merge the goal map to produce a single coherent report later?

@karkhaz

This comment has been minimized.

Contributor

karkhaz commented Feb 28, 2018

@smowton: not sure if I have a good answer for these questions, I'm not actually that familiar with many of CBMC's command line options.

  1. I'm not sure why anybody would pass --paths together with reporting options like --program-only? If you want to do --program-only, you presumably want to symex the whole program at once without doing any checks, rather than doing one path at a time, right? Perhaps I'm not understanding the use-case here, but it seems to me that you would only want to pass --paths if you're actually interested in checking properties.

  2. I'm not sure what the "goal map" is. I wasn't using --paths with --stop-on-fail, I was indeed reading the diagnostic output from the BMC result one at a time while the loop was spinning. Admittedly this is not at all elegant, and it would be great to have some sort of unified report at the end that collects the BMC results of all paths seen so far. So again I'm not totally sure if I understand the question, but I would not be opposed to making --paths imply --stop-on-fail for now until I come up with a cleaner way of presenting the results from all paths. I suppose that I'd trap SIGINT or whatever and print a report before exiting.

@smowton

This comment has been minimized.

Member

smowton commented Feb 28, 2018

Re: #1, it would potentially be useful if you wanted to see the equation before each run, which is indeed what would currently happen, but in such a case we should somehow prepend each report with a header identifying a path.

Re #2, the three options 'cover', 'fault-localization' and the default all-properties mode all build a list of all the assertions they're trying to satisfy, then make repeated solver runs to try to satisfy different goals. I guess with --paths we should probably stop trying to target a particular goal once it has been found using a particular path? So the goal list would be maintained outside the twin iterations over goals and paths, and goals incrementally reported either hit or covered as we go, before finally reporting ones we couldn't reach? Or am I getting the wrong end of the stick, and it's actually interesting to check if I can violate goal A via both paths X and Y?

@martin-cs

This comment has been minimized.

Collaborator

martin-cs commented Mar 1, 2018

( Unsolicited opinions on what the options should do)

--paths --show-vcc prints each formula instead of running the solver
--paths --show-program prints each path condition instead of running the solver
--paths --all-properties tries to prove every property using the per-path approach
--paths --cover tries to cover each location using the per-path approach
--paths --fault-localization ask David Landsberg or @theyoucheng

karkhaz added a commit to karkhaz/cbmc that referenced this pull request Mar 30, 2018

Make CBMC more fun
Summary:
========

- Add octopus ASCII art logos to CBMC and JBMC frontends
- Change the names of some directories: "goto-instrument" is now
  "goto-inkstrument", "linking" is now "inking", "goto-cc" is now
  "goto-sea-sea", etc.

```
                                      _________
     _______.         _    _     .___/         \
    /        -_      / \  / \   /  _  _        |
    |    _   _ \     |  \/  |  /  / \/ \       |
    |   / \ / \|     \      /  |  |.||.|       /
    |   |.| |.||      \    /   |  \_/\_/      /
    \_  \_/ \_//       \  /     \  ___      _/
      \      _/         \/       \_\_/     /
      |   \_/                  ___\|      /
     ..____/_..               /.-_/o\____/..
    .. || o\o \~.o.         //~   //..|| \\ ..
   ..  |/ .||    \\..     //     || ..|| ||  ..
   .. //o .o\\    || .. //      // .. // ||   .
  ..  ||  .. \o   \\  //.     //  ..  || ||   ..
..   o//  ..  \\   ^\// ..  //    .  |/ .\|    ..
.    //  ..    ||   /\    .//    .. //  . \\   ..
.   |/  ..     \|  //\|   ||     ../|  .. ||   ..
    o  ..       o  l  o  //..     .|\ ..  \\  ..
      ..                |/  ..     |/ ..   \| ..
                        o    .     o        o

           ______________  ________
          /  __ | ___ |  \/  /  __ \
          | /  \| |_/ | .  . | /  \/
          | |   | ___ | |\/| | |
          | \__/| |_/ | |  | | \__/\
           \____\____/\_|  |_/\____/
```

Logo information:
=================

The octopus on the left is the "model-checking octopus," and the one on
the right is the "path exploration octopus". Their lovemaking symbolises
the retrofitting of path-exploration functionality to CBMC in diffblue#1641.

Rationale:
==========

We're hoping to boost CBMC's uptake and retention amongst customers by
adding a fun logo. The "mating octopi" logo was crafted during a
several-month long rebranding and outreach effort. We found that
customers form positive associations with tech brands that
[feature](https://en.wikipedia.org/wiki/Tux_(mascot))
[cute](https://en.wikipedia.org/wiki/Docker_(software))
[animals](https://github.com/logos)
as opposed to
[https://www.apple.com/](fruits) or
[https://www.microsoft.com/en-gb](rectangles).
Members of the verification community have responded warmly to this
proposed logo; below are a selection of quotes:

    This is a charming logo, I hope to see it when using CBMC to verify
    my latest sorting algorithm! Just to think, if only I had devised
    such a magnificent logo for my process calculus in the 80s, it would
    have soundly beaten Robin's bald-faced ripoff.
    -- Tony

    I like the idea, but don't eight-legged animals have a very large
    footprint? The logo is also off-centre, adding a proper frame would
    help here. Finally, the octopuses appear to be hopelessly tangled up
    and ought to be separated. Fortunately, I came up with a neat trick
    back in 2001 that could help you with all of these problems...
    -- Peter

    You're adding a _logo_ to a _verification tool_? Goto hell.
    -- Edsgar

karkhaz added a commit to karkhaz/cbmc that referenced this pull request Mar 30, 2018

Make CBMC more fun
Summary:
========

- Add octopus ASCII art logos to CBMC and JBMC frontends
- Change the names of some directories: "goto-instrument" is now
  "goto-inkstrument", "linking" is now "inking", "goto-cc" is now
  "goto-sea-sea", etc.

```
                                      _________
     _______.         _    _     .___/         \
    /        -_      / \  / \   /  _  _        |
    |    _   _ \     |  \/  |  /  / \/ \       |
    |   / \ / \|     \      /  |  |.||.|       /
    |   |.| |.||      \    /   |  \_/\_/      /
    \_  \_/ \_//       \  /     \  ___      _/
      \      _/         \/       \_\_/     /
      |   \_/                  ___\|      /
     ..____/_..               /.-_/o\____/..
    .. || o\o \~.o.         //~   //..|| \\ ..
   ..  |/ .||    \\..     //     || ..|| ||  ..
   .. //o .o\\    || .. //      // .. // ||   .
  ..  ||  .. \o   \\  //.     //  ..  || ||   ..
..   o//  ..  \\   ^\// ..  //    .  |/ .\|    ..
.    //  ..    ||   /\    .//    .. //  . \\   ..
.   |/  ..     \|  //\|   ||     ../|  .. ||   ..
    o  ..       o  l  o  //..     .|\ ..  \\  ..
      ..                |/  ..     |/ ..   \| ..
                        o    .     o        o

           ______________  ________
          /  __ | ___ |  \/  /  __ \
          | /  \| |_/ | .  . | /  \/
          | |   | ___ | |\/| | |
          | \__/| |_/ | |  | | \__/\
           \____\____/\_|  |_/\____/
```

Logo information:
=================

The octopus on the left is the "model-checking octopus," and the one on
the right is the "path exploration octopus". Their lovemaking symbolises
the retrofitting of path-exploration functionality to CBMC in diffblue#1641.

Rationale:
==========

We're hoping to boost CBMC's uptake and retention amongst customers by
adding a fun logo. The "mating octopi" logo was crafted during a
several-month long rebranding and outreach effort. We found that
customers form positive associations with tech brands that
[feature](https://en.wikipedia.org/wiki/Tux_(mascot))
[cute](https://en.wikipedia.org/wiki/Docker_(software))
[animals](https://github.com/logos)
as opposed to
[https://www.apple.com/](fruits) or
[https://www.microsoft.com/en-gb](rectangles).
Members of the verification community have responded warmly to this
proposed logo; below are a selection of quotes:

    This is a charming logo, I hope to see it when using CBMC to verify
    my latest sorting algorithm! Just to think, if only I had devised
    such a magnificent logo for my process calculus in the 80s, it would
    have soundly beaten Robin's bald-faced ripoff.
    -- Tony

    I like the idea, but don't eight-legged animals have a very large
    footprint? The logo is also off-centre, adding a proper frame would
    help here. Finally, the octopuses appear to be hopelessly tangled up
    and ought to be separated. Fortunately, I came up with a neat trick
    back in 2001 that could help you with all of these problems...
    -- Peter

    You're adding a _logo_ to a _verification tool_? Goto hell.
    -- Edsgar

karkhaz added a commit to karkhaz/cbmc that referenced this pull request Mar 30, 2018

Make CBMC more fun
Summary:
========

- Add octopus ASCII art logos to CBMC and JBMC frontends
- Change the names of some directories: "goto-instrument" is now
  "goto-inkstrument", "linking" is now "inking", "goto-cc" is now
  "goto-sea-sea", etc.

```
                                      _________
     _______.         _    _     .___/         \
    /        -_      / \  / \   /  _  _        |
    |    _   _ \     |  \/  |  /  / \/ \       |
    |   / \ / \|     \      /  |  |.||.|       /
    |   |.| |.||      \    /   |  \_/\_/      /
    \_  \_/ \_//       \  /     \  ___      _/
      \      _/         \/       \_\_/     /
      |   \_/                  ___\|      /
     ..____/_..               /.-_/o\____/..
    .. || o\o \~.o.         //~   //..|| \\ ..
   ..  |/ .||    \\..     //     || ..|| ||  ..
   .. //o .o\\    || .. //      // .. // ||   .
  ..  ||  .. \o   \\  //.     //  ..  || ||   ..
..   o//  ..  \\   ^\// ..  //    .  |/ .\|    ..
.    //  ..    ||   /\    .//    .. //  . \\   ..
.   |/  ..     \|  //\|   ||     ../|  .. ||   ..
    o  ..       o  l  o  //..     .|\ ..  \\  ..
      ..                |/  ..     |/ ..   \| ..
                        o    .     o        o

           ______________  ________
          /  __ | ___ |  \/  /  __ \
          | /  \| |_/ | .  . | /  \/
          | |   | ___ | |\/| | |
          | \__/| |_/ | |  | | \__/\
           \____\____/\_|  |_/\____/
```

Logo information:
=================

The octopus on the left is the "model-checking octopus," and the one on
the right is the "path exploration octopus". Their lovemaking symbolises
the retrofitting of path-exploration functionality to CBMC in diffblue#1641.

Rationale:
==========

We're hoping to boost CBMC's uptake and retention amongst customers by
adding a fun logo. The "mating octopi" logo was crafted during a
several-month long rebranding and outreach effort. We found that
customers form positive associations with tech brands that
[feature](https://en.wikipedia.org/wiki/Tux_(mascot))
[cute](https://en.wikipedia.org/wiki/Docker_(software))
[animals](https://github.com/logos)
as opposed to
[fruits](https://www.apple.com/) or
[rectangles](https://www.microsoft.com/en-gb).
Members of the verification community have responded warmly to this
proposed logo; below are a selection of quotes:

    This is a charming logo, I hope to see it when using CBMC to verify
    my latest sorting algorithm! Just to think, if only I had devised
    such a magnificent logo for my process calculus in the 80s, it would
    have soundly beaten Robin's bald-faced ripoff.
    -- Tony

    I like the idea, but don't eight-legged animals have a very large
    footprint? The logo is also off-centre, adding a proper frame would
    help here. Finally, the octopuses appear to be hopelessly tangled up
    and ought to be separated. Fortunately, I came up with a neat trick
    back in 2001 that could help you with all of these problems...
    -- Peter

    You're adding a _logo_ to a _verification tool_? Goto hell.
    -- Edsgar

karkhaz added a commit to karkhaz/cbmc that referenced this pull request Mar 30, 2018

Make CBMC more fun
Summary:
========

- Add octopus ASCII art logos to CBMC and JBMC frontends
- Change the names of some directories: "goto-instrument" is now
  "goto-inkstrument", "linking" is now "inking", "goto-cc" is now
  "goto-sea-sea", etc.

```
                                      _________
     _______.         _    _     .___/         \
    /        -_      / \  / \   /  _  _        |
    |    _   _ \     |  \/  |  /  / \/ \       |
    |   / \ / \|     \      /  |  |.||.|       /
    |   |.| |.||      \    /   |  \_/\_/      /
    \_  \_/ \_//       \  /     \  ___      _/
      \      _/         \/       \_\_/     /
      |   \_/                  ___\|      /
     ..____/_..               /.-_/o\____/..
    .. || o\o \~.o.         //~   //..|| \\ ..
   ..  |/ .||    \\..     //     || ..|| ||  ..
   .. //o .o\\    || .. //      // .. // ||   .
  ..  ||  .. \o   \\  //.     //  ..  || ||   ..
..   o//  ..  \\   ^\// ..  //    .  |/ .\|    ..
.    //  ..    ||   /\    .//    .. //  . \\   ..
.   |/  ..     \|  //\|   ||     ../|  .. ||   ..
    o  ..       o  l  o  //..     .|\ ..  \\  ..
      ..                |/  ..     |/ ..   \| ..
                        o    .     o        o

           ______________  ________
          /  __ | ___ |  \/  /  __ \
          | /  \| |_/ | .  . | /  \/
          | |   | ___ | |\/| | |
          | \__/| |_/ | |  | | \__/\
           \____\____/\_|  |_/\____/
```

Logo information:
=================

The octopus on the left is the "model-checking octopus," and the one on
the right is the "path exploration octopus". Their lovemaking symbolises
the retrofitting of path-exploration functionality to CBMC in diffblue#1641.

Rationale:
==========

We're hoping to boost CBMC's uptake and retention amongst customers by
adding a fun logo. The "mating octopi" logo was crafted during a
several-month long rebranding and outreach effort. We found that
customers form positive associations with tech brands that
[feature](https://en.wikipedia.org/wiki/Tux_(mascot))
[cute](https://en.wikipedia.org/wiki/Docker_(software))
[animals](https://github.com/logos)
as opposed to
[fruits](https://www.apple.com/) or
[rectangles](https://www.microsoft.com/en-gb).
Members of the verification community have responded warmly to this
proposed logo; below are a selection of quotes:

    This is a charming logo, I hope to see it when using CBMC to verify
    my latest sorting algorithm! Just to think, if only I had devised
    such a magnificent logo for my process calculus in the 80s, it would
    not have been usurped by Robin's bald-faced ripoff.
    -- Tony

    I like the idea, but don't eight-legged animals have a very large
    footprint? The logo is also off-centre, adding a proper frame would
    help here. Finally, the octopuses appear to be hopelessly tangled up
    and ought to be separated. Fortunately, I came up with a neat trick
    back in 2001 that could help you with all of these problems...
    -- Peter

    You're adding a _logo_ to a _verification tool_? Goto hell.
    -- Edsgar

@karkhaz karkhaz referenced this pull request Mar 31, 2018

Closed

Make CBMC more fun #1989

smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018

Squashed 'cbmc/' changes from f7602af..207b801
207b801 Merge branch 'develop' into merge_2018-03-26
301cd46 Merge pull request diffblue#1969 from smowton/smowton/cleanup/document_sccs_guarantee
9c04abd Document grapht::SCCs
18478e9 Merge pull request diffblue#1947 from romainbrenguier/dependency-graph/stop-adding-unecessary-constraints#TG-2608
be66b35 Merge pull request diffblue#1961 from danpoe/slice-global-inits-fix
60bfbd0 Reduce string-max-length on String.equals test
50cfe34 Clear constraints at each call to dec_solve
367ca13 Ensure all atomic strings in arguments have node
0bb2fad Define a for_each_atomic_string helper function
805f45f Correct add_constraints in string_dependencies
61b3910 Add length_constraint method to builtin functions
8684e6d Helper functions for length constraints on strings
8a98246 Adapt unit tests for the new interface
c3aed85 Define two helper functions for for_each_successor
a45c64f Add tests for the use of string dependencies
e3da98c Deactivating invariant
2655a9b Rewrite axioms for insert
be5f194 Add double quotes to output_dot
4b342f7 Only add constraints on test function dependencies
3c61cf2 Add a hash function for nodes
23f8cd4 Correct name of builtin function with no eval
c487c4b Generic get_reachable function
46d2507 Add move constructors to builtin_function_nodet
6609247 Add a maybe_testing_function to builtin functions
97ee2d6 Store builtin function pointer inside builtin node
41c0294 Add constraints from the string dependencies
8a7d194 add_constraints method in string_dependencies
b8df2b3 Initialize return_code for all builtin_functions
82f552c Add and add_constraint method to builtin functions
2e7057a Remove use of unknown_dependency
408adbe never return nullptr in to_string_builtin_function
c26b83d Constructor for builtin function with no eval
54a4d7d Add class for builtin function with no eval
8e0f974 Merge pull request diffblue#1970 from tautschnig/java-bytecode-fixes
edb8eeb Merge pull request diffblue#1905 from smowton/smowton/cleanup/broken-regression-tests
c188986 Merge pull request diffblue#1957 from smowton/smowton/cleanup/show-goto-functions-documentation
df1c7e3 Builds require javac as of f66288b
1782e8f Include missing map header
55656ff Include missing invariant header
0b17511 Merge pull request diffblue#1955 from svorenova/bugfix_tg2842
eb1ac7b Merge pull request diffblue#1964 from peterschrammel/documentation/online-docs-link
356a96c Merge pull request diffblue#1953 from smowton/smowton/cleanup/document-java-synthetic-methods
19e5bba Document synthetic methods generated by the Java frontend
706ffa7 Make test lambda1 compatible with symex-driven loading
0759129 Clarify slightly that show-symbol-table et al are restricted to loaded symbols
d7efdd1 Improve docs TOC structure
4043681 Add online documentation to README
076aa5a Improving warnings for unsupported signatures for generics cont.
c63c05b Add unit tests for mocked/unsupported generics cont.
067eeff Refactoring and adding utility functions in require_type
11e9a77 Ignore generic arguments for mocked and unsupported generic classes cont.
3a45ee9 Improving warnings for unsupported signatures for generics
f3cdd97 Add unit tests for mocked/unsupported generics
51a5845 Pull out common generic classes/interfaces for unit tests
fc83526 Ignore generic arguments for mocked and unsupported generic classes
3b00bdc Fix tests with missing EXIT or SIGNAL tests
7b56203 Merge pull request diffblue#1965 from smowton/smowton/fix/reachability-slicer-incompatible-with-symex-driven-loading
5903b62 Merge pull request diffblue#1952 from diffblue/more-builtins
e25a7ac Mark the new reachability-slicer incompatible with symex-driven loading
c5b4e19 Merge pull request diffblue#1963 from tautschnig/dimacs-output
4f3fb8b Merge pull request diffblue#1958 from romainbrenguier/bugfix/insert-offset
cd184f1 Merge pull request diffblue#1780 from Charliemowood/documentation/review-cbmc-docs
1ee0dd9 Merge pull request diffblue#1943 from forejtv/forejtv/reachability-slicer
9aa70a7 Add doc README.md files to each directory
1b7f57d Use doxygen layout file
c22e2e9 Add make doc to Makefile
c50f40d Remove old doxygen module directives from header files
c1f9e34 Move SATABS references to separate from user manual
42f9f36 Improve docs content layout and front page
0afcf90 dimacs: make sure printing a dimacs is fast
a403fdd Fix a bug in slice global inits where guard expressions were disregarded
7e00a30 Merge pull request diffblue#1759 from smowton/smowton/feature/symex-driven-program-loading
22e9b32 Merge pull request diffblue#1960 from smowton/smowton/admin/remove-reuk
f10c697 Remove reuk as a code-owner
c5aa507 Document builtin function constructors
953e2df Enable show-properties with symex-driven lazy loading
6c79494 Fix broken static_init_order test descriptions
ccb2cf3 Fix broken test descriptions
8aa38e7 Add tests for symex-driven lazy loading
7b5d73b JBMC: use symex-driven lazy loading
978ca5b Add callback after symex to bmct
8df9350 Java frontend: rename externally driven loading
98741f9 Java frontend: note availability of synthetic methods
890b8b1 Remove exceptions: add per-function entry point
3ef9ec8 Correct for_each_successor method
aebadee Correct offset in eval for insert
71983b3 Remove mention of size in eval_string
4cca831 Move string_builtin_function class to a new file
6120c17 Changes to the reachability slicer
f6219d4 Merge pull request diffblue#1940 from smowton/smowton/cleanup/remove-virtual-functions
34b2b02 Merge pull request diffblue#1939 from romainbrenguier/bugfix/builtin-string-insert-eval
9d9fafa Merge pull request diffblue#1941 from diffblue/rotate
84186ff Tests for CProverString.append with start/end args
882bbb1 Fix eval of concatenation builtin functions
ad9b86c Fix add_axioms_for_concat_substr
b43bbff Tests for CProverString.substring
4be7532 Test for CProverString.insert
5f96226 Fix string constraints for substring
9ff1e82 Fix eval of insert to match string constraints
f3694af added support for rotation operators
126e90a Remove virtual functions: fix no-fallback-function mode
442f315 Merge pull request diffblue#1951 from zemanlx/support/public-cprover-documentation
8c501cc Use abstract_goto_modelt instead of goto_functionst in bmc reporting phase
760d1ca Lazy goto model: implement abstract_goto_modelt
a4f5d77 goto_modelt: implement abstract_goto_modelt
311ca9c Add abstract_goto_modelt
2fe999c Add gcloud integration to Travis
a5c26a8 Add script for uploading documentation
566539e Add encrypted GCloud key for Travis
07bafd2 move CPROVER built-in functions into the factory
7f3ba30 Merge pull request diffblue#1814 from NlightNFotis/flush-json-stream
7161f17 Merge pull request diffblue#1879 from diffblue/smt2-frontend
ab68848 tests for smt2_solver
246472f an SMT2 solver using boolbv and satcheckt
a75ee3f Add missing langapi dependency to util
d83fa17 Merge pull request diffblue#1932 from romainbrenguier/stop-adding-counter-examples
b5f12ff Correct initial index set computation
c905c2c Remove "Adding counter-examples" message
7085f9c Correct find_index function for `if`-expressions
123be20 Fix goto-diff tests that got broken by streaming json
2ab3b9c Activate JSON streaming when printing goto-traces
54bae24 Refactor huge convert function into multiple ones
a68125c Base JSON UI message handler upon json_streamt
35ac459 Introduce class for streaming JSON to the output
a2a3140 Correct bounds in instantiate method
0910010 Fix string constraints
7586f76 Only add counter examples when index set exhausted
5268c44 a translator from SMT2 into expressions
6dde6b1 add support for let_exprt
37f69b2 added to_mathematical_function_type
7b670cd fix line number counting in SMT2 tokenizer
f3cb5bb Merge pull request diffblue#1938 from romainbrenguier/fix-cmake
213cb57 Fix cmake build
9e11b41 Replace java_int_type by tyep deduced from array
fc67510 Get rid of java_bytecode includes in string solver
461b3a5 Merge pull request diffblue#1922 from romainbrenguier/dependency-graph/get-model#TG-2607
1a874b3 Add name method to builtin functions
8d4a057 Decompose if_expr when adding dependencies
cb72bb7 Correct insert builtin function construction
d0a8868 Constructor and destructor of builtin functions
7bb5aff Make node point to builtin func they result from
a89ceb0 Tests for string solver get with new dependencies
0b3796e Declare a nodet class in string_dependencies
fb676d5 Add a cache for eval in string dependences
095d57b Add concat_char builtin function for strings
44693e8 Use eval of builtin function in get when available
56cb571 Activate dependency computation in string solver
69f31c1 Add eval function to string_dependenciest
357cb44 Add const node_at function in string dependencies
e308bad Rename class to string_dependenciest
06dc6b2 Add an evaluation method to builtin functions
f6a153e Check type before adding dependencies
0139424 Fix linting problem in string_constraint
5108a72 Fix string constraints printing
a2fab10 Linting corrections in string_refinement
05a3426 Merge pull request diffblue#1925 from hannes-steffenhagen-diffblue/testpl_use_env_testpl
8869dd8 Merge pull request diffblue#1920 from diffblue/bugfix/continue_bootstrapmethods_parsing_after_unsupported_entry
d404a55 Merge pull request diffblue#1931 from owen-jones-diffblue/owen-jones-diffblue/fix-release-build-compilation
c6102f7 Merge pull request diffblue#1918 from thk123/tests/tg-2485/lambda-lazy-loading
008de5d Use environment variable for jobs in test.pl
ea6f00f Fixing linter error
0b20a81 Added explanation to the test
1974010 Adjusted the if check to aid readability
42065ec Adjust the interface of the bootstrap methods map
dcd680f Correcting formating on java file
d8edf4f Adjusted test to pass
c0f054a Removing redundant method from test
f494674 Use function that actually contains the lambdas
8615500 Added to readme that the file is compiled using the eclipse compiler
a604b26 !fixup Removed impossible condition (9fc5bfd)
12f049e Added extra information to the warnings to differentaite the different cases
1db68a5 Moved the first condition to after the explanation of our assumptions
c1aa16c Renamed parameter variables
4bb98f0 Removed impossible condition
9749d5a Refactored error reporting method into a seperate function
6400294 Replace nested else ifs with a continue on error conditions
067ccbf Rename j to boostrap_method_index
d7a4e50 Add regression test compiled with ecj
e11163c Continue parsing after unsupported  BootstrapMethods entry
e1961d8 Adding unit tests for verifying the behaviour of lazy methods on lambdas
28c6477 Adding utility for getting symbols out of the symbol table
06ab440 Merge pull request diffblue#1930 from owen-jones-diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods-v1
6eab160 Speed up resolution of virtual callsites in lazy loading v1
c470bdf Replace assert(false) by UNREACHABLE
3af5509 Merge pull request diffblue#1923 from romainbrenguier/author-refinement-util
802b819 Merge pull request diffblue#1926 from tautschnig/fix-json
08ad919 Merge pull request diffblue#1913 from thk123/refactor/lazy-load-java-class-unit-tests
1abbaff Merge pull request diffblue#1927 from peterschrammel/json-xml-timestamps
3864e6c Updating comment with relevant JIRA ticket
72fc31e Add lazy version of load_java_class
5912a04 Refactored java_load_class to allow specifying different cmd line args
9374a1f Remove trailing whitespace from timestamp string
2ae5310 Add timestamp to JSON and XML messages
22b1628 goto-analyzer (un)reachable-functions: build valid json output
1e7f2bc Merge pull request diffblue#1907 from chrisr-diffblue/travis-test-speedups
ee2cf14 Correct author entry
2e7f785 Merge pull request diffblue#1895 from romainbrenguier/dependency-graph#TG-2582
86b3e87 Merge pull request diffblue#1919 from mgudemann/enhancement/fix_diffblue_author
123541f Correct string-max-input-length tests
411e654 Unit tests for dependency graph
c4ba7b4 Separate pointer/function substitutions in solver
a599003 Define function for array_pointer_association
a556d3d Pull out a get_function_name function
859d74c Class for string builtin functions and dependences
bd8ee51 Define function template for output_dot
0b58e31 Move utility functions to string_refinement_util
68ecd9e Make interface of equation_symbol_mappingt clearer
3e688e0 Create string_refinement_util for utility function
e72eacf Pull array_pool class out of constraint generator
42971da Remove default axiom in associate array to pointer
f5adb47 Pull symbol generation out of constraint generator
e2ca928 DiffBlue -> Diffblue
d430ddc Replace copyright notice with author entry
631acab Fix Diffblue author entries
e6e5134 Merge pull request diffblue#1911 from thk123/bugfix/TG-2434/static-constructor-calling-opaque-constructor
1a89e97 Remove lambda in favour of direct construction
bf86af4 Correcting review comments
44153b7 Adding unit tests verifying initalizsers are correctly labelled
80a439d Apply clang-format
6edaaa0 Remove the uncasted member_type so all references use the correct version
e8cbf90 Adding wrappers around whether a code_type is a constructor
e5ff31f Replace checks for <init> with a call to is_constructor
b25301e Remove redundant method and constructor setter
c84cf21 Made member_type_lazy return type match what the method returns
6505e8c Merge pull request diffblue#1875 from peterschrammel/remove-cout-solvers
26ef31c Use invariant instead of abort()
fe40b19 Use invariant instead of printing error message to cerr
066ba51 Merge pull request diffblue#1778 from peterschrammel/java-array-is-object
3548d99 Merge pull request diffblue#1917 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-do-not-create-stubs-when-resolving-virtual-calls
e7a6769 Merge pull request diffblue#1877 from svorenova/specialized_generics_tg1419
b87661e Do not create stubs when resolving virtual methods
0ac57ba Rename `needed_methods` to `callable_methods`
9fef129 Rename `needed_classes` to `instantiated_classes`
0d524ee Merge pull request diffblue#1893 from diffblue/expression-printer
48024c7 Replace function applications: don't break irep sharing
86bf547 replace_expr: avoid breaking irep sharing
69bef76 Typo in function header
c53cb29 Adding and updating unit tests
a1e9d00 Updating and extending utility functions
2964910 Fix a bug in function for extracting generic interface reference
5c00440 Remove the old way of specializing generics
624cc91 Use the map of parameter-type pairs to specialize generics
3111255 Introduce a map of parameter-type pairs
aaf9477 Use ranged for and const
7018ab4 Clean up commented out code
2529211 Clang-format
f7afe1f Replace assert by invariant
fc44d99 Use invariant instead if printing error message to cout
a15b75f Merge pull request diffblue#1910 from diffblue/builtin-factory
5de436b usage of format() instead of from_expr for debugging
b38ecc3 added format() for exprt and typet
2c8ae92 Makefile: use a variable for all those generated .inc files
17d9897 switch to C++ version of find_pattern
80ee0b1 pass type definitions to the C++ front-end
15ec42f use the builtins factory in the C frontend
1711345 added a factory for builtin function declarations
4a5b952 export all gcc bultin headers
691816b Improve job scheduling when running regression tests with -jN
87526e0 Enable a coarse-grained prallelism when running regression test jobs via Makefiles
76b93e8 Factoring out a private code from module 'remove_virtual_functions.cpp'.
15d7b71 Merge pull request diffblue#1908 from mgudemann/bugfix/fix_bootstrapmethods_empty_optional
0fd6482 Add regression test
5fa3a1a Refactor: improve variable naming
ae276ef Activate two instanceof regression tests
8995fce Java arrays are instanceof Object
881b127 Refactor: use class_typet instead of struct_typet for java class
fdba57c Merge pull request diffblue#1901 from romainbrenguier/fix/quantifier_exprt
782df52 Merge pull request diffblue#1909 from chrisr-diffblue/travis-make-options-cleanup
1edf0e8 Cleanup Travis Makefile build commands
1457849 Merge pull request diffblue#1894 from thomasspriggs/lambdas_compiliers_test
0ed21ca Treat empty optional case separately
3e298ef Formmatting fixes/updates for `java_bytecode_parse_lambda_method_handle` test update.
f1ee826 Update `java_bytecode_parse_lambda_method_handle` tests to run for each java compiler.
fe34bf6 AWS Codebuild: 4th attempt to speed up install
58b4196 AWS Codebuild: 3nd attempt to speed up install
71ab5cd AWS Codebuild: 2nd attempt to speed up install
b95383a Merge branch 'develop' of github.com:diffblue/cbmc into develop
e7bb127 AWS Codebuild: avoid one round of apt-get update
f20e8d7 Merge pull request diffblue#1891 from diffblue/deprecated-exprt-methods
20fc8d1 Merge pull request diffblue#1363 from diffblue/undeclared-return-conflict
92b4873 Merge pull request diffblue#1791 from thk123/feature/make-irep-ids-modifiable-by-all
2fef8fd Merge pull request diffblue#1772 from tautschnig/fix-1771
f6890b3 modernisation of sum_expr and mul_expr
4d87ba1 remove exprt::negate, sum, mul, subtract (deprecated since 2011)
0d0dca4 Merge pull request diffblue#1839 from thomasspriggs/tidy_up1
1b24851 Merge pull request diffblue#1903 from chrisr-diffblue/travis-speedups
b19b4a2 codebuild: enable the tests
44aa443 AWS codebuild: enable ccache
8549ecb AWS codebuild: enable cache
a7cc2a0 Merge pull request diffblue#1885 from tautschnig/use-std-expr
6ef804c Merge pull request diffblue#1888 from tautschnig/linker-script-fixes
d04312f Use std_{code,expr,type} constructors
00ec070 Slightly increase the number of parallel build jobs
f0fc345 Increase ccache size for debug builds
423cd49 Ensure all compile jobs declare their compiler type
7b6f849 Avoid double invoking ccache
a75c4f0 attempt 6 to use AWS Codebuild
d3ebda0 attempt 5 to use AWS Codebuild
a185ae0 fourth attempt to use AWS Codebuild
2948a43 third attempt to use AWS Codebuild
097de57 second attempt to use AWS Codebuild
4331120 first attempt to use AWS Codebuild
5c18ccc Type conflicts on the return value of implicitly declared functions are errors
d074537 test for signature conflict with undeclared function
37a11f9 Merge pull request diffblue#1808 from LAJW/lajw/floating-point-to-java-string
b3f2320 Add unit test for floating_point_to_java_string
7ac4fda Refactor and expose floating point to java conversion in expr2java.h
1a88479 Merge pull request diffblue#1896 from NathanJPhillips/bugfix/erroneous-reference
f5330c9 Correct can_cast_expr for quantifier_exprt
00cc4b1 Merge pull request diffblue#1897 from diffblue/quantifier_exprt
8897709 Merge pull request diffblue#1800 from tautschnig/fix-process_array_expr
fd513a6 added a base class for forall_exprt and exists_exprt
c3ee2a1 Merge pull request diffblue#1010 from danpoe/no-body-inlining
8d8c2e0 Fix bug causing crash on Windows
4dd0f29 Merge pull request diffblue#1892 from diffblue/remove-OPERANDS_IN_GETSUB
b519b41 remove OPERANDS_IN_GETSUB define, which is now simply the only option
80060ea goto-diff is missing dependencies on goto-instrument and goto-symex
7a71c80 Merge pull request diffblue#1884 from mgudemann/enhancement/update_copyright_2018
bb47a84 Merge pull request diffblue#1883 from tautschnig/implement-popcount
90beed4 Merge pull request diffblue#1845 from tautschnig/fix-1837
5cdfa94 Merge pull request diffblue#1804 from mgudemann/feature/parse_bootstrapmethods_attribute
ea7975f Remove unused goto_functions parameters
76d4014 Adding tests for inner classes that capture outer class variables
9b8a73e Adding tests for lambdas as member variables
db1f3b5 Adding tests for local lambdas
ba8b958 Adding tests for static lambdas
ebdcfb1 Adding utiltiy functions required for unit tests
f79e895 Fix format and account for reviewer's comments
51bb367 Merge pull request diffblue#1886 from smowton/smowton/fix/static-inititialisers-doxygen
e0ccb12 Refactor BootstrapMethods attribute reading into function
463ffe1 Refactor parse_method_handle to just deal with the lambda special case
ca5dae4 Fixup Use the strcutured classes to simplify and make more explict the code
b56e42e Fix missing swap for classt
e3ff312 Use the strcutured classes to simplify and make more explict the code
3ac7d09 Introduce classes representing relevant constant pool entries
0e40081 Adding validation on the type of descriptor found
6d44836 Use optionalt<lambda_method_handlet> as return value
f765a0d Rename, some more comments
01dcda5 status()->debug()
603aced Add regression test for lambda functions
e79a655 Initial support for reading BootstrapMethods attribute
b371e28 Linker-scripts: support linker symbols with struct type
e999552 Linker-script processing: mind temporaries
1612f74 Do not modify object_files list while processing it
60487f7 Distribute ls_parse.py with goto-cc
631ea60 Make linker-script processing failures non-fatal
1f753d8 fixup! goto-gcc removes CPROVER macros for native gcc
716103e Implement popcount in SAT back-end
ddde9dc Introduce popcount_exprt
3e793f5 Merge pull request diffblue#1887 from diffblue/string-constant-to-util
683d821 move ansi-c/string_constant.h to util/
3188f10 Merge pull request diffblue#1795 from thk123/bugfix/TG-1358/local-variables
0cfd14b Add missing Doxygen parameter
81d2ea4 Update copyright in help output for {CJ}BM and goto-analyzer
06483f3 Merge pull request diffblue#1881 from tautschnig/fix-runtime-report
3c17453 Merge pull request diffblue#1882 from tautschnig/address_bits
ce600d9 Update copyright in .cpp/.h files
004626c Adding invariant to check instruction is normal wide
60af165 Adding handmade class file exhibiting the same problem
5bdaa64 Adding test demonstrating the too many variables problem
e976d6f Correctly handle wide iload commands
f59092c address_bits need not return an arbitrary-sized integer
3bcb3a5 Fix decision procedure runtime computation
4d33a91 Add missing brackets to multiline if statements.
357bbe4 Fix formatting in assert replacements.
f8c2b09 Replace asserts with new equivalents.
ecbbc73 Remove unused `forall_symbols` macro.
f1670b2 Refactor `forall_symbols` usage into c++11 loop.
a8319a3 Remove unused macro `forall_symbol_module_map`
96bf623 Merge pull request diffblue#1856 from thk123/refactor/fieldref_expr
3819295 Merge pull request diffblue#1797 from thk123/bugfix/TG-1358/long-jumps
7e5922a remove functions without a body
bc2c0cd Inliner fixes
0003d8a Merge pull request diffblue#1864 from owen-jones-diffblue/owen-jones-diffblue/consistent-casts-in-remove-virtual-function
d2e10af Remove the "fieldref" id
2ba794d Introduce fieldref_exprt to represent a field reference
c9f3ea4 Test casts in remove_virtual_function()
9df769a Byte offset to array index translation must use array type
f4fb099 Fix process_array_expr to take into account pointer offset
379705f Process array_equal the same way as array_{replace,copy}
c62b957 Merge pull request diffblue#1551 from tautschnig/perf-test-improvements
1dfb5cd Merge pull request diffblue#1871 from mgudemann/bugfix/superclass_references_for_implicit_generic
71b32f4 Merge pull request diffblue#1777 from romainbrenguier/refactor/java-bytecode-instrument-TG-2331
25eb1a3 Add unit test for implicitly generic super class
590fc2d Make USE_DSTRING conditional and disable it in Ubuntu/Clang/DEBUG Travis job
52290b0 Include string when not using dstringt as irep_idt representation
25ffad4 Do not use dstringt-specific APIs with irep_idt
534f4d2 Include list in expr.h
d87d6e4 Include unordered_map where using a std::unordered_map
a72f52a [TG-2585] Support implicitly generic superclasses
83d9272 Merge pull request diffblue#1870 from diffblue/chrono-precision
2dc9fcd do not round reported durations to seconds
28c3c9f Merge pull request diffblue#853 from owen-jones-diffblue/feature/pointer-function-parameters
ab1b267 Merge pull request diffblue#1832 from diffblue/smt2-backend
11f3699 Merge pull request diffblue#1853 from danpoe/is-threaded-fixes
3e7e840 Merge pull request diffblue#1829 from romainbrenguier/refactor/substitute_array_access#TG-2138
830d519 Merge pull request diffblue#1830 from romainbrenguier/feature/cover-basic-block-java#TG-1404
3a112af Merge pull request diffblue#1846 from hannes-steffenhagen-diffblue/develop-fix_appveyor
9d1e625 Merge pull request diffblue#1641 from karkhaz/kk-big-6-6
7e176f7 Make argument of instrument_code be of type codet
b0df38d Make return type of expr_instrumentation an optional
9c838a1 Documentation improvements in bytecode instrument
ea3ba42 Remove unused includes
f6488d7 Using constant string vector instead of irep_idt
d67fa60 [path explore 7/7] Path exploration documentation
53df567 [path explore 6/7] cpplint & clang-fmt agree on :
e8eec2c [path explore 5/7] Support path-based exploratio2
c88a3ab [path explore 4/7] Factor out common BMC code
d7a70e1 [path explore 3/7] Logical ops for resultt
c53d630 [path explore 2/7] Ignore jbmc binary
6d657a0 Merge pull request diffblue#1779 from diffblue/smt2-integers
63beb71 Update coverage goals in goto-diff test
654418a Unit tests for sparse_arrayt
d65bf9f Class for sparse arrays representations
773721b Refactoring of substitute array access
dc5ffc9 Documentation improvements in string solver
5f54049 Add unit tests for java block instrumentation
105c7e3 Adapt coverage test for new instrumentation
c1045aa Use [] instead of `at` on vector
6811238 cover_block implementation using bytecode location
acf9fe4 Refer to interface rather than cover_basic_blockst
3cd2f0b Put interface to cover_blocks in virtual class
8e7f129 Correct types from unsigned to std::size_t
0fc9c5e Merge pull request diffblue#1866 from romainbrenguier/feature/code-location-in-preprocessing
f270e92 Merge pull request diffblue#1835 from diffblue/remove-goto-templates
d82c586 missing header for std::time_t
fdc5b1e Add source location to code added by preprocessing
0208218 Merge pull request diffblue#1861 from peterschrammel/goto-diff-properties
8192246 Make remove_virtual_function() consistent
9c12abb make linter happy
ba8bbe2 expand goto_programt and goto_functionst templates
b36a90a Merge pull request diffblue#1851 from tautschnig/remove-expr-listt
897e29e Fix CMakeLists to correctly pass test exclusion flags
07e0d58 Merge pull request diffblue#1841 from NathanJPhillips/cleanup/remove-unused-params
4d3ab7a Merge pull request diffblue#1838 from mgudemann/bugfix/catch_unsupported_generics_exception
a8bdb09 Merge pull request diffblue#1817 from allredj/string-primitives-for-exceptions
1ebec11 get values for nondet symbols
a827c77 fix: add missing integer casts and operations
bf9b2c1 Merge pull request diffblue#1862 from diffblue/cbmc-test-results-quantifiers
2b92cd3 Update regression tests to use string primitives
dd5a674 Add jbmc string primitives to CProverString
8f6431c Introduce more string primitives in JBMC
a39fff8 remove iteration count from test result
daab304 remove spurious spaces
482ec4a edit a space
df9aab5 Test for goto-diff show properties
a4d3dc3 Show properties in goto-diff
d3eb1f3 Use CPROVER exit codes
a0e5063 Enable goto check and cover options in goto-diff
a0c45f4 Factor out show properties command line def and docs
937b5f9 Expose conversion of properties of a goto-program into a JSON array
f4a8b0c Replace cout in show_properties
c480d28 Merge pull request diffblue#1842 from NathanJPhillips/feature/depth_iterator_get_mutable
416bbe0 Allow non-const depth_iteratort to be created from a const root
ac37f0b Removed unused parameter/private field
7070296 Add unit test to Makefile
f42eeb2 Add unit test for generic superclass with unsupported signature
e760d6b Catch unsupported generics exception in superclass ref extraction
b0eb45e Merge pull request diffblue#1840 from NathanJPhillips/bugfix/test-name
6f622d1 Fixes for is_threadedt, --is-threaded
13b77d8 Include list where using a std::list and drop forall_expr_list macro
2ccc41b Remove destination directory before trying to move to it in AppVeyor
a094990 Fixed test name
a0bfd42 smt2irep now uses smt2_tokenizert
3587184 added an SMT-LIB2 tokenizer
dea2592 treat real and integer as 'numeric' in C front-end
57ecf15 + is multi-ary in SMT-LIB2
12ae728 fixes for integers in SMT2
698ccdd use a ranged for
bc0ebd3 Bounds checks in fgets, read
dda54c7 Adding test includes a jump to address 2^16
3f202fa Add support for reading nop operations
7a205f0 Correct handling of two byte offsets
cb2c7a8 Adding the irep_ids file to frequently modified low risk files
03095d4 Use svcomp18 as base
f659577 perf-test: build configuration using glucose
98b9ae6 SV-COMP now requires zip files
1c0cf32 Support custom CodeBuild templates
6eeb672 Permit selecting a regular-expression-defined set of tasks
d3b29d2 Update cprover-sv-comp, benchexec to latest version
3269da7 Utility to generate HTML reports from perf-test experiments
cf4eeb2 Move code into code block instead of copying it
7f4a79e Tidy up C symbol factory code
REVERT: f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327

git-subtree-dir: cbmc
git-subtree-split: 207b801
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment