copilot-verifier-4.1: 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
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
horizontalWCVCopilot.Verifier.Examples.ShouldPass.WCV
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
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
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.FPOps
17 (Function)Copilot.Verifier.Examples.ShouldPass.Heater
18 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
19 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
20 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateArray
21 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
22 (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
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.FPOps
19 (Function)Copilot.Verifier.Examples.ShouldPass.Heater
20 (Function)Copilot.Verifier.Examples.ShouldPass.IntOps
21 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin
22 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap
23 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero
24 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds
25 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero
26 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap
27 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge
28 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
29 (Function)Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
30 (Function)Copilot.Verifier.Examples.ShouldPass.Structs
31 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateArray
32 (Function)Copilot.Verifier.Examples.ShouldPass.UpdateStruct
33 (Function)Copilot.Verifier.Examples.ShouldPass.Voting
34 (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