Reputation: 31
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