Presentation

Version 29.0

Protocols

• Architecture
• ZeroMQ Protocol
• Unix Socket Protocol
• Batch Protocol

Kernel

• Informations
• Ast Services
• Property Services
• Project Management
• Kernel Services

Plugin Callgraph

• Callgraph Services

Plugin Dive

• Dive Services

Plugin Eva

• Eva General Services
• Eva Values

Plugin Pivot

• Pivot Table Services

Plugin Studia

• Studia

Plugin Wp

• WP Main Services
• WP Interactive Prover
• WP Tactics

Index

Index of kernel.ast

• kernel.ast.changed (SIGNAL)

• kernel.ast.compute (EXEC)

• kernel.ast.decl (DATA)

• kernel.ast.declAttributes (ARRAY)

• kernel.ast.declAttributesData (DATA)

• kernel.ast.declKind (DATA)

• kernel.ast.fetchDeclAttributes (GET)

• kernel.ast.fetchFunctions (GET)

• kernel.ast.fetchGlobals (GET)

• kernel.ast.fetchMarkerAttributes (GET)

• kernel.ast.functions (ARRAY)

• kernel.ast.functionsData (DATA)

• kernel.ast.getFiles (GET)

• kernel.ast.getFunctions (GET)

• kernel.ast.getInformation (GET)

• kernel.ast.getInformationUpdate (SIGNAL)

• kernel.ast.getMainFunction (GET)

• kernel.ast.getMarkerAt (GET)

• kernel.ast.globals (ARRAY)

• kernel.ast.globalsData (DATA)

• kernel.ast.marker (DATA)

• kernel.ast.markerAttributes (ARRAY)

• kernel.ast.markerAttributesData (DATA)

• kernel.ast.markerKind (DATA)

• kernel.ast.parseExpr (GET)

• kernel.ast.parseLval (GET)

• kernel.ast.printDeclaration (GET)

• kernel.ast.reloadDeclAttributes (GET)

• kernel.ast.reloadFunctions (GET)

• kernel.ast.reloadGlobals (GET)

• kernel.ast.reloadMarkerAttributes (GET)

• kernel.ast.setFiles (SET)

• kernel.ast.signalDeclAttributes (SIGNAL)

• kernel.ast.signalFunctions (SIGNAL)

• kernel.ast.signalGlobals (SIGNAL)

• kernel.ast.signalMarkerAttributes (SIGNAL)

• kernel.ast.source (DATA)

Index of kernel.data

• kernel.data.markdown (DATA)
• kernel.data.tag (DATA)
• kernel.data.text (DATA)

Index of kernel.project

• kernel.project.create (SET)
• kernel.project.getList (GET)
• kernel.project.projectInfo (DATA)

Index of kernel.properties

• kernel.properties.alarms (DATA)

• kernel.properties.alarmsTags (GET)

• kernel.properties.fetchStatus (GET)

• kernel.properties.propKind (DATA)

• kernel.properties.propKindTags (GET)

• kernel.properties.propStatus (DATA)

• kernel.properties.propStatusTags (GET)

• kernel.properties.reloadStatus (GET)

• kernel.properties.signalStatus (SIGNAL)

• kernel.properties.status (ARRAY)

• kernel.properties.statusData (DATA)

Index of kernel.services

• kernel.services.fetchMessage (GET)
• kernel.services.getConfig (GET)
• kernel.services.getLogs (GET)
• kernel.services.load (SET)
• kernel.services.log (DATA)
• kernel.services.logkind (DATA)
• kernel.services.logkindTags (GET)
• kernel.services.message (ARRAY)
• kernel.services.messageData (DATA)
• kernel.services.reloadMessage (GET)
• kernel.services.save (SET)
• kernel.services.setLogs (SET)
• kernel.services.signalMessage (SIGNAL)

Index of plugins.callgraph

• plugins.callgraph.callgraph (STATE)

• plugins.callgraph.compute (EXEC)

• plugins.callgraph.edge (DATA)

• plugins.callgraph.edgeKind (DATA)

• plugins.callgraph.edgeKindTags (GET)

• plugins.callgraph.getCallgraph (GET)

• plugins.callgraph.getIsComputed (GET)

• plugins.callgraph.graph (DATA)

