| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
preparation for integrating my ported copies of that project. <\Isabelle> <\Boogie>
|
| |
|
|
|
|
|
| |
changes made to the .csproj and Boogie.sln file that are necessary for the port.
My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me.
</BoogieDriver> </Boogie>
|
| |
|
|
|
|
|
| |
changes made to the .csproj and Boogie.sln file that are necessary for the port.
My Microsoft alias is t-abarbe, so if any of this stuff breaks for you, you can contact me.
</BoogieDriver> </Boogie>
|
| | |
|
| |
|
|
| |
assertions with "if"s to handle errors gently and add cycle detection check.
|
| |
|
|
| |
changes.
|
| | |
|
| |
|
|
| |
inlining algorithm.
|
| |
|
|
| |
ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
|
| | |
|
| | |
|
| |
|
|
| |
unnecessarry "Contract.Assert"s from my porting of Boogie.
|
| | |
|
| | |
|
| |
|
|
| |
/stratifiedInline:1.
|
| |
|
|
| |
implementations in the refinement VC
|
| | |
|
| |
|
|
|
| |
* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
|
| | |
|
| | |
|
| |
|
|
| |
'BoogiePL.Parser.Parse'.
|
| |
|
|
| |
tokens. Made it an extension method that takes any object implementing IObjectWithLocations. Much easier to use within the translator.
|
| |
|
|
| |
only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is *not* by reference and is *not* an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure.
|
| |
|
|
| |
Added an override of ToString so MethodParameters show up nicer in the debugger.
|
| |
|
|
| |
Adapted definition of IsGoodInhaleState and an axiom.
|
| |
|
|
| |
return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
|
| |
|
|
| |
regression test -- a sequence refined by a singly linked list.
|
| |
|
|
| |
the traversers and which contains the information that they need to share with each other.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
(for classes and methods) and "replaces .. by" (for coupling invariants.) Extended grammar, printer, resolver, and translator to support this extension. Compiler does not support the extension yet.
|
| | |
|
| |
|
|
|
|
| |
renaming the .ssc files to .cs. They are being deleted because my porting work will be done completely on my local disc, until such time that I want to merge ported code into the project.
With regards to the renaming problem, Stephan Tobies has found that the logs are kept on the CodePlex server, and are just not provided to the SVN client. He has created a Codeplex work item at http://codeplex.codeplex.com/workitem/25490. If it gets voted up sufficiently, it may get CodePlex to provide that log information, and thus help with future work regarding the Boogie depot.
|
| |
|
|
| |
Spec# Intellisense compiler during editing of a .cs file. So, in order to allow continued editing of Boogie, during my porting project I will not be renaming the .ssc files to .cs, but rather creating copies of, for example, the BoogieDriver project's files, naming them as .cs versions, and porting them the rest of the way into C#. I will build these projects and run the regression tests on them, and once (and only once) the reg tests are passed, I will commit the compiled C# output as the replacement for the Spec# component.
|
| |
|
|
|
|
| |
need to rename the .ssc files to .cs. Unfortunately, using the Tortoise SVN Source Control software, the changelog of the files I rename is lost. (I welcome anyone's ideas on how to do a more efficient/useful rename.) I will then port using VS 2010, creating a duplicate project on my harddisk, and translating it to pure C#. When I have my code successfully compiling, I will replace the Spec# version with my C# porting, run regressions, and if successful, commit my changes.
Editing Boogie in Spec# should still function with the .ssc files renamed to .cs files.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
tabarbe