Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | Add some experimental support for diagnosing timeouts. | 2015-05-18 | ||
| | | | ||||
| | * | Minor refactoring | 2015-05-17 | ||
| | | | ||||
| | * | Make caching of verification results more fine-grained for changes that ↵ | 2015-05-17 | ||
| | | | | | | | | | | | | affect preconditions. | |||
| | * | Fix for printFixedPoint when dealing with functions | 2015-05-13 | ||
| | | | ||||
* | | | Made significant changes to internal representation of BigFloat. Remains a ↵ | 2015-05-07 | ||
| | | | | | | | | | | | | work in progress | |||
| | * | 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. | |||
* | | | added decimal reading functionality to the float type | 2015-05-05 | ||
| | | | ||||
* | | | added general floating point mantissa and exponent management | 2015-05-04 | ||
| | | | ||||
* | | | integrated the named float type to act as a real in boogie | 2015-05-04 | ||
| | | | ||||
| | * | 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 | ||
| | | | ||||
* | | | modified the third float_test slightly | 2015-04-27 | ||
| | | | ||||
* | | | Began adding the float type to VC expression | 2015-04-27 | ||
| | | | ||||
* | | | Added float operations to AbsyExpr. Note that float operations work as real ↵ | 2015-04-27 | ||
| | | | | | | | | | | | | operations at the moment | |||
* | | | Finished up Parser modifications | 2015-04-27 | ||
| | | | ||||
* | | | removed the last console writes (used for testing) | 2015-04-26 | ||
| | | | ||||
* | | | Successfully parsed the float type | 2015-04-26 | ||
| | | | ||||
* | | | added float type to the set array in Parser | 2015-04-26 | ||
| | | | ||||
* | | | removed comments from Scanner.cs, changed the value of the float token kind ↵ | 2015-04-26 | ||
| | | | | | | | | | | | | to 97/98 (from 135/136) | |||
* | | | added float type to Arithmetic Expression and added a new float test | 2015-04-26 | ||
| | | | ||||
| | * | 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 | ||
| | | ||||
* | | renamed fp32 to BigFloat | 2015-04-20 | ||
| | | ||||
* | | added minor commenting to Parser.cs | 2015-04-20 | ||
| | | ||||
* | | added a collection of console writes for debugging. These should be removed ↵ | 2015-04-20 | ||
| | | | | | | | | in a future commit | |||
* | | added a file for float type testing | 2015-04-20 | ||
| | | ||||
* | | Added float type to the Parser and Scanner | 2015-04-20 | ||
| | | ||||
* | | added float tipe to AbsyExpr and IntervalDomain. The methods added may ↵ | 2015-04-20 | ||
| | | | | | | | | require later modification | |||
| * | added more examples | 2015-04-18 | ||
| | | ||||
| * | patched ghost checking | 2015-04-18 | ||
| | | ||||
| * | changed aux attribute to ghost | 2015-04-18 | ||
| | | ||||
* | | added float type definition to AbsyType and parser (parser definition may be ↵ | 2015-04-17 | ||
| | | | | | | | | unfinished) | |||
| * | fixed the treatment of extern | 2015-04-17 | ||
| | | ||||
* | | adding references to the floating point type wherever references to the real ↵ | 2015-04-17 | ||
| | | | | | | | | type exist. This remains a work in progress | |||
* | | Added the fp32 class, copied from the previously existing BigDec class. No ↵ | 2015-04-17 | ||
| | | | | | | | | significant changes from BigDec have been made | |||
| * | 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 | ||
| |