Add more builtin functions support

model-checking · May 4, 2023 · 7646caa · 7646caa
1 parent 9726c18
commit 7646caa
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
@@ -17,6 +17,7 @@ pub enum BuiltinFn {
     Copysignf,
     Cos,
     Cosf,
+    Error,
     ErrorNoLocation,
     Exp,
     Exp2,
@@ -78,6 +79,7 @@ impl ToString for BuiltinFn {
             Copysignf => "copysignf",
             Cos => "cos",
             Cosf => "cosf",
+            Error => "__error",
             ErrorNoLocation => "__errno_location",
             Exp => "exp",
             Exp2 => "exp2",
@@ -143,6 +145,7 @@ impl BuiltinFn {
             Copysignf => vec![Type::float(), Type::float()],
             Cos => vec![Type::double()],
             Cosf => vec![Type::float()],
+            Error => vec![],
             ErrorNoLocation => vec![],
             Exp => vec![Type::double()],
             Exp2 => vec![Type::double()],
@@ -201,6 +204,7 @@ impl BuiltinFn {
             Copysignf => Type::float(),
             Cos => Type::double(),
             Cosf => Type::float(),
+            Error => Type::c_int().to_pointer(),
             ErrorNoLocation => Type::c_int().to_pointer(),
             Exp => Type::double(),
             Exp2 => Type::double(),
@@ -262,6 +266,7 @@ impl BuiltinFn {
             Copysignf,
             Cos,
             Cosf,
+            Error,
             ErrorNoLocation,
             Exp,
             Exp2,