copilot-verifier-4.3: System for verifying the correctness of generated Copilot programs

Index

arrCopilot.Verifier.Examples.ShouldPass.Array
avgTempCopilot.Verifier.Examples.ShouldPass.Heater
Battery 
1 (Type/Class)Copilot.Verifier.Examples.ShouldPass.Structs
2 (Data Constructor)Copilot.Verifier.Examples.ShouldPass.Structs
3 (Type/Class)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
4 (Data Constructor)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
bytecounterCopilot.Verifier.Examples.ShouldPass.Counter
bytecounter2Copilot.Verifier.Examples.ShouldPass.Counter
clkStreamCopilot.Verifier.Examples.ShouldPass.Clock
clkStream'Copilot.Verifier.Examples.ShouldPass.Clock
clockCopilot.Verifier.Examples.ShouldPass.FPNegation
counterCopilot.Verifier.Examples.ShouldPass.Counter
ctempCopilot.Verifier.Examples.ShouldPass.Heater
dcpaCopilot.Verifier.Examples.ShouldPass.WCV
deltaCopilot.Verifier.Examples.ShouldPass.WCV
detCopilot.Verifier.Examples.ShouldPass.WCV
dthrCopilot.Verifier.Examples.ShouldPass.WCV
engineMonitorCopilot.Verifier.Examples.ShouldPass.Engine
fieldCopilot.Verifier.Examples.ShouldPass.ArrayOfStructs
flag 
1 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
2 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
ftpCopilot.Verifier.Examples.ShouldPass.FPNegation
horizontalWCVCopilot.Verifier.Examples.ShouldPass.WCV
inputCopilot.Verifier.Examples.ShouldPass.FPNegation
lastPrimeCopilot.Verifier.Examples.ShouldPass.Arith
mkSpecForCopilot.Verifier.Examples.ShouldPass.FPOps
multRingSpecCopilot.Verifier.Examples.ShouldPass.Arith
negCopilot.Verifier.Examples.ShouldPass.WCV
normCopilot.Verifier.Examples.ShouldPass.WCV
notPreviousNotCopilot.Verifier.Examples.ShouldPass.FPNegation
numVolts 
1 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
2 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
other 
1 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
2 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
pCopilot.Verifier.Examples.ShouldPass.Clock
preCopilot.Verifier.Examples.ShouldPass.FPNegation
propMyPropertyCopilot.Verifier.Examples.ShouldPass.FPNegation
resetcounterCopilot.Verifier.Examples.ShouldPass.Counter
S 
1 (Type/Class)Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
2 (Data Constructor)Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
shouldFailExamplesCopilot.Verifier.Examples
shouldPassExamplesCopilot.Verifier.Examples
spec 
1 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin
2 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap
3 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero
4 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds
5 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero
6 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap
7 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge
8 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge
9 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap
10 (Function)Copilot.Verifier.Examples.ShouldPass.Array
11 (Function)Copilot.Verifier.Examples.ShouldPass.ArrayGen
12 (Function)Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
13 (Function)Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
14 (Function)Copilot.Verifier.Examples.ShouldPass.Clock
15 (Function)Copilot.Verifier.Examples.ShouldPass.Counter
16 (Function)Copilot.Verifier.Examples.ShouldPass.FPNegation
17 (Function)Copilot.Verifier.Examples.ShouldPass.FPOps
18 (Function)Copilot.Verifier.Examples.ShouldPass.Heater
19 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
20 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
21 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateArray
22 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
23 (Function)Copilot.Verifier.Examples.ShouldPass.WCV
sqCopilot.Verifier.Examples.ShouldPass.WCV
tauCopilot.Verifier.Examples.ShouldPass.WCV
taumodCopilot.Verifier.Examples.ShouldPass.WCV
tcoaCopilot.Verifier.Examples.ShouldPass.WCV
tcoathrCopilot.Verifier.Examples.ShouldPass.WCV
tcpaCopilot.Verifier.Examples.ShouldPass.WCV
temp 
1 (Function)Copilot.Verifier.Examples.ShouldPass.Heater
2 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
3 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
tepCopilot.Verifier.Examples.ShouldPass.WCV
testOp1 
1 (Function)Copilot.Verifier.Examples.ShouldPass.FPOps
2 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
testOp2 
1 (Function)Copilot.Verifier.Examples.ShouldPass.FPOps
2 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
thetaCopilot.Verifier.Examples.ShouldPass.WCV
tpreCopilot.Verifier.Examples.ShouldPass.FPNegation
triggerOp1 
1 (Function)Copilot.Verifier.Examples.ShouldPass.FPOps
2 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
triggerOp2 
1 (Function)Copilot.Verifier.Examples.ShouldPass.FPOps
2 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
tthrCopilot.Verifier.Examples.ShouldPass.WCV
Vect2Copilot.Verifier.Examples.ShouldPass.WCV
verifySpec 
1 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin
2 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap
3 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero
4 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds
5 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero
6 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap
7 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge
8 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge
9 (Function)Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap
10 (Function)Copilot.Verifier.Examples.ShouldPass.Arith
11 (Function)Copilot.Verifier.Examples.ShouldPass.Array
12 (Function)Copilot.Verifier.Examples.ShouldPass.ArrayGen
13 (Function)Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
14 (Function)Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
15 (Function)Copilot.Verifier.Examples.ShouldPass.Clock
16 (Function)Copilot.Verifier.Examples.ShouldPass.Counter
17 (Function)Copilot.Verifier.Examples.ShouldPass.Engine
18 (Function)Copilot.Verifier.Examples.ShouldPass.FPNegation
19 (Function)Copilot.Verifier.Examples.ShouldPass.FPOps
20 (Function)Copilot.Verifier.Examples.ShouldPass.Heater
21 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
22 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin
23 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap
24 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero
25 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds
26 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero
27 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap
28 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge
29 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
30 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
31 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
32 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateArray
33 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
34 (Function)Copilot.Verifier.Examples.ShouldPass.Voting
35 (Function)Copilot.Verifier.Examples.ShouldPass.WCV
verticalWCVCopilot.Verifier.Examples.ShouldPass.WCV
Volts 
1 (Type/Class)Copilot.Verifier.Examples.ShouldPass.Structs
2 (Data Constructor)Copilot.Verifier.Examples.ShouldPass.Structs
3 (Type/Class)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
4 (Data Constructor)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
volts 
1 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
2 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
voteCopilot.Verifier.Examples.ShouldPass.Voting
wcvCopilot.Verifier.Examples.ShouldPass.WCV
windowCopilot.Verifier.Examples.ShouldPass.Heater
zthrCopilot.Verifier.Examples.ShouldPass.WCV
|*|Copilot.Verifier.Examples.ShouldPass.WCV
~=Copilot.Verifier.Examples.ShouldPass.WCV