Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Fix for printFixedPoint when dealing with functions | 2015-05-13 | ||
| | | ||||
| * | SecureVC: example | 2015-05-07 | ||
| | | ||||
| * | Fix for secureVCGen | 2015-05-07 | ||
| | | ||||
| * | Make it preserve the fact that the value of an assumption variable never ↵ | 2015-05-06 | ||
| | | | | | | | | becomes logically weaker after a havoc. | |||
| * | Fix for AbsHoudini | 2015-05-01 | ||
| | | ||||
| * | AbsHoudini: made disjunct bound a parameter | 2015-05-01 | ||
| | | ||||
| * | Add support for 'verified_under' attributes on procedure calls and invariants. | 2015-04-29 | ||
| | | ||||
| * | Try to add build status icon for the Windows build. | 2015-04-28 | ||
| | | ||||
| * | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a | 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 | 2015-04-23 | ||
|/ | ||||
* | renamed og to civl | 2015-04-22 | ||
| | ||||
* | Better error message | 2015-04-21 | ||
| | ||||
* | added more examples | 2015-04-18 | ||
| | ||||
* | patched ghost checking | 2015-04-18 | ||
| | ||||
* | changed aux attribute to ghost | 2015-04-18 | ||
| | ||||
* | fixed the treatment of extern | 2015-04-17 | ||
| | ||||
* | first check in | 2015-04-16 | ||
| | ||||
* | patched the type checker to deal with modularity | 2015-04-16 | ||
| | ||||
* | Note that CVC4 support is experimental. | 2015-04-05 | ||
| | ||||
* | Fix typo in README.md spotted by Jeroen Ketema. | 2015-04-05 | ||
| | ||||
* | Patch by Jeroen Ketema. | 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. | |||
* | Disable test is ``Test/Secure``. They aren't set up properly. | 2015-04-05 | ||
| | ||||
* | Some test cases for SecureVCGen (disabled for lit currently) | 2015-04-05 | ||
| | ||||
* | VC gen for security properties | 2015-04-05 | ||
| | ||||
* | Fix ``Test/test15/CaptureState.bpl`` test under Linux. | 2015-04-03 | ||
| | ||||
* | Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux. | 2015-04-03 | ||
| | ||||
* | Add TravisCI build status icon to README.md | 2015-04-03 | ||
| | ||||
* | Clean up .gitignore file | 2015-04-03 | ||
| | ||||
* | Remove some old mercurial files. | 2015-04-03 | ||
| | ||||
* | Add .travis.yml file for TravisCI builds. | 2015-04-03 | ||
| | ||||
* | Add initial README.md | 2015-04-03 | ||
| | ||||
* | Add LICENSE file. | 2015-04-01 | ||
| | ||||
* | updated the example to include atomic specifications (sent by Suha) | 2015-03-29 | ||
| | ||||
* | Patch by Jeroen Ketema | 2015-03-27 | ||
| | | | | Expose information about the predicate assigned to the immediate dominator of a CFG node. | |||
* | Compute MustReach information lazily, on-demand | 2015-03-16 | ||
| | ||||
* | Added MustReach information to VC gen | 2015-03-11 | ||
| | ||||
* | If using -proverLog: make sure we flush after writing every line | 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) | 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 | 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. | 2015-03-02 | ||
| | | | | DoModSetAnalysis needs to run before the linear and mover type checking. | |||
* | Parse Bv values | 2015-03-02 | ||
| | ||||
* | Fix using "mkbv" as a variable name in a boogie program. This was | 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 ↵ | 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 | 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. | |||
* | fix from Serdar and Suha | 2015-02-24 | ||
| | ||||
* | Merge. | 2015-02-18 | ||
|\ | ||||
* | | Fix bug where some reserved Z3 keywords were not sanitized | 2015-02-18 | ||
| | | | | | | | | when generating the VC. | |||
| * | Eliminated calls to deprecated method. | 2015-02-18 | ||
| | | ||||
| * | Added a setter for CommandLineOptions.ProverOptions and fixed several contracts. | 2015-02-18 | ||
|/ | ||||
* | Protect Bitvector field of BvExtractExpr when it is immutable. | 2015-02-12 | ||
| |