Adds sysconf to the list of supported builtins

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
model-checking · Jul 25, 2023 · 853913d · 853913d
1 parent a998087
commit 853913d
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 1 deletion.
diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
@@ -61,6 +61,7 @@ pub enum BuiltinFn {
     Sinf,
     Sqrt,
     Sqrtf,
+    Sysconf,
     Trunc,
     Truncf,
     Unlink,
@@ -124,6 +125,7 @@ impl ToString for BuiltinFn {
             Sinf => "sinf",
             Sqrt => "sqrt",
             Sqrtf => "sqrtf",
+            Sysconf => "sysconf",
             Trunc => "trunc",
             Truncf => "truncf",
             Unlink => "unlink",
@@ -188,6 +190,7 @@ impl BuiltinFn {
             Sinf => vec![Type::float()],
             Sqrt => vec![Type::double()],
             Sqrtf => vec![Type::float()],
+            Sysconf => vec![Type::c_int()],
             Trunc => vec![Type::double()],
             Truncf => vec![Type::float()],
             Unlink => vec![Type::c_char().to_pointer()],
@@ -251,6 +254,7 @@ impl BuiltinFn {
             Sinf => Type::float(),
             Sqrt => Type::double(),
             Sqrtf => Type::float(),
+            Sysconf => Type::c_long_int(),
             Trunc => Type::double(),
             Truncf => Type::float(),
             Unlink => Type::c_int(),
@@ -314,6 +318,7 @@ impl BuiltinFn {
             Sinf,
             Sqrt,
             Sqrtf,
+            Sysconf,
             Trunc,
             Truncf,
             Unlink,

diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -649,7 +649,10 @@ impl Type {
     pub fn is_signed(&self, mm: &MachineModel) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
-            CInteger(CIntType::Int) | CInteger(CIntType::LongInt) | CInteger(CIntType::SSizeT) | Signedbv { .. } => true,
+            CInteger(CIntType::Int)
+            | CInteger(CIntType::LongInt)
+            | CInteger(CIntType::SSizeT)
+            | Signedbv { .. } => true,
             CInteger(CIntType::Char) => !mm.char_is_unsigned,
             _ => false,
         }

diff --git a/tests/kani/LibC/sysconf.rs b/tests/kani/LibC/sysconf.rs
@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Check support for `sysconf`.
+
+#![feature(rustc_private)]
+extern crate libc;
+
+#[kani::proof]
+fn main() {
+    let page_size = unsafe { libc::sysconf(libc::_SC_PAGESIZE) } as usize;
+}