Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] A problem with math functions

> [wp} user error: Builtin \cos(real) not defined
> [wp] failure: Logic \cos undefined.

We simply did not implement all built-ins in WP.
One reason is that many SMT solvers (if not all) lack interesting properties about trigonometry.

Workarounds:
 - either use another name, like ‘cos’, and declare it using standard ACSL « logic real cos(real x); » within an axiomatic bloc, and add desired axioms and lemmas ;
 - or use a WP driver (WP manual § 2.4.10, p28) to bind `\cos` to some symbol in  your favorite SMT solver (or Coq or Why3) ; for instance, see how we handle the ‘\max’ function in '$(frama-c -print-share-path)/wp/wp.driver’

In all cases, consider using -wp-model float

	L.