Skip to content

Commit 1f6e3f0

Browse files
committed
Pass path condition instead its size. Make PC not internal to use its methods.
1 parent b362106 commit 1f6e3f0

File tree

3 files changed

+4
-3
lines changed

3 files changed

+4
-3
lines changed

VSharp.IL/CFG.fs

+2-1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ open System.Reflection
88
open System.Collections.Generic
99
open Microsoft.FSharp.Collections
1010
open VSharp
11+
open VSharp.Core
1112

1213
type ICallGraphNode =
1314
inherit IGraphNode<ICallGraphNode>
@@ -519,7 +520,7 @@ and IGraphTrackableState =
519520
abstract member CodeLocation: codeLocation
520521
abstract member CallStack: list<Method>
521522
abstract member Id: uint<stateId>
522-
abstract member PathConditionSize: uint
523+
abstract member PathCondition: pathCondition
523524
abstract member VisitedNotCoveredVerticesInZone: uint with get
524525
abstract member VisitedNotCoveredVerticesOutOfZone: uint with get
525526
abstract member VisitedAgainVertices: uint with get

VSharp.SILI.Core/PathCondition.fs

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ type pathCondition = pset<term>
77
// - PC does not contain True
88
// - if PC contains False then False is the only element in PC
99

10-
module internal PC =
10+
module PC =
1111

1212
let public empty : pathCondition = PersistentSet.empty<term>
1313
let public isEmpty pc = PersistentSet.isEmpty pc

VSharp.SILI/CILState.fs

+1-1
Original file line numberDiff line numberDiff line change
@@ -544,7 +544,7 @@ module CilState =
544544
override this.CodeLocation = this.approximateLoc
545545
override this.CallStack = Memory.StackTrace this.state.memory.Stack |> List.map (fun m -> m :?> Method)
546546
override this.Id = this.internalId
547-
override this.PathConditionSize with get () = PersistentSet.cardinality this.state.pc |> uint32
547+
override this.PathCondition with get () = this.state.pc
548548
override this.VisitedAgainVertices with get () = this.visitedAgainVertices
549549
override this.VisitedNotCoveredVerticesInZone with get () = this.visitedNotCoveredVerticesInZone
550550
override this.VisitedNotCoveredVerticesOutOfZone with get () = this.visitedNotCoveredVerticesOutOfZone

0 commit comments

Comments
 (0)