copyright + formatting

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java

@@ -388,41 +388,43 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
 
     /**
      * Conversion from C (/) semantics to solver (div) semantics.
+     *
      * @param a dividend
      * @param b divisor
      * @return expression representing C division semantics with solver operations
      */
     private Expr<?> createIntDiv(Expr<?> a, Expr<?> b) {
         DivExpr<?> aDivB = Div(a, b);
         return Ite(Geq(a, Int(0)),          // if (a >= 0)
-            aDivB,                                //   a div b
-                                                  // else
-            Ite(Neq(Mod(a, b), Int(0)),     //   if (a mod b != 0)
-                Ite(Geq(b, Int(0)),         //     if (b >= 0)
-                    Add(aDivB, Int(1)),     //       a div b + 1
-                                                  //     else
-                    Sub(aDivB, Int(1))      //       a div b - 1
-                ),                                //   else
-                aDivB                             //     a div b
-            )
+                aDivB,                                //   a div b
+                // else
+                Ite(Neq(Mod(a, b), Int(0)),     //   if (a mod b != 0)
+                        Ite(Geq(b, Int(0)),         //     if (b >= 0)
+                                Add(aDivB, Int(1)),     //       a div b + 1
+                                //     else
+                                Sub(aDivB, Int(1))      //       a div b - 1
+                        ),                                //   else
+                        aDivB                             //     a div b
+                )
         );
     }
 
     /**
      * Conversion from C (%) semantics to solver (mod) semantics.
+     *
      * @param a dividend
      * @param b divisor
      * @return expression representing C modulo semantics with solver operations
      */
     private Expr<?> createIntMod(Expr<?> a, Expr<?> b) {
         ModExpr<?> aModB = Mod(a, b);
         return Ite(Geq(a, Int(0)),  // if (a >= 0)
-            aModB,                        //   a mod b
-                                          // else
-            Ite(Geq(b, Int(0)),     //   if (b >= 0)
-                Sub(aModB, b),            //     a mod b - b
-                Add(aModB, b)             //     a mod b + b
-            )
+                aModB,                        //   a mod b
+                // else
+                Ite(Geq(b, Int(0)),     //   if (b >= 0)
+                        Sub(aModB, b),            //     a mod b - b
+                        Add(aModB, b)             //     a mod b + b
+                )
         );
     }
 

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiSingleThread.kt

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.coi
 
 import hu.bme.mit.theta.analysis.LTS

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporCoiLts.kt

@@ -1,3 +1,19 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
 package hu.bme.mit.theta.xcfa.analysis.por
 
 import hu.bme.mit.theta.analysis.LTS

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt

@@ -23,8 +23,10 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.model.XCFA
 
-open class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>) :
-    XcfaSporLts(xcfa) {
+open class XcfaAasporLts(
+    xcfa: XCFA,
+    private val ignoredVarRegistry: MutableMap<Decl<out Type>, MutableSet<ExprState>>
+) : XcfaSporLts(xcfa) {
 
     override fun <P : Prec> getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection<XcfaAction>,
         prec: P): Set<XcfaAction> {

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ConfigOptions.kt

@@ -181,7 +181,7 @@ enum class Refinement(
     ),
     MULTI_SEQ(
         refiner = { s, m ->
-            if(m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ")
+            if (m == CexMonitorOptions.CHECK) error("CexMonitor is not implemented for MULTI_SEQ")
             ExprTraceSeqItpChecker.create(BoolExprs.True(), BoolExprs.True(), s.createItpSolver())
         },
         stopCriterion = StopCriterions.fullExploration()
@@ -333,12 +333,14 @@ enum class ConeOfInfluenceMode(
         XcfaAasporCoiLts(xcfa, ivr, ConeOfInfluence.lts)
     })
     ;
+
     var porLts: LTS<XcfaState<out ExprState>, XcfaAction>? = null
 }
 
 // TODO CexMonitor: disable for multi_seq
 // TODO add new monitor to xsts cli
 enum class CexMonitorOptions {
+
     CHECK,
     DISABLE
 }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCegarConfig.kt

@@ -92,7 +92,7 @@ data class XcfaCegarConfig(
     var pruneStrategy: PruneStrategy = PruneStrategy.LAZY,
     @Parameter(names = ["--cex-monitor"],
         description = "Warning: With some configurations (e.g. lazy pruning) it is POSSIBLE (but rare) that analysis is stopped, " +
-                "even though it could still progress. If in doubt, disable this monitor and check results.")
+            "even though it could still progress. If in doubt, disable this monitor and check results.")
     var cexMonitor: CexMonitorOptions = CexMonitorOptions.DISABLE,
     @Parameter(names = ["--timeout-ms"],
         description = "Timeout for verification (only valid with --strategy SERVER), use 0 for no timeout")

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt

@@ -278,7 +278,9 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass {
         if (location.outgoingEdges.size != 1) return false
         val outEdge = location.outgoingEdges.first()
         if (
-            location.incomingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel || (it is StmtLabel && it.stmt is AssumeStmt) } }
+            location.incomingEdges.any { edge ->
+                edge.getFlatLabels().any { it is InvokeLabel || (it is StmtLabel && it.stmt is AssumeStmt) }
+            }
             || location.outgoingEdges.any { edge -> edge.getFlatLabels().any { it is InvokeLabel } }
             || (level == LbeLevel.LBE_LOCAL && !atomicPhase && isNotLocal(outEdge))
         ) {