summaryrefslogtreecommitdiff
path: root/Source/Core
Commit message (Expand)AuthorAge
* Changed the 'verifySnapshots' command-line option to accept a numeric argumen...Gravatar wuestholz2014-06-20
* Fixed crash in resolverGravatar Rustan Leino2014-06-19
* Fixed a bug in revised mod set analysisGravatar Ally Donaldson2014-06-06
* Refactored modset analysis to avoid the use of static fields. Static fields ...Gravatar Ally Donaldson2014-06-06
* Add isBvConst and asBvConst accessors to LiteralExpr to match theGravatar Dan Liew2014-05-28
* Implemented an additional type check for assumption variables.Gravatar wuestholz2014-05-27
* Merge duality changesGravatar Ken McMillan2014-05-26
|\
| * Conjecture printing for duality and child user time tracking.Gravatar Ken McMillan2014-05-26
* | Added stack boundingGravatar akashlal2014-05-10
* | Added /useBaseNameForFile command line argument. The ScannerGravatar Dan Liew2014-04-06
* | checkpointGravatar qadeer2014-05-03
* | updated the mover checksGravatar qadeer2014-04-25
* | Add support for assumption variables.Gravatar wuestholz2014-04-21
* | MergeGravatar qadeer2014-04-16
|\ \
* | | added variable hidingGravatar qadeer2014-04-16
| |/ |/|
| * Fixed malformed Contracts sectionGravatar Rustan Leino2014-04-15
| * disabled quantifier merging, except when no triggers are provided (as discuss...Gravatar Unknown2014-03-03
|/
* Added /printFixedPoint optionGravatar Ken McMillan2014-04-14
* Added option to avoid unrolling irreducible loopsGravatar akashlal2014-04-06
* Fixed class cast issue with type synonymsGravatar Ally Donaldson2014-04-01
* Change class 'LambdaVisitor' to attach checksum to expanded lambda functions.Gravatar wuestholz2014-03-17
* Fix duplicator so that BVConcatExpr and BVExtractExpr are handled. Patch by ...Gravatar Ally Donaldson2014-03-12
* MergeGravatar Rustan Leino2014-02-28
|\
* | Changed all lambda-expression rewriting to be done as a pre-processing step b...Gravatar Rustan Leino2014-02-28
| * Added /trustNonInterference optionGravatar qadeer2014-02-28
* | Changed return type of VisitLambdaExpr to just ExprGravatar Rustan Leino2014-02-27
| * added /doNotUseParallelism optionGravatar qadeer2014-02-27
|/
* Fixed tokens to improve error message produce for type errors in non-inlined ...Gravatar Rustan Leino2014-02-25
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions of...Gravatar Rustan Leino2014-02-24
* added ReadOnlyStandardVisitorGravatar qadeer2014-02-24
* Added /trustPhasesDownto optionGravatar qadeer2014-02-24
* Added /trustPhasesUpto optionGravatar qadeer2014-02-23
* Added /trustAtomicityTypes optionGravatar qadeer2014-02-22
* fixed code contracts violationsGravatar qadeer2014-02-11
* Fixed errors in the use of Code ContractsGravatar Rustan Leino2014-02-10
* Fixed bug in handling of break statementsGravatar Rustan Leino2014-02-10
* bug fix in error trace printingGravatar qadeer2014-02-05
* Option for reversing Houdini worklist (for top-down analysis)Gravatar akashlal2014-01-28
* Added functionality to rename state captures when programs are unrolled.Gravatar Ally Donaldson2014-01-17
* Integrated support for k-induction, implemented a while ago by Philipp Ruemme...Gravatar Ally Donaldson2014-01-17
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
* extended NormalSubstituter so that it can take in a forold substitutionGravatar qadeer2014-01-10
* Recursive walking of Exprs doesn't play nice when the depth of the AST is high.Gravatar akashlal2014-01-07
* Updated year in main copyright messageGravatar Rustan Leino2014-01-03
* more bug fixesGravatar qadeer2013-12-24
* bug fixes in Duplicate.cs and parsing of invariant attributesGravatar qadeer2013-12-22
* MergeGravatar qadeer2013-12-19
|\
* | various updates and tighter integration of QED stuff into mainlineGravatar qadeer2013-12-19
| * Fixed another :never_pattern bug related to nested quantifiersGravatar Rustan Leino2013-12-16
| * MergeGravatar Rustan Leino2013-12-16
| |\ | |/ |/|