← Back to PR #29083
Build Log: frama_c_codex.1.0-for-opam
Status: DEPENDENCY FAILED
Log Output
Processing: [default: loading data]
[codex.1.0-rc1: http]
[codex.1.0-rc1: extract]
-> retrieved codex.1.0-rc1 (https://github.com/codex-semantics-library/codex/archive/refs/tags/1.0-for-opam.tar.gz)
[codex: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "codex" "-j" "255" "--promote-install-files=false" "@install" (CWD=/home/opam/.opam/default/.opam-switch/build/codex.1.0-rc1)
- (cd _build/default/utils && /usr/bin/gcc -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -D_FILE_OFFSET_BITS=64 -O2 -fno-strict-aliasing -fwrapv -pthread -fPIC -g -I /home/opam/.opam/default/lib/ocaml -o int_builtins_c.o -c int_builtins_c.c)
- int_builtins_c.c:99:23: warning: conflicting types for built-in function 'ffs'; expected 'int(int)' [-Wbuiltin-declaration-mismatch]
- 99 | static inline uintnat ffs(uintnat v){
- | ^~~
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I utils/tracelog/.tracelog.objs/byte -intf-suffix .ml -no-alias-deps -open Tracelog__ -o utils/tracelog/.tracelog.objs/byte/tracelog.cmo -c -impl utils/tracelog/tracelog.ml)
- File "utils/tracelog/tracelog.ml", line 232, characters 12-23:
- 232 | let colored_log fmt =
- ^^^^^^^^^^^
- Warning 26 [unused-var]: unused variable colored_log.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -intf-suffix .ml -no-alias-deps -open Tracelog__ -o utils/tracelog/.tracelog.objs/native/tracelog.cmx -c -impl utils/tracelog/tracelog.ml)
- File "utils/tracelog/tracelog.ml", line 232, characters 12-23:
- 232 | let colored_log fmt =
- ^^^^^^^^^^^
- Warning 26 [unused-var]: unused variable colored_log.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I fixpoint/.Fixpoint.objs/byte -I /home/opam/.opam/default/lib/patricia-tree -I .codex_log.objs/byte -I utils/.datatype_sig.objs/byte -I utils/.okasakimap.objs/byte -I utils/tracelog/.tracelog.objs/byte -intf-suffix .ml -no-alias-deps -open Fixpoint -o fixpoint/.Fixpoint.objs/byte/fixpoint__Wto.cmo -c -impl fixpoint/wto.ml)
- File "fixpoint/wto.ml", line 324, characters 19-23:
- 324 | let partition ?pref ~init ~succs =
- ^^^^
- Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I fixpoint/.Fixpoint.objs/byte -I /home/opam/.opam/default/lib/patricia-tree -I .codex_log.objs/byte -I utils/.datatype_sig.objs/byte -I utils/.okasakimap.objs/byte -I utils/tracelog/.tracelog.objs/byte -intf-suffix .ml -no-alias-deps -open Fixpoint -o fixpoint/.Fixpoint.objs/byte/fixpoint__Wto_iteration.cmo -c -impl fixpoint/wto_iteration.ml)
- File "fixpoint/wto_iteration.ml", line 116, characters 8-37:
- 116 | | Wto.Component(head,part) as c ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 26 [unused-var]: unused variable c.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I fixpoint/.Fixpoint.objs/byte -I /home/opam/.opam/default/lib/patricia-tree -I .codex_log.objs/byte -I utils/.datatype_sig.objs/byte -I utils/.okasakimap.objs/byte -I utils/tracelog/.tracelog.objs/byte -intf-suffix .ml -no-alias-deps -open Fixpoint -o fixpoint/.Fixpoint.objs/byte/fixpoint__Fixpoint_wto.cmo -c -impl fixpoint/fixpoint_wto.ml)
- File "fixpoint/fixpoint_wto.ml", line 98, characters 6-35:
- 98 | | Wto.Component(head,part) as c ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 26 [unused-var]: unused variable c.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I fixpoint/.Fixpoint.objs/byte -I fixpoint/.Fixpoint.objs/native -I /home/opam/.opam/default/lib/patricia-tree -I .codex_log.objs/byte -I .codex_log.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/.okasakimap.objs/byte -I utils/.okasakimap.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -intf-suffix .ml -no-alias-deps -open Fixpoint -o fixpoint/.Fixpoint.objs/native/fixpoint__Wto.cmx -c -impl fixpoint/wto.ml)
- File "fixpoint/wto.ml", line 324, characters 19-23:
- 324 | let partition ?pref ~init ~succs =
- ^^^^
- Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I transfer_functions/.transfer_functions.objs/byte -I /home/opam/.opam/default/lib/zarith -I .codex_log.objs/byte -intf-suffix .ml -no-alias-deps -open Transfer_functions__ -o transfer_functions/.transfer_functions.objs/byte/transfer_functions__Term.cmo -c -impl transfer_functions/term.ml)
- File "transfer_functions/term.ml", line 659, characters 50-52:
- 659 | | Biadd{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.biadd ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 659, characters 53-55:
- 659 | | Biadd{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.biadd ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- File "transfer_functions/term.ml", line 660, characters 50-52:
- 660 | | Bisub{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bisub ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 660, characters 53-55:
- 660 | | Bisub{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bisub ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- File "transfer_functions/term.ml", line 661, characters 45-47:
- 661 | | Bimul{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bimul ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 661, characters 48-50:
- 661 | | Bimul{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bimul ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- File "transfer_functions/term.ml", line 666, characters 44-46:
- 666 | | Bshl{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bshl ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 666, characters 47-49:
- 666 | | Bshl{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bshl ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I fixpoint/.Fixpoint.objs/byte -I fixpoint/.Fixpoint.objs/native -I /home/opam/.opam/default/lib/patricia-tree -I .codex_log.objs/byte -I .codex_log.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/.okasakimap.objs/byte -I utils/.okasakimap.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -intf-suffix .ml -no-alias-deps -open Fixpoint -o fixpoint/.Fixpoint.objs/native/fixpoint__Wto_iteration.cmx -c -impl fixpoint/wto_iteration.ml)
- File "fixpoint/wto_iteration.ml", line 116, characters 8-37:
- 116 | | Wto.Component(head,part) as c ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 26 [unused-var]: unused variable c.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I fixpoint/.Fixpoint.objs/byte -I fixpoint/.Fixpoint.objs/native -I /home/opam/.opam/default/lib/patricia-tree -I .codex_log.objs/byte -I .codex_log.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/.okasakimap.objs/byte -I utils/.okasakimap.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -intf-suffix .ml -no-alias-deps -open Fixpoint -o fixpoint/.Fixpoint.objs/native/fixpoint__Fixpoint_wto.cmx -c -impl fixpoint/fixpoint_wto.ml)
- File "fixpoint/fixpoint_wto.ml", line 98, characters 6-35:
- 98 | | Wto.Component(head,part) as c ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 26 [unused-var]: unused variable c.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I transfer_functions/.transfer_functions.objs/byte -I transfer_functions/.transfer_functions.objs/native -I /home/opam/.opam/default/lib/zarith -I .codex_log.objs/byte -I .codex_log.objs/native -intf-suffix .ml -no-alias-deps -open Transfer_functions__ -o transfer_functions/.transfer_functions.objs/native/transfer_functions__Term.cmx -c -impl transfer_functions/term.ml)
- File "transfer_functions/term.ml", line 659, characters 50-52:
- 659 | | Biadd{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.biadd ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 659, characters 53-55:
- 659 | | Biadd{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.biadd ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- File "transfer_functions/term.ml", line 660, characters 50-52:
- 660 | | Bisub{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bisub ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 660, characters 53-55:
- 660 | | Bisub{size;nsw;nuw;nusw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bisub ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- File "transfer_functions/term.ml", line 661, characters 45-47:
- 661 | | Bimul{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bimul ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 661, characters 48-50:
- 661 | | Bimul{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bimul ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- File "transfer_functions/term.ml", line 666, characters 44-46:
- 666 | | Bshl{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bshl ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b1.
- File "transfer_functions/term.ml", line 666, characters 47-49:
- 666 | | Bshl{size;nsw;nuw} -> fun arg -> let (b1,b2) = T.extract2 arg in (* T.bshl ~size b1 b2 *) assert false
- ^^
- Warning 26 [unused-var]: unused variable b2.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I single_value_abstraction/.Single_value_abstraction.objs/byte -I /home/opam/.opam/default/lib/zarith -I ext/framac_ival/.Framac_ival.objs/byte -I lattices/.lattices.objs/byte -I transfer_functions/.transfer_functions.objs/byte -I utils/.datatype_sig.objs/byte -I utils/tracelog/.tracelog.objs/byte -intf-suffix .ml -no-alias-deps -open Single_value_abstraction__ -o single_value_abstraction/.Single_value_abstraction.objs/byte/single_value_abstraction__Quadrivalent_basis.cmo -c -impl single_value_abstraction/quadrivalent_basis.ml)
- File "single_value_abstraction/quadrivalent_basis.ml", line 29, characters 15-20:
- 29 | let unknown ?level = Top
- ^^^^^
- Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I constraints/.Constraints.objs/byte -I /home/opam/.opam/default/lib/cudd -I /home/opam/.opam/default/lib/patricia-tree -I /home/opam/.opam/default/lib/zarith -I .codex_config.objs/byte -I .codex_log.objs/byte -I ext/framac_ival/.Framac_ival.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/byte -I smtbackend/.Smtbackend.objs/byte -I transfer_functions/.transfer_functions.objs/byte -I utils/.bdd.objs/byte -I utils/.condition_map.objs/byte -I utils/.datatype_sig.objs/byte -I utils/.immutable_array.objs/byte -I utils/.immutable_dynamic_array.objs/byte -I utils/.treemap.objs/byte -I utils/tracelog/.tracelog.objs/byte -I utils/unionFind/.Union_Find.objs/byte -no-alias-deps -open Constraints__ -o constraints/.Constraints.objs/byte/constraints__Constraints_condition.cmo -c -impl constraints/constraints_condition.ml)
- File "constraints/constraints_condition.ml", line 719, characters 22-32:
- 719 | type t = Cudd.Man.d Cudd.Bdd.t
- ^^^^^^^^^^
- Error: The module Cudd.Bdd is a functor, it cannot have any components
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I single_value_abstraction/.Single_value_abstraction.objs/byte -I /home/opam/.opam/default/lib/zarith -I ext/framac_ival/.Framac_ival.objs/byte -I lattices/.lattices.objs/byte -I transfer_functions/.transfer_functions.objs/byte -I utils/.datatype_sig.objs/byte -I utils/tracelog/.tracelog.objs/byte -intf-suffix .ml -no-alias-deps -open Single_value_abstraction__ -o single_value_abstraction/.Single_value_abstraction.objs/byte/single_value_abstraction__Ival_basis.cmo -c -impl single_value_abstraction/ival_basis.ml)
- File "single_value_abstraction/ival_basis.ml", line 670, characters 10-11:
- 670 | let f fmt =
- ^
- Warning 26 [unused-var]: unused variable f.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I constraints/.Constraints.objs/byte -I /home/opam/.opam/default/lib/cudd -I /home/opam/.opam/default/lib/patricia-tree -I /home/opam/.opam/default/lib/zarith -I .codex_config.objs/byte -I .codex_log.objs/byte -I ext/framac_ival/.Framac_ival.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/byte -I smtbackend/.Smtbackend.objs/byte -I transfer_functions/.transfer_functions.objs/byte -I utils/.bdd.objs/byte -I utils/.condition_map.objs/byte -I utils/.datatype_sig.objs/byte -I utils/.immutable_array.objs/byte -I utils/.immutable_dynamic_array.objs/byte -I utils/.treemap.objs/byte -I utils/tracelog/.tracelog.objs/byte -I utils/unionFind/.Union_Find.objs/byte -intf-suffix .ml -no-alias-deps -open Constraints__ -o constraints/.Constraints.objs/byte/constraints__Constraints_smt.cmo -c -impl constraints/constraints_smt.ml)
- File "constraints/constraints_smt.ml", line 157, characters 17-22:
- 157 | let first = index in
- ^^^^^
- Warning 26 [unused-var]: unused variable first.
- File "constraints/constraints_smt.ml", line 158, characters 17-21:
- 158 | let last = index + size - 1 in
- ^^^^
- Warning 26 [unused-var]: unused variable last.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -g -bin-annot -I constraints/.Constraints.objs/byte -I /home/opam/.opam/default/lib/cudd -I /home/opam/.opam/default/lib/patricia-tree -I /home/opam/.opam/default/lib/zarith -I .codex_config.objs/byte -I .codex_log.objs/byte -I ext/framac_ival/.Framac_ival.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/byte -I smtbackend/.Smtbackend.objs/byte -I transfer_functions/.transfer_functions.objs/byte -I utils/.bdd.objs/byte -I utils/.condition_map.objs/byte -I utils/.datatype_sig.objs/byte -I utils/.immutable_array.objs/byte -I utils/.immutable_dynamic_array.objs/byte -I utils/.treemap.objs/byte -I utils/tracelog/.tracelog.objs/byte -I utils/unionFind/.Union_Find.objs/byte -intf-suffix .ml -no-alias-deps -open Constraints__ -o constraints/.Constraints.objs/byte/constraints__Constraints_constraints.cmo -c -impl constraints/constraints_constraints.ml)
- File "constraints/constraints_constraints.ml", line 398, characters 15-16:
- 398 | | Root _ -> ()
- ^
- Warning 28 [wildcard-arg-to-constant-constr]: wildcard pattern given as argument to a constant constructor
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I single_value_abstraction/.Single_value_abstraction.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/native -I /home/opam/.opam/default/lib/zarith -I ext/framac_ival/.Framac_ival.objs/byte -I ext/framac_ival/.Framac_ival.objs/native -I lattices/.lattices.objs/byte -I lattices/.lattices.objs/native -I transfer_functions/.transfer_functions.objs/byte -I transfer_functions/.transfer_functions.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -intf-suffix .ml -no-alias-deps -open Single_value_abstraction__ -o single_value_abstraction/.Single_value_abstraction.objs/native/single_value_abstraction__Quadrivalent_basis.cmx -c -impl single_value_abstraction/quadrivalent_basis.ml)
- File "single_value_abstraction/quadrivalent_basis.ml", line 29, characters 15-20:
- 29 | let unknown ?level = Top
- ^^^^^
- Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I single_value_abstraction/.Single_value_abstraction.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/native -I /home/opam/.opam/default/lib/zarith -I ext/framac_ival/.Framac_ival.objs/byte -I ext/framac_ival/.Framac_ival.objs/native -I lattices/.lattices.objs/byte -I lattices/.lattices.objs/native -I transfer_functions/.transfer_functions.objs/byte -I transfer_functions/.transfer_functions.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -intf-suffix .ml -no-alias-deps -open Single_value_abstraction__ -o single_value_abstraction/.Single_value_abstraction.objs/native/single_value_abstraction__Ival_basis.cmx -c -impl single_value_abstraction/ival_basis.ml)
- File "single_value_abstraction/ival_basis.ml", line 670, characters 10-11:
- 670 | let f fmt =
- ^
- Warning 26 [unused-var]: unused variable f.
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I constraints/.Constraints.objs/byte -I constraints/.Constraints.objs/native -I /home/opam/.opam/default/lib/cudd -I /home/opam/.opam/default/lib/patricia-tree -I /home/opam/.opam/default/lib/zarith -I .codex_config.objs/byte -I .codex_config.objs/native -I .codex_log.objs/byte -I .codex_log.objs/native -I ext/framac_ival/.Framac_ival.objs/byte -I ext/framac_ival/.Framac_ival.objs/native -I single_value_abstraction/.Single_value_abstraction.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/native -I smtbackend/.Smtbackend.objs/byte -I smtbackend/.Smtbackend.objs/native -I transfer_functions/.transfer_functions.objs/byte -I transfer_functions/.transfer_functions.objs/native -I utils/.bdd.objs/byte -I utils/.bdd.objs/native -I utils/.condition_map.objs/byte -I utils/.condition_map.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/.immutable_array.objs/byte -I utils/.immutable_array.objs/native -I utils/.immutable_dynamic_array.objs/byte -I utils/.immutable_dynamic_array.objs/native -I utils/.treemap.objs/byte -I utils/.treemap.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -I utils/unionFind/.Union_Find.objs/byte -I utils/unionFind/.Union_Find.objs/native -intf-suffix .ml -no-alias-deps -open Constraints__ -o constraints/.Constraints.objs/native/constraints__Constraints_constraints.cmx -c -impl constraints/constraints_constraints.ml)
- File "constraints/constraints_constraints.ml", line 398, characters 15-16:
- 398 | | Root _ -> ()
- ^
- Warning 28 [wildcard-arg-to-constant-constr]: wildcard pattern given as argument to a constant constructor
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -g -O3 -I constraints/.Constraints.objs/byte -I constraints/.Constraints.objs/native -I /home/opam/.opam/default/lib/cudd -I /home/opam/.opam/default/lib/patricia-tree -I /home/opam/.opam/default/lib/zarith -I .codex_config.objs/byte -I .codex_config.objs/native -I .codex_log.objs/byte -I .codex_log.objs/native -I ext/framac_ival/.Framac_ival.objs/byte -I ext/framac_ival/.Framac_ival.objs/native -I single_value_abstraction/.Single_value_abstraction.objs/byte -I single_value_abstraction/.Single_value_abstraction.objs/native -I smtbackend/.Smtbackend.objs/byte -I smtbackend/.Smtbackend.objs/native -I transfer_functions/.transfer_functions.objs/byte -I transfer_functions/.transfer_functions.objs/native -I utils/.bdd.objs/byte -I utils/.bdd.objs/native -I utils/.condition_map.objs/byte -I utils/.condition_map.objs/native -I utils/.datatype_sig.objs/byte -I utils/.datatype_sig.objs/native -I utils/.immutable_array.objs/byte -I utils/.immutable_array.objs/native -I utils/.immutable_dynamic_array.objs/byte -I utils/.immutable_dynamic_array.objs/native -I utils/.treemap.objs/byte -I utils/.treemap.objs/native -I utils/tracelog/.tracelog.objs/byte -I utils/tracelog/.tracelog.objs/native -I utils/unionFind/.Union_Find.objs/byte -I utils/unionFind/.Union_Find.objs/native -intf-suffix .ml -no-alias-deps -open Constraints__ -o constraints/.Constraints.objs/native/constraints__Constraints_smt.cmx -c -impl constraints/constraints_smt.ml)
- File "constraints/constraints_smt.ml", line 157, characters 17-22:
- 157 | let first = index in
- ^^^^^
- Warning 26 [unused-var]: unused variable first.
- File "constraints/constraints_smt.ml", line 158, characters 17-21:
- 158 | let last = index + size - 1 in
- ^^^^
- Warning 26 [unused-var]: unused variable last.
[ERROR] The compilation of codex.1.0-rc1 failed at "dune build -p codex -j 255 --promote-install-files=false @install".
build failed...
Dependency Graph
Loading graph...
View raw DOT format
digraph opam {
"alt-ergo-free.2.2.0" -> {"camlzip.1.13" "conf-autoconf.0.2" "menhir.20211128" "num.1.6" "ocaml.4.14.2" "ocplib-simplex.0.4.1" "psmt2-frontend.0.1" "zarith.1.14"}
"astring.0.8.5" -> {"ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "topkg.1.1.1"}
"base.v0.16.4" -> {"dune.3.20.2" "dune-configurator.3.20.2" "ocaml.4.14.2" "sexplib0.v0.16.0"}
"base64.3.5.2" -> {"dune.3.20.2" "ocaml.4.14.2"}
"bheap.2.0.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"bos.0.2.1" -> {"astring.0.8.5" "base-unix.base" "fmt.0.11.0" "fpath.0.7.3" "logs.0.10.0" "ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "rresult.0.7.0" "topkg.1.1.1"}
"cairo2.0.6.5" -> {"base-bigarray.base" "conf-cairo.1" "dune.3.20.2" "dune-configurator.3.20.2" "ocaml.4.14.2"}
"camlp-streams.5.0.1" -> {"dune.3.20.2" "ocaml.4.14.2"}
"camlzip.1.13" -> {"conf-zlib.1" "ocaml.4.14.2" "ocamlfind.1.9.8"}
"codex.1.0-rc1" -> {"base64.3.5.2" "bheap.2.0.0" "camlp-streams.5.0.1" "cudd.0.1.3" "dune.3.20.2" "fmt.0.11.0" "pacomb.1.3" "patricia-tree.0.11.0" "ppx_inline_test.v0.16.1" "qcheck-core.0.27" "zarith.1.14"}
"conf-cairo.1" -> "conf-pkg-config.4";
"conf-gtk3.18" -> "conf-pkg-config.4";
"conf-gtksourceview3.0+2" -> "conf-pkg-config.4";
"conf-zlib.1" -> "conf-pkg-config.4";
"cppo.1.8.0" -> {"base-unix.base" "dune.3.20.2" "ocaml.4.14.2"}
"csexp.1.5.2" -> {"dune.3.20.2" "ocaml.4.14.2"}
"ctypes.0.24.0" -> {"dune.3.20.2" "dune-configurator.3.20.2" "integers.0.7.0" "ocaml.4.14.2"}
"cudd.0.1.3" -> "dune.3.20.2";
"dune.3.20.2" -> {"base-threads.base" "base-unix.base" "ocaml.4.14.2"}
"dune-configurator.3.20.2" -> {"base-unix.base" "csexp.1.5.2" "dune.3.20.2" "ocaml.4.14.2"}
"dune-private-libs.3.20.2" -> {"csexp.1.5.2" "dune.3.20.2" "dyn.3.20.2" "ocaml.4.14.2" "pp.2.0.0" "stdune.3.20.2"}
"dune-site.3.20.2" -> {"dune.3.20.2" "dune-private-libs.3.20.2"}
"dyn.3.20.2" -> {"dune.3.20.2" "ocaml.4.14.2" "ordering.3.20.2" "pp.2.0.0"}
"fmt.0.11.0" -> {"base-unix.base" "ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "topkg.1.1.1"}
"fpath.0.7.3" -> {"astring.0.8.5" "ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "topkg.1.1.1"}
"frama-c.31.0" -> {"alt-ergo-free.2.2.0" "camlzip.1.13" "conf-gtksourceview3.0+2" "dune.3.20.2" "dune-configurator.3.20.2" "dune-site.3.20.2" "lablgtk3.3.1.5" "lablgtk3-sourceview3.3.1.5" "menhir.20211128" "ocaml.4.14.2" "ocamlgraph.2.2.0" "ppx_deriving.6.0.3" "ppx_deriving_yaml.0.4.0" "ppx_deriving_yojson.3.9.1" "unionFind.20250818" "why3.1.8.2" "yaml.3.2.0" "yojson.3.0.0" "zarith.1.14"}
"frama_c_codex.1.0-for-opam" -> {"codex.1.0-rc1" "dune.3.20.2" "frama-c.31.0"}
"integers.0.7.0" -> {"dune.3.20.2" "ocaml.4.14.2" "stdlib-shims.0.3.0"}
"jane-street-headers.v0.16.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"jst-config.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "dune-configurator.3.20.2" "ocaml.4.14.2" "ppx_assert.v0.16.0"}
"lablgtk3.3.1.5" -> {"cairo2.0.6.5" "camlp-streams.5.0.1" "conf-gtk3.18" "dune.3.20.2" "ocaml.4.14.2"}
"lablgtk3-sourceview3.3.1.5" -> {"camlp-streams.5.0.1" "conf-gtksourceview3.0+2" "dune.3.20.2" "lablgtk3.3.1.5" "ocaml.4.14.2"}
"logs.0.10.0" -> {"base-threads.base" "fmt.0.11.0" "ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "topkg.1.1.1"}
"menhir.20211128" -> {"dune.3.20.2" "menhirLib.20211128" "menhirSdk.20211128" "ocaml.4.14.2"}
"menhirLib.20211128" -> {"dune.3.20.2" "ocaml.4.14.2"}
"menhirSdk.20211128" -> {"dune.3.20.2" "ocaml.4.14.2"}
"num.1.6" -> "ocaml.4.14.2";
"ocaml.4.14.2" -> {"ocaml-base-compiler.4.14.2" "ocaml-config.2"}
"ocaml-compiler-libs.v0.12.4" -> {"dune.3.20.2" "ocaml.4.14.2"}
"ocaml-config.2" -> "ocaml-base-compiler.4.14.2";
"ocamlbuild.0.16.1" -> "ocaml.4.14.2";
"ocamlfind.1.9.8" -> "ocaml.4.14.2";
"ocamlgraph.2.2.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"ocplib-simplex.0.4.1" -> {"conf-autoconf.0.2" "num.1.6" "ocaml.4.14.2" "ocamlfind.1.9.8"}
"ordering.3.20.2" -> {"dune.3.20.2" "ocaml.4.14.2"}
"pacomb.1.3" -> {"dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0" "stdlib-shims.0.3.0"}
"patricia-tree.0.11.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"pp.2.0.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"ppx_assert.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppx_cold.v0.16.0" "ppx_compare.v0.16.0" "ppx_here.v0.16.0" "ppx_sexp_conv.v0.16.0" "ppxlib.0.35.0"}
"ppx_base.v0.16.0" -> {"dune.3.20.2" "ocaml.4.14.2" "ppx_cold.v0.16.0" "ppx_compare.v0.16.0" "ppx_enumerate.v0.16.0" "ppx_globalize.v0.16.0" "ppx_hash.v0.16.0" "ppx_sexp_conv.v0.16.0" "ppxlib.0.35.0"}
"ppx_cold.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0"}
"ppx_compare.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0"}
"ppx_derivers.1.2.1" -> {"dune.3.20.2" "ocaml.4.14.2"}
"ppx_deriving.6.0.3" -> {"cppo.1.8.0" "dune.3.20.2" "ocaml.4.14.2" "ocamlfind.1.9.8" "ppx_derivers.1.2.1" "ppxlib.0.35.0"}
"ppx_deriving_yaml.0.4.0" -> {"dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0" "yaml.3.2.0"}
"ppx_deriving_yojson.3.9.1" -> {"dune.3.20.2" "ocaml.4.14.2" "ppx_deriving.6.0.3" "ppxlib.0.35.0" "yojson.3.0.0"}
"ppx_enumerate.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0"}
"ppx_globalize.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0"}
"ppx_hash.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppx_compare.v0.16.0" "ppx_sexp_conv.v0.16.0" "ppxlib.0.35.0"}
"ppx_here.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0"}
"ppx_inline_test.v0.16.1" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0" "time_now.v0.16.0"}
"ppx_optcomp.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0" "stdio.v0.16.0"}
"ppx_sexp_conv.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2" "ppxlib.0.35.0" "sexplib0.v0.16.0"}
"ppxlib.0.35.0" -> {"dune.3.20.2" "ocaml.4.14.2" "ocaml-compiler-libs.v0.12.4" "ppx_derivers.1.2.1" "sexplib0.v0.16.0" "stdlib-shims.0.3.0"}
"psmt2-frontend.0.1" -> {"conf-autoconf.0.2" "menhir.20211128" "ocaml.4.14.2" "ocamlfind.1.9.8"}
"qcheck-core.0.27" -> {"base-unix.base" "dune.3.20.2" "ocaml.4.14.2"}
"rresult.0.7.0" -> {"ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8" "topkg.1.1.1"}
"sexplib0.v0.16.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"stdio.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "ocaml.4.14.2"}
"stdlib-shims.0.3.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"stdune.3.20.2" -> {"base-unix.base" "csexp.1.5.2" "dune.3.20.2" "dyn.3.20.2" "ocaml.4.14.2" "ordering.3.20.2" "pp.2.0.0"}
"time_now.v0.16.0" -> {"base.v0.16.4" "dune.3.20.2" "jane-street-headers.v0.16.0" "jst-config.v0.16.0" "ocaml.4.14.2" "ppx_base.v0.16.0" "ppx_optcomp.v0.16.0"}
"topkg.1.1.1" -> {"ocaml.4.14.2" "ocamlbuild.0.16.1" "ocamlfind.1.9.8"}
"unionFind.20250818" -> {"dune.3.20.2" "ocaml.4.14.2"}
"why3.1.8.2" -> {"camlzip.1.13" "menhir.20211128" "ocaml.4.14.2" "ocamlfind.1.9.8" "ocamlgraph.2.2.0" "ppx_deriving.6.0.3" "ppx_sexp_conv.v0.16.0" "zarith.1.14"}
"yaml.3.2.0" -> {"bos.0.2.1" "ctypes.0.24.0" "dune.3.20.2" "dune-configurator.3.20.2" "ocaml.4.14.2"}
"yojson.3.0.0" -> {"dune.3.20.2" "ocaml.4.14.2"}
"zarith.1.14" -> {"conf-gmp.5" "conf-pkg-config.4" "ocaml.4.14.2" "ocamlfind.1.9.8"}
}