• plugins.callgraph.isComputed (STATE)

• plugins.callgraph.signalCallgraph (SIGNAL)

• plugins.callgraph.signalIsComputed (SIGNAL)

• plugins.callgraph.vertex (DATA)

Index of plugins.dive

• plugins.dive.add (EXEC)

• plugins.dive.callsite (DATA)

• plugins.dive.callstack (DATA)

• plugins.dive.clear (EXEC)

• plugins.dive.dependency (DATA)

• plugins.dive.element (DATA)

• plugins.dive.exploration (DATA)

• plugins.dive.explorationTags (GET)

• plugins.dive.explorationWindow (DATA)

• plugins.dive.explore (EXEC)

• plugins.dive.fetchGraph (GET)

• plugins.dive.graph (ARRAY)

• plugins.dive.graphData (DATA)

• plugins.dive.hide (EXEC)

• plugins.dive.node (DATA)

• plugins.dive.nodeId (DATA)

• plugins.dive.nodeKind (DATA)

• plugins.dive.nodeKindTags (GET)

• plugins.dive.nodeLocality (DATA)

• plugins.dive.nodeRange (DATA)

• plugins.dive.nodeSpecialRange (DATA)

• plugins.dive.nodeSpecialRangeTags (GET)

• plugins.dive.range (DATA)

• plugins.dive.reloadGraph (GET)

• plugins.dive.show (EXEC)

• plugins.dive.signalGraph (SIGNAL)

• plugins.dive.taint (DATA)

• plugins.dive.taintTags (GET)

• plugins.dive.window (SET)

Index of plugins.eva.general

• plugins.eva.general.CallSite (DATA)

• plugins.eva.general.LvalueTaints (DATA)

• plugins.eva.general.alarmCategory (DATA)

• plugins.eva.general.alarmCategoryTags (GET)

• plugins.eva.general.alarmEntry (DATA)

• plugins.eva.general.computationState (STATE)

• plugins.eva.general.computationStateType (DATA)

• plugins.eva.general.deadCode (DATA)

• plugins.eva.general.fetchFunctionStats (GET)

• plugins.eva.general.fetchFunctions (GET)

• plugins.eva.general.fetchProperties (GET)

• plugins.eva.general.functionStats (ARRAY)

• plugins.eva.general.functionStatsData (DATA)

• plugins.eva.general.functions (ARRAY)

• plugins.eva.general.functionsData (DATA)

• plugins.eva.general.getCallees (GET)

• plugins.eva.general.getCallers (GET)

• plugins.eva.general.getComputationState (GET)

• plugins.eva.general.getDeadCode (GET)

• plugins.eva.general.getProgramStats (GET)

• plugins.eva.general.getStates (GET)

• plugins.eva.general.programStats (STATE)

• plugins.eva.general.programStatsType (DATA)

• plugins.eva.general.properties (ARRAY)

• plugins.eva.general.propertiesData (DATA)

• plugins.eva.general.reloadFunctionStats (GET)

• plugins.eva.general.reloadFunctions (GET)

• plugins.eva.general.reloadProperties (GET)

• plugins.eva.general.signalComputationState (SIGNAL)

• plugins.eva.general.signalFunctionStats (SIGNAL)

• plugins.eva.general.signalFunctions (SIGNAL)

• plugins.eva.general.signalProgramStats (SIGNAL)

• plugins.eva.general.signalProperties (SIGNAL)

• plugins.eva.general.statusesEntry (DATA)

• plugins.eva.general.taintStatus (DATA)

• plugins.eva.general.taintStatusTags (GET)

• plugins.eva.general.taintedLvalues (GET)

Index of plugins.eva.values

• plugins.eva.values.callsite (DATA)

• plugins.eva.values.callstack (DATA)

• plugins.eva.values.changed (SIGNAL)

• plugins.eva.values.evaluation (DATA)

• plugins.eva.values.getCallstackInfo (GET)

• plugins.eva.values.getCallstacks (GET)

• plugins.eva.values.getProbeInfo (GET)

• plugins.eva.values.getStmtInfo (GET)

• plugins.eva.values.getValues (GET)

Index of plugins.pivot.general

• plugins.pivot.general.compute (EXEC)

• plugins.pivot.general.getPivotState (GET)

