Skip to content

More fixes for real applications #283

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
wants to merge 17 commits into
base: main
Choose a base branch
from
Draft

More fixes for real applications #283

wants to merge 17 commits into from
+1,455 −220

Conversation

CaelmBleidd
Copy link
Member

No description provided.

@CaelmBleidd CaelmBleidd changed the title Caelmbleidd/fixes More fixes for real applications May 30, 2025
github-advanced-security[bot]
github-advanced-security bot found potential problems May 30, 2025
View reviewed changes
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
val resolvedArgs = expr.args.map { resolve(it) ?: return null }

val staticInstances = scope.calcOnState {
resolutionResult.properties.take(1).map { getStaticInstance(it.enclosingClass!!) }

Check warning

Code scanning / detekt

Unsafe calls on nullable types detected. These calls will throw a NullPointerException in case the nullable value is null. Warning

Calling !! on a nullable type will throw a NullPointerException at runtime in case the value is null. It should be avoided.
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

require(resolutionResult is EtsPropertyResolution.Unique)

val instance = scope.calcOnState { getStaticInstance(resolutionResult.property.enclosingClass!!) }

Check warning

Code scanning / detekt

Unsafe calls on nullable types detected. These calls will throw a NullPointerException in case the nullable value is null. Warning

Calling !! on a nullable type will throw a NullPointerException at runtime in case the value is null. It should be avoided.
usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
}

// Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,

Check warning

Code scanning / detekt

Line detected, which is longer than the defined maximum line length in the code style. Warning

Line detected, which is longer than the defined maximum line length in the code style.
usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -72,11 +75,27 @@
.filterNot { it.isStatic }
.filterNot { it.name.startsWith("%AM") }
.filterNot { it.name == "build" }
.filterNot { it.name == INSTANCE_INIT_METHOD_NAME }

Check warning

Code scanning / detekt

Disallow shadowing variable declarations. Warning test

Name shadowed: implicit lambda parameter 'it'
usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -72,11 +75,27 @@
.filterNot { it.isStatic }
.filterNot { it.name.startsWith("%AM") }
.filterNot { it.name == "build" }
.filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
.filterNot { it.name == STATIC_INIT_METHOD_NAME }

Check warning

Code scanning / detekt

Disallow shadowing variable declarations. Warning test

Name shadowed: implicit lambda parameter 'it'
usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -72,11 +75,27 @@
.filterNot { it.isStatic }
.filterNot { it.name.startsWith("%AM") }
.filterNot { it.name == "build" }
.filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
.filterNot { it.name == STATIC_INIT_METHOD_NAME }
.filterNot { it.name == CONSTRUCTOR_NAME }

Check warning

Code scanning / detekt

Disallow shadowing variable declarations. Warning test

Name shadowed: implicit lambda parameter 'it'
github-advanced-security[bot]
github-advanced-security bot found potential problems May 30, 2025
View reviewed changes
usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
options,
targets,
timeStatisticsFactory =
{ timeStatistics },

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
timeStatisticsFactory =
{ timeStatistics },
stepsStatisticsFactory =
{ stepsStatistics },

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
stepsStatisticsFactory =
{ stepsStatistics },
coverageStatisticsFactory =
{ coverageStatistics },

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
coverageStatisticsFactory =
{ coverageStatistics },
getCollectedStatesCount =
{ statesCollector.collectedStates.size }

Check warning

Code scanning / detekt

Reports mis-indented code Warning

Unexpected indentation (20) (should be 16)
usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
@@ -202,12 +204,14 @@
concreteMethods += methods
}

val limitedConcreteMethods = concreteMethods.take(5)

Check warning

Code scanning / detekt

Report magic numbers. Magic number is a numeric literal that is not defined as a constant and hence it's unclear what the purpose of this number is. It's better to declare such numbers as constants and give them a proper name. By default, -1, 0, 1, and 2 are not considered to be magic numbers. Warning

This expression contains a magic number. Consider defining it to a well named constant.
@CaelmBleidd CaelmBleidd changed the base branch from main to caelmbleidd/input_arrays June 11, 2025 08:58
@CaelmBleidd CaelmBleidd force-pushed the caelmbleidd/input_arrays branch from 87b841b to 4994227 Compare June 18, 2025 10:28
Base automatically changed from caelmbleidd/input_arrays to main June 18, 2025 10:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@CaelmBleidd @Lipen