summaryrefslogtreecommitdiff
path: root/Source/AbsInt
Commit message (Collapse)AuthorAge
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
| | | | Select 4.0 client profile on all projects
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-12-02
| | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* created a new build target called z3apidebug.Gravatar qadeer2010-08-29
| | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
* Boogie: Commented out all occurences of repeated inherited contracts - makes ↵Gravatar tabarbe2010-08-27
| | | | fewer error messages when compiling with runtime checking on.
* Boogie: Removed some errors with code contracts (commenting out ↵Gravatar tabarbe2010-08-27
| | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
* Boogie: Changed the cce classes into one separate project, which every other ↵Gravatar tabarbe2010-08-27
| | | | project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
* Boogie: Basetypes port 3/3: Committing changed referencesGravatar tabarbe2010-08-27
| | | | Z3api.csproj shouldn't get in the way this time 'round.
* Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵Gravatar tabarbe2010-08-27
| | | | files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
* Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵Gravatar tabarbe2010-08-26
| | | | Core to jive with recent changes made to the cce class.
* Boogie: Committing changed referencesGravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Removed an old task commentGravatar tabarbe2010-08-19
|
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Boogie: Sorry about that - no need for the conditional compilationGravatar tabarbe2010-08-09
|
* Boogie: Added the #if CONTRACTS_FULL statement around all usages of cce.csGravatar tabarbe2010-08-09
|
* More line ending fixups.Gravatar MichalMoskal2010-08-06
|
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Boogie: Code Contracts runtime checking was turned on in AbsInt. I turned ↵Gravatar tabarbe2010-08-04
| | | | it back off.
* Made consistent the way all of the C# projects sign themselves and include ↵Gravatar mikebarnett2010-07-30
| | | | the version information.
* Boogie: Changed references from binary to project references.Gravatar tabarbe2010-07-27
|
* Boogie: Fixing incorrect referencing of Microsoft.Contracts (the Code ↵Gravatar tabarbe2010-07-21
| | | | Contracts dll) in AbsInt, Isabelle, and Z3
* Boogie: Changed how the references in AbsInt are referenced, and fixed a ↵Gravatar tabarbe2010-07-19
| | | | typo in the Spec# version of Z3's ProverInterface.ssc
* Boogie: I have successfully ported the AbsInt project. It passes all ↵Gravatar tabarbe2010-07-16
| | | | | | regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL. Address any error complaints to t-abarbe@microsoft.com
* Boogie: Renamed the AbsInt sources for use in the port I have done. ↵Gravatar tabarbe2010-07-16
| | | | Regressions with the changed code will take ~10 minutes. I hope I don't break anyone's build.
* * Added "deprecated" comment in help message about /interprocInfer switch. ↵Gravatar rustanleino2010-02-18
| | | | | | | The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
* Also sign AbsInt.dllGravatar stobies2009-08-18
|
* Sign assembliesGravatar stobies2009-08-17
|
* Initial set of files.Gravatar mikebarnett2009-07-15