From 853913da73185131071cc13db8bd2e5805098e5c Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Thu, 22 Jun 2023 21:07:06 +0000
Subject: [PATCH] Adds sysconf to the list of supported builtins

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 cprover_bindings/src/goto_program/builtin.rs |  5 +++++
 cprover_bindings/src/goto_program/typ.rs     |  5 ++++-
 tests/kani/LibC/sysconf.rs                   | 12 ++++++++++++
 3 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/kani/LibC/sysconf.rs

diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
index 258691b9ade4..95c38d7e0f8a 100644
--- 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
index a80afe2bdc3c..9d1649b99cd1 100644
--- 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
new file mode 100644
index 000000000000..5a17dfde34eb
--- /dev/null
+++ 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;
+}