summaryrefslogtreecommitdiff
path: root/Source/Core/BoogiePL.atg
Commit message (Expand)AuthorAge
* Did more refactoring.Gravatar wuestholz2014-09-23
* bug fixes in Duplicate.cs and parsing of invariant attributesGravatar qadeer2013-12-22
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
* Fixed the Coco/R grammar and regenerated the parser.Gravatar wuestholz2013-07-22
* All ...Seq classes now goneGravatar Ally Donaldson2013-07-22
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* StringSeq: 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: PureCollections.Sequence not used anymore.Gravatar Ally Donaldson2013-07-22
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* Requires/EnsuresSeq replaced by List<Requires/Ensures>Gravatar Ally Donaldson2013-07-22
* added parallel callsGravatar Unknown2013-03-01
* removed call forall and * args to callsGravatar Unknown2013-02-23
* Refactored code that generates an axiom for a function, and changed the prett...Gravatar Rustan Leino2013-01-17
* Allow attributes on procedure formals, function formals, and bound variablesGravatar Unknown2013-01-07
* Removed old comments about "BASEMOVE" and other constructor calls, where the ...Gravatar Unknown2013-01-07
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Boogie: new syntax for integer division and modulus: use div and mod instead ...Gravatar boehmes2012-09-27
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Dafny and Boogie: get rid of 'static' fields in parserGravatar Rustan Leino2012-08-21
* added attributes to loop invariantsGravatar qadeer2012-03-23
* Boogie: Simplified (and liberalized) parsing of string literals as attribute ...Gravatar Unknown2012-03-12
* updated Boogie strings so that they can refer to \" (and more)Gravatar qadeer2012-03-12
* make the call to ProcessDataTypeConstructors in the right placeGravatar qadeer2012-03-11
* Boogie: map the given filename stdin.bpl to standard inputGravatar Unknown2012-03-09
* Fix atg file and add comment about Set/*Variable*/Gravatar Michal Moskal2011-12-07
* commented calls to GC.Collect()Gravatar qadeer2011-11-18
* changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
* Added "free call" statements that don't check the precondition in the caller.Gravatar wuestholz2011-09-14
* Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed so...Gravatar wuestholz2011-07-15
* Boogie: white-space formatingGravatar Rustan Leino2011-06-05
* close the file stream opened by the parserGravatar Unknown2011-05-19
* Boogie: Eliminated a couple of warnings by removing unused variable declarati...Gravatar wuestholz2011-01-21
* Boogie:Gravatar rustanleino2010-09-23
* Changed the interface of Parse so that it can consume a program from a StreamGravatar akashlal2010-09-03
* Boogie: Committing changed source filesGravatar tabarbe2010-08-20
* Boogie: Added boolean code expressions (sans well-formedness checks on the in...Gravatar rustanleino2010-08-10
* Boogie: Added an additional parameter 'defines' to the method 'BoogiePL.Parse...Gravatar wuestholz2010-07-06
* Updated the frame files to work with the latest Coco/R. This entails *not* ha...Gravatar mikebarnett2010-06-22
* added attributes to CallForallCmd as wellGravatar qadeer2010-03-07
* added the ability to annotate calls with attributesGravatar qadeer2010-03-06
* Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda expressions;...Gravatar MichalMoskal2010-02-19
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
* Allow ":" in addition to "returns" in function definitions. Make the pretty-p...Gravatar MichalMoskal2009-12-17
* Fixed problem where nullary function with definition had caused a crash.Gravatar rustanleino2009-08-07
* Initial set of files.Gravatar mikebarnett2009-07-15