summaryrefslogtreecommitdiff
path: root/Source/VCExpr/Boogie2VCExpr.cs
Commit message (Expand)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Added a setter for CommandLineOptions.ProverOptions and fixed several contracts.Gravatar wuestholz2015-02-18
* Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitExistsExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitForAllExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
* Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
* Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions of...Gravatar Rustan Leino2014-02-24
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
* fixed bugGravatar qadeer2013-09-09
* fixed the problem with codexprsGravatar qadeer2013-09-07
* When a codeexpr is used at the top-level in an assume statement, we use the a...Gravatar qadeer2013-09-04
* Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in cod...Gravatar wuestholz2013-07-22
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* RESeq: farewellGravatar Ally Donaldson2013-07-22
* BlockSeq: farewellGravatar Ally Donaldson2013-07-22
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* Refactoring of TypeVariableSeqGravatar Ally Donaldson2013-07-22
* Requires/EnsuresSeq replaced by List<Requires/Ensures>Gravatar Ally Donaldson2013-07-22
* Worked on the parallelization.Gravatar wuestholz2013-07-11
* Fixes for duality under corralGravatar Ken McMillan2013-06-14
* removed call forall and * args to callsGravatar Unknown2013-02-23
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Boogie:Gravatar rustanleino2010-10-12
* Boogie: Commented out all occurences of repeated inherited contracts - makes ...Gravatar tabarbe2010-08-27
* Disabled an expensive contract check. Instead, only check things that are act...Gravatar akashlal2010-08-23
* Boogie: Committing new source code for VCExprGravatar tabarbe2010-08-13
* Boogie: Renaming VCExpr sources in preparation for port commitGravatar tabarbe2010-08-13