summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Collapse)AuthorAge
...
* | Worked on the parallelization.Gravatar wuestholz2013-07-11
| |
* | Worked on the parallelization.Gravatar wuestholz2013-07-10
| |
* | Worked on the parallelization.Gravatar wuestholz2013-07-08
| |
| * mergeGravatar Pantazis Deligiannis2013-07-06
| |\ | |/ |/|
* | Fixes for duality under corralGravatar Ken McMillan2013-06-14
| |
| * CVC4 ParserGravatar pantazis2013-06-12
|/
* removed call forall and * args to callsGravatar Unknown2013-02-23
|
* Removed old comments about "BASEMOVE" and other constructor calls, where the ↵Gravatar Unknown2013-01-07
| | | | conversion from Spec# into C# moved a constructor call
* Boogie: added type 'real' with overloaded arithmetic operations plus real ↵Gravatar boehmes2012-09-27
| | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
* Removed AIFramework from Boogie -- use native trivial or native ↵Gravatar boehmes2012-09-27
| | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 02:20:33 +0000