--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Functions in Predicates



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,