summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
| * | strengthened type checkingGravatar qadeer2014-12-26
| | * Replaced properties Lhss_NRO and Rhss_NRO by methods SetLhs and SetRhs.Gravatar 0biha2014-12-25
| | * Made some compatibility fixes after running the unit tests.Gravatar 0biha2014-12-24
| | * Made invariant of class 'CommandLineOptions' robust by changing the designGravatar 0biha2014-12-24
| | * Backed out changeset: 4103d2e9c2efGravatar 0biha2014-12-24
| | * Scanner generation with CocoGravatar 0biha2014-12-24
| | * Made invariant of class 'CommandLineOptions' robust by changing the designGravatar 0biha2014-12-23
| | * Made invariant of class 'CommandLineOptions' robust by changing the designGravatar 0biha2014-12-23
| | * Made invariant of class 'CommandLineOptions' robust byGravatar 0biha2014-12-23
| | * Made invariant of class 'CommandLineOptionEngine' robust byGravatar 0biha2014-12-23
| | * Made invariant of class 'Scanner' robust by changing the design (replaced pub...Gravatar 0biha2014-12-23
| | * Made invariant of class 'ProcedureSummaryEntry' robust by changing the designGravatar 0biha2014-12-23
| | * Made invariant of class 'HavocCmd' robust by changing the design (replaced pu...Gravatar 0biha2014-12-19
| | * Made 2 invariants of type 'StateCmd' robust by changing the designGravatar 0biha2014-12-19
| | * Made 2 invariants of type 'AssignCmd' robust byGravatar 0biha2014-12-19
| | * Made invariant of class 'CommandLineOptionEngine' robust by changing the desi...Gravatar 0biha2014-12-19
| | * Made invariant of class 'Ensures' robust by changing the design (replaced pub...Gravatar 0biha2014-12-19
| * | changed type checking of yield procedures so that they can only call other yi...Gravatar qadeer2014-12-18
| |/
| * more work on reducing call stack consumptionGravatar qadeer2014-12-18
| * some refactoring to separate the concept of shared variables under refinement...Gravatar qadeer2014-12-17
| * MergeGravatar qadeer2014-12-16
| |\
| * | patched two occurrences of StackOverflowException on benchmarks from IronCladGravatar qadeer2014-12-16
| | * Added an annotation, :split_here, for predicate statements.Gravatar Bryan Parno2014-12-16
| |/
* | MergeGravatar 0biha2014-12-16
|\|
| * Fixed a precondition.Gravatar wuestholz2014-12-16
| * patched last check inGravatar qadeer2014-12-15
| * 1. made variable introduction layer explicit in the test casesGravatar qadeer2014-12-15
| * patched an expected outputGravatar qadeer2014-12-15
| * systematic renaming of phase to layerGravatar qadeer2014-12-15
* | Made 2 invariants of class 'Sequential' robust by changing the design (replac...Gravatar 0biha2014-12-15
* | Made invariant of class 'Choice' robust by changing the design (replaced publ...Gravatar 0biha2014-12-15
* | Made 2 invariants of class 'TypepedIdent' robust by changing the design (repl...Gravatar 0biha2014-12-15
* | Made invariant of class 'Requires' robust by changing the design (replaced pu...Gravatar 0biha2014-12-15
* | Made invariant of class 'Variable' robust by changing the design (replaced pu...Gravatar 0biha2014-12-09
* | Made 2 invariants of class 'TypeSynonymDecl' robust by changing the design (r...Gravatar 0biha2014-12-09
* | Made expression invariant of class 'Axiom' robust by changing the design (rep...Gravatar 0biha2014-12-09
* | Made invariant of class 'Program' robust byGravatar 0biha2014-12-09
* | Made invariant of class 'Absy' robust by changing the design (added getter/se...Gravatar 0biha2014-12-09
|/
* Reverted a change to CreateTempVariable for FixedPointVC only.Gravatar Ken McMillan2014-12-08
* Merge some FixpointVC changes that got left behindGravatar Ken McMillan2014-12-08
|\
* | Optimized the VC generation for assumption variables.Gravatar wuestholz2014-12-07
* | fixed bug due to incomplete erasure of :linear attributeGravatar qadeer2014-12-05
* | Patch by Jeroen KetemaGravatar Dan Liew2014-12-01
* | Added todos.Gravatar wuestholz2014-11-26
* | Fixed issue with resolution of function calls.Gravatar wuestholz2014-11-26
* | Fix FunctionCall.Resolve() so that when the function is resolved the type bec...Gravatar Dan Liew2014-11-25
* | Add unit test to catch another bug in Boogie where FunctionCall ShallowTypeGravatar Dan Liew2014-11-25
* | Fix bug in FunctionCall that caused the ExprTypeChecking.FunctionCall()Gravatar Dan Liew2014-11-25
* | Added a unit test to catch a bug in Boogie where a NAryExpr.ShallowTypeGravatar Dan Liew2014-11-25
* | Worked on the verification result caching (extracted functions).Gravatar wuestholz2014-11-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 16:11:28 +0000