summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| | * 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
| * | Try to add build status icon for the Windows build.Gravatar Dan Liew2015-04-28
| | * modified the third float_test slightlyGravatar Dietrich2015-04-27
| | * 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
|/ /
* | renamed og to civlGravatar qadeer2015-04-22
* | 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 a file for float type testingGravatar 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
* | added more examplesGravatar qadeer2015-04-18
* | 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
* | first check inGravatar qadeer2015-04-16
* | patched the type checker to deal with modularityGravatar qadeer2015-04-16
|/
* Note that CVC4 support is experimental.Gravatar Dan Liew2015-04-05
* Fix typo in README.md spotted by Jeroen Ketema.Gravatar Dan Liew2015-04-05
* Patch by Jeroen Ketema.Gravatar Dan Liew2015-04-05
* Disable test is ``Test/Secure``. They aren't set up properly.Gravatar Dan Liew2015-04-05
* Some test cases for SecureVCGen (disabled for lit currently)Gravatar akashlal2015-04-05
* VC gen for security propertiesGravatar akashlal2015-04-05
* Fix ``Test/test15/CaptureState.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
* Fix ``livevars/daytona_bug2_ioctl_example_2.bpl`` test under Linux.Gravatar Dan Liew2015-04-03
* Add TravisCI build status icon to README.mdGravatar Dan Liew2015-04-03
* Clean up .gitignore fileGravatar Dan Liew2015-04-03
* Remove some old mercurial files.Gravatar Dan Liew2015-04-03
* Add .travis.yml file for TravisCI builds.Gravatar Dan Liew2015-04-03
* Add initial README.mdGravatar Dan Liew2015-04-03
* Add LICENSE file.Gravatar Dan Liew2015-04-01
* updated the example to include atomic specifications (sent by Suha)Gravatar qadeer2015-03-29
* Patch by Jeroen KetemaGravatar Dan Liew2015-03-27
* Compute MustReach information lazily, on-demandGravatar akashlal2015-03-16