Fix YAML witness unassume indentation (PR #1124)

goblint · Sep 7, 2023 · d97504b · d97504b
1 parent b80c7d3
commit d97504b
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 31 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2297,8 +2297,10 @@ struct
           let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
           let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
           if ID.to_int countval = Some Z.one then (
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
-          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))]
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+              add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false);
+              eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))
+            ]
           )
           else (
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in

diff --git a/src/witness/witness.ml b/src/witness/witness.ml
@@ -306,35 +306,35 @@ struct
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
       (val if GobConfig.get_bool "witness.enabled" then (
-          let module Arg = (val ArgTool.create entrystates) in
-          let module Arg =
-          struct
-            include Arg
-
-            let find_invariant (n, c, i) =
-              let context = {Invariant.default_context with path = Some i} in
-              ask_local (n, c) (Invariant context)
-          end
-          in
-          (module Arg: BiArgInvariant)
-        )
-        else (
-          let module Arg =
-          struct
-            module Node = ArgTool.Node
-            module Edge = MyARG.InlineEdge
-            let next _ = []
-            let prev _ = []
-            let find_invariant _ = Invariant.none
-            let main_entry =
-              let lvar = WitnessUtil.find_main_entry entrystates in
-              (fst lvar, snd lvar, -1)
-            let iter_nodes f = f main_entry
-            let query _ q = Queries.Result.top q
-          end
-          in
-          (module Arg: BiArgInvariant)
-        )
+           let module Arg = (val ArgTool.create entrystates) in
+           let module Arg =
+           struct
+             include Arg
+
+             let find_invariant (n, c, i) =
+               let context = {Invariant.default_context with path = Some i} in
+               ask_local (n, c) (Invariant context)
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+         else (
+           let module Arg =
+           struct
+             module Node = ArgTool.Node
+             module Edge = MyARG.InlineEdge
+             let next _ = []
+             let prev _ = []
+             let find_invariant _ = Invariant.none
+             let main_entry =
+               let lvar = WitnessUtil.find_main_entry entrystates in
+               (fst lvar, snd lvar, -1)
+             let iter_nodes f = f main_entry
+             let query _ q = Queries.Result.top q
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
       )
     in