• plugins.pivot.general.pivotState (STATE)

• plugins.pivot.general.signalPivotState (SIGNAL)

• plugins.pivot.general.tableStateType (DATA)

Index of plugins.studia.studia

• plugins.studia.studia.effects (DATA)

• plugins.studia.studia.getReadsLval (GET)

• plugins.studia.studia.getWritesLval (GET)

Index of plugins.wp

• plugins.wp.ProverInfos (ARRAY)

• plugins.wp.ProverInfosData (DATA)

• plugins.wp.cancelProofTasks (SET)

• plugins.wp.fetchGoals (GET)

• plugins.wp.fetchProverInfos (GET)

• plugins.wp.generateRTEGuards (EXEC)

• plugins.wp.getProcess (GET)

• plugins.wp.getProvers (GET)

• plugins.wp.getScheduledTasks (GET)

• plugins.wp.getTimeout (GET)

• plugins.wp.goal (DATA)

• plugins.wp.goals (ARRAY)

• plugins.wp.goalsData (DATA)

• plugins.wp.process (STATE)

• plugins.wp.prover (DATA)

• plugins.wp.provers (STATE)

• plugins.wp.reloadGoals (GET)

• plugins.wp.reloadProverInfos (GET)

• plugins.wp.result (DATA)

• plugins.wp.serverActivity (SIGNAL)

• plugins.wp.setProcess (SET)

• plugins.wp.setProvers (SET)

• plugins.wp.setTimeout (SET)

• plugins.wp.signalGoals (SIGNAL)

• plugins.wp.signalProcess (SIGNAL)

• plugins.wp.signalProverInfos (SIGNAL)

• plugins.wp.signalProvers (SIGNAL)

• plugins.wp.signalTimeout (SIGNAL)

• plugins.wp.startProofs (EXEC)

• plugins.wp.stats (DATA)

• plugins.wp.status (DATA)

• plugins.wp.timeout (STATE)

Index of plugins.wp.tac

• plugins.wp.tac.applyTactic (EXEC)

• plugins.wp.tac.applyTacticAndProve (EXEC)

• plugins.wp.tac.configureTactics (EXEC)

• plugins.wp.tac.fetchTactical (GET)

• plugins.wp.tac.kind (DATA)

• plugins.wp.tac.parameter (DATA)

• plugins.wp.tac.reloadTactical (GET)

• plugins.wp.tac.setParameter (EXEC)

• plugins.wp.tac.signalTactical (SIGNAL)

• plugins.wp.tac.status (DATA)

• plugins.wp.tac.tactical (ARRAY)

• plugins.wp.tac.tacticalData (DATA)

• plugins.wp.tac.value (DATA)

Index of plugins.wp.tip

• plugins.wp.tip.clearGoal (SET)

• plugins.wp.tip.clearNode (SET)

• plugins.wp.tip.clearNodeTactic (SET)

• plugins.wp.tip.clearParentTactic (SET)

• plugins.wp.tip.clearProofScript (SET)

• plugins.wp.tip.clearProvers (SET)

• plugins.wp.tip.clearSelection (SET)

• plugins.wp.tip.getNodeInfos (GET)

• plugins.wp.tip.getProofStatus (GET)

• plugins.wp.tip.getResult (GET)

• plugins.wp.tip.getScriptStatus (GET)

• plugins.wp.tip.getSelection (GET)

• plugins.wp.tip.goForward (SET)

• plugins.wp.tip.goToIndex (SET)

• plugins.wp.tip.goToNode (SET)

• plugins.wp.tip.goToRoot (SET)

• plugins.wp.tip.iformat (DATA)

• plugins.wp.tip.killProvers (SET)

• plugins.wp.tip.node (DATA)

• plugins.wp.tip.part (DATA)

• plugins.wp.tip.printSequent (GET)

• plugins.wp.tip.printStatus (SIGNAL)

• plugins.wp.tip.proofStatus (SIGNAL)

• plugins.wp.tip.rformat (DATA)

• plugins.wp.tip.runProvers (SET)

• plugins.wp.tip.runScript (SET)

• plugins.wp.tip.saveScript (SET)

• plugins.wp.tip.setSelection (SET)

• plugins.wp.tip.tactic (DATA)

• plugins.wp.tip.term (DATA)