Skip to content

Commit

Permalink
[style] fixed style
Browse files Browse the repository at this point in the history
  • Loading branch information
MchKosticyn committed Mar 24, 2024
1 parent 9ddfe3e commit f33d60e
Show file tree
Hide file tree
Showing 9 changed files with 12 additions and 28 deletions.
6 changes: 3 additions & 3 deletions VSharp.Explorer/Statistics.fs
Original file line number Diff line number Diff line change
Expand Up @@ -243,10 +243,10 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage
hasNewCoverage <- hasNewCoverage || isNewBlock && method.InCoverageZone
hasNewCoverage

member x.IsBasicBlockCoveredByTest (blockStart : codeLocation) =
member x.IsBasicBlockCoveredByTest (blockEnd : codeLocation) =
let mutable coveredBlocks = ref null
if blocksCoveredByTests.TryGetValue(generalizeIfNeeded blockStart.method, coveredBlocks) then
coveredBlocks.Value.ContainsKey blockStart.offset
if blocksCoveredByTests.TryGetValue(generalizeIfNeeded blockEnd.method, coveredBlocks) then
coveredBlocks.Value.ContainsKey blockEnd.offset
else false

member x.GetCurrentCoverage (methods : Method seq) =
Expand Down
5 changes: 0 additions & 5 deletions VSharp.SILI.Core/API.fsi
Original file line number Diff line number Diff line change
Expand Up @@ -387,8 +387,3 @@ module API =
module Print =
val Dump : state -> string
val PrintPC : pathCondition -> string

// module Marshalling =
// val Unmarshal : state -> obj -> term * state
// val CanBeCalledViaReflection : state -> IFunctionIdentifier -> term option -> term list symbolicValue -> bool
// val CallViaReflection : state -> IFunctionIdentifier -> term option -> term list symbolicValue -> (term * state -> 'a) -> 'a
3 changes: 0 additions & 3 deletions VSharp.SILI.Core/Memory.fs
Original file line number Diff line number Diff line change
Expand Up @@ -1939,7 +1939,6 @@ module internal Memory =
with get() = state
and set value = state <- value


interface IMemory with

override _.AllocatedTypes
Expand Down Expand Up @@ -2062,7 +2061,6 @@ module internal Memory =
member self.Write reporter reference value = self.Write reporter reference value
member self.WriteStaticField typ field value = self.WriteStaticField typ field value


type heapReading<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> with
interface IMemoryAccessConstantSource with
override x.Compose state =
Expand Down Expand Up @@ -2103,7 +2101,6 @@ module internal Memory =
MemoryRegion.read region key (x.picker.isDefaultKey state) inst
afters |> List.map (mapsnd read) |> Merging.merge


type state with
static member MakeEmpty complete =
let memory = Memory()
Expand Down
4 changes: 2 additions & 2 deletions VSharp.SILI.Core/Pointers.fs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ module internal Pointers =
let private sizeOfUnderlyingPointerType = term >> function // for `T* ptr` returns `sizeof(T)`
| Ptr(_, Void, _) -> makeNumber 1
| Ptr(_, typ, _) -> makeNumber (internalSizeOf typ)
| t -> internalfailf "Taking sizeof underlying type of not pointer type: %O" t
| t -> internalfailf $"Taking sizeof underlying type of not pointer type: {t}"

// NOTE: returns 'ptr', shifted by 'shift' bytes
let private shift ptr shift =
Expand Down Expand Up @@ -280,7 +280,7 @@ module internal Pointers =
| OperationType.GreaterOrEqual
| OperationType.GreaterOrEqual_Un ->
simplifyPointerComparison op x y k
| _ -> internalfailf "%O is not a binary arithmetical operator" op
| _ -> internalfailf $"{op} is not a binary arithmetical operator"

let isPointerOperation op left right =
match op with
Expand Down
2 changes: 1 addition & 1 deletion VSharp.SILI.Core/TypeCasting.fs
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ module internal TypeCasting =
let rec refIsType state ref typ =
match ref.term with
| HeapRef(addr, sightType) ->
let leftType = state.memory.MostConcreteTypeOfHeapRef addr sightType
let leftType = state.memory.MostConcreteTypeOfHeapRef addr sightType
addressIsType addr leftType typ
| Ref address ->
let leftType = address.TypeOfLocation
Expand Down
6 changes: 3 additions & 3 deletions VSharp.SILI/InstructionPointer.fs
Original file line number Diff line number Diff line change
Expand Up @@ -148,9 +148,9 @@ type instructionPointer =

override x.ToString() =
match x with
| Instruction(offset, m) -> sprintf "{Instruction = %s; M = %s}" ((int offset).ToString("X")) m.FullName
| Exit m -> $"{{Exit from M = %s{m.FullName}}}"
| Leave(ip, _, offset, m) -> $"{{M = %s{m.FullName}; Leaving to %d{offset}\n;Currently in {ip}}}"
| Instruction(offset, m) -> $"{{Instruction = 0x{int offset:X}; M = {m.FullName}}}"
| Exit m -> $"{{Exit from M = {m.FullName}}}"
| Leave(ip, _, offset, m) -> $"{{M = {m.FullName}; Leaving to 0x{offset:X}\n;Currently in {ip}}}"
| SearchingForHandler(ehcs, finallyEhcs, toObserve, checkFinally) ->
$"SearchingForHandler({ehcs}, {finallyEhcs}, {toObserve}, {checkFinally})"
| SecondBypass(ip, ehcs, lastEhcs, method, restFrames, handler) ->
Expand Down
6 changes: 3 additions & 3 deletions VSharp.Solver/Z3.fs
Original file line number Diff line number Diff line change
Expand Up @@ -47,15 +47,15 @@ module internal Z3 =
{ parts : pathPart list }
with
member x.StructField fieldId =
{ x with parts = StructFieldPart fieldId :: x.parts }
{ parts = StructFieldPart fieldId :: x.parts }

member x.PointerAddress() =
assert(List.isEmpty x.parts)
{ x with parts = PointerAddress :: x.parts }
{ parts = PointerAddress :: x.parts }

member x.PointerOffset() =
assert(List.isEmpty x.parts)
{ x with parts = PointerOffset :: x.parts }
{ parts = PointerOffset :: x.parts }

member x.TypeOfLocation with get() =
assert(List.isEmpty x.parts |> not)
Expand Down
7 changes: 0 additions & 7 deletions VSharp.Utils/Collections.fs
Original file line number Diff line number Diff line change
Expand Up @@ -32,13 +32,6 @@ module public List =
let mappedPartition f xs =
mappedPartitionAcc f [] [] xs

let rec map2Different f xs1 xs2 =
match xs1, xs2 with
| Seq.Empty, [] -> []
| Seq.Empty, x2::xs2' -> f None (Some x2) :: map2Different f xs1 xs2'
| Seq.Cons(x1, xs1'), [] -> f (Some x1) None :: map2Different f xs1' xs2
| Seq.Cons(x1, xs1'), x2::xs2' -> f (Some x1) (Some x2) :: map2Different f xs1' xs2'

let append3 xs ys zs = List.append xs (List.append ys zs)

let rec filterMap2 mapper xs ys =
Expand Down
1 change: 0 additions & 1 deletion VSharp.Utils/Logger.fs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ module Logger =
let Info = 4
let Trace = 5


let mutable currentTextWriter = Console.Out
let mutable writeTimestamps = true

Expand Down

0 comments on commit f33d60e

Please sign in to comment.