summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
| * Minor refactoringGravatar Valentin Wüstholz2015-05-17
| * Make caching of verification results more fine-grained for changes that affec...Gravatar Valentin Wüstholz2015-05-17
| * Fix for printFixedPoint when dealing with functionsGravatar Akash Lal2015-05-13
* | Made significant changes to internal representation of BigFloat. Remains a w...Gravatar Dietrich2015-05-07
| * Fix for secureVCGenGravatar Akash Lal2015-05-07
| * Make it preserve the fact that the value of an assumption variable never beco...Gravatar Valentin Wüstholz2015-05-06
* | added decimal reading functionality to the float typeGravatar Dietrich2015-05-05
* | added general floating point mantissa and exponent managementGravatar Dietrich2015-05-04
* | integrated the named float type to act as a real in boogieGravatar Dietrich2015-05-04
| * Fix for AbsHoudiniGravatar akashlal2015-05-01
| * AbsHoudini: made disjunct bound a parameterGravatar akashlal2015-05-01
| * Add support for 'verified_under' attributes on procedure calls and invariants.Gravatar Valentin Wüstholz2015-04-29
* | Began adding the float type to VC expressionGravatar Dietrich2015-04-27
* | Added float operations to AbsyExpr. Note that float operations work as real ...Gravatar Dietrich2015-04-27
* | Finished up Parser modificationsGravatar Dietrich2015-04-27
* | removed the last console writes (used for testing)Gravatar Dietrich2015-04-26
* | Successfully parsed the float typeGravatar Dietrich2015-04-26
* | added float type to the set array in ParserGravatar Dietrich2015-04-26
* | removed comments from Scanner.cs, changed the value of the float token kind t...Gravatar Dietrich2015-04-26
* | added float type to Arithmetic Expression and added a new float testGravatar Dietrich2015-04-26
| * Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has aGravatar Dan Liew2015-04-26
| * Minor fixes for AbsHoudiniGravatar Akash Lal2015-04-23
| * Better error messageGravatar akashlal2015-04-21
* | renamed fp32 to BigFloatGravatar Dietrich2015-04-20
* | added minor commenting to Parser.csGravatar Dietrich2015-04-20
* | added a collection of console writes for debugging. These should be removed ...Gravatar Dietrich2015-04-20
* | Added float type to the Parser and ScannerGravatar Dietrich2015-04-20
* | added float tipe to AbsyExpr and IntervalDomain. The methods added may requi...Gravatar Dietrich2015-04-20
| * patched ghost checkingGravatar qadeer2015-04-18
| * changed aux attribute to ghostGravatar qadeer2015-04-18
* | added float type definition to AbsyType and parser (parser definition may be ...Gravatar Dietrich2015-04-17
| * fixed the treatment of externGravatar qadeer2015-04-17
* | adding references to the floating point type wherever references to the real ...Gravatar Dietrich2015-04-17
* | Added the fp32 class, copied from the previously existing BigDec class. No s...Gravatar Dietrich2015-04-17
| * patched the type checker to deal with modularityGravatar qadeer2015-04-16
|/
* Patch by Jeroen Ketema.Gravatar Dan Liew2015-04-05
* VC gen for security propertiesGravatar akashlal2015-04-05
* Patch by Jeroen KetemaGravatar Dan Liew2015-03-27
* Compute MustReach information lazily, on-demandGravatar akashlal2015-03-16
* Added MustReach information to VC genGravatar akashlal2015-03-11
* If using -proverLog: make sure we flush after writing every lineGravatar Dan Liew2015-03-10
* Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188)Gravatar Dan Liew2015-03-10
* Fix bug in BigDec.FloorCeiling() which gave the wrong answers forGravatar Dan Liew2015-03-10
* fixed crash reported by Dan.Gravatar qadeer2015-03-02
* Parse Bv valuesGravatar akashlal2015-03-02
* Fix using "mkbv" as a variable name in a boogie program. This wasGravatar Dan Liew2015-02-27
* Fix using reserved Z3 keywords for real/int arithmetic operators. These are t...Gravatar Dan Liew2015-02-27
* Fix using reserved Z3 keywords for float operators. These are takenGravatar Dan Liew2015-02-27
* Merge.Gravatar Dan Liew2015-02-18
|\
* | Fix bug where some reserved Z3 keywords were not sanitizedGravatar Dan Liew2015-02-18