index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
Commit message (
Expand
)
Author
Age
...
|
*
Minor refactoring
Valentin Wüstholz
2015-05-17
|
*
Make caching of verification results more fine-grained for changes that affec...
Valentin Wüstholz
2015-05-17
|
*
Fix for printFixedPoint when dealing with functions
Akash Lal
2015-05-13
*
|
Made significant changes to internal representation of BigFloat. Remains a w...
Dietrich
2015-05-07
|
*
Fix for secureVCGen
Akash Lal
2015-05-07
|
*
Make it preserve the fact that the value of an assumption variable never beco...
Valentin Wüstholz
2015-05-06
*
|
added decimal reading functionality to the float type
Dietrich
2015-05-05
*
|
added general floating point mantissa and exponent management
Dietrich
2015-05-04
*
|
integrated the named float type to act as a real in boogie
Dietrich
2015-05-04
|
*
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
*
|
Began adding the float type to VC expression
Dietrich
2015-04-27
*
|
Added float operations to AbsyExpr. Note that float operations work as real ...
Dietrich
2015-04-27
*
|
Finished up Parser modifications
Dietrich
2015-04-27
*
|
removed the last console writes (used for testing)
Dietrich
2015-04-26
*
|
Successfully parsed the float type
Dietrich
2015-04-26
*
|
added float type to the set array in Parser
Dietrich
2015-04-26
*
|
removed comments from Scanner.cs, changed the value of the float token kind t...
Dietrich
2015-04-26
*
|
added float type to Arithmetic Expression and added a new float test
Dietrich
2015-04-26
|
*
Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a
Dan Liew
2015-04-26
|
*
Minor fixes for AbsHoudini
Akash Lal
2015-04-23
|
*
Better error message
akashlal
2015-04-21
*
|
renamed fp32 to BigFloat
Dietrich
2015-04-20
*
|
added minor commenting to Parser.cs
Dietrich
2015-04-20
*
|
added a collection of console writes for debugging. These should be removed ...
Dietrich
2015-04-20
*
|
Added float type to the Parser and Scanner
Dietrich
2015-04-20
*
|
added float tipe to AbsyExpr and IntervalDomain. The methods added may requi...
Dietrich
2015-04-20
|
*
patched ghost checking
qadeer
2015-04-18
|
*
changed aux attribute to ghost
qadeer
2015-04-18
*
|
added float type definition to AbsyType and parser (parser definition may be ...
Dietrich
2015-04-17
|
*
fixed the treatment of extern
qadeer
2015-04-17
*
|
adding references to the floating point type wherever references to the real ...
Dietrich
2015-04-17
*
|
Added the fp32 class, copied from the previously existing BigDec class. No s...
Dietrich
2015-04-17
|
*
patched the type checker to deal with modularity
qadeer
2015-04-16
|
/
*
Patch by Jeroen Ketema.
Dan Liew
2015-04-05
*
VC gen for security properties
akashlal
2015-04-05
*
Patch by Jeroen Ketema
Dan Liew
2015-03-27
*
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
*
Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188)
Dan Liew
2015-03-10
*
Fix bug in BigDec.FloorCeiling() which gave the wrong answers for
Dan Liew
2015-03-10
*
fixed crash reported by Dan.
qadeer
2015-03-02
*
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
*
Fix using reserved Z3 keywords for real/int arithmetic operators. These are t...
Dan Liew
2015-02-27
*
Fix using reserved Z3 keywords for float operators. These are taken
Dan Liew
2015-02-27
*
Merge.
Dan Liew
2015-02-18
|
\
*
|
Fix bug where some reserved Z3 keywords were not sanitized
Dan Liew
2015-02-18
[prev]
[next]