diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal index 73d93aa94..e16806be6 100644 --- a/crux-llvm/crux-llvm.cabal +++ b/crux-llvm/crux-llvm.cabal @@ -89,7 +89,7 @@ library build-depends: aeson, bv-sized, - config-schema, + config-schema >= 1.2.2.0, data-binary-ieee754, logict, llvm-pretty, diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs index d115973da..256703fa9 100644 --- a/crux-llvm/src/Crux/LLVM/Overrides.hs +++ b/crux-llvm/src/Crux/LLVM/Overrides.hs @@ -251,6 +251,19 @@ svCompOverrides :: [OverrideTemplate (personality sym) sym arch rtp l a] svCompOverrides = [ basic_llvm_override $ + [llvmOvr| i64 @__VERIFIER_nondet_longlong() |] + (sv_comp_fresh_bits (knownNat @64)) + + -- loff_t is pretty Linux-specific, so we can't point to the C or POSIX + -- standards for justification about what size it should be. The man page + -- for lseek64 (https://linux.die.net/man/3/lseek64) is as close to a + -- definitive reference for this as I can find, which says + -- "The type loff_t is a 64-bit signed type". + , basic_llvm_override $ + [llvmOvr| i64 @__VERIFIER_nondet_loff_t() |] + (sv_comp_fresh_bits (knownNat @64)) + + , basic_llvm_override $ [llvmOvr| size_t @__VERIFIER_nondet_ulong() |] (sv_comp_fresh_bits ?ptrWidth) @@ -258,6 +271,14 @@ svCompOverrides = [llvmOvr| size_t @__VERIFIER_nondet_long() |] (sv_comp_fresh_bits ?ptrWidth) + , basic_llvm_override $ + [llvmOvr| i32 @__VERIFIER_nondet_unsigned() |] + (sv_comp_fresh_bits (knownNat @32)) + + , basic_llvm_override $ + [llvmOvr| i32 @__VERIFIER_nondet_u32() |] + (sv_comp_fresh_bits (knownNat @32)) + , basic_llvm_override $ [llvmOvr| i32 @__VERIFIER_nondet_uint() |] (sv_comp_fresh_bits (knownNat @32)) @@ -266,6 +287,10 @@ svCompOverrides = [llvmOvr| i32 @__VERIFIER_nondet_int() |] (sv_comp_fresh_bits (knownNat @32)) + , basic_llvm_override $ + [llvmOvr| i16 @__VERIFIER_nondet_u16() |] + (sv_comp_fresh_bits (knownNat @16)) + , basic_llvm_override $ [llvmOvr| i16 @__VERIFIER_nondet_ushort() |] (sv_comp_fresh_bits (knownNat @16)) @@ -274,6 +299,10 @@ svCompOverrides = [llvmOvr| i16 @__VERIFIER_nondet_short() |] (sv_comp_fresh_bits (knownNat @16)) + , basic_llvm_override $ + [llvmOvr| i8 @__VERIFIER_nondet_u8() |] + (sv_comp_fresh_bits (knownNat @8)) + , basic_llvm_override $ [llvmOvr| i8 @__VERIFIER_nondet_uchar() |] (sv_comp_fresh_bits (knownNat @8)) @@ -286,6 +315,10 @@ svCompOverrides = [llvmOvr| i1 @__VERIFIER_nondet_bool() |] (sv_comp_fresh_bits (knownNat @1)) + , basic_llvm_override $ + [llvmOvr| size_t @__VERIFIER_nondet_size_t() |] + (sv_comp_fresh_bits ?ptrWidth) + , basic_llvm_override $ [llvmOvr| float @__VERIFIER_nondet_float() |] (sv_comp_fresh_float SingleFloatRepr) diff --git a/crux/crux.cabal b/crux/crux.cabal index fbe372c3d..ae430cdd3 100644 --- a/crux/crux.cabal +++ b/crux/crux.cabal @@ -54,7 +54,7 @@ library raw-strings-qq, simple-get-opt, config-value, - config-schema, + config-schema >= 1.2.2.0, semigroupoids, unordered-containers, xml,