summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Collapse)AuthorAge
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
|
* Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
|
* Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵Gravatar Rustan Leino2011-10-27
| | | | as if the old /bv:z were used
* Name the constant used in @MV_state function applications - otherwise we get ↵Gravatar Michal Moskal2011-09-26
| | | | invalid Z3 files
* Boogie: use (WEIGHT 0) with the select-of-store axiomsGravatar Rustan Leino2011-06-29
|
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
| | | | | | Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
|
* new algorithm for dead code detection (vc:doomed)Gravatar schaef2011-03-15
|
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
|
* Replaced all dictionaries that mapped to bool (i.e., were being used to ↵Gravatar mikebarnett2011-03-10
| | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵Gravatar mikebarnett2011-03-10
| | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
* Added a new solution configuration, Checked, that builds the Checked ↵Gravatar mikebarnett2011-03-07
| | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
* Fix some more contracts.Gravatar mikebarnett2011-03-07
|
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
|
* Add VCExprNAry.UniformArguments property to return arguments of nested ↵Gravatar MichalMoskal2011-02-15
| | | | And/Or nodes.
* Move name-quoting (already for SMT2 not SMT1) into a seprate classGravatar MichalMoskal2011-02-15
|
* The TPTP backend works for some very limited examplesGravatar MichalMoskal2011-01-18
|
* Use a made-up name when Context.Lookup() cannot find a nameGravatar MichalMoskal2010-12-10
|
* 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.
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* 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: Removed an incorrect Ensures clause on a void method.Gravatar tabarbe2010-08-27
|
* 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.
* minor errorGravatar qadeer2010-08-27
|
* 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.
* Disabled an expensive contract check. Instead, only check things that are ↵Gravatar akashlal2010-08-23
| | | | actually used.
* Boogie: Committing changed referencesGravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Fixed a few contracts errorsGravatar tabarbe2010-08-19
|
* Boogie: Removed and completed a task commentGravatar tabarbe2010-08-19
|
* Chase type synonyms in arguments/results of map types when generating name ↵Gravatar MichalMoskal2010-08-18
| | | | (with tE:m).
* Change Synonym type printing to what it was, use a workaround in ↵Gravatar MichalMoskal2010-08-18
| | | | TypeToString() instead. Add test for /typeEncoding:m.
* Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵Gravatar MichalMoskal2010-08-18
| | | | use separate Z3 type per Boogie type
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
|
* Boogie: Adding 1 more necessary source file for VCExpr, removing an ↵Gravatar tabarbe2010-08-13
| | | | unnecessary one
* Boogie: Committing new source code for VCExprGravatar tabarbe2010-08-13
|
* Boogie: Renaming VCExpr sources in preparation for port commitGravatar tabarbe2010-08-13
|
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Boogie: Fixed a few line endingsGravatar tabarbe2010-08-06
|
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-17 05:46:09 +0000