diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index d337ae4f5158..dc703ce83edc 100644 --- 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,