--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on August 2010 ---
Hello, is there a possibility to create more complex predicates using complete functions? I have a function that returns a boolean value depending on 2 variables bool func1(int x, int y) { bool result; //... //... return result; } /*@ predicate is_correct(int x, int y) = (func1(x,y)); */ /*@ requires is_correct(x,y); @ ensures (\result == 1); */ int func2 (int x, int y) { // do something, that depends on x and y return 1; } However, it does not work like this. What am I doing wrong, or is it maybe not possible to use C-functions in predicates? Sincereley,