Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added /verifySnapshots:3, which prints recycled errors messages with the ↵ | Rustan Leino | 2015-08-28 |
| | | | | source locations of the new code. | ||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-06-08 |
| | |||
* | Fix minor issue. | Valentin Wüstholz | 2015-06-05 |
| | |||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-06-05 |
| | |||
* | Fix for SI: initialize extraRecBound | Akash Lal | 2015-06-05 |
| | |||
* | Merge branch 'master' of https://github.com/boogie-org/boogie | akashlal | 2015-06-01 |
|\ | |||
* | | Simplified StratifiedVC interface | akashlal | 2015-06-01 |
| | | |||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | qadeer | 2015-05-31 |
| |\ | |/ |/| | |||
| * | added assume about gate after calls and parallel calls | qadeer | 2015-05-31 |
| | | |||
* | | Improve heuristics for diagnosing timeouts. | Valentin Wüstholz | 2015-05-31 |
|/ | |||
* | Allow for extra instrumentation on program before vc gen | Akash Lal | 2015-05-25 |
| | |||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-22 |
| | |||
* | Minor changes | Valentin Wüstholz | 2015-05-20 |
| | |||
* | Minor refactoring | Valentin Wüstholz | 2015-05-20 |
| | |||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-20 |
| | |||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-19 |
| | |||
* | Make it not return cached verification results for timed-out implementations ↵ | Valentin Wüstholz | 2015-05-18 |
| | | | | when timeout diagnostics are enabled. | ||
* | Add some experimental support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-18 |
| | |||
* | Minor refactoring | Valentin Wüstholz | 2015-05-17 |
| | |||
* | Make caching of verification results more fine-grained for changes that ↵ | Valentin Wüstholz | 2015-05-17 |
| | | | | affect preconditions. | ||
* | Fix for printFixedPoint when dealing with functions | Akash Lal | 2015-05-13 |
| | |||
* | Fix for secureVCGen | Akash Lal | 2015-05-07 |
| | |||
* | Make it preserve the fact that the value of an assumption variable never ↵ | Valentin Wüstholz | 2015-05-06 |
| | | | | becomes logically weaker after a havoc. | ||
* | Fix for AbsHoudini | akashlal | 2015-05-01 |
| | |||
* | AbsHoudini: made disjunct bound a parameter | akashlal | 2015-05-01 |
| | |||
* | Add support for 'verified_under' attributes on procedure calls and invariants. | Valentin Wüstholz | 2015-04-29 |
| | |||
* | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a | Dan Liew | 2015-04-26 |
| | | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error | ||
* | Minor fixes for AbsHoudini | Akash Lal | 2015-04-23 |
| | |||
* | Better error message | akashlal | 2015-04-21 |
| | |||
* | patched ghost checking | qadeer | 2015-04-18 |
| | |||
* | changed aux attribute to ghost | qadeer | 2015-04-18 |
| | |||
* | fixed the treatment of extern | qadeer | 2015-04-17 |
| | |||
* | patched the type checker to deal with modularity | qadeer | 2015-04-16 |
| | |||
* | Patch by Jeroen Ketema. | Dan Liew | 2015-04-05 |
| | | | | | | Drop the “basic” block predication algorithm. Block predication is only used by GPUVerify, and then only in the “smart” version as the basic algorithm does not perform very well. As a consequence this code is essentially dead. | ||
* | VC gen for security properties | akashlal | 2015-04-05 |
| | |||
* | Patch by Jeroen Ketema | Dan Liew | 2015-03-27 |
| | | | | Expose information about the predicate assigned to the immediate dominator of a CFG node. | ||
* | Compute MustReach information lazily, on-demand | akashlal | 2015-03-16 |
| | |||
* | Added MustReach information to VC gen | akashlal | 2015-03-11 |
| | |||
* | If using -proverLog: make sure we flush after writing every line | Dan Liew | 2015-03-10 |
| | | | | | | | | | otherwise if either of the following happens * if the solver hangs and we do CTRL+C * if Boogie crashes then some lines will be missing from the log. | ||
* | Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188) | Dan Liew | 2015-03-10 |
| | | | | | | where setting produce-unsat-cores to true has no effect unless the option is set last. This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2 | ||
* | Fix bug in BigDec.FloorCeiling() which gave the wrong answers for | Dan Liew | 2015-03-10 |
| | | | | | negative numbers. I have decided that this method will floor towards negative infinity rather than zero to match SMT-LIBv2's to_int function. | ||
* | fixed crash reported by Dan. | qadeer | 2015-03-02 |
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | ||
* | Parse Bv values | akashlal | 2015-03-02 |
| | |||
* | Fix using "mkbv" as a variable name in a boogie program. This was | Dan Liew | 2015-02-27 |
| | | | | | taken from ``bv_decl_plugin::get_op_names(...)`` in ``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code. | ||
* | Fix using reserved Z3 keywords for real/int arithmetic operators. These are ↵ | Dan Liew | 2015-02-27 |
| | | | | | | | taken from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp`` in the Z3 4.3.2 source code. | ||
* | Fix using reserved Z3 keywords for float operators. These are taken | Dan Liew | 2015-02-27 |
| | | | | | from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp`` from the Z3 4.3.2 source code. | ||
* | Merge. | Dan Liew | 2015-02-18 |
|\ | |||
* | | Fix bug where some reserved Z3 keywords were not sanitized | Dan Liew | 2015-02-18 |
| | | | | | | | | when generating the VC. | ||
| * | Eliminated calls to deprecated method. | wuestholz | 2015-02-18 |
| | | |||
| * | Added a setter for CommandLineOptions.ProverOptions and fixed several contracts. | wuestholz | 2015-02-18 |
|/ |