summaryrefslogtreecommitdiff
path: root/Source/Core/Inline.cs
Commit message (Expand)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Let attributes live on during inliningGravatar akashlal2014-11-05
* Did more refactoring and addressed several todos.Gravatar wuestholz2014-09-23
* Did some refactoring.Gravatar wuestholz2014-09-23
* a small fix to prefix calculationGravatar qadeer2014-09-19
* a bug fix in Houdini (also AbsHoudini)Gravatar qadeer2014-09-19
* InlineAssume attribute for ensures clauses; if present, the ensures condition...Gravatar qadeer2014-09-18
* added a commentGravatar qadeer2014-09-17
* fixed a bug in inliningGravatar qadeer2014-09-17
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
* fixed code contracts violationsGravatar qadeer2014-02-11
* Remove some (redundant) preconditions to avoid 'ccrewrite' errors.Gravatar wuestholz2013-12-11
* minor fix so that variable copies in procedures and codeexprs are different.Gravatar qadeer2013-09-10
* inlining is now done in rhs of assignments for codeexprsGravatar qadeer2013-08-15
* Extended codeexpr inlining to deal with nested codeexprGravatar qadeer2013-08-15
* extended inlining to deal with codeexprsGravatar qadeer2013-08-14
* 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
* Changed Has method of PureSequence to Contains to make refactoring easier.Gravatar Ally Donaldson2013-07-22
* Requires/EnsuresSeq replaced by List<Requires/Ensures>Gravatar Ally Donaldson2013-07-22
* Large refactoring of Hashtable to Dictionary.Gravatar Ally Donaldson2013-07-22
* Added a little bit of virtual-ness to the Inliner class. This is so that I canGravatar akashlal2013-04-28
* bug fix for interaction between inlining and loopsGravatar Unknown2013-01-04
* changed behavior of InlinedEnsures so that free ensures is skipped unless an ...Gravatar qadeer2012-06-01
* fixed a completeness problem in houdini with inliningGravatar qadeer2011-12-18
* fixed bug in the inlineDepth option for houdiniGravatar qadeer2011-11-23
* changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
* changed inlining code so that candidate preconditions and postconditions are ...Gravatar qadeer2011-11-15
* added the option /inlineDepth:n. This option defaults to -1. If the user prov...Gravatar qadeer2011-11-13
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* fixed a small bug in inline codeGravatar qadeer2010-12-20
* Cleanup up the inlining codeGravatar qadeer2010-12-15
* Boogie: Committing changed source filesGravatar tabarbe2010-08-20
* Boogie: Renaming core sources in preparation for port commitGravatar tabarbe2010-08-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 04:46:01 +0000