Moon
Moon

Reputation: 31

CBMC sine and cosine functions

I am new to CBMC and SAT solver. I have read tutorials and tried some examples and trying to use CBMC for my application.

The problem is that my application uses sin and cosine functions to calculate some values. I need to do an assertion check on those calculated values. However, I realised that in CBMC, the sine and cosine functions are nothing but functions that return values between -1 to 1 non-deterministically.

Is there a way to use the sine and cosine functions normally ( for example, if I go sin(input) with the input being a variable, then it just computes the sine of input?)

Upvotes: 0

Views: 30

Answers (0)

Related Questions