diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2e797e75ec..429ca49b9b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -625,8 +625,7 @@ struct
let toInt i =
match IdxDom.to_int @@ ID.cast_to ik i with
| Some x -> Const (CInt (x,ik, None))
- | _ -> Cilfacade.mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
-
+ | _ -> Lval.any_index_exp
in
match o with
| `NoOffset -> `NoOffset
@@ -1059,7 +1058,7 @@ struct
match ofs with
| NoOffset -> `NoOffset
| Field (fld, ofs) -> `Field (fld, convert_offset a gs st ofs)
- | Index (CastE (TInt(IInt,[]), Const (CStr ("unknown",No_encoding))), ofs) -> (* special offset added by convertToQueryLval *)
+ | Index (exp, ofs) when CilType.Exp.equal exp Lval.any_index_exp -> (* special offset added by convertToQueryLval *)
`Index (IdxDom.top (), convert_offset a gs st ofs)
| Index (exp, ofs) ->
match eval_rv a gs st exp with
@@ -1637,7 +1636,7 @@ struct
let get_var = get_var
let get a gs st addrs exp = get a gs st addrs exp
- let set a ~ctx gs st lval lval_type value = set a ~ctx ~invariant:true gs st lval lval_type value
+ let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:true gs st lval lval_type ?lval_raw value
let refine_entire_var = true
let map_oldval oldval _ = oldval
@@ -2522,7 +2521,7 @@ struct
(* all updates happen in ctx with top values *)
let get_var = get_var
let get a gs st addrs exp = get a gs st addrs exp
- let set a ~ctx gs st lval lval_type value = set a ~ctx ~invariant:false gs st lval lval_type value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *)
+ let set a ~ctx gs st lval lval_type ?lval_raw value = set a ~ctx ~invariant:false gs st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *)
let refine_entire_var = false
let map_oldval oldval t_lval =
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index f99fcb28bc..af06d64435 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -20,7 +20,7 @@ sig
val get_var: Queries.ask -> (V.t -> G.t) -> D.t -> varinfo -> VD.t
val get: Queries.ask -> (V.t -> G.t) -> D.t -> AD.t -> exp option -> VD.t
- val set: Queries.ask -> ctx:(D.t, G.t, _, V.t) Analyses.ctx -> (V.t -> G.t) -> D.t -> AD.t -> typ -> VD.t -> D.t
+ val set: Queries.ask -> ctx:(D.t, G.t, _, V.t) Analyses.ctx -> (V.t -> G.t) -> D.t -> AD.t -> typ -> ?lval_raw:lval -> VD.t -> D.t
val refine_entire_var: bool
val map_oldval: VD.t -> typ -> VD.t
@@ -93,7 +93,7 @@ struct
else set a gs st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *)
let refine_lv ctx a gs st c x c' pretty exp =
- let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) v ~ctx in
+ let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in
match x with
| Var var, o when refine_entire_var ->
(* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *)
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 7f80a03094..e121bfcb3e 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -18,7 +18,7 @@ struct
let should_join x y = D.equal x y
(* NB! Currently we care only about concrete indexes. Base (seeing only a int domain
- element) answers with the string "unknown" on all non-concrete cases. *)
+ element) answers with Lval.any_index_exp on all non-concrete cases. *)
let rec conv_offset x =
match x with
| `NoOffset -> `NoOffset
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 681b0eae3c..f8d58032ff 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -109,7 +109,7 @@ struct
let i_exp =
match ValueDomain.IndexDomain.to_int i with
| Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
- | None -> MyCFG.unknown_exp
+ | None -> Lval.any_index_exp
in
`Index (i_exp, conv_offset_inv o)
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 4109fa6e2c..c0e07c82d2 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -83,7 +83,7 @@ struct
let rec unknown_index = function
| `NoOffset -> `NoOffset
| `Field (f, os) -> `Field (f, unknown_index os)
- | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
+ | `Index (i, os) -> `Index (Lval.any_index_exp, unknown_index os) (* forget specific indices *)
in
Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 01c2bbcff6..cdb3124c87 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -31,7 +31,7 @@ struct
let exitstate v : D.t = D.empty ()
(* NB! Currently we care only about concrete indexes. Base (seeing only a int domain
- element) answers with the string "unknown" on all non-concrete cases. *)
+ element) answers with Lval.any_index_exp on all non-concrete cases. *)
let rec conv_offset x =
match x with
| `NoOffset -> `NoOffset
diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
index 982cd94058..c8a8713af7 100644
--- a/src/cdomains/arrayDomain.ml
+++ b/src/cdomains/arrayDomain.ml
@@ -61,6 +61,7 @@ sig
val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
val update_length: idx -> t -> t
val project: ?varAttr:attributes -> ?typAttr:attributes -> VDQ.t -> t -> t
+ val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t
end
module type LatticeWithSmartOps =
@@ -85,7 +86,12 @@ struct
let pretty () x = text "Array: " ++ pretty () x
let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
let get ?(checkBounds=true) (ask: VDQ.t) a i = a
- let set (ask: VDQ.t) a i v = join a v
+ let set (ask: VDQ.t) a (ie, i) v =
+ match ie with
+ | Some ie when CilType.Exp.equal ie Lval.all_index_exp ->
+ v
+ | _ ->
+ join a v
let make ?(varAttr=[]) ?(typAttr=[]) i v = v
let length _ = None
@@ -100,6 +106,21 @@ struct
let smart_leq _ _ = leq
let update_length _ x = x
let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+
+ let invariant ~value_invariant ~offset ~lval x =
+ match offset with
+ (* invariants for all indices *)
+ | NoOffset when get_bool "witness.invariant.goblint" ->
+ let i_lval = Cil.addOffsetLval (Index (Lval.all_index_exp, NoOffset)) lval in
+ value_invariant ~offset ~lval:i_lval x
+ | NoOffset ->
+ Invariant.none
+ (* invariant for one index *)
+ | Index (i, offset) ->
+ value_invariant ~offset ~lval x
+ (* invariant for one field *)
+ | Field (f, offset) ->
+ Invariant.none
end
let factor () =
@@ -170,6 +191,14 @@ struct
if Z.geq min_i f then (xl, (Val.join xr v))
else if Z.lt max_i f then ((update_unrolled_values min_i max_i), xr)
else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
+ let set ask (xl, xr) (ie, i) v =
+ match ie with
+ | Some ie when CilType.Exp.equal ie Lval.all_index_exp ->
+ (* TODO: Doesn't seem to work for unassume because unrolled elements are top-initialized, not bot-initialized. *)
+ (BatList.make (factor ()) v, v)
+ | _ ->
+ set ask (xl, xr) (ie, i) v
+
let make ?(varAttr=[]) ?(typAttr=[]) _ v =
let xl = BatList.make (factor ()) v in
(xl,Val.bot ())
@@ -188,6 +217,32 @@ struct
let smart_leq _ _ = leq
let update_length _ x = x
let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+
+ let invariant ~value_invariant ~offset ~lval ((xl, xr) as x) =
+ match offset with
+ (* invariants for all indices *)
+ | NoOffset ->
+ let i_all =
+ if Val.is_bot xr then
+ Invariant.top ()
+ else if get_bool "witness.invariant.goblint" then (
+ let i_lval = Cil.addOffsetLval (Index (Lval.all_index_exp, NoOffset)) lval in
+ value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
+ )
+ else
+ Invariant.top ()
+ in
+ BatList.fold_lefti (fun acc i x ->
+ let i_lval = Cil.addOffsetLval (Index (Cil.integer i, NoOffset)) lval in
+ let i = value_invariant ~offset ~lval:i_lval x in
+ Invariant.(acc && i)
+ ) i_all xl
+ (* invariant for one index *)
+ | Index (i, offset) ->
+ Invariant.none (* TODO: look up *)
+ (* invariant for one field *)
+ | Field (f, offset) ->
+ Invariant.none
end
(** Special signature so that we can use the _with_length functions from PartitionedWithLength but still match the interface *
@@ -425,13 +480,17 @@ struct
let set_with_length length (ask:VDQ.t) x (i,_) a =
if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a\n" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
- if i = Some MyCFG.all_array_index_exp then
+ match i with
+ | Some ie when CilType.Exp.equal ie Lval.all_index_exp ->
+ (* TODO: Doesn't seem to work for unassume. *)
+ Joint a
+ | Some i when CilType.Exp.equal i Lval.any_index_exp ->
(assert !Goblintutil.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
(* the join is needed here! see e.g 30/04 *)
let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in
let r = Val.join o a in
Joint r)
- else
+ | _ ->
normalize @@
let use_last = get_string "ana.base.partition-arrays.keep-expr" = "last" in
let exp_value e =
@@ -701,6 +760,21 @@ struct
let update_length _ x = x
let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+
+ let invariant ~value_invariant ~offset ~lval x =
+ match offset with
+ (* invariants for all indices *)
+ | NoOffset when get_bool "witness.invariant.goblint" ->
+ let i_lval = Cil.addOffsetLval (Index (Lval.all_index_exp, NoOffset)) lval in
+ value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
+ | NoOffset ->
+ Invariant.none
+ (* invariant for one index *)
+ | Index (i, offset) ->
+ Invariant.none (* TODO: look up *)
+ (* invariant for one field *)
+ | Field (f, offset) ->
+ Invariant.none
end
(* This is the main array out of bounds check *)
@@ -759,6 +833,9 @@ struct
let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+ let invariant ~value_invariant ~offset ~lval (x, _) =
+ Base.invariant ~value_invariant ~offset ~lval x
+
let printXml f (x,y) =
BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y
@@ -811,6 +888,9 @@ struct
let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+ let invariant ~value_invariant ~offset ~lval (x, _) =
+ Base.invariant ~value_invariant ~offset ~lval x
+
let printXml f (x,y) =
BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y
@@ -852,6 +932,9 @@ struct
let project ?(varAttr=[]) ?(typAttr=[]) _ t = t
+ let invariant ~value_invariant ~offset ~lval (x, _) =
+ Base.invariant ~value_invariant ~offset ~lval x
+
let printXml f (x,y) =
BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Base.name ())) Base.printXml x "length" Idx.printXml y
@@ -972,4 +1055,10 @@ struct
| UnrolledDomain, (None, Some (Some x, None)) -> to_t @@ (None, None, Some (unroll_of_trivial ask x) )
| UnrolledDomain, (None, Some (None, Some x)) -> to_t @@ (None, None, Some x)
| _ -> failwith "AttributeConfiguredArrayDomain received a value where not exactly one component is set"
+
+ let invariant ~value_invariant ~offset ~lval =
+ unop'
+ (P.invariant ~value_invariant ~offset ~lval)
+ (T.invariant ~value_invariant ~offset ~lval)
+ (U.invariant ~value_invariant ~offset ~lval)
end
diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli
index 8386deb541..91e526235d 100644
--- a/src/cdomains/arrayDomain.mli
+++ b/src/cdomains/arrayDomain.mli
@@ -57,6 +57,7 @@ sig
val update_length: idx -> t -> t
val project: ?varAttr:Cil.attributes -> ?typAttr:Cil.attributes -> VDQ.t -> t -> t
+ val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t
end
module type LatticeWithSmartOps =
diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml
index 2219f7dbff..c6c585d751 100644
--- a/src/cdomains/lval.ml
+++ b/src/cdomains/lval.ml
@@ -4,6 +4,17 @@ open Pretty
module GU = Goblintutil
module M = Messages
+(** Special index expression for some unknown index.
+ Weakly updates array in assignment.
+ Used for exp.fast_global_inits. *)
+let any_index_exp = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "any_index")
+
+(** Special index expression for all indices.
+ Strongly updates array in assignment.
+ Used for Goblint-specific witness invariants. *)
+let all_index_exp = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
+
+
type ('a, 'b) offs = [
| `NoOffset
| `Field of 'a * ('a,'b) offs
@@ -583,7 +594,7 @@ struct
match o with
| `NoOffset -> a
| `Field (f,o) -> short_offs o (a^"."^f.fname)
- | `Index (e,o) when CilType.Exp.equal e MyCFG.unknown_exp -> short_offs o (a^"[?]")
+ | `Index (e,o) when CilType.Exp.equal e any_index_exp -> short_offs o (a^"[?]")
| `Index (e,o) -> short_offs o (a^"["^CilType.Exp.show e^"]")
let rec of_ciloffs x =
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 882b66859e..40904ee9b6 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -873,7 +873,7 @@ struct
let update_offset (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
let rec do_update_offset (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
- if M.tracing then M.traceli "update_offset" "do_update_offset %a %a %a\n" pretty x Offs.pretty offs pretty value;
+ if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
let mu = function `Blob (`Blob (y, s', orig), s, orig2) -> `Blob (y, ID.join s s',orig) | x -> x in
let r =
match x, offs with
@@ -1317,6 +1317,7 @@ struct
| `Address n -> ad_invariant ~vs ~offset ~lval n
| `Struct n -> Structs.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
| `Union n -> Unions.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
+ | `Array n -> CArrays.invariant ~value_invariant:(vd_invariant ~vs) ~offset ~lval n
| `Blob n when GobConfig.get_bool "ana.base.invariant.blobs" -> blob_invariant ~vs ~offset ~lval n
| _ -> Invariant.none (* TODO *)
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index b6ba0a8eb0..ac52dae19a 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -682,12 +682,12 @@ let getGlobalInits (file: file) : edges =
doInit (addOffsetLval offs lval) loc init is_zero;
lval
in
- let rec all_index = function
- | Index (e,o) -> Index (all_array_index_exp, all_index o)
- | Field (f,o) -> Field (f, all_index o)
+ let rec any_index_offset = function
+ | Index (e,o) -> Index (Lval.any_index_exp, any_index_offset o)
+ | Field (f,o) -> Field (f, any_index_offset o)
| NoOffset -> NoOffset
in
- let all_index (lh,offs) = lh, all_index offs in
+ let any_index (lh,offs) = lh, any_index_offset offs in
match init with
| SingleInit exp ->
let assign lval = (loc, Assign (lval, exp)) in
@@ -695,8 +695,8 @@ let getGlobalInits (file: file) : edges =
Instead, we get one assign for each distinct value in the array *)
if not fast_global_inits then
Hashtbl.add inits (assign lval) ()
- else if not (Hashtbl.mem inits (assign (all_index lval))) then
- Hashtbl.add inits (assign (all_index lval)) ()
+ else if not (Hashtbl.mem inits (assign (any_index lval))) then
+ Hashtbl.add inits (assign (any_index lval)) ()
else
()
| CompoundInit (typ, lst) ->
diff --git a/src/framework/myCFG.ml b/src/framework/myCFG.ml
index 0742954fe0..1b5ffba98b 100644
--- a/src/framework/myCFG.ml
+++ b/src/framework/myCFG.ml
@@ -58,8 +58,6 @@ let unknown_exp : exp = mkString "__unknown_value__"
let dummy_func = emptyFunction "__goblint_dummy_init" (* TODO get rid of this? *)
let dummy_node = FunctionEntry Cil.dummyFunDec
-let all_array_index_exp : exp = CastE(TInt(Cilfacade.ptrdiff_ikind (),[]), unknown_exp)
-
module type FileCfg =
sig
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 2ff2e8bf58..2a4f94c5c9 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1679,7 +1679,7 @@
"fast_global_inits": {
"title": "exp.fast_global_inits",
"description":
- "Only generate one 'a[MyCFG.all_array_index_exp] = x' for all assignments a[...] = x for a global array a[n].",
+ "Only generate one 'a[any_index] = x' for all assignments a[...] = x for a global array a[n].",
"type": "boolean",
"default": true
},
@@ -2319,6 +2319,12 @@
"cond",
"RETURN"
]
+ },
+ "goblint": {
+ "title": "witness.invariant.goblint",
+ "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",
+ "type": "boolean",
+ "default": false
}
},
"additionalProperties": false
diff --git a/tests/regression/56-witness/44-base-unassume-array.c b/tests/regression/56-witness/44-base-unassume-array.c
new file mode 100644
index 0000000000..c3928ae233
--- /dev/null
+++ b/tests/regression/56-witness/44-base-unassume-array.c
@@ -0,0 +1,16 @@
+// PARAM: --set ana.activated[+] unassume --set witness.yaml.unassume 44-base-unassume-array.yml --enable ana.int.interval
+#include
+
+int main() {
+ int a[10];
+
+ for (int i = 0; i < 3; i++) {
+ a[i] = i;
+ }
+
+ for (int i = 0; i < 10; i++) {
+ __goblint_check(a[i] >= 0);
+ __goblint_check(a[i] < 3);
+ }
+ return 0;
+}
diff --git a/tests/regression/56-witness/44-base-unassume-array.yml b/tests/regression/56-witness/44-base-unassume-array.yml
new file mode 100644
index 0000000000..dbf7fb8e54
--- /dev/null
+++ b/tests/regression/56-witness/44-base-unassume-array.yml
@@ -0,0 +1,58 @@
+- entry_type: loop_invariant
+ metadata:
+ format_version: "0.1"
+ uuid: c03a4c45-567e-4791-ac75-0675f782dc8c
+ creation_time: 2023-05-10T15:02:06Z
+ producer:
+ name: Goblint
+ version: heads/array-witness-invariant-0-gfb806119b-dirty
+ command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''44-base-unassume-array.c''
+ ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set''
+ ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir''
+ ''.goblint-56-44'''
+ task:
+ input_files:
+ - 44-base-unassume-array.c
+ input_file_hashes:
+ 44-base-unassume-array.c: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726
+ data_model: LP64
+ language: C
+ location:
+ file_name: 44-base-unassume-array.c
+ file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726
+ line: 7
+ column: 6
+ function: main
+ loop_invariant:
+ string: 0 <= a[(long )"all_index"]
+ type: assertion
+ format: C
+- entry_type: loop_invariant
+ metadata:
+ format_version: "0.1"
+ uuid: c03a4c45-567e-4791-ac75-0675f782dc8c
+ creation_time: 2023-05-10T15:02:06Z
+ producer:
+ name: Goblint
+ version: heads/array-witness-invariant-0-gfb806119b-dirty
+ command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''44-base-unassume-array.c''
+ ''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set''
+ ''dbg.debug'' ''true'' ''--enable'' ''dbg.timing.enabled'' ''--set'' ''goblint-dir''
+ ''.goblint-56-44'''
+ task:
+ input_files:
+ - 44-base-unassume-array.c
+ input_file_hashes:
+ 44-base-unassume-array.c: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726
+ data_model: LP64
+ language: C
+ location:
+ file_name: 44-base-unassume-array.c
+ file_hash: 9d9dc013c8d8aee483852aa73d0b4ac48ee7ea0f5433dc86ee28c3fe54c49726
+ line: 7
+ column: 6
+ function: main
+ loop_invariant:
+ string: a[(long )"all_index"] < 3
+ type: assertion
+ format: C