Open Tasks - Fixed Open Tasks

Fixed Tasks

FileTypeMessage
ExpVisitorIR.javaTODOUpdate the type checker?
TypeVisitorIR.javaTODOMorten initially requested some way of knowing whether a type originates
PatternTrans.javaTODOMake it such that the successer var is passed on (multiple binds)
DeclVisitorIR.javaFIXMEpatterns should be handled by transformations
TypePredHandler.javaTODOConsider this for the atomic statement
TypePredUtil.javaTODOConsider better handling
JmlGenUtil.javaTODOCurrently invariant method are named on the form "module_typename" although this does not truly
TypePredDecorator.javaTODOMake this case handle state designators
IROperatorLookup.javaTODOThis is not the way to do it! Fix operator precedence!
Exp2StmTrans.javaTODO
JavaCodeGen.javaTODOneeds to take all of them into account
IROperatorLookup.javaTODOOperators must be added as they come. Are there more to be added?
TransAssistantIR.javaFIXMEmake this method work on generic PMUltipleBinds
PatternTrans.javaTODOcurrently values patterns are replaced by strings
ModuleToClassTransformation.javaTODOImplement the import analysis cases
TransAssistantIR.javaTODOThis actually forces the return type to be 'void'. Maybe generalise?
PExpAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PExpAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PExpAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PExpAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PPatternAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PPatternAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PBindAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PMultipleBindAssistantInterpreter.javaFIXMEshould we handle exceptions like this
TraceRunnerMain.javaTODOAuto-generated catch block
TraceRunnerMain.javaTODOHandle the error in VDMJ, terminate?
RecAccessorTrans.javaTODOPrivatise record fields?
RecInvTransformation.javaTODOConstructing names like this will work since names on the form _<name> cannot appear in a VDM model. What
SClassDefinitionAssistantInterpreter.javaTODOrewrite this???
SClassDefinitionAssistantInterpreter.javaFIXMEThis ought to be done at the end of type checking...
TestRunner.javaTODOAuto-generated catch block
ACpuClassDefinitionAssistantInterpreter.javaTODOHere is one basis to pass the parameter with the Context.
TraceNode.javaTODOType check missing here If the type check fails we would also have to do filtering
IsaTranslations.javaFIXMEUnhack invariant extraction for named types
IsaTranslations.javaFIXMEUnhack invariant extraction for namedt ypes
TraceNode.javaTODOTo be done. Consider where the right place is to check for this.
IsaTranslations.javaFIXMEUnhack result name extraction for implicit functions
AllVariableNameLocator.javaTODOAuto-generated method stub
VdmSlNewModuleWizard.javaTODODefine operations here\n"
VdmPpProjectNature.javaTODOAuto-generated method stub
VdmPpProjectNature.javaTODOAuto-generated method stub
VdmTypeCheckerUi.javaTODOwe may be able to use the istypechecked and istypecorrect in a better way here
VdmNewProjectWizard.javaTODOAuto-generated catch block
VdmPpNewClassWizard.javaTODODefine instance variables here\n"
VdmPpNewClassWizard.javaTODODefine functions here\n"
VdmPpRuntimeUtil.javaFIXMEthis might not has any errors if it goes wrong
VdmPpNewClassWizard.javaTODODefine types here\n"
VdmCompletionHelper.javaTODOAuto-generated method stub
VdmCompletionHelper.javaTODOTemp class which has to be removed and replaced with the NameGen from package org.overture.codegen.vdm2jml.util; since it duplicates functionality
ImportStandardLibraryMarkerResolution.javaTODOAuto-generated method stub
NameGen.javaTODOTemp class which has to be removed and replaced with the NameGen from package org.overture.codegen.vdm2jml.util; since it duplicates functionality
EditorUtility.javaTODOAuto-generated catch block
VdmTypeCheckerUi.javaTODOwe may be able to use the istypechecked and istypecorrect in a better way here
EditorUtility.javaTODOAuto-generated catch block
EditorUtility.javaTODOAuto-generated catch block
VdmSlRuntimeUtil.javaFIXMEthrow approiate error
VdmSlRuntimeUtil.javaFIXMEthis might not has any errors if it goes wrong
VdmSlProjectNature.javaTODOAuto-generated method stub
VdmSlProjectNature.javaTODOAuto-generated method stub
VdmSlNewModuleWizard.javaTODODefine values here\n"
VdmSlNewModuleWizard.javaTODODefine functions here\n"
VdmSlNewModuleWizard.javaTODODefine state here\n"
VdmSlNewModuleWizard.javaTODODefine types here\n"
VdmRtProjectNature.javaTODOAuto-generated method stub
VdmRtRuntimeChecksLaunchConfigurationTab.javaTODOAuto-generated catch block
VdmPpNewClassWizard.javaTODODefine Combinatorial Test Traces here\n" + "end "
VdmRtProjectNature.javaTODOAuto-generated method stub
VdmRtNewSystemWizard.javaTODOStatic operation , 100);\n\n"+
VdmRtNewSystemWizard.javaTODOStatic operation , 100);\n*/\n"+
VdmRtNewSystemWizard.javaTODODefine deployable objects as static instance variables\n"+
VdmRtNewSystemWizard.javaTODODeploy deployable object to cpu's\n/*\n"+
Vdm2UmlCommand.javaTODOAuto-generated catch block
UmlTypeCreator.javaTODOAuto-generated method stub
ValidationConjecturesView.javaTODOAuto-generated method stub
Vdm2UmlCommand.javaTODOAuto-generated catch block
AdapterFactoryWorkbenchAdapter.javaTODOAuto-generated method stub
VdmAnnotationHover.javaTODOAuto-generated catch block
Vdm2Uml.javaTODOfix for modelio not supporting version 4.0.0 of EMF UML
Vdm2UmlAssociationUtil.javaTODOAuto-generated catch block
TraceViewer.javaFIXMEAll these magic numbers?!
TraceViewer.javaTODORemove magic numbers
OverviewEventViewer.javaTODOMVQ This info is not used?
OverviewEventViewer.javaFIXMEMagic numbers
TraceFileRunner.javaTODORemove DUMMY. Introduced to hack time travels
ValidationConjecturesView.javaTODOAuto-generated constructor stub
BusMessageEventHandler.javaTODOMVQ Review if all objects are required in all draw methods
TraceFileRunner.javaFIXME- MVQ Dirty hack in order to extend the blue line (Active/Blocked) to the end of canvas.
VdmResourceDragAdapterAssistant.javaTODOAuto-generated constructor stub
VdmResourceDragAdapterAssistant.javaTODOAuto-generated method stub
VdmElementLabels.javaTODOthis map should be deleted when the AST fix is made
VdmElementLabels.javaTODOAuto-generated method stub
VdmLanguagePropertyPage.javaTODOAuto-generated catch block
VdmLanguagePropertyPage.javaTODOAuto-generated catch block
VdmResourceDragAdapterAssistant.javaTODOAuto-generated method stub
VdmOutlineTreeContentProvider.javaTODOAuto-generated method stub
VdmExternalEditor.javaFIXME
VdmCodeScanner.javaTODOthis is a hack to get latex related stuff commented
VdmAnnotationHover.javaTODOAuto-generated catch block
VdmEditor.javaTODOdon't search for mutexes
VdmElementImageDescriptor.javaFIXMEthis was never used why was it here? -jwc/22Feb2013
VdmElementImageProvider.javaTODOthis map should be deleted when the AST fix is made
GotoDefinitionHandler.javaTODOAuto-generated catch block
GotoDefinitionHandler.javaTODOAuto-generated catch block
ConjectureData.javaTODOCheck if conjecture already exists in the list
ConjectureMarker.javaTODOAuto-generated method stub
Xetex.javaTODOAuto-generated catch block
VdmQuickInterpreter.javaTODOAuto-generated catch block
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
CpuEventViewer.javaTODOMAA
CpuEventViewer.javaTODO");
PdfLatex.javaTODOAuto-generated catch block
PdfLatex.javaTODOAuto-generated catch block
WorkbenchPropertyPage1.javaTODOAuto-generated catch block
LatexUtils.javaTODOCheck whether this must be the else case of (model == null || !model.isTypeCorrect())
Xetex.javaTODOAuto-generated catch block
Xetex.javaTODOAuto-generated catch block
PdfLatex.javaTODOAuto-generated catch block
ProcessConsolePrinter.javaTODOAuto-generated catch block
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
OverviewEventViewer.javaTODOMVQ This info is not used?
OverviewEventViewer.javaTODOMVQ This info is not used?
DummyViewer.javaTODOAuto-generated method stub
OverviewEventViewer.javaTODOMVQ This info is not used?
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
DummyViewer.javaTODOAuto-generated method stub
VdmLineBreakpointPropertyPage.javaTODOHELP CONTEXT
JarClassSelector.javaTODOAuto-generated method stub
VdmLineBreakpointPropertyPage.javaTODOI removed this label until we find a solution to fidn the member
VdmLineBreakpointPropertyPage.javaTODOthe member should be reated here
AsyncCaller.javaTODOAuto-generated catch block
DebuggerPropertiesManager.javaTODOAuto-generated catch block
ProcessConsolePrinter.javaTODOAuto-generated catch block
AsyncCaller.javaTODOAuto-generated catch block
VdmDebugModelPresentation.javaTODOAuto-generated method stub
VdmDebugModelPresentation.javaTODOAuto-generated method stub
VdmDebugModelPresentation.javaTODOit fixes the source lookup for wordDocs - not sure if this has other implications
VdmDebugModelPresentation.javaTODOAuto-generated catch block
VdmBreakpointPropertyPage.javaTODOproperty page 10 (VdmBreakpointPropertyPage)",
VdmBreakpointPropertyPage.javaTODOPlatformUI.getWorkbench().getHelpSystem().setHelp(getControl(),
VdmLineBreakpointAdapter.javaTODOAuto-generated catch block
VdmBreakpointPropertyPage.javaTODOproperty title (VdmBreakpointPropertyPage)");
ExternalCoverageEditor.javaTODOAuto-generated catch block
OpenVdmToolsProjectCommandHandler.javaTODOAuto-generated catch block
CoverageEditor.javaTODOAuto-generated catch block
ExternalCoverageEditor.javaTODOAuto-generated catch block
WorkbenchPropertyPage1.javaTODOAuto-generated constructor stub
WorkbenchPropertyPage1.javaTODOAuto-generated method stub
WorkbenchPreferencePageCsk.javaTODOAuto-generated method stub
DotHandler.javaTODOAuto-generated catch block
StorageManager.javaTODOAuto-generated catch block
TracesTreeView.javaTODO
TracesXmlStoreReader.javaTODO
StorageManager.javaTODOcould not parse file. Posible not found
ViewContentProvider.javaTODOAuto-generated catch block
ViewContentProvider.javaTODOAuto-generated catch block
ViewContentProvider.javaTODOAuto-generated catch block
ViewContentProvider.javaTODOAuto-generated catch block
DbgpDebugger.javaTODOerror handling
DbgpDebugger.javaTODOhandling
DbgpDebugger.javaFIXMEshould use single command queue here to guarantee we handle responses in the same sequences as we send
DbgpDebugger.javaTODOerror handling
DbgpSuspendOperation.javaTODOthink about what to do with this status
VdmThreadEventHandler.javaTODOtemporary fix. Collapses all threads except the running one
DbgpDebugger.javaTODOto debug log
DbgpOperation.javaTODOimprove
VdmVariable.javaTODOlocalize
VdmVariable.javaTODOUse key if provided
VdmThread.javaTODOAuto-generated catch block
VdmThreadStateManager.javaFIXMEI believe that the current debugger do not support any comminication while running
VdmEvaluationEngine.javaTODOimprove
VdmEvaluationEngine.javaTODOAuto-generated method stub
VdmVariable.javaTODOperform more smart verification
VdmVariableWrapperValue.javaTODOAuto-generated method stub
VdmLaunchShortcut.javaTODOget ISourceUnit from editor
VdmLaunchShortcut.javaTODO
VdmLineBreakpointPropertiesRulerActionDelegate.javaTODOAuto-generated constructor stub
WatchCommand.javaTODOAuto-generated method stub
VdmBreakpointAdapterFactory.javaTODOAuto-generated catch block
VdmBreakpointAdapterFactory.javaTODOAuto-generated method stub
VmArgumentsLaunchConfigurationTab.javaTODOAuto-generated catch block
VmArgumentsLaunchConfigurationTab.javaTODOAuto-generated catch block
VdmThreadEventHandler.javaTODOAuto-generated catch block
LogView.javaFIXMEwhat is this! why is it here and is it used
VdmThreadEventHandler.javaTODOAuto-generated catch block
VdmThreadEventHandler.javaTODOAuto-generated catch block
DebugConsoleManager.javaTODOwe allow both debug and run here...
VdmStreamProxy.javaTODOis there a better way to access these internal preferences??
LogView.javaTODOAuto-generated catch block
LogView.javaTODOAuto-generated method stub
DbgpRequest.javaTODOoptimize - send directly to stream without string
IDbgpContinuationCommands.javaTODOadd detach handling to commands and DbgpDetachedException!!!
VdmDebugPlugin.javaTODO
DbgpRawListener.javaTODOAuto-generated method stub
DbgpDebugingEngine.javaFIXMEthis event is delivered on the separate thread, so sometimes logging misses a few initial packets.
DbgpPropertyCommands.javaTODOcheck length!!!
DbgpDebugingEngine.javaFIXME[OutOfMemory]
DbgpDebugingEngine.javaFIXME[OutOfMemory] The start is skipped if a out of memory exception have occurred. The memory here is the
ClasspathUtils.javaTODOClasspathUtils.collectClasspath(new String[] { GenericOvertureInstallType.EMBEDDED_VDMJ_BUNDLE_ID, GenericOvertureInstallType.DBGP_FOR_VDMJ_BUNDLE_ID }, result);
ClasspathUtils.javaTODOput in constant file
Options.javaTODOAuto-generated catch block
Options.javaTODOAuto-generated catch block
ResourceManager.javaFIXMEuse new method isProjectBuildConttent(file)
VdmProject.javaTODOcheck this, does it break something? not using the actual location. This was changed to do linked files.
ResourceManager.javaTODOAuto-generated catch block
ResourceManager.javaTODOAuto-generated catch block
VdmDebugTarget.javaTODOAuto-generated catch block
VdmLineBreakpoint.javaTODOAuto-generated catch block
VdmDebugTarget.javaTODOAuto-generated method stub
VdmDebugTarget.javaTODOAuto-generated method stub
VdmThread.javaTODOlog exception
VdmThread.javaTODOremove state from name
VdmStackFrame.javaTODOAuto-generated catch block
VdmThread.javaTODOlog exception
DbgpXmlParser.javaTODOthis should probably be logged
IVdmBreakpointListener.javaTODOimplement
DbgpPacketReceiver.javaTODOcorrect init tag handling without this hack
DbgpXmlEntityParser.javaTODOCheck ATTR_TYPE who knows when. According to the http//xdebug.org/docs-dbgp.php#stack-get
VdmDebugTarget.javaTODOAuto-generated catch block
VdmDebugTarget.javaTODOAuto-generated method stub
SetVdmType.javaTODOAuto-generated constructor stub
VdmConsoleInputListener.javaTODOAuto-generated catch block
TypeDisplayer.javaTODOAuto-generated method stub
TypeDisplayer.javaTODOAuto-generated method stub
VoidBasisChecker.javaTODOAuto-generated method stub
VoidBasisChecker.javaTODOAuto-generated method stub
PTypeResolver.javaTODOAuto-generated method stub
VdmjBuilder.javaFIXMEfire build complete event
VdmjBuilder.javaTODOAuto-generated catch block
TypeCheckerStmVisitor.javaTODOfix
VdmModelException.javaTODOAuto-generated method stub
VdmModelWorkingCopy.javaFIXMEstate!!
IVdmElement.javaTODO(philippe) predicate shouldn't throw an exception
VdmModelException.javaTODOAuto-generated constructor stub
TypeCheckerExpVisitor.javaTODOcheck if this is still needed?!
ExitTypeCollector.javaTODOWe don't know what an expression call will raise
ExitTypeCollector.javaTODOWe don't know what an expression will raise
ExitTypeCollector.javaTODOWe don't know what an operation call will raise
ExitTypeCollector.javaTODOWe don't know what an operation call will raise
MultipleBindLister.javaTODOAuto-generated method stub
PureDefinitionChecker.javaTODOAuto-generated method stub
PogParamStmVisitor.javaFIXMEState Inv For Atomic assignments
VdmLocaleExtractor.javaTODOAuto-generated method stub
StateDesignatorNameGetter.javaTODOAuto-generated method stub
VariableSubVisitor.javaFIXMEcomplete the variable substitution visitor
StatementExpressionFinder.javaTODOAuto-generated method stub
ValueCollector.javaTODOAuto-generated method stub
ValueCollector.javaTODOAuto-generated method stub
AllValuesCollector.javaTODOHere we have a strange behavior from transforming this call to type.apply(THIS,ctxt)
OperationValue.javaTODO
StatementFinder.javaTODOAuto-generated method stub
StatementFinder.javaTODOAuto-generated method stub
ClassTypeChecker.javaFIXMEinternal error
ModuleTypeChecker.javaFIXMEinternal error
PrettyPrinterVisitorDefinitions.javaTODOAuto-generated method stub
PrettyPrinterVisitorDefinitions.javaTODOAuto-generated method stub
PrettyPrinterVisitor.javaTODOAuto-generated method stub
PrettyPrinterVisitor.javaTODOAuto-generated method stub
TypePrettyPrinterVisitor.javaTODOAuto-generated method stub
TypePrettyPrinterVisitor.javaTODOAuto-generated method stub
NamedValueLister.javaTODOAuto-generated catch block
ExpressionFinder.javaTODOAuto-generated method stub
InstanceVariableChecker.javaTODOAuto-generated method stub
NamedValueLister.javaTODOAuto-generated method stub
NamedValueLister.javaTODOAuto-generated method stub
DefinitionRunTimeChecker.javaTODOAuto-generated method stub
DefinitionStatementFinder.javaTODOAuto-generated method stub
Delegate.javaFIXMEthis is to handle inheritance in the same way as VDMJ did. See CSV and IO, where the subclass
DefinitionRunTimeChecker.javaTODOAuto-generated method stub
DefinitionValueChecker.javaTODOAuto-generated method stub
ExpressionFinder.javaTODOAuto-generated method stub
DefinitionStatementFinder.javaTODOAuto-generated method stub
DefinitionValueChecker.javaTODOAuto-generated method stub
ConstrainedPatternChecker.javaTODOAuto-generated method stub
ConstrainedPatternChecker.javaTODOAuto-generated method stub
BindValueCollector.javaTODOAuto-generated method stub
LengthFinder.javaTODOAuto-generated method stub
LengthFinder.javaTODOAuto-generated method stub
IdentifierPatternFinder.javaTODOAuto-generated method stub
ExpExpressionFinder.javaTODOAuto-generated method stub
ExpExpressionFinder.javaTODOAuto-generated method stub
ValuesDefinitionLocator.javaTODOAuto-generated method stub
ValuesDefinitionLocator.javaTODOAuto-generated method stub
SubExpressionsLocator.javaTODOAuto-generated method stub
SubExpressionsLocator.javaTODOAuto-generated method stub
ExpressionValueCollector.javaTODOAuto-generated method stub
ExpressionValueCollector.javaTODOAuto-generated method stub
ExpressionEvaluator.javaFIXMEnot good
ExpressionEvaluator.javaFIXMEnot good
DBGPReaderV2.javaTODO
ExpressionEvaluator.javaTODONot very efficient to do this every time. But we can't
Context.javaTODO
Context.javaTODOSlow though.
RTThreadCreateMessage.javaTODOChange show trace to allow thread name to allow easier inspection of text log file //+
NextGenRTLogger.javaTODOAuto-generated catch block
PStmAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PTypeAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PPatternAssistantInterpreter.javaFIXMEshould we handle exceptions like this
PStmAssistantInterpreter.javaFIXMEshould we handle exceptions like this
DBGPReader.javaTODOthis needs to be checked when
DBGPReaderV2.javaTODOBUG Here is a problem if the evaluate is suspended in a
DBGPExecProcesser.javaTODOAuto-generated catch block
DBGPReader.javaTODOHandle the error in VDMJ, terminate?
ObjectThread.javaFIXMEuse visitor here
SequenceTraceNode.javaTODOnot good, poor performance
CPUResource.javaTODOoptimize by converting the speed into the correct units only once
ObjectThread.javaFIXMEuse visitor here
ClassListInterpreter.javaTODOCheck this method, where it is used.
ClassListInterpreter.javaFIXMEthis exception should be thrown
TraceExpander.javaTODOAuto-generated method stub
TraceExpander.javaTODOAuto-generated method stub
BasicRuntimeValidator.javaTODOAuto-generated catch block
BasicRuntimeValidator.javaTODOAuto-generated catch block
SourceFile.javaTODOremove this filtering it can never happen because of the new scanner
Tracepoint.javaFIXMEuse visitor here
ValueObserver.javaTODOAuto-generated catch block
BUSResource.javaTODOoptimize by converting the speed into the correct units only once
OperationValidationExpression.javaTODOThe names should probably be changed to LexNameToken
OperationValidationExpression.javaTODOAuto-generated method stub